src/Sequents/ILL/ILL_kleene_lemmas.ML
author wenzelm
Sun, 18 Sep 2005 15:20:08 +0200
changeset 17481 75166ebb619b
parent 6252 935f183bf406
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     1
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     2
(* from [kleene 52] pp 118,119 *)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     3
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     4
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     5
val k49a = auto1 "|- [* A > ( - ( - A)) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     6
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     7
val k49b = auto1 "|- [*( - ( - ( - A))) = ( - A)*]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     8
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     9
val k49c = auto1 "|- [* (A | - A) > ( - - A = A) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    10
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    11
val k50a = auto2 "|- [* - (A = - A) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    12
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    13
(*
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    14
         [rtac impr_contract 1 THEN REPEAT (rtac conj_lemma 1),
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    15
	  res_inst_tac [("A","!((! A) -o 0)")] cut 1
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    16
	  THEN rtac context1 1
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    17
	  THEN ALLGOALS (best_tac power_cs)]);
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    18
*)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    19
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    20
val k51a = auto2 "|- [* - - (A | - A) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    21
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    22
val k51b = auto2 "|- [* - - (- - A > A) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    23
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    24
val k56a = auto1 "|- [* (A | B) > - (- A & - B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    25
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    26
val k56b = auto1 "|- [* (-A | B) > - (A & -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    27
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    28
val k57a = auto1 "|- [* (A & B) > - (-A | -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    29
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    30
val k57b = auto2 "|- [* (A & -B) > -(-A | B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    31
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    32
val k58a = auto1 "|- [* (A > B) > - (A & -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    33
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    34
val k58b = auto1 "|- [* (A > -B) = -(A & B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    35
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    36
val k58c = auto1 "|- [* - (A & B) = (- - A > - B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    37
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    38
val k58d = auto1 "|- [* (- - A > - B) = - - (-A | -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    39
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    40
val k58e = auto1 "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    41
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    42
val k58f = auto1 "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    43
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    44
val k58g = auto1 "|- [* (- -A > B) > - (A & -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    45
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    46
val k59a = auto1 "|- [* (-A | B) > (A > B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    47
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    48
val k59b = auto2 "|- [* (A > B) > - - (-A | B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    49
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    50
val k59c = auto2 "|- [* (-A > B) > - -(A | B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    51
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    52
val k60a = auto1 "|- [* (A & B) > - (A > -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    53
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    54
val k60b = auto1 "|- [* (A & -B) > - (A > B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    55
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    56
val k60c = auto1 "|- [* ( - - A & B) > - (A > -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    57
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    58
val k60d = auto1 "|- [* (- - A & - B) = - (A > B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    59
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    60
val k60e = auto1 "|- [* - (A > B) = - (-A | B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    61
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    62
val k60f = auto1 "|- [* - (-A | B) = - - (A & -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    63
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    64
val k60g = auto2 "|- [* - - (A > B) = - (A & -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    65
    
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    66
(*
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    67
 [step_tac safe_cs 1, best_tac safe_cs 1,
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    68
 rtac impr 1 THEN rtac impr_contract 1
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    69
 THEN best_tac safe_cs 1];
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    70
*)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    71
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    72
val k60h = auto1 "|- [* - (A & -B) = (A > - -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    73
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    74
val k60i = auto1 "|- [* (A > - -B) = (- -A > - -B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    75
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    76
val k61a = auto1 "|- [* (A | B) > (-A > B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    77
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    78
val k61b = auto2 "|- [* - (A | B) = - (-A > B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    79
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    80
val k62a = auto1 "|- [* (-A | -B) > - (A & B) *]";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    81