isabelle: src/Sequents/ILL_predlog.thy@d2c97fc18704 (annotated)

21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	1	(* $Id$ *)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	2
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	3	theory ILL_predlog
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	4	imports ILL
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	5	begin
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	6
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	7	typedecl plf
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	8
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	9	consts
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	10	conj :: "[plf,plf] => plf" (infixr "&" 35)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	11	disj :: "[plf,plf] => plf" (infixr "\|" 35)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	12	impl :: "[plf,plf] => plf" (infixr ">" 35)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	13	eq :: "[plf,plf] => plf" (infixr "=" 35)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	14	ff :: "plf"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	15
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	16	PL :: "plf => o" ("[* / _ / *]" [] 100)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	17
22895 adc529c89281 tuned syntax; wenzelm parents: 21427 diff changeset	18	syntax
adc529c89281 tuned syntax; wenzelm parents: 21427 diff changeset	19	"_NG" :: "plf => plf" ("- _ " [50] 55)
adc529c89281 tuned syntax; wenzelm parents: 21427 diff changeset	20
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	21	translations
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	22
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	23	"[* A & B ]" == "[A] && [B*]"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	24	"[* A \| B ]" == "![A] ++ ![B*]"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	25	"[* - A ]" == "[A > ff*]"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	26	"[* ff *]" == "0"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	27	"[* A = B ]" => "[ (A > B) & (B > A) *]"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	28
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	29	"[* A > B ]" == "![A] -o [B*]"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	30
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	31	(* another translations for linear implication:
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	32	"[* A > B ]" == "!([A] -o [B])" )
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	33
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	34	(* from [kleene 52] pp 118,119 *)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	35
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	36	lemma k49a: "\|- [* A > ( - ( - A)) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	37	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	38
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	39	lemma k49b: "\|- [( - ( - ( - A))) = ( - A)]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	40	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	41
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	42	lemma k49c: "\|- [* (A \| - A) > ( - - A = A) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	43	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	44
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	45	lemma k50a: "\|- [* - (A = - A) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	46	by best_power
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	47
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	48	lemma k51a: "\|- [* - - (A \| - A) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	49	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	50
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	51	lemma k51b: "\|- [* - - (- - A > A) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	52	by best_power
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	53
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	54	lemma k56a: "\|- [* (A \| B) > - (- A & - B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	55	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	56
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	57	lemma k56b: "\|- [* (-A \| B) > - (A & -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	58	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	59
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	60	lemma k57a: "\|- [* (A & B) > - (-A \| -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	61	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	62
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	63	lemma k57b: "\|- [* (A & -B) > -(-A \| B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	64	by best_power
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	65
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	66	lemma k58a: "\|- [* (A > B) > - (A & -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	67	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	68
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	69	lemma k58b: "\|- [* (A > -B) = -(A & B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	70	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	71
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	72	lemma k58c: "\|- [* - (A & B) = (- - A > - B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	73	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	74
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	75	lemma k58d: "\|- [* (- - A > - B) = - - (-A \| -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	76	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	77
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	78	lemma k58e: "! [* - -B > B ] \|- [ (- -A > B) = (A > B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	79	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	80
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	81	lemma k58f: "! [* - -B > B ] \|- [ (A > B) = - (A & -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	82	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	83
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	84	lemma k58g: "\|- [* (- -A > B) > - (A & -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	85	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	86
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	87	lemma k59a: "\|- [* (-A \| B) > (A > B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	88	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	89
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	90	lemma k59b: "\|- [* (A > B) > - - (-A \| B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	91	by best_power
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	92
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	93	lemma k59c: "\|- [* (-A > B) > - -(A \| B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	94	by best_power
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	95
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	96	lemma k60a: "\|- [* (A & B) > - (A > -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	97	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	98
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	99	lemma k60b: "\|- [* (A & -B) > - (A > B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	100	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	101
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	102	lemma k60c: "\|- [* ( - - A & B) > - (A > -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	103	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	104
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	105	lemma k60d: "\|- [* (- - A & - B) = - (A > B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	106	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	107
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	108	lemma k60e: "\|- [* - (A > B) = - (-A \| B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	109	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	110
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	111	lemma k60f: "\|- [* - (-A \| B) = - - (A & -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	112	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	113
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	114	lemma k60g: "\|- [* - - (A > B) = - (A & -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	115	by best_power
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	116
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	117	lemma k60h: "\|- [* - (A & -B) = (A > - -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	118	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	119
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	120	lemma k60i: "\|- [* (A > - -B) = (- -A > - -B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	121	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	122
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	123	lemma k61a: "\|- [* (A \| B) > (-A > B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	124	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	125
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	126	lemma k61b: "\|- [* - (A \| B) = - (-A > B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	127	by best_power
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	128
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	129	lemma k62a: "\|- [* (-A \| -B) > - (A & B) *]"
21427 7c8f4a331f9b converted legacy ML scripts; wenzelm parents: 21426 diff changeset	130	by best_safe
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	131
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	132	end

author	nipkow
	Tue, 01 Sep 2009 19:48:11 +0200
changeset 32475	d2c97fc18704
parent 22895	adc529c89281
child 35054	a5db9779b026
permissions	-rw-r--r--