src/FOLP/FOLP.thy
 author haftmann Thu Nov 23 17:03:27 2017 +0000 (20 months ago) changeset 67087 733017b19de9 parent 61337 4645502c3c64 child 69593 3dda49e08b9d permissions -rw-r--r--
generalized more lemmas
```     1 (*  Title:      FOLP/FOLP.thy
```
```     2     Author:     Martin D Coen, Cambridge University Computer Laboratory
```
```     3     Copyright   1992  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 section \<open>Classical First-Order Logic with Proofs\<close>
```
```     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_goal 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_goal 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_goal 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_goal 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_goal 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 \<open>DEPTH_SOLVE (assume_tac @{context} 1 ORELSE
```
```    60        resolve_tac @{context} [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1)\<close>)
```
```    61   done
```
```    62
```
```    63 (*Double negation law*)
```
```    64 schematic_goal 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_goal 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 \<open>DEPTH_SOLVE_1 (eresolve_tac @{context} @{thms impCE} 1 ORELSE
```
```    84       eresolve_tac @{context} [@{thm notE}, @{thm impE}] 1 THEN assume_tac @{context} 1 ORELSE
```
```    85       assume_tac @{context} 1 ORELSE
```
```    86       resolve_tac @{context} [@{thm r1}, @{thm r2}] 1)\<close>)+
```
```    87   done
```
```    88
```
```    89
```
```    90 (*Should be used as swap since ~P becomes redundant*)
```
```    91 schematic_goal swap:
```
```    92   assumes major: "p:~P"
```
```    93     and r: "!!x. x:~Q ==> f(x):P"
```
```    94   shows "?p : Q"
```
```    95   apply (rule classical)
```
```    96   apply (rule major [THEN notE])
```
```    97   apply (rule r)
```
```    98   apply assumption
```
```    99   done
```
```   100
```
```   101 ML_file "classical.ML"      (* Patched because matching won't instantiate proof *)
```
```   102 ML_file "simp.ML"           (* Patched because matching won't instantiate proof *)
```
```   103
```
```   104 ML \<open>
```
```   105 structure Cla = Classical
```
```   106 (
```
```   107   val sizef = size_of_thm
```
```   108   val mp = @{thm mp}
```
```   109   val not_elim = @{thm notE}
```
```   110   val swap = @{thm swap}
```
```   111   fun hyp_subst_tacs ctxt = [hyp_subst_tac ctxt]
```
```   112 );
```
```   113 open Cla;
```
```   114
```
```   115 (*Propositional rules
```
```   116   -- iffCE might seem better, but in the examples in ex/cla
```
```   117      run about 7% slower than with iffE*)
```
```   118 val prop_cs =
```
```   119   empty_cs addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI},
```
```   120       @{thm impI}, @{thm notI}, @{thm iffI}]
```
```   121     addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffE}];
```
```   122
```
```   123 (*Quantifier rules*)
```
```   124 val FOLP_cs =
```
```   125   prop_cs addSIs [@{thm allI}] addIs [@{thm exI}, @{thm ex1I}]
```
```   126     addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm allE}];
```
```   127
```
```   128 val FOLP_dup_cs =
```
```   129   prop_cs addSIs [@{thm allI}] addIs [@{thm exCI}, @{thm ex1I}]
```
```   130     addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];
```
```   131 \<close>
```
```   132
```
```   133 schematic_goal cla_rews:
```
```   134   "?p1 : P | ~P"
```
```   135   "?p2 : ~P | P"
```
```   136   "?p3 : ~ ~ P <-> P"
```
```   137   "?p4 : (~P --> P) <-> P"
```
```   138   apply (tactic \<open>ALLGOALS (Cla.fast_tac @{context} FOLP_cs)\<close>)
```
```   139   done
```
```   140
```
```   141 ML_file "simpdata.ML"
```
```   142
```
```   143 end
```