23664

1 
theory ComputeHOL


2 
imports 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 

23667

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

23664

149 
end

23667

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 
local


176 
val sym_HOL = @{thm "HOL.sym"}


177 
val sym_Pure = @{thm "ProtoPure.symmetric"}


178 
in


179 
fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th]))


180 
end


181 


182 
local


183 
val trans_HOL = @{thm "HOL.trans"}


184 
val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"}


185 
val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"}


186 
val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"}


187 
fun tr [] th1 th2 = trans_HOL OF [th1, th2]


188 
 tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2)


189 
in


190 
fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2


191 
end


192 


193 
end


194 
*}


195 


196 
end
