isabelle: doc-src/ZF/FOL-eg.txt@b3e7863a5060 (annotated)

6121 5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	1	(** FOL examples **)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	2
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	3	Pretty.setmargin 72; (existing macros just allow this margin)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	4	print_depth 0;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	5
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	6	(* Intuitionistic examples *)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	7
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	8	context IFOL.thy;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	9
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	10	(Quantifier example from Logic&Computation)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	11	Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	12	by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	13	by (resolve_tac [allI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	14	by (resolve_tac [exI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	15	by (eresolve_tac [exE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	16	choplev 2;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	17	by (eresolve_tac [exE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	18	by (resolve_tac [exI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	19	by (eresolve_tac [allE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	20	by (assume_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	21
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	22
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	23	(Example of Dyckhoff's method)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	24	Goalw [not_def] "~ ~ ((P-->Q) \| (Q-->P))";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	25	by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	26	by (eresolve_tac [disj_impE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	27	by (eresolve_tac [imp_impE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	28	by (eresolve_tac [imp_impE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	29	by (REPEAT (eresolve_tac [FalseE] 2));
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	30	by (assume_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	31
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	32
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	33
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	34
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	35
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	36	(* Classical examples *)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	37
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	38	context FOL.thy;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	39
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	40	Goal "EX y. ALL x. P(y)-->P(x)";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	41	by (resolve_tac [exCI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	42	by (resolve_tac [allI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	43	by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	44	by (eresolve_tac [allE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	45	prth (allI RSN (2,swap));
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	46	by (eresolve_tac [it] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	47	by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	48	by (eresolve_tac [notE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	49	by (assume_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	50	Goal "EX y. ALL x. P(y)-->P(x)";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	51	by (Blast_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	52
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	53
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	54
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	55	- Goal "EX y. ALL x. P(y)-->P(x)";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	56	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	57	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	58	1. EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	59	- by (resolve_tac [exCI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	60	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	61	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	62	1. ALL y. ~(ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	63	- by (resolve_tac [allI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	64	Level 2
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	65	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	66	1. !!x. ALL y. ~(ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	67	- by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	68	Level 3
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	69	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	70	1. !!x. [\| ALL y. ~(ALL x. P(y) --> P(x)); P(?a) \|] ==> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	71	- by (eresolve_tac [allE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	72	Level 4
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	73	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	74	1. !!x. [\| P(?a); ~(ALL xa. P(?y3(x)) --> P(xa)) \|] ==> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	75	- prth (allI RSN (2,swap));
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	76	[\| ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) \|] ==> ?Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	77	- by (eresolve_tac [it] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	78	Level 5
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	79	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	80	1. !!x xa. [\| P(?a); ~P(x) \|] ==> P(?y3(x)) --> P(xa)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	81	- by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	82	Level 6
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	83	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	84	1. !!x xa. [\| P(?a); ~P(x); P(?y3(x)) \|] ==> P(xa)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	85	- by (eresolve_tac [notE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	86	Level 7
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	87	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	88	1. !!x xa. [\| P(?a); P(?y3(x)) \|] ==> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	89	- by (assume_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	90	Level 8
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	91	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	92	No subgoals!
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	93	- Goal "EX y. ALL x. P(y)-->P(x)";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	94	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	95	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	96	1. EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	97	- by (best_tac FOL_dup_cs 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	98	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	99	EX y. ALL x. P(y) --> P(x)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	100	No subgoals!
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	101
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	102
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	103	(** finally, the example FOL/ex/if.ML **)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	104
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	105	> val prems = goalw if_thy [if_def]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	106	# "[\| P ==> Q; ~P ==> R \|] ==> if(P,Q,R)";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	107	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	108	if(P,Q,R)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	109	1. P & Q \| ~P & R
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	110	> by (Classical.fast_tac (FOL_cs addIs prems) 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	111	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	112	if(P,Q,R)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	113	No subgoals!
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	114	> val ifI = result();
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	115
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	116
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	117	> val major::prems = goalw if_thy [if_def]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	118	# "[\| if(P,Q,R); [\| P; Q \|] ==> S; [\| ~P; R \|] ==> S \|] ==> S";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	119	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	120	S
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	121	1. S
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	122	> by (cut_facts_tac [major] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	123	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	124	S
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	125	1. P & Q \| ~P & R ==> S
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	126	> by (Classical.fast_tac (FOL_cs addIs prems) 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	127	Level 2
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	128	S
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	129	No subgoals!
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	130	> val ifE = result();
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	131
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	132	> goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	133	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	134	if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	135	1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	136	> by (resolve_tac [iffI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	137	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	138	if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	139	1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	140	2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	141	> by (eresolve_tac [ifE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	142	Level 2
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	143	if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	144	1. [\| P; if(Q,A,B) \|] ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	145	2. [\| ~P; if(Q,C,D) \|] ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	146	3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	147	> by (eresolve_tac [ifE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	148	Level 3
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	149	if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	150	1. [\| P; Q; A \|] ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	151	2. [\| P; ~Q; B \|] ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	152	3. [\| ~P; if(Q,C,D) \|] ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	153	4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	154	> by (resolve_tac [ifI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	155	Level 4
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	156	if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	157	1. [\| P; Q; A; Q \|] ==> if(P,A,C)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	158	2. [\| P; Q; A; ~Q \|] ==> if(P,B,D)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	159	3. [\| P; ~Q; B \|] ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	160	4. [\| ~P; if(Q,C,D) \|] ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	161	5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	162	> by (resolve_tac [ifI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	163	Level 5
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	164	if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	165	1. [\| P; Q; A; Q; P \|] ==> A
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	166	2. [\| P; Q; A; Q; ~P \|] ==> C
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	167	3. [\| P; Q; A; ~Q \|] ==> if(P,B,D)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	168	4. [\| P; ~Q; B \|] ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	169	5. [\| ~P; if(Q,C,D) \|] ==> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	170	6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	171
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	172	> choplev 0;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	173	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	174	if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	175	1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	176	> val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	177	> by (Classical.fast_tac if_cs 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	178	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	179	if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	180	No subgoals!
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	181	> val if_commute = result();
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	182
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	183	> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	184	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	185	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	186	1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	187	> by (Classical.fast_tac if_cs 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	188	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	189	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	190	No subgoals!
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	191	> val nested_ifs = result();
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	192
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	193
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	194	> choplev 0;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	195	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	196	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	197	1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	198	> by (rewrite_goals_tac [if_def]);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	199	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	200	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	201	1. (P & Q \| ~P & R) & A \| ~(P & Q \| ~P & R) & B <->
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	202	P & (Q & A \| ~Q & B) \| ~P & (R & A \| ~R & B)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	203	> by (Classical.fast_tac FOL_cs 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	204	Level 2
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	205	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	206	No subgoals!
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	207
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	208
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	209	> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	210	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	211	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	212	1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	213	> by (REPEAT (Classical.step_tac if_cs 1));
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	214	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	215	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	216	1. [\| A; ~P; R; ~P; R \|] ==> B
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	217	2. [\| B; ~P; ~R; ~P; ~R \|] ==> A
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	218	3. [\| ~P; R; B; ~P; R \|] ==> A
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	219	4. [\| ~P; ~R; A; ~B; ~P \|] ==> R
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	220
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	221	> choplev 0;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	222	Level 0
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	223	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	224	1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	225	> by (rewrite_goals_tac [if_def]);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	226	Level 1
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	227	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	228	1. (P & Q \| ~P & R) & A \| ~(P & Q \| ~P & R) & B <->
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	229	P & (Q & A \| ~Q & B) \| ~P & (R & B \| ~R & A)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	230	> by (Classical.fast_tac FOL_cs 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	231	by: tactic failed
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	232	Exception- ERROR raised
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	233	Exception failure raised
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	234
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	235	> by (REPEAT (Classical.step_tac FOL_cs 1));
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	236	Level 2
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	237	if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	238	1. [\| A; ~P; R; ~P; R; ~False \|] ==> B
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	239	2. [\| A; ~P; R; R; ~False; ~B; ~B \|] ==> Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	240	3. [\| B; ~P; ~R; ~P; ~A \|] ==> R
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	241	4. [\| B; ~P; ~R; ~Q; ~A \|] ==> R
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	242	5. [\| B; ~R; ~P; ~A; ~R; Q; ~False \|] ==> A
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	243	6. [\| ~P; R; B; ~P; R; ~False \|] ==> A
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	244	7. [\| ~P; ~R; A; ~B; ~R \|] ==> P
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and paulson parents: diff changeset	245	8. [\| ~P; ~R; A; ~B; ~R \|] ==> Q

author	wenzelm
	Sun, 04 Feb 2001 19:46:31 +0100
changeset 11058	b3e7863a5060
parent 6121	5fe77b9b5185
permissions	-rw-r--r--