src/HOL/Matrix_LP/ComputeHOL.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 63167 0909deb8059b
permissions -rw-r--r--
tuned: each session has at most one defining entry;
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 \<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
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 \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> '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 = (\<lambda> 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 = (\<lambda> 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) = (\<lambda> 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 \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> '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 = (\<lambda> (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) = (\<lambda> (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) = (\<lambda> (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 \<dots> *)
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@63167
   137
ML \<open>
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@59582
   151
fun lhs_of eq = fst (Thm.dest_equals (Thm.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@63167
   185
\<close>
wenzelm@23667
   186
wenzelm@23667
   187
end