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