src/FOLP/FOLP.thy
changeset 61337 4645502c3c64
parent 60770 240563fbf41d
child 69593 3dda49e08b9d
     1.1 --- a/src/FOLP/FOLP.thy	Tue Oct 06 13:31:44 2015 +0200
     1.2 +++ b/src/FOLP/FOLP.thy	Tue Oct 06 15:14:28 2015 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  (*** Classical introduction rules for | and EX ***)
     1.6  
     1.7 -schematic_lemma disjCI:
     1.8 +schematic_goal disjCI:
     1.9    assumes "!!x. x:~Q ==> f(x):P"
    1.10    shows "?p : P|Q"
    1.11    apply (rule classical)
    1.12 @@ -24,7 +24,7 @@
    1.13    done
    1.14  
    1.15  (*introduction rule involving only EX*)
    1.16 -schematic_lemma ex_classical:
    1.17 +schematic_goal ex_classical:
    1.18    assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"
    1.19    shows "?p : EX x. P(x)"
    1.20    apply (rule classical)
    1.21 @@ -32,7 +32,7 @@
    1.22    done
    1.23  
    1.24  (*version of above, simplifying ~EX to ALL~ *)
    1.25 -schematic_lemma exCI:
    1.26 +schematic_goal exCI:
    1.27    assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"
    1.28    shows "?p : EX x. P(x)"
    1.29    apply (rule ex_classical)
    1.30 @@ -41,7 +41,7 @@
    1.31    apply (erule exI)
    1.32    done
    1.33  
    1.34 -schematic_lemma excluded_middle: "?p : ~P | P"
    1.35 +schematic_goal excluded_middle: "?p : ~P | P"
    1.36    apply (rule disjCI)
    1.37    apply assumption
    1.38    done
    1.39 @@ -50,7 +50,7 @@
    1.40  (*** Special elimination rules *)
    1.41  
    1.42  (*Classical implies (-->) elimination. *)
    1.43 -schematic_lemma impCE:
    1.44 +schematic_goal impCE:
    1.45    assumes major: "p:P-->Q"
    1.46      and r1: "!!x. x:~P ==> f(x):R"
    1.47      and r2: "!!y. y:Q ==> g(y):R"
    1.48 @@ -61,7 +61,7 @@
    1.49    done
    1.50  
    1.51  (*Double negation law*)
    1.52 -schematic_lemma notnotD: "p:~~P ==> ?p : P"
    1.53 +schematic_goal notnotD: "p:~~P ==> ?p : P"
    1.54    apply (rule classical)
    1.55    apply (erule notE)
    1.56    apply assumption
    1.57 @@ -72,7 +72,7 @@
    1.58  
    1.59  (*Classical <-> elimination.  Proof substitutes P=Q in
    1.60      ~P ==> ~Q    and    P ==> Q  *)
    1.61 -schematic_lemma iffCE:
    1.62 +schematic_goal iffCE:
    1.63    assumes major: "p:P<->Q"
    1.64      and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
    1.65      and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
    1.66 @@ -88,7 +88,7 @@
    1.67  
    1.68  
    1.69  (*Should be used as swap since ~P becomes redundant*)
    1.70 -schematic_lemma swap:
    1.71 +schematic_goal swap:
    1.72    assumes major: "p:~P"
    1.73      and r: "!!x. x:~Q ==> f(x):P"
    1.74    shows "?p : Q"
    1.75 @@ -130,7 +130,7 @@
    1.76      addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];
    1.77  \<close>
    1.78  
    1.79 -schematic_lemma cla_rews:
    1.80 +schematic_goal cla_rews:
    1.81    "?p1 : P | ~P"
    1.82    "?p2 : ~P | P"
    1.83    "?p3 : ~ ~ P <-> P"