author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46988  9f492f5b0cec 
child 55413  a8e96847523c 
permissions  rwrr 
25216  1 
theory ComputeHOL 
37872
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
32491
diff
changeset

2 
imports Complex_Main "Compute_Oracle/Compute_Oracle" 
23664  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 

38273  65 
definition option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" 
66 
where "option_case_compute opt a f = option_case a f opt" 

23664  67 

68 
lemma option_case_compute: "option_case = (\<lambda> a f opt. option_case_compute opt a f)" 

69 
by (simp add: option_case_compute_def) 

70 

71 
lemma option_case_compute_None: "option_case_compute None = (\<lambda> a f. a)" 

72 
apply (rule ext)+ 

73 
apply (simp add: option_case_compute_def) 

74 
done 

75 

76 
lemma option_case_compute_Some: "option_case_compute (Some x) = (\<lambda> a f. f x)" 

77 
apply (rule ext)+ 

78 
apply (simp add: option_case_compute_def) 

79 
done 

80 

81 
lemmas compute_option_case = option_case_compute option_case_compute_None option_case_compute_Some 

82 

83 
lemmas compute_option = compute_the compute_None_Some_eq compute_Some_None_eq compute_None_None_eq compute_Some_Some_eq compute_option_case 

84 

85 
(**** compute_list_length ****) 

86 

87 
lemma length_cons:"length (x#xs) = 1 + (length xs)" 

88 
by simp 

89 

90 
lemma length_nil: "length [] = 0" 

91 
by simp 

92 

93 
lemmas compute_list_length = length_nil length_cons 

94 

95 
(*** compute_list_case ***) 

96 

38273  97 
definition list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a" 
98 
where "list_case_compute l a f = list_case a f l" 

23664  99 

100 
lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)" 

101 
apply (rule ext)+ 

102 
apply (simp add: list_case_compute_def) 

103 
done 

104 

105 
lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)" 

106 
apply (rule ext)+ 

107 
apply (simp add: list_case_compute_def) 

108 
done 

109 

110 
lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))" 

111 
apply (rule ext)+ 

112 
apply (simp add: list_case_compute_def) 

113 
done 

114 

115 
lemmas compute_list_case = list_case_compute list_case_compute_empty list_case_compute_cons 

116 

117 
(*** compute_list_nth ***) 

118 
(* Of course, you will need computation with nats for this to work \<dots> *) 

119 

120 
lemma compute_list_nth: "((x#xs) ! n) = (if n = 0 then x else (xs ! (n  1)))" 

121 
by (cases n, auto) 

122 

123 
(*** compute_list ***) 

124 

125 
lemmas compute_list = compute_list_case compute_list_length compute_list_nth 

126 

127 
(*** compute_let ***) 

128 

129 
lemmas compute_let = Let_def 

130 

131 
(***********************) 

132 
(* Everything together *) 

133 
(***********************) 

134 

135 
lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let 

136 

23667  137 
ML {* 
138 
signature ComputeHOL = 

139 
sig 

140 
val prep_thms : thm list > thm list 

141 
val to_meta_eq : thm > thm 

142 
val to_hol_eq : thm > thm 

143 
val symmetric : thm > thm 

144 
val trans : thm > thm > thm 

23664  145 
end 
23667  146 

147 
structure ComputeHOL : ComputeHOL = 

148 
struct 

149 

150 
local 

151 
fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq)); 

152 
in 

46984  153 
fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [ct]) 
23667  154 
 rewrite_conv (eq :: eqs) ct = 
155 
Thm.instantiate (Thm.match (lhs_of eq, ct)) eq 

156 
handle Pattern.MATCH => rewrite_conv eqs ct; 

157 
end 

158 

159 
val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}]))) 

160 

161 
val eq_th = @{thm "HOL.eq_reflection"} 

162 
val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"} 

163 
val bool_to_true = @{thm "ComputeHOL.bool_to_true"} 

164 

165 
fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th] 

166 

167 
fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] 

168 

169 
fun prep_thms ths = map (convert_conditions o to_meta_eq) ths 

170 

26424  171 
fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th] 
23667  172 

173 
local 

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

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

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

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

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

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

180 
in 

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

182 
end 

183 

184 
end 

185 
*} 

186 

187 
end 