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