doc-src/Logics/FOL-eg.txt
author clasohm
Thu, 29 Jun 1995 12:28:27 +0200
changeset 1163 c080ff36d24e
parent 104 d8205bb279a7
child 5151 1e944fe5ce96
permissions -rw-r--r--
changed 'chol' labels to 'hol'; added a few parentheses
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
(**** FOL examples ****)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
Pretty.setmargin 72;  (*existing macros just allow this margin*)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
print_depth 0;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
(*** Intuitionistic examples ***)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
(*Quantifier example from Logic&Computation*)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
goal Int_Rule.thy "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
by (resolve_tac [impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
by (resolve_tac [allI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
by (resolve_tac [exI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
by (eresolve_tac [exE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
choplev 2;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
by (eresolve_tac [exE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
by (resolve_tac [exI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
by (eresolve_tac [allE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
by (assume_tac 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
(*Example of Dyckhoff's method*)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
goalw Int_Rule.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
by (resolve_tac [impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
by (eresolve_tac [disj_impE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
by (eresolve_tac [imp_impE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
by (eresolve_tac [imp_impE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
by (REPEAT (eresolve_tac [FalseE] 2));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
by (assume_tac 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
- goal Int_Rule.thy "(EX ay. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
- by (resolve_tac [impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
 1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
- by (resolve_tac [allI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
- by (resolve_tac [exI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
 1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
- by (eresolve_tac [exE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
Level 4
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
- choplev 2;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
- by (eresolve_tac [exE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
 1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
- by (resolve_tac [exI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
Level 4
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
- by (eresolve_tac [allE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
Level 5
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
 1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
- by (assume_tac 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
Level 6
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
> goalw Int_Rule.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
~ ~ ((P --> Q) | (Q --> P))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
 1. ((P --> Q) | (Q --> P) --> False) --> False
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
> by (resolve_tac [impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
~ ~ ((P --> Q) | (Q --> P))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
 1. (P --> Q) | (Q --> P) --> False ==> False
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
> by (eresolve_tac [disj_impE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
~ ~ ((P --> Q) | (Q --> P))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
 1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
> by (eresolve_tac [imp_impE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
~ ~ ((P --> Q) | (Q --> P))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
 1. [| (Q --> P) --> False; P; Q --> False |] ==> Q
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
 2. [| (Q --> P) --> False; False |] ==> False
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
> by (eresolve_tac [imp_impE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
Level 4
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
~ ~ ((P --> Q) | (Q --> P))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
 1. [| P; Q --> False; Q; P --> False |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
 2. [| P; Q --> False; False |] ==> Q
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
 3. [| (Q --> P) --> False; False |] ==> False
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
> by (REPEAT (eresolve_tac [FalseE] 2));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
Level 5
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
~ ~ ((P --> Q) | (Q --> P))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
 1. [| P; Q --> False; Q; P --> False |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
> by (assume_tac 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
Level 6
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
~ ~ ((P --> Q) | (Q --> P))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
(*** Classical examples ***)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
goal cla_thy "EX y. ALL x. P(y)-->P(x)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
by (resolve_tac [exCI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
by (resolve_tac [allI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
by (resolve_tac [impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
by (eresolve_tac [allE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
prth (allI RSN (2,swap));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
by (eresolve_tac [it] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
by (resolve_tac [impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
by (eresolve_tac [notE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
by (assume_tac 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
goal cla_thy "EX y. ALL x. P(y)-->P(x)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
by (best_tac FOL_dup_cs 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
- goal cla_thy "EX y. ALL x. P(y)-->P(x)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
 1. EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
- by (resolve_tac [exCI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
 1. ALL y. ~(ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
- by (resolve_tac [allI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
 1. !!x. ALL y. ~(ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
- by (resolve_tac [impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
 1. !!x. [| ALL y. ~(ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
- by (eresolve_tac [allE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
Level 4
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
 1. !!x. [| P(?a); ~(ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
- prth (allI RSN (2,swap));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
[| ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) |] ==> ?Q
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
- by (eresolve_tac [it] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
Level 5
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
 1. !!x xa. [| P(?a); ~P(x) |] ==> P(?y3(x)) --> P(xa)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
- by (resolve_tac [impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
Level 6
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
 1. !!x xa. [| P(?a); ~P(x); P(?y3(x)) |] ==> P(xa)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
- by (eresolve_tac [notE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
Level 7
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
- by (assume_tac 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
Level 8
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
- goal cla_thy "EX y. ALL x. P(y)-->P(x)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
 1. EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
- by (best_tac FOL_dup_cs 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
(**** finally, the example FOL/ex/if.ML ****)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
> val prems = goalw if_thy [if_def]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
#    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
if(P,Q,R)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
 1. P & Q | ~P & R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
> by (Classical.fast_tac (FOL_cs addIs prems) 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
if(P,Q,R)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
> val ifI = result();
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
> val major::prems = goalw if_thy [if_def]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
#    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
S
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
 1. S
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
> by (cut_facts_tac [major] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
S
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
 1. P & Q | ~P & R ==> S
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
> by (Classical.fast_tac (FOL_cs addIs prems) 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
S
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
> val ifE = result();
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
> goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
> by (resolve_tac [iffI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
> by (eresolve_tac [ifE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
 2. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
> by (eresolve_tac [ifE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
 2. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
 3. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
> by (resolve_tac [ifI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
Level 4
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
 1. [| P; Q; A; Q |] ==> if(P,A,C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
 2. [| P; Q; A; ~Q |] ==> if(P,B,D)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
 3. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
 4. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
> by (resolve_tac [ifI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
Level 5
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
 1. [| P; Q; A; Q; P |] ==> A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
 2. [| P; Q; A; Q; ~P |] ==> C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
 3. [| P; Q; A; ~Q |] ==> if(P,B,D)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
 4. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
 5. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
> choplev 0;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
> val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
> by (Classical.fast_tac if_cs 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
> val if_commute = result();
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
> by (Classical.fast_tac if_cs 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
> val nested_ifs = result();
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
> choplev 0;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
> by (rewrite_goals_tac [if_def]);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
    P & (Q & A | ~Q & B) | ~P & (R & A | ~R & B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
> by (Classical.fast_tac FOL_cs 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
> by (REPEAT (Classical.step_tac if_cs 1));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
 1. [| A; ~P; R; ~P; R |] ==> B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
 2. [| B; ~P; ~R; ~P; ~R |] ==> A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
 3. [| ~P; R; B; ~P; R |] ==> A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
 4. [| ~P; ~R; A; ~B; ~P |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
> choplev 0;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
> by (rewrite_goals_tac [if_def]);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
    P & (Q & A | ~Q & B) | ~P & (R & B | ~R & A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
> by (Classical.fast_tac FOL_cs 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
by: tactic failed
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
Exception- ERROR raised
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
Exception failure raised
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
> by (REPEAT (Classical.step_tac FOL_cs 1));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
 1. [| A; ~P; R; ~P; R; ~False |] ==> B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
 2. [| A; ~P; R; R; ~False; ~B; ~B |] ==> Q
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
 3. [| B; ~P; ~R; ~P; ~A |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
 4. [| B; ~P; ~R; ~Q; ~A |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
 5. [| B; ~R; ~P; ~A; ~R; Q; ~False |] ==> A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
 6. [| ~P; R; B; ~P; R; ~False |] ==> A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
 7. [| ~P; ~R; A; ~B; ~R |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
 8. [| ~P; ~R; A; ~B; ~R |] ==> Q