src/CTT/Bool.thy

fixed bug in the "fast_descrs" optimization;
the bug is that two sets may actually be the same but because of the three-valued logic a different "The" or "Eps" is chosen; e.g. consider the set {1, 2}. If it is approximated in one place as {1, 2?} and in another place as {1?, 2}, then "Eps" would return 1 in the first case and 2 in the second case. This is of course wrong, because both sets potentially represent {1, 2}.
The current fix has a very negative impact on precision.

(*  Title:      CTT/bool
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge
*)

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

theory Bool
imports CTT
begin

definition
  Bool :: "t" where
  "Bool == T+T"

definition
  true :: "i" where
  "true == inl(tt)"

definition
  false :: "i" where
  "false == inr(tt)"

definition
  cond :: "[i,i,i]=>i" where
  "cond(a,b,c) == when(a, %u. b, %u. c)"

lemmas bool_defs = Bool_def true_def false_def cond_def


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

(*formation rule*)
lemma boolF: "Bool type"
apply (unfold bool_defs)
apply (tactic "typechk_tac []")
done


(*introduction rules for true, false*)

lemma boolI_true: "true : Bool"
apply (unfold bool_defs)
apply (tactic "typechk_tac []")
done

lemma boolI_false: "false : Bool"
apply (unfold bool_defs)
apply (tactic "typechk_tac []")
done

(*elimination rule: typing of cond*)
lemma boolE: 
    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
apply (unfold bool_defs)
apply (tactic "typechk_tac []")
apply (erule_tac [!] TE)
apply (tactic "typechk_tac []")
done

lemma boolEL: 
    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]  
     ==> cond(p,a,b) = cond(q,c,d) : C(p)"
apply (unfold bool_defs)
apply (rule PlusEL)
apply (erule asm_rl refl_elem [THEN TEL])+
done

(*computation rules for true, false*)

lemma boolC_true: 
    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
apply (unfold bool_defs)
apply (rule comp_rls)
apply (tactic "typechk_tac []")
apply (erule_tac [!] TE)
apply (tactic "typechk_tac []")
done

lemma boolC_false: 
    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
apply (unfold bool_defs)
apply (rule comp_rls)
apply (tactic "typechk_tac []")
apply (erule_tac [!] TE)
apply (tactic "typechk_tac []")
done

end