# HG changeset patch # User haftmann # Date 1164631353 -3600 # Node ID 268b6bed0cc87ef31fe9d096ac32e40ceebabb29 # Parent 54cc492d80a9f05e8af45d2d8ba2ac79433c0b11 removed HOL structure diff -r 54cc492d80a9 -r 268b6bed0cc8 src/HOL/Code_Generator.thy --- 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)); diff -r 54cc492d80a9 -r 268b6bed0cc8 src/HOL/HOL.ML --- 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; diff -r 54cc492d80a9 -r 268b6bed0cc8 src/HOL/Import/hol4rews.ML --- 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 diff -r 54cc492d80a9 -r 268b6bed0cc8 src/HOL/Lambda/WeakNorm.thy --- 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; diff -r 54cc492d80a9 -r 268b6bed0cc8 src/HOL/Library/EfficientNat.thy --- 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 {* diff -r 54cc492d80a9 -r 268b6bed0cc8 src/HOL/Orderings.thy --- 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 \ Q \ P \ Q" + less_bool_def: "P < Q \ P \ Q \ P \ Q" + by default (auto simp add: le_bool_def less_bool_def) + +lemma le_boolI: "(P \ Q) \ P \ Q" + by (simp add: le_bool_def) + +lemma le_boolI': "P \ Q \ P \ Q" + by (simp add: le_bool_def) + +lemma le_boolE: "P \ Q \ P \ (Q \ R) \ R" + by (simp add: le_bool_def) + +lemma le_boolD: "P \ Q \ P \ Q" + by (simp add: le_bool_def) + subsection {* Monotonicity, syntactic least value operator and min/max *} locale mono = diff -r 54cc492d80a9 -r 268b6bed0cc8 src/HOL/Tools/datatype_codegen.ML --- 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 diff -r 54cc492d80a9 -r 268b6bed0cc8 src/HOL/Tools/record_package.ML --- 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) diff -r 54cc492d80a9 -r 268b6bed0cc8 src/HOL/ex/MT.ML --- 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}";