removed HOL structure
authorhaftmann
Mon Nov 27 13:42:33 2006 +0100 (2006-11-27)
changeset 21546268b6bed0cc8
parent 21545 54cc492d80a9
child 21547 9c9fdf4c2949
removed HOL structure
src/HOL/Code_Generator.thy
src/HOL/HOL.ML
src/HOL/Import/hol4rews.ML
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Orderings.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/record_package.ML
src/HOL/ex/MT.ML
     1.1 --- a/src/HOL/Code_Generator.thy	Mon Nov 27 13:42:30 2006 +0100
     1.2 +++ b/src/HOL/Code_Generator.thy	Mon Nov 27 13:42:33 2006 +0100
     1.3 @@ -64,11 +64,11 @@
     1.4  setup {*
     1.5  let
     1.6  
     1.7 +val TrueI = thm "TrueI"
     1.8  fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
     1.9    (Drule.goals_conv (equal i) Codegen.evaluation_conv));
    1.10 -
    1.11  val evaluation_meth =
    1.12 -  Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1));
    1.13 +  Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac TrueI 1));
    1.14  
    1.15  in
    1.16  
    1.17 @@ -143,7 +143,7 @@
    1.18    in Thm.invoke_oracle_i thy oracle_name (thy, Eval t) end;
    1.19  
    1.20  fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    1.21 -  (Drule.goals_conv (equal i) (HOL.Trueprop_conv conv)));
    1.22 +  (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv conv)));
    1.23  
    1.24  val method =
    1.25    Method.no_args (Method.METHOD (fn _ =>
    1.26 @@ -163,7 +163,7 @@
    1.27  setup {*
    1.28  let
    1.29    fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    1.30 -    (Drule.goals_conv (equal i) (HOL.Trueprop_conv
    1.31 +    (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv
    1.32        NBE.normalization_conv)));
    1.33    val normalization_meth =
    1.34      Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl] 1));
     2.1 --- a/src/HOL/HOL.ML	Mon Nov 27 13:42:30 2006 +0100
     2.2 +++ b/src/HOL/HOL.ML	Mon Nov 27 13:42:33 2006 +0100
     2.3 @@ -1,19 +1,36 @@
     2.4  (* legacy ML bindings *)
     2.5  
     2.6 -val HOL_cs = HOL.claset;
     2.7 -val HOL_basic_ss = HOL.simpset_basic;
     2.8 -val HOL_ss = HOL.simpset;
     2.9 -val hol_simplify = HOL.simplify;
    2.10 +val Blast_tac = Blast.Blast_tac;
    2.11 +val blast_tac = Blast.blast_tac;
    2.12 +
    2.13 +(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
    2.14 +local
    2.15 +  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
    2.16 +    | wrong_prem (Bound _) = true
    2.17 +    | wrong_prem _ = false;
    2.18 +  val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
    2.19 +  val spec = thm "spec"
    2.20 +  val mp = thm "mp"
    2.21 +in
    2.22 +  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
    2.23 +  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
    2.24 +end;
    2.25 +
    2.26 +fun strip_tac i = REPEAT (resolve_tac [thm "impI", thm "allI"] i);
    2.27  
    2.28  val split_tac        = Splitter.split_tac;
    2.29  val split_inside_tac = Splitter.split_inside_tac;
    2.30  val split_asm_tac    = Splitter.split_asm_tac;
    2.31 +
    2.32  val op addsplits     = Splitter.addsplits;
    2.33  val op delsplits     = Splitter.delsplits;
    2.34  val Addsplits        = Splitter.Addsplits;
    2.35  val Delsplits        = Splitter.Delsplits;
    2.36  
    2.37 -open HOL;
    2.38 +val HOL_basic_ss = Simpdata.simpset_basic;
    2.39 +val hol_simplify = Simpdata.simplify;
    2.40 +
    2.41 +open Simpdata;
    2.42  val claset = Classical.claset;
    2.43  val simpset = Simplifier.simpset;
    2.44  val simplify = Simplifier.simplify;
    2.45 @@ -21,6 +38,51 @@
    2.46  open BasicClassical;
    2.47  open Clasimp;
    2.48  
    2.49 +val eq_reflection = thm "eq_reflection";
    2.50 +val def_imp_eq = thm "def_imp_eq";
    2.51 +val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
    2.52 +val ccontr = thm "ccontr";
    2.53 +val impI = thm "impI";
    2.54 +val impCE = thm "impCE";
    2.55 +val notI = thm "notI";
    2.56 +val notE = thm "notE";
    2.57 +val iffI = thm "iffI";
    2.58 +val iffCE = thm "iffCE";
    2.59 +val conjI = thm "conjI";
    2.60 +val conjE = thm "conjE";
    2.61 +val disjCI = thm "disjCI";
    2.62 +val disjE = thm "disjE";
    2.63 +val TrueI = thm "TrueI";
    2.64 +val FalseE = thm "FalseE";
    2.65 +val allI = thm "allI";
    2.66 +val allE = thm "allE";
    2.67 +val exI = thm "exI";
    2.68 +val exE = thm "exE";
    2.69 +val ex_ex1I = thm "ex_ex1I";
    2.70 +val the_equality = thm "the_equality";
    2.71 +val mp = thm "mp";
    2.72 +val rev_mp = thm "rev_mp"
    2.73 +val classical = thm "classical";
    2.74 +val subst = thm "subst";
    2.75 +val refl = thm "refl";
    2.76 +val sym = thm "sym";
    2.77 +val trans = thm "trans";
    2.78 +val arg_cong = thm "arg_cong";
    2.79 +val iffD1 = thm "iffD1";
    2.80 +val iffD2 = thm "iffD2";
    2.81 +val disjE = thm "disjE";
    2.82 +val conjE = thm "conjE";
    2.83 +val exE = thm "exE";
    2.84 +val contrapos_nn = thm "contrapos_nn";
    2.85 +val contrapos_pp = thm "contrapos_pp";
    2.86 +val notnotD = thm "notnotD";
    2.87 +val conjunct1 = thm "conjunct1";
    2.88 +val conjunct2 = thm "conjunct2";
    2.89 +val spec = thm "spec";
    2.90 +val imp_cong = thm "imp_cong";
    2.91 +val the_sym_eq_trivial = thm "the_sym_eq_trivial";
    2.92 +val triv_forall_equality = thm "triv_forall_equality";
    2.93 +val case_split = thm "case_split_thm";
    2.94  val ext = thm "ext"
    2.95  val True_def = thm "True_def"
    2.96  val All_def = thm "All_def"
    2.97 @@ -75,7 +137,6 @@
    2.98  val let_weak_cong = thm "let_weak_cong"
    2.99  val eq_cong2 = thm "eq_cong2"
   2.100  val if_distrib = thm "if_distrib"
   2.101 -val expand_case = thm "expand_case"
   2.102  val restrict_to_left = thm "restrict_to_left"
   2.103  val all_conj_distrib = thm "all_conj_distrib";
   2.104  val atomize_not = thm "atomize_not";
   2.105 @@ -150,8 +211,6 @@
   2.106  structure HOL =
   2.107  struct
   2.108  
   2.109 -open HOL;
   2.110 -
   2.111  val thy = the_context ();
   2.112  
   2.113  end;
     3.1 --- a/src/HOL/Import/hol4rews.ML	Mon Nov 27 13:42:30 2006 +0100
     3.2 +++ b/src/HOL/Import/hol4rews.ML	Mon Nov 27 13:42:33 2006 +0100
     3.3 @@ -261,17 +261,21 @@
     3.4  val hol4_debug = ref false
     3.5  fun message s = if !hol4_debug then writeln s else ()
     3.6  
     3.7 +local
     3.8 +  val eq_reflection = thm "eq_reflection"
     3.9 +in
    3.10  fun add_hol4_rewrite (Context.Theory thy, th) =
    3.11      let
    3.12  	val _ = message "Adding HOL4 rewrite"
    3.13 -	val th1 = th RS HOL.eq_reflection
    3.14 +	val th1 = th RS eq_reflection
    3.15  	val current_rews = HOL4Rewrites.get thy
    3.16  	val new_rews = insert Thm.eq_thm th1 current_rews
    3.17  	val updated_thy  = HOL4Rewrites.put new_rews thy
    3.18      in
    3.19  	(Context.Theory updated_thy,th1)
    3.20      end
    3.21 -  | add_hol4_rewrite (context, th) = (context, th RS HOL.eq_reflection);
    3.22 +  | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
    3.23 +end
    3.24  
    3.25  fun ignore_hol4 bthy bthm thy =
    3.26      let
     4.1 --- a/src/HOL/Lambda/WeakNorm.thy	Mon Nov 27 13:42:30 2006 +0100
     4.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Mon Nov 27 13:42:33 2006 +0100
     4.3 @@ -584,7 +584,7 @@
     4.4  *}
     4.5  
     4.6  code_gen
     4.7 -  type_NF (SML *)
     4.8 +  type_NF (SML #)
     4.9  
    4.10  ML {*
    4.11  structure Norm = ROOT.WeakNorm;
     5.1 --- a/src/HOL/Library/EfficientNat.thy	Mon Nov 27 13:42:30 2006 +0100
     5.2 +++ b/src/HOL/Library/EfficientNat.thy	Mon Nov 27 13:42:33 2006 +0100
     5.3 @@ -315,10 +315,14 @@
     5.4  
     5.5  end; (*local*)
     5.6  
     5.7 -fun lift_obj_eq f thy =
     5.8 +local
     5.9 +  val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
    5.10 +  val eq_reflection = thm "eq_reflection";
    5.11 +in fun lift_obj_eq f thy =
    5.12    map (fn thm => thm RS meta_eq_to_obj_eq)
    5.13    #> f thy
    5.14 -  #> map (fn thm => thm RS HOL.eq_reflection)
    5.15 +  #> map (fn thm => thm RS eq_reflection)
    5.16 +end
    5.17  *}
    5.18  
    5.19  setup {*
     6.1 --- a/src/HOL/Orderings.thy	Mon Nov 27 13:42:30 2006 +0100
     6.2 +++ b/src/HOL/Orderings.thy	Mon Nov 27 13:42:33 2006 +0100
     6.3 @@ -822,6 +822,25 @@
     6.4    leave out the "(xtrans)" above.
     6.5  *)
     6.6  
     6.7 +subsection {* Order on bool *}
     6.8 +
     6.9 +instance bool :: linorder 
    6.10 +  le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
    6.11 +  less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
    6.12 +  by default (auto simp add: le_bool_def less_bool_def)
    6.13 +
    6.14 +lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
    6.15 +  by (simp add: le_bool_def)
    6.16 +
    6.17 +lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
    6.18 +  by (simp add: le_bool_def)
    6.19 +
    6.20 +lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    6.21 +  by (simp add: le_bool_def)
    6.22 +
    6.23 +lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    6.24 +  by (simp add: le_bool_def)
    6.25 +
    6.26  subsection {* Monotonicity, syntactic least value operator and min/max *}
    6.27  
    6.28  locale mono =
     7.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Nov 27 13:42:30 2006 +0100
     7.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Nov 27 13:42:33 2006 +0100
     7.3 @@ -406,6 +406,8 @@
     7.4  local
     7.5    val not_sym = thm "HOL.not_sym";
     7.6    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
     7.7 +  val refl = thm "refl";
     7.8 +  val eqTrueI = thm "eqTrueI";
     7.9  in
    7.10  
    7.11  fun get_eq_datatype thy dtco =
    7.12 @@ -416,11 +418,10 @@
    7.13          val ct' = Thm.cterm_of thy
    7.14            (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
    7.15          val cty' = Thm.ctyp_of_term ct';
    7.16 -        val refl = Thm.prop_of HOL.refl;
    7.17          val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
    7.18            (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
    7.19 -          refl NONE;
    7.20 -      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
    7.21 +          (Thm.prop_of refl) NONE;
    7.22 +      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) refl] end;
    7.23      val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
    7.24      val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
    7.25      val ctxt = ProofContext.init thy;
    7.26 @@ -498,11 +499,26 @@
    7.27    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    7.28     of SOME _ => get_eq_datatype thy tyco
    7.29      | NONE => [TypecopyPackage.get_eq thy tyco];
    7.30 +  fun constrain_op_eq_thms thy thms =
    7.31 +    let
    7.32 +      fun add_eq (Const ("op =", ty)) =
    7.33 +            fold (insert (eq_fst (op =)))
    7.34 +              (Term.add_tvarsT ty [])
    7.35 +        | add_eq _ =
    7.36 +            I
    7.37 +      val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
    7.38 +      val instT = map (fn (v_i, sort) =>
    7.39 +        (Thm.ctyp_of thy (TVar (v_i, sort)),
    7.40 +           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [HOLogic.class_eq]))))) eqs;
    7.41 +    in
    7.42 +      thms
    7.43 +      |> map (Thm.instantiate (instT, []))
    7.44 +    end;
    7.45  in
    7.46    fun get_eq thy tyco =
    7.47      get_eq_thms thy tyco
    7.48      |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
    7.49 -    |> HOL.constrain_op_eq_thms thy
    7.50 +    |> constrain_op_eq_thms thy
    7.51  end;
    7.52  
    7.53  type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
     8.1 --- a/src/HOL/Tools/record_package.ML	Mon Nov 27 13:42:30 2006 +0100
     8.2 +++ b/src/HOL/Tools/record_package.ML	Mon Nov 27 13:42:33 2006 +0100
     8.3 @@ -54,6 +54,7 @@
     8.4  structure RecordPackage: RECORD_PACKAGE =
     8.5  struct
     8.6  
     8.7 +val eq_reflection = thm "eq_reflection";
     8.8  val rec_UNIV_I = thm "rec_UNIV_I";
     8.9  val rec_True_simp = thm "rec_True_simp";
    8.10  val Pair_eq = thm "Product_Type.Pair_eq";
    8.11 @@ -1205,8 +1206,8 @@
    8.12                              | SOME (all_thm, All_thm, Ex_thm,_)
    8.13                                 => SOME (case quantifier of
    8.14                                            "all" => all_thm
    8.15 -                                        | "All" => All_thm RS HOL.eq_reflection
    8.16 -                                        | "Ex"  => Ex_thm RS HOL.eq_reflection
    8.17 +                                        | "All" => All_thm RS eq_reflection
    8.18 +                                        | "Ex"  => Ex_thm RS eq_reflection
    8.19                                          | _     => error "record_split_simproc"))
    8.20                          else NONE
    8.21                        end)
     9.1 --- a/src/HOL/ex/MT.ML	Mon Nov 27 13:42:30 2006 +0100
     9.2 +++ b/src/HOL/ex/MT.ML	Mon Nov 27 13:42:33 2006 +0100
     9.3 @@ -602,7 +602,7 @@
     9.4  (* ############################################################ *)
     9.5  
     9.6  fun excluded_middle_tac sP =
     9.7 -  res_inst_tac [("Q", sP)] (excluded_middle RS HOL.disjE);
     9.8 +  res_inst_tac [("Q", sP)] (excluded_middle RS disjE);
     9.9  
    9.10  Goal "[| ve hastyenv te; v hasty t |] ==> \
    9.11  \        ve + {ev |-> v} hastyenv te + {ev |=> t}";