isabelle: src/CTT/Bool.thy@4a92178011e7 (annotated)

41959 b460124855b8 tuned headers; wenzelm parents: 35762 diff changeset	1	(* Title: CTT/Bool.thy
1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	2	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Copyright 1991 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	4	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
17441 5b5feca0344a converted to Isar theory format; wenzelm parents: 3837 diff changeset	6	header {* The two-element type (booleans and conditionals) *}
5b5feca0344a converted to Isar theory format; wenzelm parents: 3837 diff changeset	7
5b5feca0344a converted to Isar theory format; wenzelm parents: 3837 diff changeset	8	theory Bool
5b5feca0344a converted to Isar theory format; wenzelm parents: 3837 diff changeset	9	imports CTT
5b5feca0344a converted to Isar theory format; wenzelm parents: 3837 diff changeset	10	begin
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	11
19762 957bcf55c98f tuned; wenzelm parents: 19761 diff changeset	12	definition
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19762 diff changeset	13	Bool :: "t" where
19761 5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	14	"Bool == T+T"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	15
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19762 diff changeset	16	definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19762 diff changeset	17	true :: "i" where
19761 5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	18	"true == inl(tt)"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	19
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19762 diff changeset	20	definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19762 diff changeset	21	false :: "i" where
19761 5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	22	"false == inr(tt)"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	23
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19762 diff changeset	24	definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19762 diff changeset	25	cond :: "[i,i,i]=>i" where
19761 5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	26	"cond(a,b,c) == when(a, %u. b, %u. c)"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	27
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	28	lemmas bool_defs = Bool_def true_def false_def cond_def
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	29
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	30
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	31	subsection {* Derivation of rules for the type Bool *}
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	32
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	33	(formation rule)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	34	lemma boolF: "Bool type"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	35	apply (unfold bool_defs)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	36	apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	37	done
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	38
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	39
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	40	(introduction rules for true, false)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	41
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	42	lemma boolI_true: "true : Bool"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	43	apply (unfold bool_defs)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	44	apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	45	done
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	46
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	47	lemma boolI_false: "false : Bool"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	48	apply (unfold bool_defs)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	49	apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	50	done
17441 5b5feca0344a converted to Isar theory format; wenzelm parents: 3837 diff changeset	51
19761 5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	52	(elimination rule: typing of cond)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	53	lemma boolE:
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	54	"[\| p:Bool; a : C(true); b : C(false) \|] ==> cond(p,a,b) : C(p)"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	55	apply (unfold bool_defs)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	56	apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	57	apply (erule_tac [!] TE)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	58	apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	59	done
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	60
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	61	lemma boolEL:
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	62	"[\| p = q : Bool; a = c : C(true); b = d : C(false) \|]
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	63	==> cond(p,a,b) = cond(q,c,d) : C(p)"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	64	apply (unfold bool_defs)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	65	apply (rule PlusEL)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	66	apply (erule asm_rl refl_elem [THEN TEL])+
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	67	done
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	68
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	69	(computation rules for true, false)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	70
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	71	lemma boolC_true:
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	72	"[\| a : C(true); b : C(false) \|] ==> cond(true,a,b) = a : C(true)"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	73	apply (unfold bool_defs)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	74	apply (rule comp_rls)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	75	apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	76	apply (erule_tac [!] TE)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	77	apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	78	done
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	79
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	80	lemma boolC_false:
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	81	"[\| a : C(true); b : C(false) \|] ==> cond(false,a,b) = b : C(false)"
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	82	apply (unfold bool_defs)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	83	apply (rule comp_rls)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	84	apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	85	apply (erule_tac [!] TE)
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	86	apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 17441 diff changeset	87	done
17441 5b5feca0344a converted to Isar theory format; wenzelm parents: 3837 diff changeset	88
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	89	end

author	traytel
	Fri, 01 Mar 2013 22:15:31 +0100
changeset 51319	4a92178011e7
parent 41959	b460124855b8
child 58889	5b7a9633cfa8
permissions	-rw-r--r--