src/Sequents/ILL.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 2073 fb0655539d05
child 6451 bc943acc5fda
permissions -rw-r--r--
tidying
     1 (*  Title:      Sequents/ILL.ML
     2     ID:         $Id$
     3     Author:     Sara Kalvala and Valeria de Paiva
     4     Copyright   1992  University of Cambridge
     5 
     6 *)
     7 
     8 open ILL;
     9 
    10 
    11 val lazy_cs = empty_pack
    12  add_safes [tensl, conjr, disjl, promote0,
    13 	    context2,context3]
    14  add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr,
    15 	       impr, tensr, impl, derelict, weaken,
    16 		 promote1, promote2,context1,context4a,context4b];
    17 
    18 fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n);
    19 
    20 fun auto x = prove_goal thy x (fn prems => [best_tac lazy_cs 1]);
    21 
    22 val aux_impl = prove_goal thy "$F, $G |- A ==> $F, !(A -o B), $G |- B"
    23 (fn prems => [rtac derelict 1 THEN rtac impl 1 THEN rtac identity 2
    24 	THEN rtac context1 1 THEN rtac (hd(prems)) 1]);
    25 
    26 val conj_lemma =
    27 prove_goal thy " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
    28 (fn prems => [rtac contract 1,
    29 	res_inst_tac [("A","(!A) >< (!B)")] cut 1,
    30 	rtac tensr 2,
    31 	rtac (auto "! (A && B) |- !A") 3,
    32 	rtac (auto "! (A && B) |- !B") 3,
    33 	rtac context1 2,
    34 	rtac tensl 2,
    35 	rtac (hd(prems)) 2,
    36 	rtac context3 1,
    37 	rtac context3 1,
    38 	rtac context1 1]);
    39 
    40 val impr_contract =
    41 prove_goal thy "!A, !A, $G |- B ==> $G |- (!A) -o B"
    42 (fn prems => [rtac impr 1 THEN rtac contract 1
    43 		 THEN rtac (hd(prems)) 1]);
    44 
    45 
    46 val impr_contr_der =
    47 prove_goal thy "A, !A, $G |- B ==> $G |- (!A) -o B"
    48 (fn prems => [rtac impr 1 THEN rtac contract 1 THEN rtac derelict 1
    49 		 THEN rtac (hd(prems)) 1]);
    50 
    51 val contrad1 =
    52 prove_goal thy "$F, (!B) -o 0, $G, !B, $H |- A"
    53 (fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
    54 	  rtac zerol 1]);
    55 
    56 
    57 val contrad2 =
    58 prove_goal thy "$F, !B, $G, (!B) -o 0, $H |- A"
    59 (fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
    60 	  rtac zerol 1]);
    61 
    62 val ll_mp =
    63 prove_goal thy "A -o B, A |- B"
    64 (fn _ => [rtac impl 1 THEN rtac identity 2 THEN rtac identity 2
    65 	 THEN rtac context1 1]);
    66 
    67 val mp_rule1 =
    68 prove_goal thy "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
    69 (fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
    70 		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
    71 		rtac context1 1]);
    72 
    73 val mp_rule2 =
    74 prove_goal thy "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
    75 (fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
    76 		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
    77 		rtac context1 1]);
    78 
    79 val or_to_and =
    80 prove_goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
    81 (fn _ => [best_tac lazy_cs 1]);
    82 
    83 val o_a_rule =
    84 prove_goal thy "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
    85 \         $F, !((!(A ++ B)) -o 0), $G |- C"
    86 (fn prems => [rtac cut 1, rtac or_to_and 2, rtac (hd(prems)) 2,
    87 		rtac context3 1, rtac context1 1]);
    88 
    89 
    90 
    91 val conj_imp =
    92  prove_goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
    93 (fn _ => [rtac impr 1,rtac conj_lemma 1, rtac disjl 1,
    94 	  ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs)]);
    95 
    96 
    97 val not_imp = auto "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0";
    98 
    99 val a_not_a =
   100 prove_goal thy "!A -o (!A -o 0) |- !A -o 0"
   101      (fn _ => [rtac impr 1, rtac contract 1, rtac impl 1,
   102 	  rtac context1 1 THEN rtac identity 2, best_tac lazy_cs 1]);
   103 
   104 val a_not_a_rule =
   105 prove_goal thy "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
   106  (fn prems => [res_inst_tac [("A","!A -o 0")] cut 1,
   107                rtac a_not_a 2 THEN rtac (hd(prems)) 2
   108 		 THEN best_tac lazy_cs 1]);
   109 
   110 fun thm_to_rule x y =
   111 prove_goal thy x (fn prems => [rtac cut 1, rtac y 2, rtac (hd(prems)) 2,
   112 				best_tac lazy_cs 1]);
   113 
   114 val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
   115 			contrad2, mp_rule1, mp_rule2, o_a_rule,
   116 			a_not_a_rule]
   117 		add_unsafes [aux_impl];
   118 
   119 val power_cs = safe_cs add_unsafes [impr_contr_der];
   120 
   121 fun auto1 x = prove_goal thy x (fn prems => [best_tac safe_cs 1]) ;
   122 
   123 fun auto2 x = prove_goal thy x (fn prems => [best_tac power_cs 1]) ;
   124 
   125 
   126 (* some examples from Troelstra and van Dalen
   127 
   128 auto1  "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0";
   129 
   130 auto1  "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))";
   131 
   132 auto1  "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |- \
   133 \        (!A) -o ( (!  ((!B) -o 0)) -o 0)";
   134 
   135 
   136 auto2  "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |- \
   137 \         (!((! ((!A) -o B) ) -o 0)) -o 0";
   138 
   139 
   140                                                          *)