cv_repScript.sml

1(*
2  Define cv_rep and prove a few lemmas used in proof automation
3*)
4Theory cv_rep
5Ancestors
6  cv cv_type
7
8Overload c2n[local] = “cv$c2n”
9Overload c2b[local] = “cv$c2b”
10Overload Num[local] = “cv$Num”
11Overload Pair[local] = “cv$Pair”
12
13Definition cv_rep_def:
14  cv_rep pre_cond (cv_tm:cv) (from_fun:'a -> cv) hol_tm <=>
15    pre_cond ==>
16    from_fun hol_tm = cv_tm
17End
18
19Theorem cv_rep_trivial:
20  !f n. cv_rep T (f n) f n
21Proof
22  fs [cv_rep_def]
23QED
24
25Theorem cv_rep_move:
26  (b ==> cv_rep p x y z) = cv_rep (b /\ p) x y z
27Proof
28  Cases_on ‘b’ \\ gvs [cv_rep_def]
29QED
30
31Theorem cv_rep_eval:
32  cv_rep p y f (x:'a) ==>
33  from_to f t ==>
34  p ==> x = t y
35Proof
36  rw [] \\ gvs [cv_rep_def,from_to_def]
37QED
38
39Theorem cv_rep_assum:
40  cv_rep p (cv (g a)) (f:'a -> cv) x ==>
41  !cv_a p_a.
42    cv_rep p_a cv_a g a ==>
43    cv_rep (p_a /\ p) (cv cv_a) f x
44Proof
45  gvs [cv_rep_def]
46QED
47
48Theorem IMP_COMM:
49  (b1 ==> b2 ==> c) = (b2 ==> b1 ==> c)
50Proof
51  Cases_on ‘b1’ \\ Cases_on ‘b2’ \\ rewrite_tac []
52QED
53
54Theorem IMP_CANCEL:
55  (b ==> b ==> c) = (b ==> c)
56Proof
57  Cases_on ‘b’ \\ fs []
58QED
59
60Theorem if_eq_zero:
61  (if n = 0 then x else y) = (if 0 < (n:num) then y else x:'a)
62Proof
63  Cases_on ‘n’ \\ gvs []
64QED
65
66Theorem lt_zero:
67  0 < n <=> n <> 0:num
68Proof
69  Cases_on ‘n’ \\ gvs []
70QED
71
72Theorem cv_eval[compute]:
73  c2n (Num n) = n /\
74  c2n (Pair x y) = 0 /\
75  c2b (Num n) = (n <> 0) /\
76  c2b (Pair x y) = F
77Proof
78  gvs [cvTheory.c2n_def,cvTheory.c2b_def]
79  \\ Cases_on ‘n’ \\ gvs []
80QED
81
82Theorem UNCURRY_pair_case:
83  !f. UNCURRY f = \x. case x of (x,y) => f x y
84Proof
85  strip_tac \\ fs [FUN_EQ_THM] \\ Cases \\ fs []
86QED
87
88Definition cv_proj_def:
89  cv_proj [] v = v /\
90  cv_proj (T::xs) v = cv_fst (cv_proj xs v) /\
91  cv_proj (F::xs) v = cv_snd (cv_proj xs v)
92End
93
94Theorem cv_proj_less_eq:
95  !v xs. cv_size (cv_proj xs v) <= cv_size v
96Proof
97  gen_tac \\ Induct \\ gvs [cv_proj_def]
98  \\ Cases \\ gvs [cv_proj_def] \\ rw []
99  \\ irule arithmeticTheory.LESS_EQ_TRANS
100  \\ pop_assum $ irule_at (Pos last)
101  \\ Cases_on ‘cv_proj xs v’ \\ gvs []
102QED
103
104Theorem to_cv_proj:
105  cv_fst = cv_proj [T] /\
106  cv_snd = cv_proj [F] /\
107  cv_proj xs (cv_proj ys b) = cv_proj (xs ++ ys) b
108Proof
109  gvs [FUN_EQ_THM,cv_proj_def]
110  \\ Induct_on ‘xs’ \\ gvs [cv_proj_def]
111  \\ Cases \\ gvs [cv_proj_def]
112QED
113
114Theorem cv_termination_simp:
115  (c2b (cv_ispair cv_v) = ?x1 x2. cv_v = Pair x1 x2) /\
116  (c2b (cv_lt (Num 0) cv_v) = ?k. cv_v = Num (SUC k)) /\
117  (c2b (cv_lt (Num (NUMERAL (BIT1 n))) (cv_fst cv_v)) <=>
118   ?k z. cv_v = Pair (Num k) z /\ NUMERAL (BIT1 n) < k) /\
119  (c2b (cv_lt (Num (NUMERAL (BIT2 n))) (cv_fst cv_v)) <=>
120   ?k z. cv_v = Pair (Num k) z /\ NUMERAL (BIT2 n) < k) /\
121  (cv_fst cv_v = Pair x y <=> ?z. cv_v = Pair (Pair x y) z) /\
122  (cv_snd cv_v = Pair x y <=> ?z. cv_v = Pair z (Pair x y)) /\
123  (cv_fst cv_v = Num (SUC k) <=> ?z. cv_v = Pair (Num (SUC k)) z) /\
124  (cv_snd cv_v = Num (SUC k) <=> ?z. cv_v = Pair z (Num (SUC k)))
125Proof
126  Cases_on ‘cv_v’ \\ gvs [] \\ rw []
127  \\ gvs [c2b_def,arithmeticTheory.NUMERAL_DEF]
128  \\ rpt $ pop_assum mp_tac
129  \\ rewrite_tac [arithmeticTheory.BIT1,arithmeticTheory.BIT2] \\ gvs []
130  >- (Cases_on ‘m’ \\ gvs [])
131  \\ rename [‘cv_lt _ g’] \\ Cases_on ‘g’ \\ fs [] \\ rw []
132QED
133
134Definition implies_def:
135  implies x y <=> (x ==> y)
136End
137
138Theorem cv_postprocess:
139  cv_if c x x = x
140Proof
141  fs [cv_if_def]
142QED