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