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