doc-src/ZF/FOL-eg.txt
changeset 14152 12f6f18e7afc
parent 14151 b8bb6a6a2c46
child 14153 76a6ba67bd15
     1.1 --- a/doc-src/ZF/FOL-eg.txt	Fri Aug 15 13:45:39 2003 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,245 +0,0 @@
     1.4 -(**** FOL examples ****)
     1.5 -
     1.6 -Pretty.setmargin 72;  (*existing macros just allow this margin*)
     1.7 -print_depth 0;
     1.8 -
     1.9 -(*** Intuitionistic examples ***)
    1.10 -
    1.11 -context IFOL.thy;
    1.12 -
    1.13 -(*Quantifier example from Logic&Computation*)
    1.14 -Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
    1.15 -by (resolve_tac [impI] 1);
    1.16 -by (resolve_tac [allI] 1);
    1.17 -by (resolve_tac [exI] 1);
    1.18 -by (eresolve_tac [exE] 1);
    1.19 -choplev 2;
    1.20 -by (eresolve_tac [exE] 1);
    1.21 -by (resolve_tac [exI] 1);
    1.22 -by (eresolve_tac [allE] 1);
    1.23 -by (assume_tac 1);
    1.24 -
    1.25 -
    1.26 -(*Example of Dyckhoff's method*)
    1.27 -Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
    1.28 -by (resolve_tac [impI] 1);
    1.29 -by (eresolve_tac [disj_impE] 1);
    1.30 -by (eresolve_tac [imp_impE] 1);
    1.31 -by (eresolve_tac [imp_impE] 1);
    1.32 -by (REPEAT (eresolve_tac [FalseE] 2));
    1.33 -by (assume_tac 1);
    1.34 -
    1.35 -
    1.36 -
    1.37 -
    1.38 -
    1.39 -(*** Classical examples ***)
    1.40 -
    1.41 -context FOL.thy;
    1.42 -
    1.43 -Goal "EX y. ALL x. P(y)-->P(x)";
    1.44 -by (resolve_tac [exCI] 1);
    1.45 -by (resolve_tac [allI] 1);
    1.46 -by (resolve_tac [impI] 1);
    1.47 -by (eresolve_tac [allE] 1);
    1.48 -prth (allI RSN (2,swap));
    1.49 -by (eresolve_tac [it] 1);
    1.50 -by (resolve_tac [impI] 1);
    1.51 -by (eresolve_tac [notE] 1);
    1.52 -by (assume_tac 1);
    1.53 -Goal "EX y. ALL x. P(y)-->P(x)";
    1.54 -by (Blast_tac 1);
    1.55 -
    1.56 -
    1.57 -
    1.58 -- Goal "EX y. ALL x. P(y)-->P(x)";
    1.59 -Level 0
    1.60 -EX y. ALL x. P(y) --> P(x)
    1.61 - 1. EX y. ALL x. P(y) --> P(x)
    1.62 -- by (resolve_tac [exCI] 1);
    1.63 -Level 1
    1.64 -EX y. ALL x. P(y) --> P(x)
    1.65 - 1. ALL y. ~(ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)
    1.66 -- by (resolve_tac [allI] 1);
    1.67 -Level 2
    1.68 -EX y. ALL x. P(y) --> P(x)
    1.69 - 1. !!x. ALL y. ~(ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)
    1.70 -- by (resolve_tac [impI] 1);
    1.71 -Level 3
    1.72 -EX y. ALL x. P(y) --> P(x)
    1.73 - 1. !!x. [| ALL y. ~(ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)
    1.74 -- by (eresolve_tac [allE] 1);
    1.75 -Level 4
    1.76 -EX y. ALL x. P(y) --> P(x)
    1.77 - 1. !!x. [| P(?a); ~(ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)
    1.78 -- prth (allI RSN (2,swap));
    1.79 -[| ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) |] ==> ?Q
    1.80 -- by (eresolve_tac [it] 1);
    1.81 -Level 5
    1.82 -EX y. ALL x. P(y) --> P(x)
    1.83 - 1. !!x xa. [| P(?a); ~P(x) |] ==> P(?y3(x)) --> P(xa)
    1.84 -- by (resolve_tac [impI] 1);
    1.85 -Level 6
    1.86 -EX y. ALL x. P(y) --> P(x)
    1.87 - 1. !!x xa. [| P(?a); ~P(x); P(?y3(x)) |] ==> P(xa)
    1.88 -- by (eresolve_tac [notE] 1);
    1.89 -Level 7
    1.90 -EX y. ALL x. P(y) --> P(x)
    1.91 - 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)
    1.92 -- by (assume_tac 1);
    1.93 -Level 8
    1.94 -EX y. ALL x. P(y) --> P(x)
    1.95 -No subgoals!
    1.96 -- Goal "EX y. ALL x. P(y)-->P(x)";
    1.97 -Level 0
    1.98 -EX y. ALL x. P(y) --> P(x)
    1.99 - 1. EX y. ALL x. P(y) --> P(x)
   1.100 -- by (best_tac FOL_dup_cs 1);
   1.101 -Level 1
   1.102 -EX y. ALL x. P(y) --> P(x)
   1.103 -No subgoals!
   1.104 -
   1.105 -
   1.106 -(**** finally, the example FOL/ex/if.ML ****)
   1.107 -
   1.108 -> val prems = goalw if_thy [if_def]
   1.109 -#    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
   1.110 -Level 0
   1.111 -if(P,Q,R)
   1.112 - 1. P & Q | ~P & R
   1.113 -> by (Classical.fast_tac (FOL_cs addIs prems) 1);
   1.114 -Level 1
   1.115 -if(P,Q,R)
   1.116 -No subgoals!
   1.117 -> val ifI = result();
   1.118 -
   1.119 -
   1.120 -> val major::prems = goalw if_thy [if_def]
   1.121 -#    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
   1.122 -Level 0
   1.123 -S
   1.124 - 1. S
   1.125 -> by (cut_facts_tac [major] 1);
   1.126 -Level 1
   1.127 -S
   1.128 - 1. P & Q | ~P & R ==> S
   1.129 -> by (Classical.fast_tac (FOL_cs addIs prems) 1);
   1.130 -Level 2
   1.131 -S
   1.132 -No subgoals!
   1.133 -> val ifE = result();
   1.134 -
   1.135 -> goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
   1.136 -Level 0
   1.137 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.138 - 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.139 -> by (resolve_tac [iffI] 1);
   1.140 -Level 1
   1.141 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.142 - 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))
   1.143 - 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.144 -> by (eresolve_tac [ifE] 1);
   1.145 -Level 2
   1.146 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.147 - 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.148 - 2. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.149 - 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.150 -> by (eresolve_tac [ifE] 1);
   1.151 -Level 3
   1.152 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.153 - 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.154 - 2. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.155 - 3. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.156 - 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.157 -> by (resolve_tac [ifI] 1);
   1.158 -Level 4
   1.159 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.160 - 1. [| P; Q; A; Q |] ==> if(P,A,C)
   1.161 - 2. [| P; Q; A; ~Q |] ==> if(P,B,D)
   1.162 - 3. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.163 - 4. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.164 - 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.165 -> by (resolve_tac [ifI] 1);
   1.166 -Level 5
   1.167 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.168 - 1. [| P; Q; A; Q; P |] ==> A
   1.169 - 2. [| P; Q; A; Q; ~P |] ==> C
   1.170 - 3. [| P; Q; A; ~Q |] ==> if(P,B,D)
   1.171 - 4. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.172 - 5. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.173 - 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.174 -
   1.175 -> choplev 0;
   1.176 -Level 0
   1.177 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.178 - 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.179 -> val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
   1.180 -> by (Classical.fast_tac if_cs 1);
   1.181 -Level 1
   1.182 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.183 -No subgoals!
   1.184 -> val if_commute = result();
   1.185 -
   1.186 -> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
   1.187 -Level 0
   1.188 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.189 - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.190 -> by (Classical.fast_tac if_cs 1);
   1.191 -Level 1
   1.192 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.193 -No subgoals!
   1.194 -> val nested_ifs = result();
   1.195 -
   1.196 -
   1.197 -> choplev 0;
   1.198 -Level 0
   1.199 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.200 - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.201 -> by (rewrite_goals_tac [if_def]);
   1.202 -Level 1
   1.203 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.204 - 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
   1.205 -    P & (Q & A | ~Q & B) | ~P & (R & A | ~R & B)
   1.206 -> by (Classical.fast_tac FOL_cs 1);
   1.207 -Level 2
   1.208 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.209 -No subgoals!
   1.210 -
   1.211 -
   1.212 -> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
   1.213 -Level 0
   1.214 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.215 - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.216 -> by (REPEAT (Classical.step_tac if_cs 1));
   1.217 -Level 1
   1.218 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.219 - 1. [| A; ~P; R; ~P; R |] ==> B
   1.220 - 2. [| B; ~P; ~R; ~P; ~R |] ==> A
   1.221 - 3. [| ~P; R; B; ~P; R |] ==> A
   1.222 - 4. [| ~P; ~R; A; ~B; ~P |] ==> R
   1.223 -
   1.224 -> choplev 0;
   1.225 -Level 0
   1.226 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.227 - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.228 -> by (rewrite_goals_tac [if_def]);
   1.229 -Level 1
   1.230 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.231 - 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
   1.232 -    P & (Q & A | ~Q & B) | ~P & (R & B | ~R & A)
   1.233 -> by (Classical.fast_tac FOL_cs 1);
   1.234 -by: tactic failed
   1.235 -Exception- ERROR raised
   1.236 -Exception failure raised
   1.237 -
   1.238 -> by (REPEAT (Classical.step_tac FOL_cs 1));
   1.239 -Level 2
   1.240 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.241 - 1. [| A; ~P; R; ~P; R; ~False |] ==> B
   1.242 - 2. [| A; ~P; R; R; ~False; ~B; ~B |] ==> Q
   1.243 - 3. [| B; ~P; ~R; ~P; ~A |] ==> R
   1.244 - 4. [| B; ~P; ~R; ~Q; ~A |] ==> R
   1.245 - 5. [| B; ~R; ~P; ~A; ~R; Q; ~False |] ==> A
   1.246 - 6. [| ~P; R; B; ~P; R; ~False |] ==> A
   1.247 - 7. [| ~P; ~R; A; ~B; ~R |] ==> P
   1.248 - 8. [| ~P; ~R; A; ~B; ~R |] ==> Q