"atomize" for classical tactics;
authorwenzelm
Fri Nov 03 21:31:11 2000 +0100 (2000-11-03)
changeset 10383a092ae7bb2a6
parent 10382 1fb807260ff1
child 10384 a499b9ce2ffe
"atomize" for classical tactics;
src/FOL/FOL.thy
src/FOL/cladata.ML
src/HOL/HOL.thy
src/HOL/cladata.ML
     1.1 --- a/src/FOL/FOL.thy	Fri Nov 03 21:29:56 2000 +0100
     1.2 +++ b/src/FOL/FOL.thy	Fri Nov 03 21:31:11 2000 +0100
     1.3 @@ -24,31 +24,31 @@
     1.4  subsection {* Setup of several proof tools *}
     1.5  
     1.6  use "FOL_lemmas1.ML"
     1.7 -use "cladata.ML"
     1.8 -setup Cla.setup
     1.9 -setup clasetup
    1.10  
    1.11  lemma all_eq: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
    1.12  proof (rule equal_intr_rule)
    1.13    assume "!!x. P(x)"
    1.14 -  show "ALL x. P(x)" ..
    1.15 +  show "ALL x. P(x)" by (rule allI)
    1.16  next
    1.17    assume "ALL x. P(x)"
    1.18 -  thus "!!x. P(x)" ..
    1.19 +  thus "!!x. P(x)" by (rule allE)
    1.20  qed
    1.21  
    1.22  lemma imp_eq: "(A ==> B) == Trueprop (A --> B)"
    1.23  proof (rule equal_intr_rule)
    1.24    assume r: "A ==> B"
    1.25 -  show "A --> B"
    1.26 -    by (rule) (rule r)
    1.27 +  show "A --> B" by (rule impI) (rule r)
    1.28  next
    1.29    assume "A --> B" and A
    1.30 -  thus B ..
    1.31 +  thus B by (rule mp)
    1.32  qed
    1.33  
    1.34  lemmas atomize = all_eq imp_eq
    1.35  
    1.36 +use "cladata.ML"
    1.37 +setup Cla.setup
    1.38 +setup clasetup
    1.39 +
    1.40  use "blastdata.ML"
    1.41  setup Blast.setup
    1.42  use "FOL_lemmas2.ML"
     2.1 --- a/src/FOL/cladata.ML	Fri Nov 03 21:29:56 2000 +0100
     2.2 +++ b/src/FOL/cladata.ML	Fri Nov 03 21:31:11 2000 +0100
     2.3 @@ -24,12 +24,11 @@
     2.4    val classical = classical
     2.5    val sizef     = size_of_thm
     2.6    val hyp_subst_tacs=[hyp_subst_tac]
     2.7 +  val atomize	= thms "atomize"
     2.8    end;
     2.9  
    2.10  structure Cla = ClassicalFun(Classical_Data);
    2.11  structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
    2.12 -structure Obtain = ObtainFun(val atomic_thesis = FOLogic.atomic_Trueprop and
    2.13 -  that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]);
    2.14  
    2.15  
    2.16  (*Better for fast_tac: needs no quantifier duplication!*)
     3.1 --- a/src/HOL/HOL.thy	Fri Nov 03 21:29:56 2000 +0100
     3.2 +++ b/src/HOL/HOL.thy	Fri Nov 03 21:31:11 2000 +0100
     3.3 @@ -196,32 +196,31 @@
     3.4  
     3.5  use "HOL_lemmas.ML"
     3.6  
     3.7 -use "cladata.ML"
     3.8 -setup hypsubst_setup
     3.9 -setup Classical.setup
    3.10 -setup clasetup
    3.11 -
    3.12  lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
    3.13  proof (rule equal_intr_rule)
    3.14    assume "!!x. P x"
    3.15 -  show "ALL x. P x" ..
    3.16 +  show "ALL x. P x" by (rule allI)
    3.17  next
    3.18    assume "ALL x. P x"
    3.19 -  thus "!!x. P x" ..
    3.20 +  thus "!!x. P x" by (rule allE)
    3.21  qed
    3.22  
    3.23  lemma imp_eq: "(A ==> B) == Trueprop (A --> B)"
    3.24  proof (rule equal_intr_rule)
    3.25    assume r: "A ==> B"
    3.26 -  show "A --> B"
    3.27 -    by (rule) (rule r)
    3.28 +  show "A --> B" by (rule impI) (rule r)
    3.29  next
    3.30    assume "A --> B" and A
    3.31 -  thus B ..
    3.32 +  thus B by (rule mp)
    3.33  qed
    3.34  
    3.35  lemmas atomize = all_eq imp_eq
    3.36  
    3.37 +use "cladata.ML"
    3.38 +setup hypsubst_setup
    3.39 +setup Classical.setup
    3.40 +setup clasetup
    3.41 +
    3.42  use "blastdata.ML"
    3.43  setup Blast.setup
    3.44  
     4.1 --- a/src/HOL/cladata.ML	Fri Nov 03 21:29:56 2000 +0100
     4.2 +++ b/src/HOL/cladata.ML	Fri Nov 03 21:31:11 2000 +0100
     4.3 @@ -47,6 +47,7 @@
     4.4    val classical = classical
     4.5    val sizef     = size_of_thm
     4.6    val hyp_subst_tacs=[hyp_subst_tac]
     4.7 +  val atomize	= thms "atomize"
     4.8    end;
     4.9  
    4.10  structure Classical = ClassicalFun(Classical_Data);
    4.11 @@ -56,9 +57,6 @@
    4.12  
    4.13  bind_thm ("contrapos_np", inst "Pa" "?Q" swap);
    4.14  
    4.15 -structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
    4.16 -  that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
    4.17 -
    4.18  (*Propositional rules*)
    4.19  val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    4.20                         addSEs [conjE,disjE,impCE,FalseE,iffCE];