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