src/Pure/Pure.thy
 changeset 19121 d7fd5415a781 parent 19048 2b875dd5eb4c child 19783 82f365a14960
```     1.1 --- a/src/Pure/Pure.thy	Wed Feb 22 22:18:31 2006 +0100
1.2 +++ b/src/Pure/Pure.thy	Wed Feb 22 22:18:32 2006 +0100
1.3 @@ -42,61 +42,40 @@
1.4    shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
1.5  proof
1.6    assume conj: "!!x. PROP A(x) && PROP B(x)"
1.7 -  fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X"
1.8 -  show "PROP X"
1.9 -  proof (rule r)
1.10 +  show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
1.11 +  proof -
1.12      fix x
1.13 -    from conj show "PROP A(x)" .
1.14 -    from conj show "PROP B(x)" .
1.15 +    from conj show "PROP A(x)" by (rule conjunctionD1)
1.16 +    from conj show "PROP B(x)" by (rule conjunctionD2)
1.17    qed
1.18  next
1.19    assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
1.20    fix x
1.21 -  fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X"
1.22 -  show "PROP X"
1.23 -  proof (rule r)
1.24 -    show "PROP A(x)"
1.25 -    proof (rule conj)
1.26 -      assume "!!x. PROP A(x)"
1.27 -      then show "PROP A(x)" .
1.28 -    qed
1.29 -    show "PROP B(x)"
1.30 -    proof (rule conj)
1.31 -      assume "!!x. PROP B(x)"
1.32 -      then show "PROP B(x)" .
1.33 -    qed
1.34 +  show "PROP A(x) && PROP B(x)"
1.35 +  proof -
1.36 +    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
1.37 +    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
1.38    qed
1.39  qed
1.40
1.41 -lemma imp_conjunction [unfolded prop_def]:
1.42 +lemma imp_conjunction:
1.43    includes meta_conjunction_syntax
1.44 -  shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
1.45 -  unfolding prop_def
1.46 +  shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
1.47  proof
1.48    assume conj: "PROP A ==> PROP B && PROP C"
1.49 -  fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
1.50 -  show "PROP X"
1.51 -  proof (rule r)
1.52 +  show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
1.53 +  proof -
1.54      assume "PROP A"
1.55 -    from conj [OF `PROP A`] show "PROP B" .
1.56 -    from conj [OF `PROP A`] show "PROP C" .
1.57 +    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
1.58 +    from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
1.59    qed
1.60  next
1.61    assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
1.62    assume "PROP A"
1.63 -  fix X assume r: "PROP B ==> PROP C ==> PROP X"
1.64 -  show "PROP X"
1.65 -  proof (rule r)
1.66 -    show "PROP B"
1.67 -    proof (rule conj)
1.68 -      assume "PROP A ==> PROP B"
1.69 -      from this [OF `PROP A`] show "PROP B" .
1.70 -    qed
1.71 -    show "PROP C"
1.72 -    proof (rule conj)
1.73 -      assume "PROP A ==> PROP C"
1.74 -      from this [OF `PROP A`] show "PROP C" .
1.75 -    qed
1.76 +  show "PROP B && PROP C"
1.77 +  proof -
1.78 +    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
1.79 +    from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
1.80    qed
1.81  qed
1.82
1.83 @@ -112,14 +91,9 @@
1.84    assume conj: "PROP A && PROP B"
1.85    show "PROP C"
1.86    proof (rule r)
1.87 -    from conj show "PROP A" .
1.88 -    from conj show "PROP B" .
1.89 +    from conj show "PROP A" by (rule conjunctionD1)
1.90 +    from conj show "PROP B" by (rule conjunctionD2)
1.91    qed
1.92  qed
1.93
1.94 -lemma conjunction_assoc:
1.95 -  includes meta_conjunction_syntax
1.96 -  shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
1.97 -  unfolding conjunction_imp .
1.98 -
1.99  end
```