# HG changeset patch # User haftmann # Date 1160735564 -7200 # Node ID 0eae3fb489361be11647539e5475b50087319873 # Parent 330a8a6dd53ce554f52e4acb53aaa6f125c11348 lifted claset setup from ML to Isar level diff -r 330a8a6dd53c -r 0eae3fb48936 src/HOL/HOL.ML --- a/src/HOL/HOL.ML Fri Oct 13 09:02:21 2006 +0200 +++ b/src/HOL/HOL.ML Fri Oct 13 12:32:44 2006 +0200 @@ -1,5 +1,6 @@ (* legacy ML bindings *) +val prop_cs = HOL.claset_prop; val HOL_cs = HOL.claset; val HOL_basic_ss = HOL.simpset_basic; val HOL_ss = HOL.simpset; @@ -18,6 +19,8 @@ val claset = Classical.claset; val simpset = Simplifier.simpset; val simplify = Simplifier.simplify; +open Hypsubst; +open BasicClassical; open Clasimp; val ext = thm "ext" diff -r 330a8a6dd53c -r 0eae3fb48936 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Oct 13 09:02:21 2006 +0200 +++ b/src/HOL/HOL.thy Fri Oct 13 12:32:44 2006 +0200 @@ -863,10 +863,63 @@ use "cladata.ML" setup Hypsubst.hypsubst_setup -setup {* ContextRules.addSWrapper (fn tac => HOL.hyp_subst_tac' ORELSE' tac) *} +setup {* +let + (*prevent substitution on bool*) + fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso + Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false) + (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm; +in + ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) +end +*} setup Classical.setup setup ResAtpset.setup -setup {* fn thy => (Classical.change_claset_of thy (K HOL.claset); thy) *} + +declare iffI [intro!] + and notI [intro!] + and impI [intro!] + and disjCI [intro!] + and conjI [intro!] + and TrueI [intro!] + and refl [intro!] + +declare iffCE [elim!] + and FalseE [elim!] + and impCE [elim!] + and disjE [elim!] + and conjE [elim!] + and conjE [elim!] + +ML {* +structure HOL = +struct + +open HOL; + +val claset_prop = Classical.claset_of (the_context ()); + +end; +*} + +declare ex_ex1I [intro!] + and allI [intro!] + and the_equality [intro] + and exI [intro] + +declare exE [elim!] + allE [elim] + +ML {* +structure HOL = +struct + +open HOL; + +val claset = Classical.claset_of (the_context ()); + +end; +*} lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" apply (erule swap) @@ -901,6 +954,9 @@ fun case_tac a = res_inst_tac [("P", a)] case_split; +val Blast_tac = Blast.Blast_tac; +val blast_tac = Blast.blast_tac; + end; *} diff -r 330a8a6dd53c -r 0eae3fb48936 src/HOL/blastdata.ML --- a/src/HOL/blastdata.ML Fri Oct 13 09:02:21 2006 +0200 +++ b/src/HOL/blastdata.ML Fri Oct 13 12:32:44 2006 +0200 @@ -15,13 +15,3 @@ end; structure Blast = BlastFun(Blast_Data); - -structure HOL = -struct - -open HOL; - -val Blast_tac = Blast.Blast_tac; -val blast_tac = Blast.blast_tac; - -end; \ No newline at end of file diff -r 330a8a6dd53c -r 0eae3fb48936 src/HOL/cladata.ML --- a/src/HOL/cladata.ML Fri Oct 13 09:02:21 2006 +0200 +++ b/src/HOL/cladata.ML Fri Oct 13 12:32:44 2006 +0200 @@ -34,25 +34,3 @@ structure Classical = ClassicalFun(Classical_Data); structure BasicClassical: BASIC_CLASSICAL = Classical; - -structure HOL = -struct - -open HOL; -open Hypsubst; -open BasicClassical; - -(*prevent substitution on bool*) -fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso - Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false) - (nth (Thm.prems_of thm) (i - 1)) then hyp_subst_tac i thm else no_tac thm; - -(*Propositional rules*) -val prop_cs = empty_cs addSIs [HOL.refl, HOL.TrueI, HOL.conjI, HOL.disjCI, HOL.impI, HOL.notI, HOL.iffI] - addSEs [HOL.conjE, HOL.disjE, HOL.impCE, HOL.FalseE, HOL.iffCE]; - -(*Quantifier rules*) -val claset = prop_cs addSIs [HOL.allI, HOL.ex_ex1I] addIs [HOL.exI, HOL.the_equality] - addSEs [HOL.exE] addEs [HOL.allE]; - -end;