src/FOLP/FOLP.thy
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57009 8cb6a5f1ae84
parent 48891 c0eafbd55de3
child 58889 5b7a9633cfa8
permissions -rw-r--r--
added SML implementation of MaSh
     1 (*  Title:      FOLP/FOLP.thy
     2     Author:     Martin D Coen, Cambridge University Computer Laboratory
     3     Copyright   1992  University of Cambridge
     4 *)
     5 
     6 header {* Classical First-Order Logic with Proofs *}
     7 
     8 theory FOLP
     9 imports IFOLP
    10 begin
    11 
    12 axiomatization cla :: "[p=>p]=>p"
    13   where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    14 
    15 
    16 (*** Classical introduction rules for | and EX ***)
    17 
    18 schematic_lemma disjCI:
    19   assumes "!!x. x:~Q ==> f(x):P"
    20   shows "?p : P|Q"
    21   apply (rule classical)
    22   apply (assumption | rule assms disjI1 notI)+
    23   apply (assumption | rule disjI2 notE)+
    24   done
    25 
    26 (*introduction rule involving only EX*)
    27 schematic_lemma ex_classical:
    28   assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"
    29   shows "?p : EX x. P(x)"
    30   apply (rule classical)
    31   apply (rule exI, rule assms, assumption)
    32   done
    33 
    34 (*version of above, simplifying ~EX to ALL~ *)
    35 schematic_lemma exCI:
    36   assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"
    37   shows "?p : EX x. P(x)"
    38   apply (rule ex_classical)
    39   apply (rule notI [THEN allI, THEN assms])
    40   apply (erule notE)
    41   apply (erule exI)
    42   done
    43 
    44 schematic_lemma excluded_middle: "?p : ~P | P"
    45   apply (rule disjCI)
    46   apply assumption
    47   done
    48 
    49 
    50 (*** Special elimination rules *)
    51 
    52 (*Classical implies (-->) elimination. *)
    53 schematic_lemma impCE:
    54   assumes major: "p:P-->Q"
    55     and r1: "!!x. x:~P ==> f(x):R"
    56     and r2: "!!y. y:Q ==> g(y):R"
    57   shows "?p : R"
    58   apply (rule excluded_middle [THEN disjE])
    59    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
    60        resolve_tac [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *})
    61   done
    62 
    63 (*Double negation law*)
    64 schematic_lemma notnotD: "p:~~P ==> ?p : P"
    65   apply (rule classical)
    66   apply (erule notE)
    67   apply assumption
    68   done
    69 
    70 
    71 (*** Tactics for implication and contradiction ***)
    72 
    73 (*Classical <-> elimination.  Proof substitutes P=Q in
    74     ~P ==> ~Q    and    P ==> Q  *)
    75 schematic_lemma iffCE:
    76   assumes major: "p:P<->Q"
    77     and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
    78     and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
    79   shows "?p : R"
    80   apply (insert major)
    81   apply (unfold iff_def)
    82   apply (rule conjE)
    83   apply (tactic {* DEPTH_SOLVE_1 (etac @{thm impCE} 1 ORELSE
    84       eresolve_tac [@{thm notE}, @{thm impE}] 1 THEN atac 1 ORELSE atac 1 ORELSE
    85       resolve_tac [@{thm r1}, @{thm r2}] 1) *})+
    86   done
    87 
    88 
    89 (*Should be used as swap since ~P becomes redundant*)
    90 schematic_lemma swap:
    91   assumes major: "p:~P"
    92     and r: "!!x. x:~Q ==> f(x):P"
    93   shows "?p : Q"
    94   apply (rule classical)
    95   apply (rule major [THEN notE])
    96   apply (rule r)
    97   apply assumption
    98   done
    99 
   100 ML_file "classical.ML"      (* Patched because matching won't instantiate proof *)
   101 ML_file "simp.ML"           (* Patched because matching won't instantiate proof *)
   102 
   103 ML {*
   104 structure Cla = Classical
   105 (
   106   val sizef = size_of_thm
   107   val mp = @{thm mp}
   108   val not_elim = @{thm notE}
   109   val swap = @{thm swap}
   110   val hyp_subst_tacs = [hyp_subst_tac]
   111 );
   112 open Cla;
   113 
   114 (*Propositional rules
   115   -- iffCE might seem better, but in the examples in ex/cla
   116      run about 7% slower than with iffE*)
   117 val prop_cs =
   118   empty_cs addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI},
   119       @{thm impI}, @{thm notI}, @{thm iffI}]
   120     addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffE}];
   121 
   122 (*Quantifier rules*)
   123 val FOLP_cs =
   124   prop_cs addSIs [@{thm allI}] addIs [@{thm exI}, @{thm ex1I}]
   125     addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm allE}];
   126 
   127 val FOLP_dup_cs =
   128   prop_cs addSIs [@{thm allI}] addIs [@{thm exCI}, @{thm ex1I}]
   129     addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];
   130 *}
   131 
   132 schematic_lemma cla_rews:
   133   "?p1 : P | ~P"
   134   "?p2 : ~P | P"
   135   "?p3 : ~ ~ P <-> P"
   136   "?p4 : (~P --> P) <-> P"
   137   apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})
   138   done
   139 
   140 ML_file "simpdata.ML"
   141 
   142 end