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