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