--- a/src/HOL/Code_Generator.thy Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/Code_Generator.thy Mon Nov 27 13:42:33 2006 +0100
@@ -64,11 +64,11 @@
setup {*
let
+val TrueI = thm "TrueI"
fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
(Drule.goals_conv (equal i) Codegen.evaluation_conv));
-
val evaluation_meth =
- Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1));
+ Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac TrueI 1));
in
@@ -143,7 +143,7 @@
in Thm.invoke_oracle_i thy oracle_name (thy, Eval t) end;
fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
- (Drule.goals_conv (equal i) (HOL.Trueprop_conv conv)));
+ (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv conv)));
val method =
Method.no_args (Method.METHOD (fn _ =>
@@ -163,7 +163,7 @@
setup {*
let
fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
- (Drule.goals_conv (equal i) (HOL.Trueprop_conv
+ (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv
NBE.normalization_conv)));
val normalization_meth =
Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl] 1));
--- a/src/HOL/HOL.ML Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/HOL.ML Mon Nov 27 13:42:33 2006 +0100
@@ -1,19 +1,36 @@
(* legacy ML bindings *)
-val HOL_cs = HOL.claset;
-val HOL_basic_ss = HOL.simpset_basic;
-val HOL_ss = HOL.simpset;
-val hol_simplify = HOL.simplify;
+val Blast_tac = Blast.Blast_tac;
+val blast_tac = Blast.blast_tac;
+
+(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
+local
+ fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
+ | wrong_prem (Bound _) = true
+ | wrong_prem _ = false;
+ val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
+ val spec = thm "spec"
+ val mp = thm "mp"
+in
+ fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
+ fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
+end;
+
+fun strip_tac i = REPEAT (resolve_tac [thm "impI", thm "allI"] i);
val split_tac = Splitter.split_tac;
val split_inside_tac = Splitter.split_inside_tac;
val split_asm_tac = Splitter.split_asm_tac;
+
val op addsplits = Splitter.addsplits;
val op delsplits = Splitter.delsplits;
val Addsplits = Splitter.Addsplits;
val Delsplits = Splitter.Delsplits;
-open HOL;
+val HOL_basic_ss = Simpdata.simpset_basic;
+val hol_simplify = Simpdata.simplify;
+
+open Simpdata;
val claset = Classical.claset;
val simpset = Simplifier.simpset;
val simplify = Simplifier.simplify;
@@ -21,6 +38,51 @@
open BasicClassical;
open Clasimp;
+val eq_reflection = thm "eq_reflection";
+val def_imp_eq = thm "def_imp_eq";
+val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
+val ccontr = thm "ccontr";
+val impI = thm "impI";
+val impCE = thm "impCE";
+val notI = thm "notI";
+val notE = thm "notE";
+val iffI = thm "iffI";
+val iffCE = thm "iffCE";
+val conjI = thm "conjI";
+val conjE = thm "conjE";
+val disjCI = thm "disjCI";
+val disjE = thm "disjE";
+val TrueI = thm "TrueI";
+val FalseE = thm "FalseE";
+val allI = thm "allI";
+val allE = thm "allE";
+val exI = thm "exI";
+val exE = thm "exE";
+val ex_ex1I = thm "ex_ex1I";
+val the_equality = thm "the_equality";
+val mp = thm "mp";
+val rev_mp = thm "rev_mp"
+val classical = thm "classical";
+val subst = thm "subst";
+val refl = thm "refl";
+val sym = thm "sym";
+val trans = thm "trans";
+val arg_cong = thm "arg_cong";
+val iffD1 = thm "iffD1";
+val iffD2 = thm "iffD2";
+val disjE = thm "disjE";
+val conjE = thm "conjE";
+val exE = thm "exE";
+val contrapos_nn = thm "contrapos_nn";
+val contrapos_pp = thm "contrapos_pp";
+val notnotD = thm "notnotD";
+val conjunct1 = thm "conjunct1";
+val conjunct2 = thm "conjunct2";
+val spec = thm "spec";
+val imp_cong = thm "imp_cong";
+val the_sym_eq_trivial = thm "the_sym_eq_trivial";
+val triv_forall_equality = thm "triv_forall_equality";
+val case_split = thm "case_split_thm";
val ext = thm "ext"
val True_def = thm "True_def"
val All_def = thm "All_def"
@@ -75,7 +137,6 @@
val let_weak_cong = thm "let_weak_cong"
val eq_cong2 = thm "eq_cong2"
val if_distrib = thm "if_distrib"
-val expand_case = thm "expand_case"
val restrict_to_left = thm "restrict_to_left"
val all_conj_distrib = thm "all_conj_distrib";
val atomize_not = thm "atomize_not";
@@ -150,8 +211,6 @@
structure HOL =
struct
-open HOL;
-
val thy = the_context ();
end;
--- a/src/HOL/Import/hol4rews.ML Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/Import/hol4rews.ML Mon Nov 27 13:42:33 2006 +0100
@@ -261,17 +261,21 @@
val hol4_debug = ref false
fun message s = if !hol4_debug then writeln s else ()
+local
+ val eq_reflection = thm "eq_reflection"
+in
fun add_hol4_rewrite (Context.Theory thy, th) =
let
val _ = message "Adding HOL4 rewrite"
- val th1 = th RS HOL.eq_reflection
+ val th1 = th RS eq_reflection
val current_rews = HOL4Rewrites.get thy
val new_rews = insert Thm.eq_thm th1 current_rews
val updated_thy = HOL4Rewrites.put new_rews thy
in
(Context.Theory updated_thy,th1)
end
- | add_hol4_rewrite (context, th) = (context, th RS HOL.eq_reflection);
+ | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
+end
fun ignore_hol4 bthy bthm thy =
let
--- a/src/HOL/Lambda/WeakNorm.thy Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Mon Nov 27 13:42:33 2006 +0100
@@ -584,7 +584,7 @@
*}
code_gen
- type_NF (SML *)
+ type_NF (SML #)
ML {*
structure Norm = ROOT.WeakNorm;
--- a/src/HOL/Library/EfficientNat.thy Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Mon Nov 27 13:42:33 2006 +0100
@@ -315,10 +315,14 @@
end; (*local*)
-fun lift_obj_eq f thy =
+local
+ val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
+ val eq_reflection = thm "eq_reflection";
+in fun lift_obj_eq f thy =
map (fn thm => thm RS meta_eq_to_obj_eq)
#> f thy
- #> map (fn thm => thm RS HOL.eq_reflection)
+ #> map (fn thm => thm RS eq_reflection)
+end
*}
setup {*
--- a/src/HOL/Orderings.thy Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/Orderings.thy Mon Nov 27 13:42:33 2006 +0100
@@ -822,6 +822,25 @@
leave out the "(xtrans)" above.
*)
+subsection {* Order on bool *}
+
+instance bool :: linorder
+ le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
+ less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
+ by default (auto simp add: le_bool_def less_bool_def)
+
+lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
+ by (simp add: le_bool_def)
+
+lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
+ by (simp add: le_bool_def)
+
+lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
+ by (simp add: le_bool_def)
+
+lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
+ by (simp add: le_bool_def)
+
subsection {* Monotonicity, syntactic least value operator and min/max *}
locale mono =
--- a/src/HOL/Tools/datatype_codegen.ML Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Mon Nov 27 13:42:33 2006 +0100
@@ -406,6 +406,8 @@
local
val not_sym = thm "HOL.not_sym";
val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
+ val refl = thm "refl";
+ val eqTrueI = thm "eqTrueI";
in
fun get_eq_datatype thy dtco =
@@ -416,11 +418,10 @@
val ct' = Thm.cterm_of thy
(Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
val cty' = Thm.ctyp_of_term ct';
- val refl = Thm.prop_of HOL.refl;
val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
(K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
- refl NONE;
- in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
+ (Thm.prop_of refl) NONE;
+ in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) refl] end;
val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
val ctxt = ProofContext.init thy;
@@ -498,11 +499,26 @@
fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
of SOME _ => get_eq_datatype thy tyco
| NONE => [TypecopyPackage.get_eq thy tyco];
+ fun constrain_op_eq_thms thy thms =
+ let
+ fun add_eq (Const ("op =", ty)) =
+ fold (insert (eq_fst (op =)))
+ (Term.add_tvarsT ty [])
+ | add_eq _ =
+ I
+ val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
+ val instT = map (fn (v_i, sort) =>
+ (Thm.ctyp_of thy (TVar (v_i, sort)),
+ Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [HOLogic.class_eq]))))) eqs;
+ in
+ thms
+ |> map (Thm.instantiate (instT, []))
+ end;
in
fun get_eq thy tyco =
get_eq_thms thy tyco
|> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
- |> HOL.constrain_op_eq_thms thy
+ |> constrain_op_eq_thms thy
end;
type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
--- a/src/HOL/Tools/record_package.ML Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Mon Nov 27 13:42:33 2006 +0100
@@ -54,6 +54,7 @@
structure RecordPackage: RECORD_PACKAGE =
struct
+val eq_reflection = thm "eq_reflection";
val rec_UNIV_I = thm "rec_UNIV_I";
val rec_True_simp = thm "rec_True_simp";
val Pair_eq = thm "Product_Type.Pair_eq";
@@ -1205,8 +1206,8 @@
| SOME (all_thm, All_thm, Ex_thm,_)
=> SOME (case quantifier of
"all" => all_thm
- | "All" => All_thm RS HOL.eq_reflection
- | "Ex" => Ex_thm RS HOL.eq_reflection
+ | "All" => All_thm RS eq_reflection
+ | "Ex" => Ex_thm RS eq_reflection
| _ => error "record_split_simproc"))
else NONE
end)
--- a/src/HOL/ex/MT.ML Mon Nov 27 13:42:30 2006 +0100
+++ b/src/HOL/ex/MT.ML Mon Nov 27 13:42:33 2006 +0100
@@ -602,7 +602,7 @@
(* ############################################################ *)
fun excluded_middle_tac sP =
- res_inst_tac [("Q", sP)] (excluded_middle RS HOL.disjE);
+ res_inst_tac [("Q", sP)] (excluded_middle RS disjE);
Goal "[| ve hastyenv te; v hasty t |] ==> \
\ ve + {ev |-> v} hastyenv te + {ev |=> t}";