wneuper/isa: src/CTT/Bool.thy@d88f7fc62a40

     1 (*  Title:      CTT/Bool.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1991  University of Cambridge

     4 *)

     6 header {* The two-element type (booleans and conditionals) *}

     8 theory Bool

     9 imports CTT

    10 begin

    12 definition

    13   Bool :: "t" where

    14   "Bool == T+T"

    16 definition

    17   true :: "i" where

    18   "true == inl(tt)"

    20 definition

    21   false :: "i" where

    22   "false == inr(tt)"

    24 definition

    25   cond :: "[i,i,i]=>i" where

    26   "cond(a,b,c) == when(a, %u. b, %u. c)"

    28 lemmas bool_defs = Bool_def true_def false_def cond_def

    31 subsection {* Derivation of rules for the type Bool *}

    33 (*formation rule*)

    34 lemma boolF: "Bool type"

    35 apply (unfold bool_defs)

    36 apply (tactic "typechk_tac []")

    37 done

    40 (*introduction rules for true, false*)

    42 lemma boolI_true: "true : Bool"

    43 apply (unfold bool_defs)

    44 apply (tactic "typechk_tac []")

    45 done

    47 lemma boolI_false: "false : Bool"

    48 apply (unfold bool_defs)

    49 apply (tactic "typechk_tac []")

    50 done

    52 (*elimination rule: typing of cond*)

    53 lemma boolE:

    54     "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"

    55 apply (unfold bool_defs)

    56 apply (tactic "typechk_tac []")

    57 apply (erule_tac [!] TE)

    58 apply (tactic "typechk_tac []")

    59 done

    61 lemma boolEL:

    62     "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]

    63      ==> cond(p,a,b) = cond(q,c,d) : C(p)"

    64 apply (unfold bool_defs)

    65 apply (rule PlusEL)

    66 apply (erule asm_rl refl_elem [THEN TEL])+

    67 done

    69 (*computation rules for true, false*)

    71 lemma boolC_true:

    72     "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"

    73 apply (unfold bool_defs)

    74 apply (rule comp_rls)

    75 apply (tactic "typechk_tac []")

    76 apply (erule_tac [!] TE)

    77 apply (tactic "typechk_tac []")

    78 done

    80 lemma boolC_false:

    81     "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"

    82 apply (unfold bool_defs)

    83 apply (rule comp_rls)

    84 apply (tactic "typechk_tac []")

    85 apply (erule_tac [!] TE)

    86 apply (tactic "typechk_tac []")

    87 done

    89 end

author	wenzelm
	Mon, 19 Sep 2011 22:13:51 +0200
changeset 45872	d88f7fc62a40
parent 42830	b460124855b8
child 59180	85ec71012df8
permissions	-rw-r--r--