src/FOLP/FOLP.thy

   classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
 
 
 (*** Classical introduction rules for | and EX ***)
 
-lemma disjCI:
+schematic_lemma disjCI:
   assumes "!!x. x:~Q ==> f(x):P"
   shows "?p : P|Q"
   apply (rule classical)
   apply (assumption | rule assms disjI1 notI)+
   apply (assumption | rule disjI2 notE)+
   done
 
 (*introduction rule involving only EX*)
-lemma ex_classical:
+schematic_lemma ex_classical:
   assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"
   shows "?p : EX x. P(x)"
   apply (rule classical)
   apply (rule exI, rule assms, assumption)
   done
 
 (*version of above, simplifying ~EX to ALL~ *)
-lemma exCI:
+schematic_lemma exCI:
   assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"
   shows "?p : EX x. P(x)"
   apply (rule ex_classical)
   apply (rule notI [THEN allI, THEN assms])
   apply (erule notE)
   apply (erule exI)
   done
 
-lemma excluded_middle: "?p : ~P | P"
+schematic_lemma excluded_middle: "?p : ~P | P"
   apply (rule disjCI)
   apply assumption
   done
 
 
 (*** Special elimination rules *)
 
 (*Classical implies (-->) elimination. *)
-lemma impCE:
+schematic_lemma impCE:
   assumes major: "p:P-->Q"
     and r1: "!!x. x:~P ==> f(x):R"
     and r2: "!!y. y:Q ==> g(y):R"
   shows "?p : R"
   apply (rule excluded_middle [THEN disjE])
    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
        resolve_tac [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *})
   done
 
 (*Double negation law*)
-lemma notnotD: "p:~~P ==> ?p : P"
+schematic_lemma notnotD: "p:~~P ==> ?p : P"
   apply (rule classical)
   apply (erule notE)
   apply assumption
   done
 
 
 (*** Tactics for implication and contradiction ***)
 
 (*Classical <-> elimination.  Proof substitutes P=Q in
     ~P ==> ~Q    and    P ==> Q  *)
-lemma iffCE:
+schematic_lemma iffCE:
   assumes major: "p:P<->Q"
     and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
     and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
   shows "?p : R"
   apply (insert major)

       resolve_tac [@{thm r1}, @{thm r2}] 1) *})+
   done
 
 
 (*Should be used as swap since ~P becomes redundant*)
-lemma swap:
+schematic_lemma swap:
   assumes major: "p:~P"
     and r: "!!x. x:~Q ==> f(x):P"
   shows "?p : Q"
   apply (rule classical)
   apply (rule major [THEN notE])

 val FOLP_dup_cs =
   prop_cs addSIs [@{thm allI}] addIs [@{thm exCI}, @{thm ex1I}]
     addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];
 *}
 
-lemma cla_rews:
+schematic_lemma cla_rews:
   "?p1 : P | ~P"
   "?p2 : ~P | P"
   "?p3 : ~ ~ P <-> P"
   "?p4 : (~P --> P) <-> P"
   apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})