removed legacy ML file;
authorwenzelm
Mon Jul 09 22:37:48 2007 +0200 (2007-07-09)
changeset 23667a4e93948f72a
parent 23666 48816d825078
child 23668 8b5a2a79a6e3
removed legacy ML file;
fixed prems_conv;
src/HOL/Tools/ComputeHOL.ML
src/HOL/Tools/ComputeHOL.thy
     1.1 --- a/src/HOL/Tools/ComputeHOL.ML	Mon Jul 09 22:06:49 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,54 +0,0 @@
     1.4 -signature ComputeHOL =
     1.5 -sig
     1.6 -  val prep_thms : thm list -> thm list
     1.7 -  val to_meta_eq : thm -> thm
     1.8 -  val to_hol_eq : thm -> thm
     1.9 -  val symmetric : thm -> thm 
    1.10 -  val trans : thm -> thm -> thm
    1.11 -end
    1.12 -
    1.13 -structure ComputeHOL : ComputeHOL =
    1.14 -struct
    1.15 -
    1.16 -fun all_prems_conv ci ct = Conv.prems_conv (Logic.count_prems (term_of ct)) ci ct
    1.17 -
    1.18 -local
    1.19 -fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
    1.20 -in
    1.21 -fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
    1.22 -  | rewrite_conv (eq :: eqs) ct =
    1.23 -      Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
    1.24 -      handle Pattern.MATCH => rewrite_conv eqs ct;
    1.25 -end
    1.26 -
    1.27 -val convert_conditions = Conv.fconv_rule (all_prems_conv (fn _ => Conv.else_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}], Conv.all_conv)))
    1.28 -
    1.29 -val eq_th = @{thm "HOL.eq_reflection"}
    1.30 -val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"}
    1.31 -val bool_to_true = @{thm "ComputeHOL.bool_to_true"}
    1.32 -
    1.33 -fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th]
    1.34 -
    1.35 -fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] 
    1.36 -
    1.37 -fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
    1.38 -
    1.39 -local
    1.40 -    val sym_HOL = @{thm "HOL.sym"}
    1.41 -    val sym_Pure = @{thm "ProtoPure.symmetric"}
    1.42 -in
    1.43 -  fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th]))
    1.44 -end
    1.45 -
    1.46 -local
    1.47 -    val trans_HOL = @{thm "HOL.trans"}
    1.48 -    val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"}
    1.49 -    val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"}
    1.50 -    val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"}
    1.51 -    fun tr [] th1 th2 = trans_HOL OF [th1, th2]
    1.52 -      | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) 
    1.53 -in
    1.54 -  fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2
    1.55 -end
    1.56 -
    1.57 -end
    1.58 \ No newline at end of file
     2.1 --- a/src/HOL/Tools/ComputeHOL.thy	Mon Jul 09 22:06:49 2007 +0200
     2.2 +++ b/src/HOL/Tools/ComputeHOL.thy	Mon Jul 09 22:37:48 2007 +0200
     2.3 @@ -138,4 +138,59 @@
     2.4  
     2.5  lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let
     2.6  
     2.7 +ML {*
     2.8 +signature ComputeHOL =
     2.9 +sig
    2.10 +  val prep_thms : thm list -> thm list
    2.11 +  val to_meta_eq : thm -> thm
    2.12 +  val to_hol_eq : thm -> thm
    2.13 +  val symmetric : thm -> thm 
    2.14 +  val trans : thm -> thm -> thm
    2.15  end
    2.16 +
    2.17 +structure ComputeHOL : ComputeHOL =
    2.18 +struct
    2.19 +
    2.20 +local
    2.21 +fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
    2.22 +in
    2.23 +fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
    2.24 +  | rewrite_conv (eq :: eqs) ct =
    2.25 +      Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
    2.26 +      handle Pattern.MATCH => rewrite_conv eqs ct;
    2.27 +end
    2.28 +
    2.29 +val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}])))
    2.30 +
    2.31 +val eq_th = @{thm "HOL.eq_reflection"}
    2.32 +val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"}
    2.33 +val bool_to_true = @{thm "ComputeHOL.bool_to_true"}
    2.34 +
    2.35 +fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th]
    2.36 +
    2.37 +fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] 
    2.38 +
    2.39 +fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
    2.40 +
    2.41 +local
    2.42 +    val sym_HOL = @{thm "HOL.sym"}
    2.43 +    val sym_Pure = @{thm "ProtoPure.symmetric"}
    2.44 +in
    2.45 +  fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th]))
    2.46 +end
    2.47 +
    2.48 +local
    2.49 +    val trans_HOL = @{thm "HOL.trans"}
    2.50 +    val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"}
    2.51 +    val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"}
    2.52 +    val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"}
    2.53 +    fun tr [] th1 th2 = trans_HOL OF [th1, th2]
    2.54 +      | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) 
    2.55 +in
    2.56 +  fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2
    2.57 +end
    2.58 +
    2.59 +end
    2.60 +*}
    2.61 +
    2.62 +end