--- a/doc-src/Intro/quant.txt Mon Aug 27 20:19:09 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,244 +0,0 @@
-(**** 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);
-