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

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

author	blanchet
	Wed, 04 Jan 2012 00:32:02 +0100
changeset 46109	03e3b4b401e9
parent 35762	af3ff2ba4c54
child 61385	538100cc4399
permissions	-rw-r--r--