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

lcp@105	1	Pretty.setmargin 72; (existing macros just allow this margin)
lcp@105	2	print_depth 0;
lcp@105	3
lcp@105	4	(operations for "thm")
lcp@105	5
lcp@105	6	prth mp;
lcp@105	7
lcp@105	8	prth (mp RS mp);
lcp@105	9
lcp@105	10	prth (conjunct1 RS mp);
lcp@105	11	prth (conjunct1 RSN (2,mp));
lcp@105	12
lcp@105	13	prth (mp RS conjunct1);
lcp@105	14	prth (spec RS it);
lcp@105	15	prth (standard it);
lcp@105	16
lcp@105	17	prth spec;
lcp@105	18	prth (it RS mp);
lcp@105	19	prth (it RS conjunct1);
lcp@105	20	prth (standard it);
lcp@105	21
lcp@105	22	- prth spec;
lcp@105	23	ALL x. ?P(x) ==> ?P(?x)
lcp@105	24	- prth (it RS mp);
lcp@105	25	[\| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) \|] ==> ?Q2(?x1)
lcp@105	26	- prth (it RS conjunct1);
lcp@105	27	[\| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) \|] ==> ?P6(?x2)
lcp@105	28	- prth (standard it);
lcp@105	29	[\| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) \|] ==> ?Pa(?x)
lcp@105	30
lcp@105	31	(flexflex pairs)
lcp@105	32	- prth refl;
lcp@105	33	?a = ?a
lcp@105	34	- prth exI;
lcp@105	35	?P(?x) ==> EX x. ?P(x)
lcp@105	36	- prth (refl RS exI);
lcp@105	37	?a3(?x) == ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)
lcp@105	38	- prthq (flexflex_rule it);
lcp@105	39	EX x. ?a4 = ?a4
lcp@105	40
lcp@105	41	(Usage of RL)
lcp@105	42	- val reflk = prth (read_instantiate [("a","k")] refl);
lcp@105	43	k = k
lcp@105	44	val reflk = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
lcp@105	45	- prth (reflk RS exI);
lcp@105	46
lcp@105	47	uncaught exception THM
lcp@105	48	- prths ([reflk] RL [exI]);
lcp@105	49	EX x. x = x
lcp@105	50
lcp@105	51	EX x. k = x
lcp@105	52
lcp@105	53	EX x. x = k
lcp@105	54
lcp@105	55	EX x. k = k
lcp@105	56
lcp@105	57
lcp@105	58
lcp@105	59	(tactics )
lcp@105	60
lcp@459	61	goal FOL.thy "P\|P --> P";
lcp@105	62	by (resolve_tac [impI] 1);
lcp@105	63	by (resolve_tac [disjE] 1);
lcp@105	64	by (assume_tac 3);
lcp@105	65	by (assume_tac 2);
lcp@105	66	by (assume_tac 1);
lcp@105	67	val mythm = prth(result());
lcp@105	68
lcp@105	69
lcp@459	70	goal FOL.thy "(P & Q) \| R --> (P \| R)";
lcp@105	71	by (resolve_tac [impI] 1);
lcp@105	72	by (eresolve_tac [disjE] 1);
lcp@105	73	by (dresolve_tac [conjunct1] 1);
lcp@105	74	by (resolve_tac [disjI1] 1);
lcp@105	75	by (resolve_tac [disjI2] 2);
lcp@105	76	by (REPEAT (assume_tac 1));
lcp@105	77
lcp@105	78
lcp@459	79	- goal FOL.thy "(P & Q) \| R --> (P \| R)";
lcp@105	80	Level 0
lcp@105	81	P & Q \| R --> P \| R
lcp@105	82	1. P & Q \| R --> P \| R
lcp@105	83	- by (resolve_tac [impI] 1);
lcp@105	84	Level 1
lcp@105	85	P & Q \| R --> P \| R
lcp@105	86	1. P & Q \| R ==> P \| R
lcp@105	87	- by (eresolve_tac [disjE] 1);
lcp@105	88	Level 2
lcp@105	89	P & Q \| R --> P \| R
lcp@105	90	1. P & Q ==> P \| R
lcp@105	91	2. R ==> P \| R
lcp@105	92	- by (dresolve_tac [conjunct1] 1);
lcp@105	93	Level 3
lcp@105	94	P & Q \| R --> P \| R
lcp@105	95	1. P ==> P \| R
lcp@105	96	2. R ==> P \| R
lcp@105	97	- by (resolve_tac [disjI1] 1);
lcp@105	98	Level 4
lcp@105	99	P & Q \| R --> P \| R
lcp@105	100	1. P ==> P
lcp@105	101	2. R ==> P \| R
lcp@105	102	- by (resolve_tac [disjI2] 2);
lcp@105	103	Level 5
lcp@105	104	P & Q \| R --> P \| R
lcp@105	105	1. P ==> P
lcp@105	106	2. R ==> R
lcp@105	107	- by (REPEAT (assume_tac 1));
lcp@105	108	Level 6
lcp@105	109	P & Q \| R --> P \| R
lcp@105	110	No subgoals!
lcp@105	111
lcp@105	112
lcp@459	113	goal FOL.thy "(P \| Q) \| R --> P \| (Q \| R)";
lcp@105	114	by (resolve_tac [impI] 1);
lcp@105	115	by (eresolve_tac [disjE] 1);
lcp@105	116	by (eresolve_tac [disjE] 1);
lcp@105	117	by (resolve_tac [disjI1] 1);
lcp@105	118	by (resolve_tac [disjI2] 2);
lcp@105	119	by (resolve_tac [disjI1] 2);
lcp@105	120	by (resolve_tac [disjI2] 3);
lcp@105	121	by (resolve_tac [disjI2] 3);
lcp@105	122	by (REPEAT (assume_tac 1));

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