isabelle: src/FOLP/ex/Foundation.thy@73df5884edcf (annotated)

41777 1f7cbe39d425 more precise headers; wenzelm parents: 41526 diff changeset	1	(* Title: FOLP/ex/Foundation.thy
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	2	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	3	Copyright 1991 University of Cambridge
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	4	*)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	5
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	6	header "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	7
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	8	theory Foundation
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	9	imports IFOLP
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	10	begin
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	11
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	12	schematic_lemma "?p : A&B --> (C-->A&C)"
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	13	apply (rule impI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	14	apply (rule impI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	15	apply (rule conjI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	16	prefer 2 apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	17	apply (rule conjunct1)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	18	apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	19	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	20
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	21	text {A form of conj-elimination}
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	22	schematic_lemma
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	23	assumes "p : A & B"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	24	and "!!x y. x : A ==> y : B ==> f(x, y) : C"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	25	shows "?p : C"
41526 54b4686704af eliminated global prems; wenzelm parents: 36319 diff changeset	26	apply (rule assms)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	27	apply (rule conjunct1)
41526 54b4686704af eliminated global prems; wenzelm parents: 36319 diff changeset	28	apply (rule assms)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	29	apply (rule conjunct2)
41526 54b4686704af eliminated global prems; wenzelm parents: 36319 diff changeset	30	apply (rule assms)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	31	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	32
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	33	schematic_lemma
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	34	assumes "!!A x. x : ~ ~A ==> cla(x) : A"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	35	shows "?p : B \| ~B"
41526 54b4686704af eliminated global prems; wenzelm parents: 36319 diff changeset	36	apply (rule assms)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	37	apply (rule notI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	38	apply (rule_tac P = "~B" in notE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	39	apply (rule_tac [2] notI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	40	apply (rule_tac [2] P = "B \| ~B" in notE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	41	prefer 2 apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	42	apply (rule_tac [2] disjI1)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	43	prefer 2 apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	44	apply (rule notI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	45	apply (rule_tac P = "B \| ~B" in notE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	46	apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	47	apply (rule disjI2)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	48	apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	49	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	50
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	51	schematic_lemma
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	52	assumes "!!A x. x : ~ ~A ==> cla(x) : A"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	53	shows "?p : B \| ~B"
41526 54b4686704af eliminated global prems; wenzelm parents: 36319 diff changeset	54	apply (rule assms)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	55	apply (rule notI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	56	apply (rule notE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	57	apply (rule_tac [2] notI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	58	apply (erule_tac [2] notE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	59	apply (erule_tac [2] disjI1)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	60	apply (rule notI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	61	apply (erule notE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	62	apply (erule disjI2)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	63	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	64
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	65
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	66	schematic_lemma
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	67	assumes "p : A \| ~A"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	68	and "q : ~ ~A"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	69	shows "?p : A"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	70	apply (rule disjE)
41526 54b4686704af eliminated global prems; wenzelm parents: 36319 diff changeset	71	apply (rule assms)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	72	apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	73	apply (rule FalseE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	74	apply (rule_tac P = "~A" in notE)
41526 54b4686704af eliminated global prems; wenzelm parents: 36319 diff changeset	75	apply (rule assms)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	76	apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	77	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	78
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	79
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	80	subsection "Examples with quantifiers"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	81
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	82	schematic_lemma
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	83	assumes "p : ALL z. G(z)"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	84	shows "?p : ALL z. G(z)\|H(z)"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	85	apply (rule allI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	86	apply (rule disjI1)
41526 54b4686704af eliminated global prems; wenzelm parents: 36319 diff changeset	87	apply (rule assms [THEN spec])
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	88	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	89
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	90	schematic_lemma "?p : ALL x. EX y. x=y"
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	91	apply (rule allI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	92	apply (rule exI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	93	apply (rule refl)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	94	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	95
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	96	schematic_lemma "?p : EX y. ALL x. x=y"
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	97	apply (rule exI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	98	apply (rule allI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	99	apply (rule refl)?
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	100	oops
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	101
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	102	text {* Parallel lifting example. *}
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	103	schematic_lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	104	apply (rule exI allI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	105	apply (rule exI allI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	106	apply (rule exI allI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	107	apply (rule exI allI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	108	apply (rule exI allI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	109	oops
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	110
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	111	schematic_lemma
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	112	assumes "p : (EX z. F(z)) & B"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	113	shows "?p : EX z. F(z) & B"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	114	apply (rule conjE)
41526 54b4686704af eliminated global prems; wenzelm parents: 36319 diff changeset	115	apply (rule assms)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	116	apply (rule exE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	117	apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	118	apply (rule exI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	119	apply (rule conjI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	120	apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	121	apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	122	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	123
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	124	text {* A bigger demonstration of quantifiers -- not in the paper. *}
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	125	schematic_lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	126	apply (rule impI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	127	apply (rule allI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	128	apply (rule exE, assumption)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	129	apply (rule exI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	130	apply (rule allE, assumption)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	131	apply assumption
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	132	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	133
31b38a39e589 eliminated some legacy ML files; wenzelm parents: diff changeset	134	end

author	blanchet
	Wed, 24 Sep 2014 15:46:40 +0200
changeset 58430	73df5884edcf
parent 41777	1f7cbe39d425
child 58889	5b7a9633cfa8
permissions	-rw-r--r--