1 theory ComputeHOL |
|
2 imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle" |
|
3 begin |
|
4 |
|
5 lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq) |
|
6 lemma meta_eq_trivial: "x == y \<Longrightarrow> x == y" by simp |
|
7 lemma meta_eq_imp_eq: "x == y \<Longrightarrow> x = y" by auto |
|
8 lemma eq_trivial: "x = y \<Longrightarrow> x = y" by auto |
|
9 lemma bool_to_true: "x :: bool \<Longrightarrow> x == True" by simp |
|
10 lemma transmeta_1: "x = y \<Longrightarrow> y == z \<Longrightarrow> x = z" by simp |
|
11 lemma transmeta_2: "x == y \<Longrightarrow> y = z \<Longrightarrow> x = z" by simp |
|
12 lemma transmeta_3: "x == y \<Longrightarrow> y == z \<Longrightarrow> x = z" by simp |
|
13 |
|
14 |
|
15 (**** compute_if ****) |
|
16 |
|
17 lemma If_True: "If True = (\<lambda> x y. x)" by ((rule ext)+,auto) |
|
18 lemma If_False: "If False = (\<lambda> x y. y)" by ((rule ext)+, auto) |
|
19 |
|
20 lemmas compute_if = If_True If_False |
|
21 |
|
22 (**** compute_bool ****) |
|
23 |
|
24 lemma bool1: "(\<not> True) = False" by blast |
|
25 lemma bool2: "(\<not> False) = True" by blast |
|
26 lemma bool3: "(P \<and> True) = P" by blast |
|
27 lemma bool4: "(True \<and> P) = P" by blast |
|
28 lemma bool5: "(P \<and> False) = False" by blast |
|
29 lemma bool6: "(False \<and> P) = False" by blast |
|
30 lemma bool7: "(P \<or> True) = True" by blast |
|
31 lemma bool8: "(True \<or> P) = True" by blast |
|
32 lemma bool9: "(P \<or> False) = P" by blast |
|
33 lemma bool10: "(False \<or> P) = P" by blast |
|
34 lemma bool11: "(True \<longrightarrow> P) = P" by blast |
|
35 lemma bool12: "(P \<longrightarrow> True) = True" by blast |
|
36 lemma bool13: "(True \<longrightarrow> P) = P" by blast |
|
37 lemma bool14: "(P \<longrightarrow> False) = (\<not> P)" by blast |
|
38 lemma bool15: "(False \<longrightarrow> P) = True" by blast |
|
39 lemma bool16: "(False = False) = True" by blast |
|
40 lemma bool17: "(True = True) = True" by blast |
|
41 lemma bool18: "(False = True) = False" by blast |
|
42 lemma bool19: "(True = False) = False" by blast |
|
43 |
|
44 lemmas compute_bool = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 bool11 bool12 bool13 bool14 bool15 bool16 bool17 bool18 bool19 |
|
45 |
|
46 |
|
47 (*** compute_pair ***) |
|
48 |
|
49 lemma compute_fst: "fst (x,y) = x" by simp |
|
50 lemma compute_snd: "snd (x,y) = y" by simp |
|
51 lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \<and> b = d)" by auto |
|
52 |
|
53 lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp |
|
54 |
|
55 lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_simp |
|
56 |
|
57 (*** compute_option ***) |
|
58 |
|
59 lemma compute_the: "the (Some x) = x" by simp |
|
60 lemma compute_None_Some_eq: "(None = Some x) = False" by auto |
|
61 lemma compute_Some_None_eq: "(Some x = None) = False" by auto |
|
62 lemma compute_None_None_eq: "(None = None) = True" by auto |
|
63 lemma compute_Some_Some_eq: "(Some x = Some y) = (x = y)" by auto |
|
64 |
|
65 definition |
|
66 option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
|
67 where |
|
68 "option_case_compute opt a f = option_case a f opt" |
|
69 |
|
70 lemma option_case_compute: "option_case = (\<lambda> a f opt. option_case_compute opt a f)" |
|
71 by (simp add: option_case_compute_def) |
|
72 |
|
73 lemma option_case_compute_None: "option_case_compute None = (\<lambda> a f. a)" |
|
74 apply (rule ext)+ |
|
75 apply (simp add: option_case_compute_def) |
|
76 done |
|
77 |
|
78 lemma option_case_compute_Some: "option_case_compute (Some x) = (\<lambda> a f. f x)" |
|
79 apply (rule ext)+ |
|
80 apply (simp add: option_case_compute_def) |
|
81 done |
|
82 |
|
83 lemmas compute_option_case = option_case_compute option_case_compute_None option_case_compute_Some |
|
84 |
|
85 lemmas compute_option = compute_the compute_None_Some_eq compute_Some_None_eq compute_None_None_eq compute_Some_Some_eq compute_option_case |
|
86 |
|
87 (**** compute_list_length ****) |
|
88 |
|
89 lemma length_cons:"length (x#xs) = 1 + (length xs)" |
|
90 by simp |
|
91 |
|
92 lemma length_nil: "length [] = 0" |
|
93 by simp |
|
94 |
|
95 lemmas compute_list_length = length_nil length_cons |
|
96 |
|
97 (*** compute_list_case ***) |
|
98 |
|
99 definition |
|
100 list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a" |
|
101 where |
|
102 "list_case_compute l a f = list_case a f l" |
|
103 |
|
104 lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)" |
|
105 apply (rule ext)+ |
|
106 apply (simp add: list_case_compute_def) |
|
107 done |
|
108 |
|
109 lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)" |
|
110 apply (rule ext)+ |
|
111 apply (simp add: list_case_compute_def) |
|
112 done |
|
113 |
|
114 lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))" |
|
115 apply (rule ext)+ |
|
116 apply (simp add: list_case_compute_def) |
|
117 done |
|
118 |
|
119 lemmas compute_list_case = list_case_compute list_case_compute_empty list_case_compute_cons |
|
120 |
|
121 (*** compute_list_nth ***) |
|
122 (* Of course, you will need computation with nats for this to work \<dots> *) |
|
123 |
|
124 lemma compute_list_nth: "((x#xs) ! n) = (if n = 0 then x else (xs ! (n - 1)))" |
|
125 by (cases n, auto) |
|
126 |
|
127 (*** compute_list ***) |
|
128 |
|
129 lemmas compute_list = compute_list_case compute_list_length compute_list_nth |
|
130 |
|
131 (*** compute_let ***) |
|
132 |
|
133 lemmas compute_let = Let_def |
|
134 |
|
135 (***********************) |
|
136 (* Everything together *) |
|
137 (***********************) |
|
138 |
|
139 lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let |
|
140 |
|
141 ML {* |
|
142 signature ComputeHOL = |
|
143 sig |
|
144 val prep_thms : thm list -> thm list |
|
145 val to_meta_eq : thm -> thm |
|
146 val to_hol_eq : thm -> thm |
|
147 val symmetric : thm -> thm |
|
148 val trans : thm -> thm -> thm |
|
149 end |
|
150 |
|
151 structure ComputeHOL : ComputeHOL = |
|
152 struct |
|
153 |
|
154 local |
|
155 fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq)); |
|
156 in |
|
157 fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", []) |
|
158 | rewrite_conv (eq :: eqs) ct = |
|
159 Thm.instantiate (Thm.match (lhs_of eq, ct)) eq |
|
160 handle Pattern.MATCH => rewrite_conv eqs ct; |
|
161 end |
|
162 |
|
163 val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}]))) |
|
164 |
|
165 val eq_th = @{thm "HOL.eq_reflection"} |
|
166 val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"} |
|
167 val bool_to_true = @{thm "ComputeHOL.bool_to_true"} |
|
168 |
|
169 fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th] |
|
170 |
|
171 fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] |
|
172 |
|
173 fun prep_thms ths = map (convert_conditions o to_meta_eq) ths |
|
174 |
|
175 fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th] |
|
176 |
|
177 local |
|
178 val trans_HOL = @{thm "HOL.trans"} |
|
179 val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"} |
|
180 val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"} |
|
181 val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"} |
|
182 fun tr [] th1 th2 = trans_HOL OF [th1, th2] |
|
183 | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) |
|
184 in |
|
185 fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2 |
|
186 end |
|
187 |
|
188 end |
|
189 *} |
|
190 |
|
191 end |
|