induct method: localize rews for rule;
authorwenzelm
Mon Nov 19 20:46:05 2001 +0100 (2001-11-19)
changeset 122400760eda193c4
parent 12239 ee360f910ec8
child 12241 c4a2a0686238
induct method: localize rews for rule;
src/FOL/FOL.thy
src/HOL/HOL.thy
src/Provers/induct_method.ML
     1.1 --- a/src/FOL/FOL.thy	Mon Nov 19 17:42:00 2001 +0100
     1.2 +++ b/src/FOL/FOL.thy	Mon Nov 19 20:46:05 2001 +0100
     1.3 @@ -65,6 +65,9 @@
     1.4  lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq
     1.5  lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
     1.6  
     1.7 +lemma all_conj_eq: "(ALL x. P(x)) & (ALL y. Q(y)) == (ALL x y. P(x) & Q(y))"
     1.8 +  by simp
     1.9 +
    1.10  hide const induct_forall induct_implies induct_equal
    1.11  
    1.12  
    1.13 @@ -75,12 +78,13 @@
    1.14    (struct
    1.15      val dest_concls = FOLogic.dest_concls;
    1.16      val cases_default = thm "case_split";
    1.17 -    val local_imp_def = thm "induct_implies_def";
    1.18      val local_impI = thm "induct_impliesI";
    1.19      val conjI = thm "conjI";
    1.20      val atomize = thms "induct_atomize";
    1.21      val rulify1 = thms "induct_rulify1";
    1.22      val rulify2 = thms "induct_rulify2";
    1.23 +    val localize = [Thm.symmetric (thm "induct_implies_def"),
    1.24 +      Thm.symmetric (thm "atomize_all"), thm "all_conj_eq"];
    1.25    end);
    1.26  *}
    1.27  
     2.1 --- a/src/HOL/HOL.thy	Mon Nov 19 17:42:00 2001 +0100
     2.2 +++ b/src/HOL/HOL.thy	Mon Nov 19 20:46:05 2001 +0100
     2.3 @@ -321,12 +321,12 @@
     2.4    (struct
     2.5      val dest_concls = HOLogic.dest_concls;
     2.6      val cases_default = thm "case_split";
     2.7 -    val local_imp_def = thm "induct_implies_def";
     2.8      val local_impI = thm "induct_impliesI";
     2.9      val conjI = thm "conjI";
    2.10      val atomize = thms "induct_atomize";
    2.11      val rulify1 = thms "induct_rulify1";
    2.12      val rulify2 = thms "induct_rulify2";
    2.13 +    val localize = [Thm.symmetric (thm "induct_implies_def")];
    2.14    end);
    2.15  *}
    2.16  
     3.1 --- a/src/Provers/induct_method.ML	Mon Nov 19 17:42:00 2001 +0100
     3.2 +++ b/src/Provers/induct_method.ML	Mon Nov 19 20:46:05 2001 +0100
     3.3 @@ -10,12 +10,12 @@
     3.4  sig
     3.5    val dest_concls: term -> term list
     3.6    val cases_default: thm
     3.7 -  val local_imp_def: thm
     3.8    val local_impI: thm
     3.9    val conjI: thm
    3.10    val atomize: thm list
    3.11    val rulify1: thm list
    3.12    val rulify2: thm list
    3.13 +  val localize: thm list
    3.14  end;
    3.15  
    3.16  signature INDUCT_METHOD =
    3.17 @@ -150,7 +150,7 @@
    3.18    Tactic.rewrite_goal_tac Data.rulify2 THEN'
    3.19    Tactic.norm_hhf_tac;
    3.20  
    3.21 -val localize = Tactic.simplify false [Thm.symmetric Data.local_imp_def];
    3.22 +val localize = Tactic.norm_hhf o Tactic.simplify false Data.localize;
    3.23  
    3.24  
    3.25  (* imp_intr --- limited to atomic prems *)