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