src/HOL/Tools/ComputeHOL.thy
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 28562 4e74209f113e
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25216
eb512c1717ea adapted Compute...
obua
parents: 23667
diff changeset
     1
theory ComputeHOL
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 26424
diff changeset
     2
imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
23664
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     3
begin
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     4
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     5
lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     6
lemma meta_eq_trivial: "x == y \<Longrightarrow> x == y" by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     7
lemma meta_eq_imp_eq: "x == y \<Longrightarrow> x = y" by auto
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     8
lemma eq_trivial: "x = y \<Longrightarrow> x = y" by auto
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     9
lemma bool_to_true: "x :: bool \<Longrightarrow> x == True"  by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    10
lemma transmeta_1: "x = y \<Longrightarrow> y == z \<Longrightarrow> x = z" by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    11
lemma transmeta_2: "x == y \<Longrightarrow> y = z \<Longrightarrow> x = z" by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    12
lemma transmeta_3: "x == y \<Longrightarrow> y == z \<Longrightarrow> x = z" by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    13
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    14
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    15
(**** compute_if ****)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    16
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    17
lemma If_True: "If True = (\<lambda> x y. x)" by ((rule ext)+,auto)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    18
lemma If_False: "If False = (\<lambda> x y. y)" by ((rule ext)+, auto)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    19
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    20
lemmas compute_if = If_True If_False
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    21
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    22
(**** compute_bool ****)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    23
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    24
lemma bool1: "(\<not> True) = False"  by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    25
lemma bool2: "(\<not> False) = True"  by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    26
lemma bool3: "(P \<and> True) = P" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    27
lemma bool4: "(True \<and> P) = P" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    28
lemma bool5: "(P \<and> False) = False" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    29
lemma bool6: "(False \<and> P) = False" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    30
lemma bool7: "(P \<or> True) = True" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    31
lemma bool8: "(True \<or> P) = True" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    32
lemma bool9: "(P \<or> False) = P" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    33
lemma bool10: "(False \<or> P) = P" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    34
lemma bool11: "(True \<longrightarrow> P) = P" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    35
lemma bool12: "(P \<longrightarrow> True) = True" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    36
lemma bool13: "(True \<longrightarrow> P) = P" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    37
lemma bool14: "(P \<longrightarrow> False) = (\<not> P)" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    38
lemma bool15: "(False \<longrightarrow> P) = True" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    39
lemma bool16: "(False = False) = True" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    40
lemma bool17: "(True = True) = True" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    41
lemma bool18: "(False = True) = False" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    42
lemma bool19: "(True = False) = False" by blast
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    43
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    44
lemmas compute_bool = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 bool11 bool12 bool13 bool14 bool15 bool16 bool17 bool18 bool19
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    45
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    46
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    47
(*** compute_pair ***)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    48
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    49
lemma compute_fst: "fst (x,y) = x" by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    50
lemma compute_snd: "snd (x,y) = y" by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    51
lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \<and> b = d)" by auto
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    52
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    53
lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    54
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    55
lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    56
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    57
(*** compute_option ***)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    58
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    59
lemma compute_the: "the (Some x) = x" by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    60
lemma compute_None_Some_eq: "(None = Some x) = False" by auto
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    61
lemma compute_Some_None_eq: "(Some x = None) = False" by auto
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    62
lemma compute_None_None_eq: "(None = None) = True" by auto
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    63
lemma compute_Some_Some_eq: "(Some x = Some y) = (x = y)" by auto
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    64
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    65
definition
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    66
   option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    67
where
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    68
   "option_case_compute opt a f = option_case a f opt"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    69
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    70
lemma option_case_compute: "option_case = (\<lambda> a f opt. option_case_compute opt a f)"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    71
  by (simp add: option_case_compute_def)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    72
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    73
lemma option_case_compute_None: "option_case_compute None = (\<lambda> a f. a)"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    74
  apply (rule ext)+
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    75
  apply (simp add: option_case_compute_def)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    76
  done
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    77
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    78
lemma option_case_compute_Some: "option_case_compute (Some x) = (\<lambda> a f. f x)"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    79
  apply (rule ext)+
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    80
  apply (simp add: option_case_compute_def)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    81
  done
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    82
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    83
lemmas compute_option_case = option_case_compute option_case_compute_None option_case_compute_Some
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    84
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    86
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    87
(**** compute_list_length ****)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    88
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    89
lemma length_cons:"length (x#xs) = 1 + (length xs)"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    90
  by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    91
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    92
lemma length_nil: "length [] = 0"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    93
  by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    94
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    95
lemmas compute_list_length = length_nil length_cons
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    96
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    97
(*** compute_list_case ***)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    98
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    99
definition
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   100
  list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   101
where
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   102
  "list_case_compute l a f = list_case a f l"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   103
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   104
lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   105
  apply (rule ext)+
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   106
  apply (simp add: list_case_compute_def)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   107
  done
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   108
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   109
lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   110
  apply (rule ext)+
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   111
  apply (simp add: list_case_compute_def)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   112
  done
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   113
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   114
lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   115
  apply (rule ext)+
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   116
  apply (simp add: list_case_compute_def)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   117
  done
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   118
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   119
lemmas compute_list_case = list_case_compute list_case_compute_empty list_case_compute_cons
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   120
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   121
(*** compute_list_nth ***)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   122
(* Of course, you will need computation with nats for this to work \<dots> *)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   123
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   124
lemma compute_list_nth: "((x#xs) ! n) = (if n = 0 then x else (xs ! (n - 1)))"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   125
  by (cases n, auto)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   126
  
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   127
(*** compute_list ***)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   128
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   129
lemmas compute_list = compute_list_case compute_list_length compute_list_nth
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   130
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   131
(*** compute_let ***)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   132
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   133
lemmas compute_let = Let_def
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   134
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   135
(***********************)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   136
(* Everything together *)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   137
(***********************)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   138
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   139
lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   140
23667
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   141
ML {*
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   142
signature ComputeHOL =
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   143
sig
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   144
  val prep_thms : thm list -> thm list
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   145
  val to_meta_eq : thm -> thm
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   146
  val to_hol_eq : thm -> thm
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   147
  val symmetric : thm -> thm 
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   148
  val trans : thm -> thm -> thm
23664
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
   149
end
23667
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   150
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   151
structure ComputeHOL : ComputeHOL =
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   152
struct
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   153
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   154
local
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   155
fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   156
in
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   157
fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   158
  | rewrite_conv (eq :: eqs) ct =
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   159
      Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   160
      handle Pattern.MATCH => rewrite_conv eqs ct;
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   161
end
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   162
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   163
val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}])))
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   164
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   165
val eq_th = @{thm "HOL.eq_reflection"}
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   166
val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"}
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   167
val bool_to_true = @{thm "ComputeHOL.bool_to_true"}
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   168
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   169
fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th]
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   170
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   171
fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] 
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   172
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   173
fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   174
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 25216
diff changeset
   175
fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th]
23667
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   176
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   177
local
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   178
    val trans_HOL = @{thm "HOL.trans"}
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   179
    val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"}
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   180
    val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"}
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   181
    val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"}
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   182
    fun tr [] th1 th2 = trans_HOL OF [th1, th2]
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   183
      | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) 
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   184
in
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   185
  fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   186
end
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   187
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   188
end
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   189
*}
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   190
a4e93948f72a removed legacy ML file;
wenzelm
parents: 23664
diff changeset
   191
end