Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Sequents/ILL.thy
author wenzelm
Wed, 09 May 2007 19:37:19 +0200
changeset 22894 619b270607ac
parent 21588 cd0dc678a205
child 30515 4120fc59dd85
permissions -rw-r--r--
eliminated unnamed infixes; 
     1 (*  Title:      Sequents/ILL.thy

     2     ID:         $Id$

     3     Author:     Sara Kalvala and Valeria de Paiva

     4     Copyright   1995  University of Cambridge

     5 *)

     6 

     7 theory ILL

     8 imports Sequents

     9 begin

    10 

    11 consts

    12   Trueprop       :: "two_seqi"

    13 

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

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

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

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

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

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

    20   zero :: "o"                  ("0")

    21   top :: "o"                   ("1")

    22   eye :: "o"                   ("I")

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

    24 

    25 

    26   (* context manipulation *)

    27 

    28  Context      :: "two_seqi"

    29 

    30   (* promotion rule *)

    31 

    32   PromAux :: "three_seqi"

    33 

    34 syntax

    35   "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)

    36   "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)

    37   "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")

    38 

    39 parse_translation {*

    40   [("@Trueprop", single_tr "Trueprop"),

    41    ("@Context", two_seq_tr "Context"),

    42    ("@PromAux", three_seq_tr "PromAux")] *}

    43 

    44 print_translation {*

    45   [("Trueprop", single_tr' "@Trueprop"),

    46    ("Context", two_seq_tr'"@Context"),

    47    ("PromAux", three_seq_tr'"@PromAux")] *}

    48 

    49 defs

    50 

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

    52 

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

    54 

    55 

    56 axioms

    57 

    58 identity:        "P |- P"

    59 

    60 zerol:           "$G, 0, $H |- A"

    61 

    62   (* RULES THAT DO NOT DIVIDE CONTEXT *)

    63 

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

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

    66 

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

    68 

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

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

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

    72 

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

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

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

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

    77 

    78 

    79 

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

    81 

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

    83 

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

    85                  $F |- B |]

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

    87 

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

    89 

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

    91 

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

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

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

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

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

    97 

    98 

    99       (* RULES THAT DIVIDE CONTEXT *)

   100 

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

   102                      $F |- A ;

   103                      $J |- B     |]

   104                      ==> $G |- A >< B"

   105 

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

   107                      B, $F |- C ;

   108                         $G |- A |]

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

   110 

   111 

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

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

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

   115 

   116 

   117   (* CONTEXT RULES *)

   118 

   119 context1:     "$G :=: $G"

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

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

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

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

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

   125 

   126 

   127 ML {*

   128 

   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"];

   136 

   137 local

   138   val promote0 = thm "promote0"

   139   val promote1 = thm "promote1"

   140   val promote2 = thm "promote2"

   141 in

   142 

   143 fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n)

   144 

   145 end

   146 *}

   147 

   148 method_setup best_lazy =

   149   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *}

   150   "lazy classical reasoning"

   151 

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

   153   apply (rule derelict)

   154   apply (rule impl)

   155   apply (rule_tac [2] identity)

   156   apply (rule context1)

   157   apply assumption

   158   done

   159 

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

   161   apply (rule contract)

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

   163   apply (rule_tac [2] tensr)

   164   prefer 3

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

   166   apply assumption

   167   apply best_lazy

   168   prefer 3

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

   170   apply assumption

   171   apply best_lazy

   172   apply (rule_tac [2] context1)

   173   apply (rule_tac [2] tensl)

   174   prefer 2 apply (assumption)

   175   apply (rule context3)

   176   apply (rule context3)

   177   apply (rule context1)

   178   done

   179 

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

   181   apply (rule impr)

   182   apply (rule contract)

   183   apply assumption

   184   done

   185 

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

   187   apply (rule impr)

   188   apply (rule contract)

   189   apply (rule derelict)

   190   apply assumption

   191   done

   192 

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

   194   apply (rule impl)

   195   apply (rule_tac [3] identity)

   196   apply (rule context3)

   197   apply (rule context1)

   198   apply (rule zerol)

   199   done

   200 

   201 

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

   203   apply (rule impl)

   204   apply (rule_tac [3] identity)

   205   apply (rule context3)

   206   apply (rule context1)

   207   apply (rule zerol)

   208   done

   209 

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

   211   apply (rule impl)

   212   apply (rule_tac [2] identity)

   213   apply (rule_tac [2] identity)

   214   apply (rule context1)

   215   done

   216 

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

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

   219   apply (rule_tac [2] ll_mp)

   220   prefer 2 apply (assumption)

   221   apply (rule context3)

   222   apply (rule context3)

   223   apply (rule context1)

   224   done

   225 

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

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

   228   apply (rule_tac [2] ll_mp)

   229   prefer 2 apply (assumption)

   230   apply (rule context3)

   231   apply (rule context3)

   232   apply (rule context1)

   233   done

   234 

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

   236   by best_lazy

   237 

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

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

   240   apply (rule cut)

   241   apply (rule_tac [2] or_to_and)

   242   prefer 2 apply (assumption)

   243   apply (rule context3)

   244   apply (rule context1)

   245   done

   246 

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

   248   apply (rule impr)

   249   apply (rule conj_lemma)

   250   apply (rule disjl)

   251   apply (rule mp_rule1, best_lazy)+

   252   done

   253 

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

   255   by best_lazy

   256 

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

   258   apply (rule impr)

   259   apply (rule contract)

   260   apply (rule impl)

   261   apply (rule_tac [3] identity)

   262   apply (rule context1)

   263   apply best_lazy

   264   done

   265 

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

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

   268   apply (rule_tac [2] a_not_a)

   269   prefer 2 apply (assumption)

   270   apply best_lazy

   271   done

   272 

   273 ML {*

   274 

   275 val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1",

   276                                  thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule",

   277                                  thm "a_not_a_rule"]

   278                       add_unsafes [thm "aux_impl"];

   279 

   280 val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];

   281 *}

   282 

   283 

   284 method_setup best_safe =

   285   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} ""

   286 

   287 method_setup best_power =

   288   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} ""

   289 

   290 

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

   292 

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

   294   by best_safe

   295 

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

   297   by best_safe

   298 

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

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

   301   by best_safe

   302 

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

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

   305   by best_power

   306 

   307 end
wneuper/isa