src/HOL/Matrix/ComputeHOL.thy
 author wenzelm Fri Dec 17 17:43:54 2010 +0100 (2010-12-17) changeset 41229 d797baa3d57c parent 38273 d31a34569542 child 46984 0f1e85fcf5f4 permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
```     1 theory ComputeHOL
```
```     2 imports Complex_Main "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 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"
```
```    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
```
```    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"
```
```    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
```
```   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
```
```   145 end
```
```   146
```
```   147 structure ComputeHOL : ComputeHOL =
```
```   148 struct
```
```   149
```
```   150 local
```
```   151 fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
```
```   152 in
```
```   153 fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
```
```   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
```
```   171 fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th]
```
```   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
```