src/Sequents/ILL.ML
author kleing
Sat, 30 Apr 2005 14:18:36 +0200
changeset 15900 d6156cb8dc2e
parent 9259 103acc345f75
child 17481 75166ebb619b
permissions -rw-r--r--
fixed typo
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     1
(*  Title:      Sequents/ILL.ML
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     2
    ID:         $Id$
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     3
    Author:     Sara Kalvala and Valeria de Paiva
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     5
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     6
*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     7
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     8
val lazy_cs = empty_pack
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     9
 add_safes [tensl, conjr, disjl, promote0,
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    10
	    context2,context3]
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    11
 add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr,
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    12
	       impr, tensr, impl, derelict, weaken,
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    13
		 promote1, promote2,context1,context4a,context4b];
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    14
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    15
fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n);
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    16
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    17
fun auto x = prove_goal thy x (fn prems => [best_tac lazy_cs 1]);
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    18
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    19
Goal "$F, $G |- A ==> $F, !(A -o B), $G |- B";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    20
by (rtac derelict 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    21
by (rtac impl 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    22
by (rtac identity 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    23
by (rtac context1 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    24
by (assume_tac 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    25
qed "aux_impl";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    26
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    27
Goal " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    28
by (rtac contract 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    29
by (res_inst_tac [("A","(!A) >< (!B)")] cut 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    30
by (rtac tensr 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    31
by (rtac (auto "! (A && B) |- !A") 3);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    32
by (rtac (auto "! (A && B) |- !B") 3);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    33
by (rtac context1 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    34
by (rtac tensl 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    35
by (assume_tac 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    36
by (rtac context3 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    37
by (rtac context3 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    38
by (rtac context1 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    39
qed "conj_lemma";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    40
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    41
Goal "!A, !A, $G |- B ==> $G |- (!A) -o B";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    42
by (rtac impr 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    43
by (rtac contract 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    44
by (assume_tac 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    45
qed "impr_contract";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    46
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    47
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    48
Goal "A, !A, $G |- B ==> $G |- (!A) -o B";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    49
by (rtac impr 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    50
by (rtac contract 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    51
by (rtac derelict 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    52
by (assume_tac 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    53
qed "impr_contr_der";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    54
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    55
val _ = goal thy "$F, (!B) -o 0, $G, !B, $H |- A";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    56
by (rtac impl 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    57
by (rtac identity 3);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    58
by (rtac context3 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    59
by (rtac context1 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    60
by (rtac zerol 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    61
qed "contrad1";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    62
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    63
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    64
val _ = goal thy "$F, !B, $G, (!B) -o 0, $H |- A";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    65
by (rtac impl 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    66
by (rtac identity 3);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    67
by (rtac context3 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    68
by (rtac context1 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    69
by (rtac zerol 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    70
qed "contrad2";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    71
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    72
val _ = goal thy "A -o B, A |- B";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    73
by (rtac impl 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    74
by (rtac identity 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    75
by (rtac identity 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    76
by (rtac context1 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    77
qed "ll_mp";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    78
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    79
Goal "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    80
by (res_inst_tac [("A","B")] cut 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    81
by (rtac ll_mp 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    82
by (assume_tac 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    83
by (rtac context3 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    84
by (rtac context3 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    85
by (rtac context1 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    86
qed "mp_rule1";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    87
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    88
Goal "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    89
by (res_inst_tac [("A","B")] cut 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    90
by (rtac ll_mp 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    91
by (assume_tac 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    92
by (rtac context3 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    93
by (rtac context3 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    94
by (rtac context1 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    95
qed "mp_rule2";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    96
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    97
val _ = goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    98
by (best_tac lazy_cs 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
    99
qed "or_to_and";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   100
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   101
Goal "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   102
\         $F, !((!(A ++ B)) -o 0), $G |- C";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   103
by (rtac cut 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   104
by (rtac or_to_and 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   105
by (assume_tac 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   106
by (rtac context3 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   107
by (rtac context1 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   108
qed "o_a_rule";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   109
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   110
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   111
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   112
val _ = goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   113
by (rtac impr 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   114
by (rtac conj_lemma 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   115
by (rtac disjl 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   116
by (ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs));
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   117
qed "conj_imp";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   118
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   119
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   120
val not_imp = auto "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   121
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   122
Goal "!A -o (!A -o 0) |- !A -o 0";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   123
by (rtac impr 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   124
by (rtac contract 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   125
by (rtac impl 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   126
by (rtac identity 3);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   127
by (rtac context1 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   128
by (best_tac lazy_cs 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   129
qed "a_not_a";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   130
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   131
Goal "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B";
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   132
by (res_inst_tac [("A","!A -o 0")] cut 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   133
by (rtac a_not_a 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   134
by (assume_tac 2);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   135
by (best_tac lazy_cs 1);
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   136
qed "a_not_a_rule";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   137
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   138
fun thm_to_rule x y =
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   139
    prove_goal thy x
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   140
      (fn [prem] => [(rtac cut 1), (rtac y 2), (rtac prem 2),
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   141
	 	     (best_tac lazy_cs 1)]);
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   142
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   143
val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
9259
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   144
				 contrad2, mp_rule1, mp_rule2, o_a_rule,
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   145
				 a_not_a_rule]
103acc345f75 removal of batch style, and tidying
paulson
parents: 6451
diff changeset
   146
		      add_unsafes [aux_impl];
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   147
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   148
val power_cs = safe_cs add_unsafes [impr_contr_der];
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   149
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   150
fun auto1 x = prove_goal thy x (fn prems => [best_tac safe_cs 1]) ;
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   151
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   152
fun auto2 x = prove_goal thy x (fn prems => [best_tac power_cs 1]) ;
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   153
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   154
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   155
(* some examples from Troelstra and van Dalen
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   156
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   157
auto1  "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   158
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   159
auto1  "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   160
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   161
auto1  "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |- \
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   162
\        (!A) -o ( (!  ((!B) -o 0)) -o 0)";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   163
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   164
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   165
auto2  "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |- \
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   166
\         (!((! ((!A) -o B) ) -o 0)) -o 0";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   167
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   168
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   169
                                                         *)