src/HOL/Matrix/ComputeHOL.thy
author haftmann
Fri Nov 27 08:41:10 2009 +0100 (2009-11-27)
changeset 33963 977b94b64905
parent 32491 d5d8bea0cd94
child 37872 d83659570337
permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
obua@25216
     1
theory ComputeHOL
haftmann@28562
     2
imports Complex_Main "~~/src/Tools/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 \<Longrightarrow> x == y" by simp
obua@23664
     7
lemma meta_eq_imp_eq: "x == y \<Longrightarrow> x = y" by auto
obua@23664
     8
lemma eq_trivial: "x = y \<Longrightarrow> x = y" by auto
obua@23664
     9
lemma bool_to_true: "x :: bool \<Longrightarrow> x == True"  by simp
obua@23664
    10
lemma transmeta_1: "x = y \<Longrightarrow> y == z \<Longrightarrow> x = z" by simp
obua@23664
    11
lemma transmeta_2: "x == y \<Longrightarrow> y = z \<Longrightarrow> x = z" by simp
obua@23664
    12
lemma transmeta_3: "x == y \<Longrightarrow> y == z \<Longrightarrow> 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 = (\<lambda> x y. x)" by ((rule ext)+,auto)
obua@23664
    18
lemma If_False: "If False = (\<lambda> 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: "(\<not> True) = False"  by blast
obua@23664
    25
lemma bool2: "(\<not> False) = True"  by blast
obua@23664
    26
lemma bool3: "(P \<and> True) = P" by blast
obua@23664
    27
lemma bool4: "(True \<and> P) = P" by blast
obua@23664
    28
lemma bool5: "(P \<and> False) = False" by blast
obua@23664
    29
lemma bool6: "(False \<and> P) = False" by blast
obua@23664
    30
lemma bool7: "(P \<or> True) = True" by blast
obua@23664
    31
lemma bool8: "(True \<or> P) = True" by blast
obua@23664
    32
lemma bool9: "(P \<or> False) = P" by blast
obua@23664
    33
lemma bool10: "(False \<or> P) = P" by blast
obua@23664
    34
lemma bool11: "(True \<longrightarrow> P) = P" by blast
obua@23664
    35
lemma bool12: "(P \<longrightarrow> True) = True" by blast
obua@23664
    36
lemma bool13: "(True \<longrightarrow> P) = P" by blast
obua@23664
    37
lemma bool14: "(P \<longrightarrow> False) = (\<not> P)" by blast
obua@23664
    38
lemma bool15: "(False \<longrightarrow> 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 \<and> b = d)" by auto
obua@23664
    52
obua@23664
    53
lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp
obua@23664
    54
obua@23664
    55
lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_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
obua@23664
    65
definition
obua@23664
    66
   option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
obua@23664
    67
where
obua@23664
    68
   "option_case_compute opt a f = option_case a f opt"
obua@23664
    69
obua@23664
    70
lemma option_case_compute: "option_case = (\<lambda> a f opt. option_case_compute opt a f)"
obua@23664
    71
  by (simp add: option_case_compute_def)
obua@23664
    72
obua@23664
    73
lemma option_case_compute_None: "option_case_compute None = (\<lambda> a f. a)"
obua@23664
    74
  apply (rule ext)+
obua@23664
    75
  apply (simp add: option_case_compute_def)
obua@23664
    76
  done
obua@23664
    77
obua@23664
    78
lemma option_case_compute_Some: "option_case_compute (Some x) = (\<lambda> a f. f x)"
obua@23664
    79
  apply (rule ext)+
obua@23664
    80
  apply (simp add: option_case_compute_def)
obua@23664
    81
  done
obua@23664
    82
obua@23664
    83
lemmas compute_option_case = option_case_compute option_case_compute_None option_case_compute_Some
obua@23664
    84
obua@23664
    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
obua@23664
    86
obua@23664
    87
(**** compute_list_length ****)
obua@23664
    88
obua@23664
    89
lemma length_cons:"length (x#xs) = 1 + (length xs)"
obua@23664
    90
  by simp
obua@23664
    91
obua@23664
    92
lemma length_nil: "length [] = 0"
obua@23664
    93
  by simp
obua@23664
    94
obua@23664
    95
lemmas compute_list_length = length_nil length_cons
obua@23664
    96
obua@23664
    97
(*** compute_list_case ***)
obua@23664
    98
obua@23664
    99
definition
obua@23664
   100
  list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
obua@23664
   101
where
obua@23664
   102
  "list_case_compute l a f = list_case a f l"
obua@23664
   103
obua@23664
   104
lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
obua@23664
   105
  apply (rule ext)+
obua@23664
   106
  apply (simp add: list_case_compute_def)
obua@23664
   107
  done
obua@23664
   108
obua@23664
   109
lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)"
obua@23664
   110
  apply (rule ext)+
obua@23664
   111
  apply (simp add: list_case_compute_def)
obua@23664
   112
  done
obua@23664
   113
obua@23664
   114
lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))"
obua@23664
   115
  apply (rule ext)+
obua@23664
   116
  apply (simp add: list_case_compute_def)
obua@23664
   117
  done
obua@23664
   118
obua@23664
   119
lemmas compute_list_case = list_case_compute list_case_compute_empty list_case_compute_cons
obua@23664
   120
obua@23664
   121
(*** compute_list_nth ***)
obua@23664
   122
(* Of course, you will need computation with nats for this to work \<dots> *)
obua@23664
   123
obua@23664
   124
lemma compute_list_nth: "((x#xs) ! n) = (if n = 0 then x else (xs ! (n - 1)))"
obua@23664
   125
  by (cases n, auto)
obua@23664
   126
  
obua@23664
   127
(*** compute_list ***)
obua@23664
   128
obua@23664
   129
lemmas compute_list = compute_list_case compute_list_length compute_list_nth
obua@23664
   130
obua@23664
   131
(*** compute_let ***)
obua@23664
   132
obua@23664
   133
lemmas compute_let = Let_def
obua@23664
   134
obua@23664
   135
(***********************)
obua@23664
   136
(* Everything together *)
obua@23664
   137
(***********************)
obua@23664
   138
obua@23664
   139
lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let
obua@23664
   140
wenzelm@23667
   141
ML {*
wenzelm@23667
   142
signature ComputeHOL =
wenzelm@23667
   143
sig
wenzelm@23667
   144
  val prep_thms : thm list -> thm list
wenzelm@23667
   145
  val to_meta_eq : thm -> thm
wenzelm@23667
   146
  val to_hol_eq : thm -> thm
wenzelm@23667
   147
  val symmetric : thm -> thm 
wenzelm@23667
   148
  val trans : thm -> thm -> thm
obua@23664
   149
end
wenzelm@23667
   150
wenzelm@23667
   151
structure ComputeHOL : ComputeHOL =
wenzelm@23667
   152
struct
wenzelm@23667
   153
wenzelm@23667
   154
local
wenzelm@23667
   155
fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
wenzelm@23667
   156
in
wenzelm@23667
   157
fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
wenzelm@23667
   158
  | rewrite_conv (eq :: eqs) ct =
wenzelm@23667
   159
      Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
wenzelm@23667
   160
      handle Pattern.MATCH => rewrite_conv eqs ct;
wenzelm@23667
   161
end
wenzelm@23667
   162
wenzelm@23667
   163
val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}])))
wenzelm@23667
   164
wenzelm@23667
   165
val eq_th = @{thm "HOL.eq_reflection"}
wenzelm@23667
   166
val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"}
wenzelm@23667
   167
val bool_to_true = @{thm "ComputeHOL.bool_to_true"}
wenzelm@23667
   168
wenzelm@23667
   169
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
   170
wenzelm@23667
   171
fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] 
wenzelm@23667
   172
wenzelm@23667
   173
fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
wenzelm@23667
   174
wenzelm@26424
   175
fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th]
wenzelm@23667
   176
wenzelm@23667
   177
local
wenzelm@23667
   178
    val trans_HOL = @{thm "HOL.trans"}
wenzelm@23667
   179
    val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"}
wenzelm@23667
   180
    val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"}
wenzelm@23667
   181
    val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"}
wenzelm@23667
   182
    fun tr [] th1 th2 = trans_HOL OF [th1, th2]
wenzelm@23667
   183
      | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) 
wenzelm@23667
   184
in
wenzelm@23667
   185
  fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2
wenzelm@23667
   186
end
wenzelm@23667
   187
wenzelm@23667
   188
end
wenzelm@23667
   189
*}
wenzelm@23667
   190
wenzelm@23667
   191
end