wneuper/isa: src/Sequents/ILL.thy@473303ef6e34

     1 (*  Title:      Sequents/ILL.thy

     2     Author:     Sara Kalvala and Valeria de Paiva

     3     Copyright   1995  University of Cambridge

     4 *)

     6 theory ILL

     7 imports Sequents

     8 begin

    10 consts

    11   Trueprop       :: "two_seqi"

    13   tens :: "[o, o] => o"        (infixr "><" 35)

    14   limp :: "[o, o] => o"        (infixr "-o" 45)

    15   liff :: "[o, o] => o"        (infixr "o-o" 45)

    16   FShriek :: "o => o"          ("! _" [100] 1000)

    17   lconj :: "[o, o] => o"       (infixr "&&" 35)

    18   ldisj :: "[o, o] => o"       (infixr "++" 35)

    19   zero :: "o"                  ("0")

    20   top :: "o"                   ("1")

    21   eye :: "o"                   ("I")

    22   aneg :: "o=>o"               ("~_")

    25   (* context manipulation *)

    27  Context      :: "two_seqi"

    29   (* promotion rule *)

    31   PromAux :: "three_seqi"

    33 syntax

    34   "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)

    35   "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)

    36   "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")

    38 parse_translation {*

    39   [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),

    40    (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),

    41    (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]

    42 *}

    44 print_translation {*

    45   [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),

    46    (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),

    47    (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]

    48 *}

    50 defs

    52 liff_def:        "P o-o Q == (P -o Q) >< (Q -o P)"

    54 aneg_def:        "~A == A -o 0"

    57 axiomatization where

    59 identity:        "P |- P" and

    61 zerol:           "$G, 0, $H |- A" and

    63   (* RULES THAT DO NOT DIVIDE CONTEXT *)

    65 derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C" and

    66   (* unfortunately, this one removes !A  *)

    68 contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" and

    70 weaken:     "$F, $G |- C ==> $G, !A, $F |- C" and

    71   (* weak form of weakening, in practice just to clean context *)

    72   (* weaken and contract not needed (CHECK)  *)

    74 promote2:        "promaux{ || $H || B} ==> $H |- !B" and

    75 promote1:        "promaux{!A, $G || $H || B}

    76                   ==> promaux {$G || $H, !A || B}" and

    77 promote0:        "$G |- A ==> promaux {$G || || A}" and

    81 tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" and

    83 impr:      "A, $F |- B ==> $F |- A -o B" and

    85 conjr:           "[| $F |- A ;

    86                  $F |- B |]

    87                 ==> $F |- (A && B)" and

    89 conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C" and

    91 conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C" and

    93 disjrl:          "$G |- A ==> $G |- A ++ B" and

    94 disjrr:          "$G |- B ==> $G |- A ++ B" and

    95 disjl:           "[| $G, A, $H |- C ;

    96                      $G, B, $H |- C |]

    97                  ==> $G, A ++ B, $H |- C" and

   100       (* RULES THAT DIVIDE CONTEXT *)

   102 tensr:           "[| $F, $J :=: $G;

   103                      $F |- A ;

   104                      $J |- B     |]

   105                      ==> $G |- A >< B" and

   107 impl:            "[| $G, $F :=: $J, $H ;

   108                      B, $F |- C ;

   109                         $G |- A |]

   110                      ==> $J, A -o B, $H |- C" and

   113 cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;

   114           $H1, $H2, $H3, $H4 |- A ;

   115           $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B" and

   118   (* CONTEXT RULES *)

   120 context1:     "$G :=: $G" and

   121 context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" and

   122 context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" and

   123 context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G" and

   124 context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G" and

   125 context5:     "$F, $G :=: $H ==> $G, $F :=: $H"

   128 ML {*

   129 val lazy_cs = empty_pack

   130   add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0},

   131     @{thm context2}, @{thm context3}]

   132   add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr},

   133     @{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl},

   134     @{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2},

   135     @{thm context1}, @{thm context4a}, @{thm context4b}];

   137 fun prom_tac n =

   138   REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n)

   139 *}

   141 method_setup best_lazy =

   142   {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *}

   143   "lazy classical reasoning"

   145 lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"

   146   apply (rule derelict)

   147   apply (rule impl)

   148   apply (rule_tac [2] identity)

   149   apply (rule context1)

   150   apply assumption

   151   done

   153 lemma conj_lemma: " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"

   154   apply (rule contract)

   155   apply (rule_tac A = " (!A) >< (!B) " in cut)

   156   apply (rule_tac [2] tensr)

   157   prefer 3

   158   apply (subgoal_tac "! (A && B) |- !A")

   159   apply assumption

   160   apply best_lazy

   161   prefer 3

   162   apply (subgoal_tac "! (A && B) |- !B")

   163   apply assumption

   164   apply best_lazy

   165   apply (rule_tac [2] context1)

   166   apply (rule_tac [2] tensl)

   167   prefer 2 apply (assumption)

   168   apply (rule context3)

   169   apply (rule context3)

   170   apply (rule context1)

   171   done

   173 lemma impr_contract: "!A, !A, $G |- B ==> $G |- (!A) -o B"

   174   apply (rule impr)

   175   apply (rule contract)

   176   apply assumption

   177   done

   179 lemma impr_contr_der: "A, !A, $G |- B ==> $G |- (!A) -o B"

   180   apply (rule impr)

   181   apply (rule contract)

   182   apply (rule derelict)

   183   apply assumption

   184   done

   186 lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A"

   187   apply (rule impl)

   188   apply (rule_tac [3] identity)

   189   apply (rule context3)

   190   apply (rule context1)

   191   apply (rule zerol)

   192   done

   195 lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A"

   196   apply (rule impl)

   197   apply (rule_tac [3] identity)

   198   apply (rule context3)

   199   apply (rule context1)

   200   apply (rule zerol)

   201   done

   203 lemma ll_mp: "A -o B, A |- B"

   204   apply (rule impl)

   205   apply (rule_tac [2] identity)

   206   apply (rule_tac [2] identity)

   207   apply (rule context1)

   208   done

   210 lemma mp_rule1: "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"

   211   apply (rule_tac A = "B" in cut)

   212   apply (rule_tac [2] ll_mp)

   213   prefer 2 apply (assumption)

   214   apply (rule context3)

   215   apply (rule context3)

   216   apply (rule context1)

   217   done

   219 lemma mp_rule2: "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"

   220   apply (rule_tac A = "B" in cut)

   221   apply (rule_tac [2] ll_mp)

   222   prefer 2 apply (assumption)

   223   apply (rule context3)

   224   apply (rule context3)

   225   apply (rule context1)

   226   done

   228 lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"

   229   by best_lazy

   231 lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==>

   232           $F, !((!(A ++ B)) -o 0), $G |- C"

   233   apply (rule cut)

   234   apply (rule_tac [2] or_to_and)

   235   prefer 2 apply (assumption)

   236   apply (rule context3)

   237   apply (rule context1)

   238   done

   240 lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"

   241   apply (rule impr)

   242   apply (rule conj_lemma)

   243   apply (rule disjl)

   244   apply (rule mp_rule1, best_lazy)+

   245   done

   247 lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"

   248   by best_lazy

   250 lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"

   251   apply (rule impr)

   252   apply (rule contract)

   253   apply (rule impl)

   254   apply (rule_tac [3] identity)

   255   apply (rule context1)

   256   apply best_lazy

   257   done

   259 lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"

   260   apply (rule_tac A = "!A -o 0" in cut)

   261   apply (rule_tac [2] a_not_a)

   262   prefer 2 apply (assumption)

   263   apply best_lazy

   264   done

   266 ML {*

   267 val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1},

   268                                  @{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule},

   269                                  @{thm a_not_a_rule}]

   270                       add_unsafes [@{thm aux_impl}];

   272 val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}];

   273 *}

   276 method_setup best_safe =

   277   {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *}

   279 method_setup best_power =

   280   {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *}

   283 (* Some examples from Troelstra and van Dalen *)

   285 lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"

   286   by best_safe

   288 lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"

   289   by best_safe

   291 lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |-

   292         (!A) -o ( (!  ((!B) -o 0)) -o 0)"

   293   by best_safe

   295 lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |-

   296           (!((! ((!A) -o B) ) -o 0)) -o 0"

   297   by best_power

   299 end

author	wenzelm
	Thu, 28 Feb 2013 14:22:14 +0100
changeset 52446	473303ef6e34
parent 43685	5af15f1e2ef6
child 53280	36ffe23b25f8
permissions	-rw-r--r--