simplified Pure conjunction;
authorwenzelm
Wed Feb 22 22:18:32 2006 +0100 (2006-02-22 ago)
changeset 19121d7fd5415a781
parent 19120 353d349740de
child 19122 e1b6a5071348
simplified Pure conjunction;
src/HOL/HOL.thy
src/Provers/induct_method.ML
src/Pure/Pure.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Feb 22 22:18:31 2006 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Feb 22 22:18:32 2006 +0100
     1.3 @@ -888,18 +888,21 @@
     1.4  qed
     1.5  
     1.6  lemma atomize_conj [atomize]:
     1.7 -  "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
     1.8 +  includes meta_conjunction_syntax
     1.9 +  shows "(A && B) == Trueprop (A & B)"
    1.10  proof
    1.11 -  assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
    1.12 -  show "A & B" by (rule conjI)
    1.13 +  assume conj: "A && B"
    1.14 +  show "A & B"
    1.15 +  proof (rule conjI)
    1.16 +    from conj show A by (rule conjunctionD1)
    1.17 +    from conj show B by (rule conjunctionD2)
    1.18 +  qed
    1.19  next
    1.20 -  fix C
    1.21 -  assume "A & B"
    1.22 -  assume "A ==> B ==> PROP C"
    1.23 -  thus "PROP C"
    1.24 -  proof this
    1.25 -    show A by (rule conjunct1)
    1.26 -    show B by (rule conjunct2)
    1.27 +  assume conj: "A & B"
    1.28 +  show "A && B"
    1.29 +  proof -
    1.30 +    from conj show A ..
    1.31 +    from conj show B ..
    1.32    qed
    1.33  qed
    1.34  
     2.1 --- a/src/Provers/induct_method.ML	Wed Feb 22 22:18:31 2006 +0100
     2.2 +++ b/src/Provers/induct_method.ML	Wed Feb 22 22:18:32 2006 +0100
     2.3 @@ -42,7 +42,6 @@
     2.4  val all_conjunction = thm "Pure.all_conjunction";
     2.5  val imp_conjunction = thm "Pure.imp_conjunction";
     2.6  val conjunction_imp = thm "Pure.conjunction_imp";
     2.7 -val conjunction_assoc = thm "Pure.conjunction_assoc";
     2.8  val conjunction_congs = [all_conjunction, imp_conjunction];
     2.9  
    2.10  
    2.11 @@ -182,23 +181,11 @@
    2.12      val (As, B) = Logic.strip_horn (Thm.prop_of thm);
    2.13    in (thy, Logic.list_implies (map rulify As, rulify B)) end;
    2.14  
    2.15 -val curry_prems_tac =
    2.16 -  let
    2.17 -    val rule = conjunction_imp;
    2.18 -    val thy = Thm.theory_of_thm rule;
    2.19 -    val proc = Simplifier.simproc_i thy "curry_prems"
    2.20 -      [#1 (Logic.dest_equals (Thm.prop_of rule))]
    2.21 -      (fn _ => fn ss => fn _ =>  (*WORKAROUND: prevent descending into meta conjunctions*)
    2.22 -        if exists (equal propT o #2 o #1) (#2 (#bounds (#1 (Simplifier.rep_ss ss))))
    2.23 -        then NONE else SOME rule);
    2.24 -    val ss = MetaSimplifier.theory_context thy Simplifier.empty_ss addsimprocs [proc];
    2.25 -  in Simplifier.full_simp_tac ss end;
    2.26 -
    2.27  val rulify_tac =
    2.28    Tactic.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
    2.29    Tactic.rewrite_goal_tac Data.rulify_fallback THEN'
    2.30    Tactic.conjunction_tac THEN_ALL_NEW
    2.31 -  (curry_prems_tac THEN' Tactic.norm_hhf_tac);
    2.32 +  (Tactic.rewrite_goal_tac [conjunction_imp] THEN' Tactic.norm_hhf_tac);
    2.33  
    2.34  
    2.35  (* prepare rule *)
     3.1 --- a/src/Pure/Pure.thy	Wed Feb 22 22:18:31 2006 +0100
     3.2 +++ b/src/Pure/Pure.thy	Wed Feb 22 22:18:32 2006 +0100
     3.3 @@ -42,61 +42,40 @@
     3.4    shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
     3.5  proof
     3.6    assume conj: "!!x. PROP A(x) && PROP B(x)"
     3.7 -  fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X"
     3.8 -  show "PROP X"
     3.9 -  proof (rule r)
    3.10 +  show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
    3.11 +  proof -
    3.12      fix x
    3.13 -    from conj show "PROP A(x)" .
    3.14 -    from conj show "PROP B(x)" .
    3.15 +    from conj show "PROP A(x)" by (rule conjunctionD1)
    3.16 +    from conj show "PROP B(x)" by (rule conjunctionD2)
    3.17    qed
    3.18  next
    3.19    assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    3.20    fix x
    3.21 -  fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X"
    3.22 -  show "PROP X"
    3.23 -  proof (rule r)
    3.24 -    show "PROP A(x)"
    3.25 -    proof (rule conj)
    3.26 -      assume "!!x. PROP A(x)"
    3.27 -      then show "PROP A(x)" .
    3.28 -    qed
    3.29 -    show "PROP B(x)"
    3.30 -    proof (rule conj)
    3.31 -      assume "!!x. PROP B(x)"
    3.32 -      then show "PROP B(x)" .
    3.33 -    qed
    3.34 +  show "PROP A(x) && PROP B(x)"
    3.35 +  proof -
    3.36 +    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
    3.37 +    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
    3.38    qed
    3.39  qed
    3.40  
    3.41 -lemma imp_conjunction [unfolded prop_def]:
    3.42 +lemma imp_conjunction:
    3.43    includes meta_conjunction_syntax
    3.44 -  shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    3.45 -  unfolding prop_def
    3.46 +  shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    3.47  proof
    3.48    assume conj: "PROP A ==> PROP B && PROP C"
    3.49 -  fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
    3.50 -  show "PROP X"
    3.51 -  proof (rule r)
    3.52 +  show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    3.53 +  proof -
    3.54      assume "PROP A"
    3.55 -    from conj [OF `PROP A`] show "PROP B" .
    3.56 -    from conj [OF `PROP A`] show "PROP C" .
    3.57 +    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    3.58 +    from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    3.59    qed
    3.60  next
    3.61    assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    3.62    assume "PROP A"
    3.63 -  fix X assume r: "PROP B ==> PROP C ==> PROP X"
    3.64 -  show "PROP X"
    3.65 -  proof (rule r)
    3.66 -    show "PROP B"
    3.67 -    proof (rule conj)
    3.68 -      assume "PROP A ==> PROP B"
    3.69 -      from this [OF `PROP A`] show "PROP B" .
    3.70 -    qed
    3.71 -    show "PROP C"
    3.72 -    proof (rule conj)
    3.73 -      assume "PROP A ==> PROP C"
    3.74 -      from this [OF `PROP A`] show "PROP C" .
    3.75 -    qed
    3.76 +  show "PROP B && PROP C"
    3.77 +  proof -
    3.78 +    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    3.79 +    from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    3.80    qed
    3.81  qed
    3.82  
    3.83 @@ -112,14 +91,9 @@
    3.84    assume conj: "PROP A && PROP B"
    3.85    show "PROP C"
    3.86    proof (rule r)
    3.87 -    from conj show "PROP A" .
    3.88 -    from conj show "PROP B" .
    3.89 +    from conj show "PROP A" by (rule conjunctionD1)
    3.90 +    from conj show "PROP B" by (rule conjunctionD2)
    3.91    qed
    3.92  qed
    3.93  
    3.94 -lemma conjunction_assoc:
    3.95 -  includes meta_conjunction_syntax
    3.96 -  shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
    3.97 -  unfolding conjunction_imp .
    3.98 -
    3.99  end