wneuper/isa: doc-src/Intro/quant.txt@20e3616b2d9c (annotated)

lcp@105	1	(** quantifier examples -- process using Doc/tout quant.txt **)
lcp@105	2
lcp@105	3	Pretty.setmargin 72; (existing macros just allow this margin)
lcp@105	4	print_depth 0;
lcp@105	5
lcp@105	6
lcp@105	7	goal Int_Rule.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))";
lcp@105	8	by (resolve_tac [impI] 1);
lcp@105	9	by (dresolve_tac [spec] 1);
lcp@105	10	by (resolve_tac [allI] 1);
lcp@105	11	by (dresolve_tac [spec] 1);
lcp@105	12	by (resolve_tac [allI] 1);
lcp@105	13	by (assume_tac 1);
lcp@105	14	choplev 1;
lcp@105	15	by (resolve_tac [allI] 1);
lcp@105	16	by (resolve_tac [allI] 1);
lcp@105	17	by (dresolve_tac [spec] 1);
lcp@105	18	by (dresolve_tac [spec] 1);
lcp@105	19	by (assume_tac 1);
lcp@105	20
lcp@105	21	choplev 0;
lcp@105	22	by (REPEAT (assume_tac 1
lcp@105	23	ORELSE resolve_tac [impI,allI] 1
lcp@105	24	ORELSE dresolve_tac [spec] 1));
lcp@105	25
lcp@105	26
lcp@105	27	- goal Int_Rule.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))";
lcp@105	28	Level 0
lcp@105	29	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	30	1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	31	val it = [] : thm list
lcp@105	32	- by (resolve_tac [impI] 1);
lcp@105	33	Level 1
lcp@105	34	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	35	1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
lcp@105	36	val it = () : unit
lcp@105	37	- by (dresolve_tac [spec] 1);
lcp@105	38	Level 2
lcp@105	39	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	40	1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)
lcp@105	41	val it = () : unit
lcp@105	42	- by (resolve_tac [allI] 1);
lcp@105	43	Level 3
lcp@105	44	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	45	1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)
lcp@105	46	val it = () : unit
lcp@105	47	- by (dresolve_tac [spec] 1);
lcp@105	48	Level 4
lcp@105	49	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	50	1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)
lcp@105	51	val it = () : unit
lcp@105	52	- by (resolve_tac [allI] 1);
lcp@105	53	Level 5
lcp@105	54	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	55	1. !!z w. P(?x1,?y3(z)) ==> P(w,z)
lcp@105	56	val it = () : unit
lcp@105	57	- by (assume_tac 1);
lcp@105	58	by: tactic returned no results
lcp@105	59
lcp@105	60	uncaught exception ERROR
lcp@105	61	- choplev 1;
lcp@105	62	Level 1
lcp@105	63	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	64	1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
lcp@105	65	val it = () : unit
lcp@105	66	- by (resolve_tac [allI] 1);
lcp@105	67	Level 2
lcp@105	68	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	69	1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)
lcp@105	70	val it = () : unit
lcp@105	71	- by (resolve_tac [allI] 1);
lcp@105	72	Level 3
lcp@105	73	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	74	1. !!z w. ALL x y. P(x,y) ==> P(w,z)
lcp@105	75	val it = () : unit
lcp@105	76	- by (dresolve_tac [spec] 1);
lcp@105	77	Level 4
lcp@105	78	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	79	1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)
lcp@105	80	val it = () : unit
lcp@105	81	- by (dresolve_tac [spec] 1);
lcp@105	82	Level 5
lcp@105	83	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	84	1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)
lcp@105	85	val it = () : unit
lcp@105	86	- by (assume_tac 1);
lcp@105	87	Level 6
lcp@105	88	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	89	No subgoals!
lcp@105	90
lcp@105	91	> choplev 0;
lcp@105	92	Level 0
lcp@105	93	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	94	1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	95	> by (REPEAT (assume_tac 1
lcp@105	96	# ORELSE resolve_tac [impI,allI] 1
lcp@105	97	# ORELSE dresolve_tac [spec] 1));
lcp@105	98	Level 1
lcp@105	99	(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
lcp@105	100	No subgoals!
lcp@105	101
lcp@105	102
lcp@105	103
lcp@105	104	goal FOL_thy "ALL x. EX y. x=y";
lcp@105	105	by (resolve_tac [allI] 1);
lcp@105	106	by (resolve_tac [exI] 1);
lcp@105	107	by (resolve_tac [refl] 1);
lcp@105	108
lcp@105	109	- goal Int_Rule.thy "ALL x. EX y. x=y";
lcp@105	110	Level 0
lcp@105	111	ALL x. EX y. x = y
lcp@105	112	1. ALL x. EX y. x = y
lcp@105	113	val it = [] : thm list
lcp@105	114	- by (resolve_tac [allI] 1);
lcp@105	115	Level 1
lcp@105	116	ALL x. EX y. x = y
lcp@105	117	1. !!x. EX y. x = y
lcp@105	118	val it = () : unit
lcp@105	119	- by (resolve_tac [exI] 1);
lcp@105	120	Level 2
lcp@105	121	ALL x. EX y. x = y
lcp@105	122	1. !!x. x = ?y1(x)
lcp@105	123	val it = () : unit
lcp@105	124	- by (resolve_tac [refl] 1);
lcp@105	125	Level 3
lcp@105	126	ALL x. EX y. x = y
lcp@105	127	No subgoals!
lcp@105	128	val it = () : unit
lcp@105	129	-
lcp@105	130
lcp@105	131	goal FOL_thy "EX y. ALL x. x=y";
lcp@105	132	by (resolve_tac [exI] 1);
lcp@105	133	by (resolve_tac [allI] 1);
lcp@105	134	by (resolve_tac [refl] 1);
lcp@105	135
lcp@105	136	- goal Int_Rule.thy "EX y. ALL x. x=y";
lcp@105	137	Level 0
lcp@105	138	EX y. ALL x. x = y
lcp@105	139	1. EX y. ALL x. x = y
lcp@105	140	val it = [] : thm list
lcp@105	141	- by (resolve_tac [exI] 1);
lcp@105	142	Level 1
lcp@105	143	EX y. ALL x. x = y
lcp@105	144	1. ALL x. x = ?y
lcp@105	145	val it = () : unit
lcp@105	146	- by (resolve_tac [allI] 1);
lcp@105	147	Level 2
lcp@105	148	EX y. ALL x. x = y
lcp@105	149	1. !!x. x = ?y
lcp@105	150	val it = () : unit
lcp@105	151	- by (resolve_tac [refl] 1);
lcp@105	152	by: tactic returned no results
lcp@105	153
lcp@105	154	uncaught exception ERROR
lcp@105	155
lcp@105	156
lcp@105	157
lcp@105	158	goal FOL_thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
lcp@105	159	by (resolve_tac [exI, allI] 1);
lcp@105	160	by (resolve_tac [exI, allI] 1);
lcp@105	161	by (resolve_tac [exI, allI] 1);
lcp@105	162	by (resolve_tac [exI, allI] 1);
lcp@105	163	by (resolve_tac [exI, allI] 1);
lcp@105	164
lcp@105	165	- goal Int_Rule.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
lcp@105	166	Level 0
lcp@105	167	EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
lcp@105	168	1. EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
lcp@105	169	val it = [] : thm list
lcp@105	170	- by (resolve_tac [exI, allI] 1);
lcp@105	171	Level 1
lcp@105	172	EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
lcp@105	173	1. ALL x. EX v. ALL y. EX w. P(?u,x,v,y,w)
lcp@105	174	val it = () : unit
lcp@105	175	- by (resolve_tac [exI, allI] 1);
lcp@105	176	Level 2
lcp@105	177	EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
lcp@105	178	1. !!x. EX v. ALL y. EX w. P(?u,x,v,y,w)
lcp@105	179	val it = () : unit
lcp@105	180	- by (resolve_tac [exI, allI] 1);
lcp@105	181	Level 3
lcp@105	182	EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
lcp@105	183	1. !!x. ALL y. EX w. P(?u,x,?v2(x),y,w)
lcp@105	184	val it = () : unit
lcp@105	185	- by (resolve_tac [exI, allI] 1);
lcp@105	186	Level 4
lcp@105	187	EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
lcp@105	188	1. !!x y. EX w. P(?u,x,?v2(x),y,w)
lcp@105	189	val it = () : unit
lcp@105	190	- by (resolve_tac [exI, allI] 1);
lcp@105	191	Level 5
lcp@105	192	EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
lcp@105	193	1. !!x y. P(?u,x,?v2(x),y,?w4(x,y))
lcp@105	194	val it = () : unit
lcp@105	195
lcp@105	196
lcp@105	197	goal FOL_thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
lcp@105	198	by (REPEAT (resolve_tac [impI] 1));
lcp@105	199	by (eresolve_tac [exE] 1);
lcp@105	200	by (dresolve_tac [spec] 1);
lcp@105	201	by (eresolve_tac [mp] 1);
lcp@105	202	by (assume_tac 1);
lcp@105	203
lcp@105	204	- goal Int_Rule.thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
lcp@105	205	Level 0
lcp@105	206	(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
lcp@105	207	1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
lcp@105	208	val it = [] : thm list
lcp@105	209	- by (REPEAT (resolve_tac [impI] 1));
lcp@105	210	Level 1
lcp@105	211	(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
lcp@105	212	1. [\| ALL x. P(x) --> Q; EX x. P(x) \|] ==> Q
lcp@105	213	val it = () : unit
lcp@105	214	- by (eresolve_tac [exE] 1);
lcp@105	215	Level 2
lcp@105	216	(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
lcp@105	217	1. !!x. [\| ALL x. P(x) --> Q; P(x) \|] ==> Q
lcp@105	218	val it = () : unit
lcp@105	219	- by (dresolve_tac [spec] 1);
lcp@105	220	Level 3
lcp@105	221	(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
lcp@105	222	1. !!x. [\| P(x); P(?x3(x)) --> Q \|] ==> Q
lcp@105	223	val it = () : unit
lcp@105	224	- by (eresolve_tac [mp] 1);
lcp@105	225	Level 4
lcp@105	226	(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
lcp@105	227	1. !!x. P(x) ==> P(?x3(x))
lcp@105	228	val it = () : unit
lcp@105	229	- by (assume_tac 1);
lcp@105	230	Level 5
lcp@105	231	(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
lcp@105	232	No subgoals!
lcp@105	233
lcp@105	234
lcp@105	235	goal FOL_thy "((EX x.P(x)) --> Q) --> (ALL x.P(x)-->Q)";
lcp@105	236	by (REPEAT (resolve_tac [impI] 1));
lcp@105	237
lcp@105	238
lcp@105	239	goal FOL_thy "(EX x.P(x) --> Q) --> (ALL x.P(x))-->Q";
lcp@105	240	by (REPEAT (resolve_tac [impI] 1));
lcp@105	241	by (eresolve_tac [exE] 1);
lcp@105	242	by (eresolve_tac [mp] 1);
lcp@105	243	by (eresolve_tac [spec] 1);
lcp@105	244

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 105	216d6ed87399
permissions	-rw-r--r--