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/Intro/quant.txt
changeset 105 216d6ed87399 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Intro/quant.txt	Wed Nov 10 05:06:55 1993 +0100
@@ -0,0 +1,244 @@
+(**** quantifier examples -- process using Doc/tout quant.txt  ****)
+
+Pretty.setmargin 72;  (*existing macros just allow this margin*)
+print_depth 0;
+
+
+goal Int_Rule.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
+by (resolve_tac [impI] 1);
+by (dresolve_tac [spec] 1);
+by (resolve_tac [allI] 1);
+by (dresolve_tac [spec] 1);
+by (resolve_tac [allI] 1);
+by (assume_tac 1);
+choplev 1;
+by (resolve_tac [allI] 1);
+by (resolve_tac [allI] 1);
+by (dresolve_tac [spec] 1);
+by (dresolve_tac [spec] 1);
+by (assume_tac 1);
+
+choplev 0;
+by (REPEAT (assume_tac 1
+     ORELSE resolve_tac [impI,allI] 1
+     ORELSE dresolve_tac [spec] 1));
+
+
+- goal Int_Rule.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
+Level 0
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+val it = [] : thm list
+- by (resolve_tac [impI] 1);
+Level 1
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
+val it = () : unit
+- by (dresolve_tac [spec] 1);
+Level 2
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)
+val it = () : unit
+- by (resolve_tac [allI] 1);
+Level 3
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)
+val it = () : unit
+- by (dresolve_tac [spec] 1);
+Level 4
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)
+val it = () : unit
+- by (resolve_tac [allI] 1);
+Level 5
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)
+val it = () : unit
+- by (assume_tac 1);
+by: tactic returned no results
+
+uncaught exception ERROR
+- choplev 1;
+Level 1
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
+val it = () : unit
+- by (resolve_tac [allI] 1);
+Level 2
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)
+val it = () : unit
+- by (resolve_tac [allI] 1);
+Level 3
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. !!z w. ALL x y. P(x,y) ==> P(w,z)
+val it = () : unit
+- by (dresolve_tac [spec] 1);
+Level 4
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)
+val it = () : unit
+- by (dresolve_tac [spec] 1);
+Level 5
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)
+val it = () : unit
+- by (assume_tac 1);
+Level 6
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+No subgoals!
+
+> choplev 0;
+Level 0
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+ 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+> by (REPEAT (assume_tac 1
+#      ORELSE resolve_tac [impI,allI] 1
+#      ORELSE dresolve_tac [spec] 1));
+Level 1
+(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
+No subgoals!
+
+
+
+goal FOL_thy "ALL x. EX y. x=y";
+by (resolve_tac [allI] 1);
+by (resolve_tac [exI] 1);
+by (resolve_tac [refl] 1);
+
+- goal Int_Rule.thy "ALL x. EX y. x=y";
+Level 0
+ALL x. EX y. x = y
+ 1. ALL x. EX y. x = y
+val it = [] : thm list
+- by (resolve_tac [allI] 1);
+Level 1
+ALL x. EX y. x = y
+ 1. !!x. EX y. x = y
+val it = () : unit
+- by (resolve_tac [exI] 1);
+Level 2
+ALL x. EX y. x = y
+ 1. !!x. x = ?y1(x)
+val it = () : unit
+- by (resolve_tac [refl] 1);
+Level 3
+ALL x. EX y. x = y
+No subgoals!
+val it = () : unit
+-
+
+goal FOL_thy "EX y. ALL x. x=y";
+by (resolve_tac [exI] 1);
+by (resolve_tac [allI] 1);
+by (resolve_tac [refl] 1);
+
+- goal Int_Rule.thy "EX y. ALL x. x=y";
+Level 0
+EX y. ALL x. x = y
+ 1. EX y. ALL x. x = y
+val it = [] : thm list
+- by (resolve_tac [exI] 1);
+Level 1
+EX y. ALL x. x = y
+ 1. ALL x. x = ?y
+val it = () : unit
+- by (resolve_tac [allI] 1);
+Level 2
+EX y. ALL x. x = y
+ 1. !!x. x = ?y
+val it = () : unit
+- by (resolve_tac [refl] 1);
+by: tactic returned no results
+
+uncaught exception ERROR
+
+
+
+goal FOL_thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
+by (resolve_tac [exI, allI] 1);
+by (resolve_tac [exI, allI] 1);
+by (resolve_tac [exI, allI] 1);
+by (resolve_tac [exI, allI] 1);
+by (resolve_tac [exI, allI] 1);
+
+- goal Int_Rule.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
+Level 0
+EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
+ 1. EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
+val it = [] : thm list
+- by (resolve_tac [exI, allI] 1);
+Level 1
+EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
+ 1. ALL x. EX v. ALL y. EX w. P(?u,x,v,y,w)
+val it = () : unit
+- by (resolve_tac [exI, allI] 1);
+Level 2
+EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
+ 1. !!x. EX v. ALL y. EX w. P(?u,x,v,y,w)
+val it = () : unit
+- by (resolve_tac [exI, allI] 1);
+Level 3
+EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
+ 1. !!x. ALL y. EX w. P(?u,x,?v2(x),y,w)
+val it = () : unit
+- by (resolve_tac [exI, allI] 1);
+Level 4
+EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
+ 1. !!x y. EX w. P(?u,x,?v2(x),y,w)
+val it = () : unit
+- by (resolve_tac [exI, allI] 1);
+Level 5
+EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
+ 1. !!x y. P(?u,x,?v2(x),y,?w4(x,y))
+val it = () : unit
+
+
+goal FOL_thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
+by (REPEAT (resolve_tac [impI] 1));
+by (eresolve_tac [exE] 1);
+by (dresolve_tac [spec] 1);
+by (eresolve_tac [mp] 1);
+by (assume_tac 1);
+
+- goal Int_Rule.thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
+Level 0
+(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
+ 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
+val it = [] : thm list
+- by (REPEAT (resolve_tac [impI] 1));
+Level 1
+(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
+ 1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q
+val it = () : unit
+- by (eresolve_tac [exE] 1);
+Level 2
+(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
+ 1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q
+val it = () : unit
+- by (dresolve_tac [spec] 1);
+Level 3
+(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
+ 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q
+val it = () : unit
+- by (eresolve_tac [mp] 1);
+Level 4
+(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
+ 1. !!x. P(x) ==> P(?x3(x))
+val it = () : unit
+- by (assume_tac 1);
+Level 5
+(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
+No subgoals!
+
+
+goal FOL_thy "((EX x.P(x)) --> Q) --> (ALL x.P(x)-->Q)";
+by (REPEAT (resolve_tac [impI] 1));
+
+
+goal FOL_thy "(EX x.P(x) --> Q) --> (ALL x.P(x))-->Q";
+by (REPEAT (resolve_tac [impI] 1));
+by (eresolve_tac [exE] 1);
+by (eresolve_tac [mp] 1);
+by (eresolve_tac [spec] 1);
+
isabelle