--- a/src/HOL/HOL.thy Wed Feb 22 22:18:31 2006 +0100
+++ b/src/HOL/HOL.thy Wed Feb 22 22:18:32 2006 +0100
@@ -888,18 +888,21 @@
qed
lemma atomize_conj [atomize]:
- "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
+ includes meta_conjunction_syntax
+ shows "(A && B) == Trueprop (A & B)"
proof
- assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
- show "A & B" by (rule conjI)
+ assume conj: "A && B"
+ show "A & B"
+ proof (rule conjI)
+ from conj show A by (rule conjunctionD1)
+ from conj show B by (rule conjunctionD2)
+ qed
next
- fix C
- assume "A & B"
- assume "A ==> B ==> PROP C"
- thus "PROP C"
- proof this
- show A by (rule conjunct1)
- show B by (rule conjunct2)
+ assume conj: "A & B"
+ show "A && B"
+ proof -
+ from conj show A ..
+ from conj show B ..
qed
qed
--- a/src/Provers/induct_method.ML Wed Feb 22 22:18:31 2006 +0100
+++ b/src/Provers/induct_method.ML Wed Feb 22 22:18:32 2006 +0100
@@ -42,7 +42,6 @@
val all_conjunction = thm "Pure.all_conjunction";
val imp_conjunction = thm "Pure.imp_conjunction";
val conjunction_imp = thm "Pure.conjunction_imp";
-val conjunction_assoc = thm "Pure.conjunction_assoc";
val conjunction_congs = [all_conjunction, imp_conjunction];
@@ -182,23 +181,11 @@
val (As, B) = Logic.strip_horn (Thm.prop_of thm);
in (thy, Logic.list_implies (map rulify As, rulify B)) end;
-val curry_prems_tac =
- let
- val rule = conjunction_imp;
- val thy = Thm.theory_of_thm rule;
- val proc = Simplifier.simproc_i thy "curry_prems"
- [#1 (Logic.dest_equals (Thm.prop_of rule))]
- (fn _ => fn ss => fn _ => (*WORKAROUND: prevent descending into meta conjunctions*)
- if exists (equal propT o #2 o #1) (#2 (#bounds (#1 (Simplifier.rep_ss ss))))
- then NONE else SOME rule);
- val ss = MetaSimplifier.theory_context thy Simplifier.empty_ss addsimprocs [proc];
- in Simplifier.full_simp_tac ss end;
-
val rulify_tac =
Tactic.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
Tactic.rewrite_goal_tac Data.rulify_fallback THEN'
Tactic.conjunction_tac THEN_ALL_NEW
- (curry_prems_tac THEN' Tactic.norm_hhf_tac);
+ (Tactic.rewrite_goal_tac [conjunction_imp] THEN' Tactic.norm_hhf_tac);
(* prepare rule *)
--- a/src/Pure/Pure.thy Wed Feb 22 22:18:31 2006 +0100
+++ b/src/Pure/Pure.thy Wed Feb 22 22:18:32 2006 +0100
@@ -42,61 +42,40 @@
shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
proof
assume conj: "!!x. PROP A(x) && PROP B(x)"
- fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X"
- show "PROP X"
- proof (rule r)
+ show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
+ proof -
fix x
- from conj show "PROP A(x)" .
- from conj show "PROP B(x)" .
+ from conj show "PROP A(x)" by (rule conjunctionD1)
+ from conj show "PROP B(x)" by (rule conjunctionD2)
qed
next
assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
fix x
- fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X"
- show "PROP X"
- proof (rule r)
- show "PROP A(x)"
- proof (rule conj)
- assume "!!x. PROP A(x)"
- then show "PROP A(x)" .
- qed
- show "PROP B(x)"
- proof (rule conj)
- assume "!!x. PROP B(x)"
- then show "PROP B(x)" .
- qed
+ show "PROP A(x) && PROP B(x)"
+ proof -
+ show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
+ show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
qed
qed
-lemma imp_conjunction [unfolded prop_def]:
+lemma imp_conjunction:
includes meta_conjunction_syntax
- shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
- unfolding prop_def
+ shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
proof
assume conj: "PROP A ==> PROP B && PROP C"
- fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
- show "PROP X"
- proof (rule r)
+ show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
+ proof -
assume "PROP A"
- from conj [OF `PROP A`] show "PROP B" .
- from conj [OF `PROP A`] show "PROP C" .
+ from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
+ from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
qed
next
assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
assume "PROP A"
- fix X assume r: "PROP B ==> PROP C ==> PROP X"
- show "PROP X"
- proof (rule r)
- show "PROP B"
- proof (rule conj)
- assume "PROP A ==> PROP B"
- from this [OF `PROP A`] show "PROP B" .
- qed
- show "PROP C"
- proof (rule conj)
- assume "PROP A ==> PROP C"
- from this [OF `PROP A`] show "PROP C" .
- qed
+ show "PROP B && PROP C"
+ proof -
+ from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
+ from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
qed
qed
@@ -112,14 +91,9 @@
assume conj: "PROP A && PROP B"
show "PROP C"
proof (rule r)
- from conj show "PROP A" .
- from conj show "PROP B" .
+ from conj show "PROP A" by (rule conjunctionD1)
+ from conj show "PROP B" by (rule conjunctionD2)
qed
qed
-lemma conjunction_assoc:
- includes meta_conjunction_syntax
- shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
- unfolding conjunction_imp .
-
end