Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/ZF/FOL-eg.txt
changeset 6121 5fe77b9b5185 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/FOL-eg.txt	Wed Jan 13 16:36:36 1999 +0100
@@ -0,0 +1,245 @@
+(**** FOL examples ****)
+
+Pretty.setmargin 72;  (*existing macros just allow this margin*)
+print_depth 0;
+
+(*** Intuitionistic examples ***)
+
+context IFOL.thy;
+
+(*Quantifier example from Logic&Computation*)
+Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
+by (resolve_tac [impI] 1);
+by (resolve_tac [allI] 1);
+by (resolve_tac [exI] 1);
+by (eresolve_tac [exE] 1);
+choplev 2;
+by (eresolve_tac [exE] 1);
+by (resolve_tac [exI] 1);
+by (eresolve_tac [allE] 1);
+by (assume_tac 1);
+
+
+(*Example of Dyckhoff's method*)
+Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
+by (resolve_tac [impI] 1);
+by (eresolve_tac [disj_impE] 1);
+by (eresolve_tac [imp_impE] 1);
+by (eresolve_tac [imp_impE] 1);
+by (REPEAT (eresolve_tac [FalseE] 2));
+by (assume_tac 1);
+
+
+
+
+
+(*** Classical examples ***)
+
+context FOL.thy;
+
+Goal "EX y. ALL x. P(y)-->P(x)";
+by (resolve_tac [exCI] 1);
+by (resolve_tac [allI] 1);
+by (resolve_tac [impI] 1);
+by (eresolve_tac [allE] 1);
+prth (allI RSN (2,swap));
+by (eresolve_tac [it] 1);
+by (resolve_tac [impI] 1);
+by (eresolve_tac [notE] 1);
+by (assume_tac 1);
+Goal "EX y. ALL x. P(y)-->P(x)";
+by (Blast_tac 1);
+
+
+
+- Goal "EX y. ALL x. P(y)-->P(x)";
+Level 0
+EX y. ALL x. P(y) --> P(x)
+ 1. EX y. ALL x. P(y) --> P(x)
+- by (resolve_tac [exCI] 1);
+Level 1
+EX y. ALL x. P(y) --> P(x)
+ 1. ALL y. ~(ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)
+- by (resolve_tac [allI] 1);
+Level 2
+EX y. ALL x. P(y) --> P(x)
+ 1. !!x. ALL y. ~(ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)
+- by (resolve_tac [impI] 1);
+Level 3
+EX y. ALL x. P(y) --> P(x)
+ 1. !!x. [| ALL y. ~(ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)
+- by (eresolve_tac [allE] 1);
+Level 4
+EX y. ALL x. P(y) --> P(x)
+ 1. !!x. [| P(?a); ~(ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)
+- prth (allI RSN (2,swap));
+[| ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) |] ==> ?Q
+- by (eresolve_tac [it] 1);
+Level 5
+EX y. ALL x. P(y) --> P(x)
+ 1. !!x xa. [| P(?a); ~P(x) |] ==> P(?y3(x)) --> P(xa)
+- by (resolve_tac [impI] 1);
+Level 6
+EX y. ALL x. P(y) --> P(x)
+ 1. !!x xa. [| P(?a); ~P(x); P(?y3(x)) |] ==> P(xa)
+- by (eresolve_tac [notE] 1);
+Level 7
+EX y. ALL x. P(y) --> P(x)
+ 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)
+- by (assume_tac 1);
+Level 8
+EX y. ALL x. P(y) --> P(x)
+No subgoals!
+- Goal "EX y. ALL x. P(y)-->P(x)";
+Level 0
+EX y. ALL x. P(y) --> P(x)
+ 1. EX y. ALL x. P(y) --> P(x)
+- by (best_tac FOL_dup_cs 1);
+Level 1
+EX y. ALL x. P(y) --> P(x)
+No subgoals!
+
+
+(**** finally, the example FOL/ex/if.ML ****)
+
+> val prems = goalw if_thy [if_def]
+#    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
+Level 0
+if(P,Q,R)
+ 1. P & Q | ~P & R
+> by (Classical.fast_tac (FOL_cs addIs prems) 1);
+Level 1
+if(P,Q,R)
+No subgoals!
+> val ifI = result();
+
+
+> val major::prems = goalw if_thy [if_def]
+#    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
+Level 0
+S
+ 1. S
+> by (cut_facts_tac [major] 1);
+Level 1
+S
+ 1. P & Q | ~P & R ==> S
+> by (Classical.fast_tac (FOL_cs addIs prems) 1);
+Level 2
+S
+No subgoals!
+> val ifE = result();
+
+> goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
+Level 0
+if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+ 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+> by (resolve_tac [iffI] 1);
+Level 1
+if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+ 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))
+ 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
+> by (eresolve_tac [ifE] 1);
+Level 2
+if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+ 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))
+ 2. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
+ 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
+> by (eresolve_tac [ifE] 1);
+Level 3
+if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+ 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))
+ 2. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
+ 3. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
+ 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
+> by (resolve_tac [ifI] 1);
+Level 4
+if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+ 1. [| P; Q; A; Q |] ==> if(P,A,C)
+ 2. [| P; Q; A; ~Q |] ==> if(P,B,D)
+ 3. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
+ 4. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
+ 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
+> by (resolve_tac [ifI] 1);
+Level 5
+if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+ 1. [| P; Q; A; Q; P |] ==> A
+ 2. [| P; Q; A; Q; ~P |] ==> C
+ 3. [| P; Q; A; ~Q |] ==> if(P,B,D)
+ 4. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
+ 5. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
+ 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
+
+> choplev 0;
+Level 0
+if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+ 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+> val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
+> by (Classical.fast_tac if_cs 1);
+Level 1
+if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
+No subgoals!
+> val if_commute = result();
+
+> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
+Level 0
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
+ 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
+> by (Classical.fast_tac if_cs 1);
+Level 1
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
+No subgoals!
+> val nested_ifs = result();
+
+
+> choplev 0;
+Level 0
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
+ 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
+> by (rewrite_goals_tac [if_def]);
+Level 1
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
+ 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
+    P & (Q & A | ~Q & B) | ~P & (R & A | ~R & B)
+> by (Classical.fast_tac FOL_cs 1);
+Level 2
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
+No subgoals!
+
+
+> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
+Level 0
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
+ 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
+> by (REPEAT (Classical.step_tac if_cs 1));
+Level 1
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
+ 1. [| A; ~P; R; ~P; R |] ==> B
+ 2. [| B; ~P; ~R; ~P; ~R |] ==> A
+ 3. [| ~P; R; B; ~P; R |] ==> A
+ 4. [| ~P; ~R; A; ~B; ~P |] ==> R
+
+> choplev 0;
+Level 0
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
+ 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
+> by (rewrite_goals_tac [if_def]);
+Level 1
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
+ 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
+    P & (Q & A | ~Q & B) | ~P & (R & B | ~R & A)
+> by (Classical.fast_tac FOL_cs 1);
+by: tactic failed
+Exception- ERROR raised
+Exception failure raised
+
+> by (REPEAT (Classical.step_tac FOL_cs 1));
+Level 2
+if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
+ 1. [| A; ~P; R; ~P; R; ~False |] ==> B
+ 2. [| A; ~P; R; R; ~False; ~B; ~B |] ==> Q
+ 3. [| B; ~P; ~R; ~P; ~A |] ==> R
+ 4. [| B; ~P; ~R; ~Q; ~A |] ==> R
+ 5. [| B; ~R; ~P; ~A; ~R; Q; ~False |] ==> A
+ 6. [| ~P; R; B; ~P; R; ~False |] ==> A
+ 7. [| ~P; ~R; A; ~B; ~R |] ==> P
+ 8. [| ~P; ~R; A; ~B; ~R |] ==> Q
isabelle