src/HOL/HOL.thy
 changeset 12937 0c4fd7529467 parent 12892 a0b2acb7d6fa child 13412 666137b488a4
```     1.1 --- a/src/HOL/HOL.thy	Mon Feb 25 20:46:09 2002 +0100
1.2 +++ b/src/HOL/HOL.thy	Mon Feb 25 20:48:14 2002 +0100
1.3 @@ -201,7 +201,10 @@
1.4  subsubsection {* Intuitionistic Reasoning *}
1.5
1.6  lemma impE':
1.7 -  (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
1.8 +  assumes 1: "P --> Q"
1.9 +    and 2: "Q ==> R"
1.10 +    and 3: "P --> Q ==> P"
1.11 +  shows R
1.12  proof -
1.13    from 3 and 1 have P .
1.14    with 1 have Q by (rule impE)
1.15 @@ -209,13 +212,18 @@
1.16  qed
1.17
1.18  lemma allE':
1.19 -  (assumes 1: "ALL x. P x" and 2: "P x ==> ALL x. P x ==> Q") Q
1.20 +  assumes 1: "ALL x. P x"
1.21 +    and 2: "P x ==> ALL x. P x ==> Q"
1.22 +  shows Q
1.23  proof -
1.24    from 1 have "P x" by (rule spec)
1.25    from this and 1 show Q by (rule 2)
1.26  qed
1.27
1.28 -lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
1.29 +lemma notE':
1.30 +  assumes 1: "~ P"
1.31 +    and 2: "~ P ==> P"
1.32 +  shows R
1.33  proof -
1.34    from 2 and 1 have P .
1.35    with 1 show R by (rule notE)
1.36 @@ -309,7 +317,8 @@
1.37  lemma eta_contract_eq: "(%s. f s) = f" ..
1.38
1.39  lemma simp_thms:
1.40 -  (not_not: "(~ ~ P) = P" and
1.41 +  shows not_not: "(~ ~ P) = P"
1.42 +  and
1.43      "(P ~= Q) = (P = (~Q))"
1.44      "(P | ~P) = True"    "(~P | P) = True"
1.45      "((~P) = (~Q)) = (P=Q)"
1.46 @@ -333,7 +342,7 @@
1.47      "!!P. (EX x. x=t & P(x)) = P(t)"
1.48      "!!P. (EX x. t=x & P(x)) = P(t)"
1.49      "!!P. (ALL x. x=t --> P(x)) = P(t)"
1.50 -    "!!P. (ALL x. t=x --> P(x)) = P(t)")
1.51 +    "!!P. (ALL x. t=x --> P(x)) = P(t)"
1.52    by (blast, blast, blast, blast, blast, rules+)
1.53
1.54  lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
1.55 @@ -360,19 +369,19 @@
1.56    by (rules | blast)+
1.57
1.58  lemma eq_ac:
1.59 - (eq_commute: "(a=b) = (b=a)" and
1.60 -  eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" and
1.61 -  eq_assoc: "((P=Q)=R) = (P=(Q=R))") by (rules, blast+)
1.62 +  shows eq_commute: "(a=b) = (b=a)"
1.63 +    and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
1.64 +    and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)
1.65  lemma neq_commute: "(a~=b) = (b~=a)" by rules
1.66
1.67  lemma conj_comms:
1.68 - (conj_commute: "(P&Q) = (Q&P)" and
1.69 -  conj_left_commute: "(P&(Q&R)) = (Q&(P&R))") by rules+
1.70 +  shows conj_commute: "(P&Q) = (Q&P)"
1.71 +    and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by rules+
1.72  lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules
1.73
1.74  lemma disj_comms:
1.75 - (disj_commute: "(P|Q) = (Q|P)" and
1.76 -  disj_left_commute: "(P|(Q|R)) = (Q|(P|R))") by rules+
1.77 +  shows disj_commute: "(P|Q) = (Q|P)"
1.78 +    and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by rules+
1.79  lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by rules
1.80
1.81  lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by rules
```