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