src/Sequents/ILL.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 62144 bdab93ccfaf8
child 69593 3dda49e08b9d
permissions -rw-r--r--
more permissive;
     1 (*  Title:      Sequents/ILL.thy
     2     Author:     Sara Kalvala and Valeria de Paiva
     3     Copyright   1995  University of Cambridge
     4 *)
     5 
     6 theory ILL
     7 imports Sequents
     8 begin
     9 
    10 consts
    11   Trueprop       :: "two_seqi"
    12 
    13   tens :: "[o, o] \<Rightarrow> o"        (infixr "><" 35)
    14   limp :: "[o, o] \<Rightarrow> o"        (infixr "-o" 45)
    15   FShriek :: "o \<Rightarrow> o"          ("! _" [100] 1000)
    16   lconj :: "[o, o] \<Rightarrow> o"       (infixr "&&" 35)
    17   ldisj :: "[o, o] \<Rightarrow> o"       (infixr "++" 35)
    18   zero :: "o"                  ("0")
    19   top :: "o"                   ("1")
    20   eye :: "o"                   ("I")
    21 
    22 
    23   (* context manipulation *)
    24 
    25  Context      :: "two_seqi"
    26 
    27   (* promotion rule *)
    28 
    29   PromAux :: "three_seqi"
    30 
    31 syntax
    32   "_Trueprop" :: "single_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
    33   "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    34   "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
    35 
    36 parse_translation \<open>
    37   [(@{syntax_const "_Trueprop"}, K (single_tr @{const_syntax Trueprop})),
    38    (@{syntax_const "_Context"}, K (two_seq_tr @{const_syntax Context})),
    39    (@{syntax_const "_PromAux"}, K (three_seq_tr @{const_syntax PromAux}))]
    40 \<close>
    41 
    42 print_translation \<open>
    43   [(@{const_syntax Trueprop}, K (single_tr' @{syntax_const "_Trueprop"})),
    44    (@{const_syntax Context}, K (two_seq_tr' @{syntax_const "_Context"})),
    45    (@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
    46 \<close>
    47 
    48 definition liff :: "[o, o] \<Rightarrow> o"  (infixr "o-o" 45)
    49   where "P o-o Q == (P -o Q) >< (Q -o P)"
    50 
    51 definition aneg :: "o\<Rightarrow>o"  ("~_")
    52   where "~A == A -o 0"
    53 
    54 
    55 axiomatization where
    56 
    57 identity:        "P \<turnstile> P" and
    58 
    59 zerol:           "$G, 0, $H \<turnstile> A" and
    60 
    61   (* RULES THAT DO NOT DIVIDE CONTEXT *)
    62 
    63 derelict:   "$F, A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
    64   (* unfortunately, this one removes !A  *)
    65 
    66 contract:  "$F, !A, !A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
    67 
    68 weaken:     "$F, $G \<turnstile> C \<Longrightarrow> $G, !A, $F \<turnstile> C" and
    69   (* weak form of weakening, in practice just to clean context *)
    70   (* weaken and contract not needed (CHECK)  *)
    71 
    72 promote2:        "promaux{ || $H || B} \<Longrightarrow> $H \<turnstile> !B" and
    73 promote1:        "promaux{!A, $G || $H || B}
    74                   \<Longrightarrow> promaux {$G || $H, !A || B}" and
    75 promote0:        "$G \<turnstile> A \<Longrightarrow> promaux {$G || || A}" and
    76 
    77 
    78 
    79 tensl:     "$H, A, B, $G \<turnstile> C \<Longrightarrow> $H, A >< B, $G \<turnstile> C" and
    80 
    81 impr:      "A, $F \<turnstile> B \<Longrightarrow> $F \<turnstile> A -o B" and
    82 
    83 conjr:           "\<lbrakk>$F \<turnstile> A ;
    84                  $F \<turnstile> B\<rbrakk>
    85                 \<Longrightarrow> $F \<turnstile> (A && B)" and
    86 
    87 conjll:          "$G, A, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and
    88 
    89 conjlr:          "$G, B, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and
    90 
    91 disjrl:          "$G \<turnstile> A \<Longrightarrow> $G \<turnstile> A ++ B" and
    92 disjrr:          "$G \<turnstile> B \<Longrightarrow> $G \<turnstile> A ++ B" and
    93 disjl:           "\<lbrakk>$G, A, $H \<turnstile> C ;
    94                    $G, B, $H \<turnstile> C\<rbrakk>
    95                  \<Longrightarrow> $G, A ++ B, $H \<turnstile> C" and
    96 
    97 
    98       (* RULES THAT DIVIDE CONTEXT *)
    99 
   100 tensr:           "\<lbrakk>$F, $J :=: $G;
   101                    $F \<turnstile> A ;
   102                    $J \<turnstile> B\<rbrakk>
   103                      \<Longrightarrow> $G \<turnstile> A >< B" and
   104 
   105 impl:            "\<lbrakk>$G, $F :=: $J, $H ;
   106                    B, $F \<turnstile> C ;
   107                    $G \<turnstile> A\<rbrakk>
   108                      \<Longrightarrow> $J, A -o B, $H \<turnstile> C" and
   109 
   110 
   111 cut: "\<lbrakk> $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
   112         $H1, $H2, $H3, $H4 \<turnstile> A ;
   113         $J1, $J2, A, $J3, $J4 \<turnstile> B\<rbrakk> \<Longrightarrow> $F \<turnstile> B" and
   114 
   115 
   116   (* CONTEXT RULES *)
   117 
   118 context1:     "$G :=: $G" and
   119 context2:     "$F, $G :=: $H, !A, $G \<Longrightarrow> $F, A, $G :=: $H, !A, $G" and
   120 context3:     "$F, $G :=: $H, $J \<Longrightarrow> $F, A, $G :=: $H, A, $J" and
   121 context4a:    "$F :=: $H, $G \<Longrightarrow> $F :=: $H, !A, $G" and
   122 context4b:    "$F, $H :=: $G \<Longrightarrow> $F, !A, $H :=: $G" and
   123 context5:     "$F, $G :=: $H \<Longrightarrow> $G, $F :=: $H"
   124 
   125 text "declarations for lazy classical reasoning:"
   126 lemmas [safe] =
   127   context3
   128   context2
   129   promote0
   130   disjl
   131   conjr
   132   tensl
   133 lemmas [unsafe] =
   134   context4b
   135   context4a
   136   context1
   137   promote2
   138   promote1
   139   weaken
   140   derelict
   141   impl
   142   tensr
   143   impr
   144   disjrr
   145   disjrl
   146   conjlr
   147   conjll
   148   zerol
   149   identity
   150 
   151 lemma aux_impl: "$F, $G \<turnstile> A \<Longrightarrow> $F, !(A -o B), $G \<turnstile> B"
   152   apply (rule derelict)
   153   apply (rule impl)
   154   apply (rule_tac [2] identity)
   155   apply (rule context1)
   156   apply assumption
   157   done
   158 
   159 lemma conj_lemma: " $F, !A, !B, $G \<turnstile> C \<Longrightarrow> $F, !(A && B), $G \<turnstile> C"
   160   apply (rule contract)
   161   apply (rule_tac A = " (!A) >< (!B) " in cut)
   162   apply (rule_tac [2] tensr)
   163   prefer 3
   164   apply (subgoal_tac "! (A && B) \<turnstile> !A")
   165   apply assumption
   166   apply best
   167   prefer 3
   168   apply (subgoal_tac "! (A && B) \<turnstile> !B")
   169   apply assumption
   170   apply best
   171   apply (rule_tac [2] context1)
   172   apply (rule_tac [2] tensl)
   173   prefer 2 apply assumption
   174   apply (rule context3)
   175   apply (rule context3)
   176   apply (rule context1)
   177   done
   178 
   179 lemma impr_contract: "!A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B"
   180   apply (rule impr)
   181   apply (rule contract)
   182   apply assumption
   183   done
   184 
   185 lemma impr_contr_der: "A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B"
   186   apply (rule impr)
   187   apply (rule contract)
   188   apply (rule derelict)
   189   apply assumption
   190   done
   191 
   192 lemma contrad1: "$F, (!B) -o 0, $G, !B, $H \<turnstile> A"
   193   apply (rule impl)
   194   apply (rule_tac [3] identity)
   195   apply (rule context3)
   196   apply (rule context1)
   197   apply (rule zerol)
   198   done
   199 
   200 
   201 lemma contrad2: "$F, !B, $G, (!B) -o 0, $H \<turnstile> A"
   202   apply (rule impl)
   203   apply (rule_tac [3] identity)
   204   apply (rule context3)
   205   apply (rule context1)
   206   apply (rule zerol)
   207   done
   208 
   209 lemma ll_mp: "A -o B, A \<turnstile> B"
   210   apply (rule impl)
   211   apply (rule_tac [2] identity)
   212   apply (rule_tac [2] identity)
   213   apply (rule context1)
   214   done
   215 
   216 lemma mp_rule1: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A, $G, A -o B, $H \<turnstile> C"
   217   apply (rule_tac A = "B" in cut)
   218   apply (rule_tac [2] ll_mp)
   219   prefer 2 apply (assumption)
   220   apply (rule context3)
   221   apply (rule context3)
   222   apply (rule context1)
   223   done
   224 
   225 lemma mp_rule2: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A -o B, $G, A, $H \<turnstile> C"
   226   apply (rule_tac A = "B" in cut)
   227   apply (rule_tac [2] ll_mp)
   228   prefer 2 apply (assumption)
   229   apply (rule context3)
   230   apply (rule context3)
   231   apply (rule context1)
   232   done
   233 
   234 lemma or_to_and: "!((!(A ++ B)) -o 0) \<turnstile> !( ((!A) -o 0) && ((!B) -o 0))"
   235   by best
   236 
   237 lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G \<turnstile> C \<Longrightarrow>
   238           $F, !((!(A ++ B)) -o 0), $G \<turnstile> C"
   239   apply (rule cut)
   240   apply (rule_tac [2] or_to_and)
   241   prefer 2 apply (assumption)
   242   apply (rule context3)
   243   apply (rule context1)
   244   done
   245 
   246 lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) \<turnstile> (!(A && B)) -o C"
   247   apply (rule impr)
   248   apply (rule conj_lemma)
   249   apply (rule disjl)
   250   apply (rule mp_rule1, best)+
   251   done
   252 
   253 lemma not_imp: "!A, !((!B) -o 0) \<turnstile> (!((!A) -o B)) -o 0"
   254   by best
   255 
   256 lemma a_not_a: "!A -o (!A -o 0) \<turnstile> !A -o 0"
   257   apply (rule impr)
   258   apply (rule contract)
   259   apply (rule impl)
   260   apply (rule_tac [3] identity)
   261   apply (rule context1)
   262   apply best
   263   done
   264 
   265 lemma a_not_a_rule: "$J1, !A -o 0, $J2 \<turnstile> B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 \<turnstile> B"
   266   apply (rule_tac A = "!A -o 0" in cut)
   267   apply (rule_tac [2] a_not_a)
   268   prefer 2 apply assumption
   269   apply best
   270   done
   271 
   272 ML \<open>
   273   val safe_pack =
   274     @{context}
   275     |> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1
   276         contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule}
   277     |> Cla.add_unsafe @{thm aux_impl}
   278     |> Cla.get_pack;
   279 
   280   val power_pack =
   281     Cla.put_pack safe_pack @{context}
   282     |> Cla.add_unsafe @{thm impr_contr_der}
   283     |> Cla.get_pack;
   284 \<close>
   285 
   286 method_setup best_safe =
   287   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt)))\<close>
   288 
   289 method_setup best_power =
   290   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack power_pack ctxt)))\<close>
   291 
   292 
   293 (* Some examples from Troelstra and van Dalen *)
   294 
   295 lemma "!((!A) -o ((!B) -o 0)) \<turnstile> (!(A && B)) -o 0"
   296   by best_safe
   297 
   298 lemma "!((!(A && B)) -o 0) \<turnstile> !((!A) -o ((!B) -o 0))"
   299   by best_safe
   300 
   301 lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) \<turnstile>
   302         (!A) -o ( (!  ((!B) -o 0)) -o 0)"
   303   by best_safe
   304 
   305 lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) \<turnstile>
   306           (!((! ((!A) -o B) ) -o 0)) -o 0"
   307   by best_power
   308 
   309 end