Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/Logics/FOL-eg.txt
author lcp
Mon, 21 Nov 1994 10:51:40 +0100
changeset 718 efca1e0710fb
parent 104 d8205bb279a7
child 5151 1e944fe5ce96
permissions -rw-r--r--
page 157 erratum 
     1 (**** FOL examples ****)

     2 

     3 Pretty.setmargin 72;  (*existing macros just allow this margin*)

     4 print_depth 0;

     5 

     6 (*** Intuitionistic examples ***)

     7 

     8 (*Quantifier example from Logic&Computation*)

     9 goal Int_Rule.thy "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";

    10 by (resolve_tac [impI] 1);

    11 by (resolve_tac [allI] 1);

    12 by (resolve_tac [exI] 1);

    13 by (eresolve_tac [exE] 1);

    14 choplev 2;

    15 by (eresolve_tac [exE] 1);

    16 by (resolve_tac [exI] 1);

    17 by (eresolve_tac [allE] 1);

    18 by (assume_tac 1);

    19 

    20 

    21 (*Example of Dyckhoff's method*)

    22 goalw Int_Rule.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))";

    23 by (resolve_tac [impI] 1);

    24 by (eresolve_tac [disj_impE] 1);

    25 by (eresolve_tac [imp_impE] 1);

    26 by (eresolve_tac [imp_impE] 1);

    27 by (REPEAT (eresolve_tac [FalseE] 2));

    28 by (assume_tac 1);

    29 

    30 

    31 

    32 - goal Int_Rule.thy "(EX ay. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";

    33 Level 0

    34 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    35  1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    36 - by (resolve_tac [impI] 1);

    37 Level 1

    38 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    39  1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)

    40 - by (resolve_tac [allI] 1);

    41 Level 2

    42 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    43  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)

    44 - by (resolve_tac [exI] 1);

    45 Level 3

    46 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    47  1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))

    48 - by (eresolve_tac [exE] 1);

    49 Level 4

    50 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    51  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))

    52 - choplev 2;

    53 Level 2

    54 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    55  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)

    56 - by (eresolve_tac [exE] 1);

    57 Level 3

    58 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    59  1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)

    60 - by (resolve_tac [exI] 1);

    61 Level 4

    62 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    63  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))

    64 - by (eresolve_tac [allE] 1);

    65 Level 5

    66 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    67  1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))

    68 - by (assume_tac 1);

    69 Level 6

    70 (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))

    71 No subgoals!

    72 

    73 

    74 

    75 > goalw Int_Rule.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))";

    76 Level 0

    77 ~ ~ ((P --> Q) | (Q --> P))

    78  1. ((P --> Q) | (Q --> P) --> False) --> False

    79 > by (resolve_tac [impI] 1);

    80 Level 1

    81 ~ ~ ((P --> Q) | (Q --> P))

    82  1. (P --> Q) | (Q --> P) --> False ==> False

    83 > by (eresolve_tac [disj_impE] 1);

    84 Level 2

    85 ~ ~ ((P --> Q) | (Q --> P))

    86  1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False

    87 > by (eresolve_tac [imp_impE] 1);

    88 Level 3

    89 ~ ~ ((P --> Q) | (Q --> P))

    90  1. [| (Q --> P) --> False; P; Q --> False |] ==> Q

    91  2. [| (Q --> P) --> False; False |] ==> False

    92 > by (eresolve_tac [imp_impE] 1);

    93 Level 4

    94 ~ ~ ((P --> Q) | (Q --> P))

    95  1. [| P; Q --> False; Q; P --> False |] ==> P

    96  2. [| P; Q --> False; False |] ==> Q

    97  3. [| (Q --> P) --> False; False |] ==> False

    98 > by (REPEAT (eresolve_tac [FalseE] 2));

    99 Level 5

   100 ~ ~ ((P --> Q) | (Q --> P))

   101  1. [| P; Q --> False; Q; P --> False |] ==> P

   102 > by (assume_tac 1);

   103 Level 6

   104 ~ ~ ((P --> Q) | (Q --> P))

   105 No subgoals!

   106 

   107 

   108 

   109 

   110 (*** Classical examples ***)

   111 

   112 goal cla_thy "EX y. ALL x. P(y)-->P(x)";

   113 by (resolve_tac [exCI] 1);

   114 by (resolve_tac [allI] 1);

   115 by (resolve_tac [impI] 1);

   116 by (eresolve_tac [allE] 1);

   117 prth (allI RSN (2,swap));

   118 by (eresolve_tac [it] 1);

   119 by (resolve_tac [impI] 1);

   120 by (eresolve_tac [notE] 1);

   121 by (assume_tac 1);

   122 goal cla_thy "EX y. ALL x. P(y)-->P(x)";

   123 by (best_tac FOL_dup_cs 1);

   124 

   125 

   126 

   127 - goal cla_thy "EX y. ALL x. P(y)-->P(x)";

   128 Level 0

   129 EX y. ALL x. P(y) --> P(x)

   130  1. EX y. ALL x. P(y) --> P(x)

   131 - by (resolve_tac [exCI] 1);

   132 Level 1

   133 EX y. ALL x. P(y) --> P(x)

   134  1. ALL y. ~(ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)

   135 - by (resolve_tac [allI] 1);

   136 Level 2

   137 EX y. ALL x. P(y) --> P(x)

   138  1. !!x. ALL y. ~(ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)

   139 - by (resolve_tac [impI] 1);

   140 Level 3

   141 EX y. ALL x. P(y) --> P(x)

   142  1. !!x. [| ALL y. ~(ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)

   143 - by (eresolve_tac [allE] 1);

   144 Level 4

   145 EX y. ALL x. P(y) --> P(x)

   146  1. !!x. [| P(?a); ~(ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)

   147 - prth (allI RSN (2,swap));

   148 [| ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) |] ==> ?Q

   149 - by (eresolve_tac [it] 1);

   150 Level 5

   151 EX y. ALL x. P(y) --> P(x)

   152  1. !!x xa. [| P(?a); ~P(x) |] ==> P(?y3(x)) --> P(xa)

   153 - by (resolve_tac [impI] 1);

   154 Level 6

   155 EX y. ALL x. P(y) --> P(x)

   156  1. !!x xa. [| P(?a); ~P(x); P(?y3(x)) |] ==> P(xa)

   157 - by (eresolve_tac [notE] 1);

   158 Level 7

   159 EX y. ALL x. P(y) --> P(x)

   160  1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)

   161 - by (assume_tac 1);

   162 Level 8

   163 EX y. ALL x. P(y) --> P(x)

   164 No subgoals!

   165 - goal cla_thy "EX y. ALL x. P(y)-->P(x)";

   166 Level 0

   167 EX y. ALL x. P(y) --> P(x)

   168  1. EX y. ALL x. P(y) --> P(x)

   169 - by (best_tac FOL_dup_cs 1);

   170 Level 1

   171 EX y. ALL x. P(y) --> P(x)

   172 No subgoals!

   173 

   174 

   175 (**** finally, the example FOL/ex/if.ML ****)

   176 

   177 > val prems = goalw if_thy [if_def]

   178 #    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";

   179 Level 0

   180 if(P,Q,R)

   181  1. P & Q | ~P & R

   182 > by (Classical.fast_tac (FOL_cs addIs prems) 1);

   183 Level 1

   184 if(P,Q,R)

   185 No subgoals!

   186 > val ifI = result();

   187 

   188 

   189 > val major::prems = goalw if_thy [if_def]

   190 #    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";

   191 Level 0

   192 S

   193  1. S

   194 > by (cut_facts_tac [major] 1);

   195 Level 1

   196 S

   197  1. P & Q | ~P & R ==> S

   198 > by (Classical.fast_tac (FOL_cs addIs prems) 1);

   199 Level 2

   200 S

   201 No subgoals!

   202 > val ifE = result();

   203 

   204 > goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";

   205 Level 0

   206 if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   207  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   208 > by (resolve_tac [iffI] 1);

   209 Level 1

   210 if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   211  1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))

   212  2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))

   213 > by (eresolve_tac [ifE] 1);

   214 Level 2

   215 if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   216  1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))

   217  2. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))

   218  3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))

   219 > by (eresolve_tac [ifE] 1);

   220 Level 3

   221 if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   222  1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))

   223  2. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))

   224  3. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))

   225  4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))

   226 > by (resolve_tac [ifI] 1);

   227 Level 4

   228 if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   229  1. [| P; Q; A; Q |] ==> if(P,A,C)

   230  2. [| P; Q; A; ~Q |] ==> if(P,B,D)

   231  3. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))

   232  4. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))

   233  5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))

   234 > by (resolve_tac [ifI] 1);

   235 Level 5

   236 if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   237  1. [| P; Q; A; Q; P |] ==> A

   238  2. [| P; Q; A; Q; ~P |] ==> C

   239  3. [| P; Q; A; ~Q |] ==> if(P,B,D)

   240  4. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))

   241  5. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))

   242  6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))

   243 

   244 > choplev 0;

   245 Level 0

   246 if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   247  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   248 > val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];

   249 > by (Classical.fast_tac if_cs 1);

   250 Level 1

   251 if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))

   252 No subgoals!

   253 > val if_commute = result();

   254 

   255 > goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";

   256 Level 0

   257 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))

   258  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))

   259 > by (Classical.fast_tac if_cs 1);

   260 Level 1

   261 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))

   262 No subgoals!

   263 > val nested_ifs = result();

   264 

   265 

   266 > choplev 0;

   267 Level 0

   268 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))

   269  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))

   270 > by (rewrite_goals_tac [if_def]);

   271 Level 1

   272 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))

   273  1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->

   274     P & (Q & A | ~Q & B) | ~P & (R & A | ~R & B)

   275 > by (Classical.fast_tac FOL_cs 1);

   276 Level 2

   277 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))

   278 No subgoals!

   279 

   280 

   281 > goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";

   282 Level 0

   283 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))

   284  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))

   285 > by (REPEAT (Classical.step_tac if_cs 1));

   286 Level 1

   287 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))

   288  1. [| A; ~P; R; ~P; R |] ==> B

   289  2. [| B; ~P; ~R; ~P; ~R |] ==> A

   290  3. [| ~P; R; B; ~P; R |] ==> A

   291  4. [| ~P; ~R; A; ~B; ~P |] ==> R

   292 

   293 > choplev 0;

   294 Level 0

   295 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))

   296  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))

   297 > by (rewrite_goals_tac [if_def]);

   298 Level 1

   299 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))

   300  1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->

   301     P & (Q & A | ~Q & B) | ~P & (R & B | ~R & A)

   302 > by (Classical.fast_tac FOL_cs 1);

   303 by: tactic failed

   304 Exception- ERROR raised

   305 Exception failure raised

   306 

   307 > by (REPEAT (Classical.step_tac FOL_cs 1));

   308 Level 2

   309 if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))

   310  1. [| A; ~P; R; ~P; R; ~False |] ==> B

   311  2. [| A; ~P; R; R; ~False; ~B; ~B |] ==> Q

   312  3. [| B; ~P; ~R; ~P; ~A |] ==> R

   313  4. [| B; ~P; ~R; ~Q; ~A |] ==> R

   314  5. [| B; ~R; ~P; ~A; ~R; Q; ~False |] ==> A

   315  6. [| ~P; R; B; ~P; R; ~False |] ==> A

   316  7. [| ~P; ~R; A; ~B; ~R |] ==> P

   317  8. [| ~P; ~R; A; ~B; ~R |] ==> Q
wneuper/isa