src/CTT/Bool.thy
author wenzelm
Sun, 12 Mar 2017 18:50:02 +0100
changeset 65202 187277b77d50
parent 64980 7dc25cf5793e
permissions -rw-r--r--
suppress vacuous messages;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58977
diff changeset
     6
section \<open>The two-element type (booleans and conditionals)\<close>
17441
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
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
     9
  imports CTT
17441
5b5feca0344a converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    10
begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    12
definition Bool :: "t"
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    13
  where "Bool \<equiv> T+T"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    14
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    15
definition true :: "i"
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    16
  where "true \<equiv> inl(tt)"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    17
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    18
definition false :: "i"
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    19
  where "false \<equiv> inr(tt)"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    20
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    21
definition cond :: "[i,i,i]\<Rightarrow>i"
64980
7dc25cf5793e misc tuning;
wenzelm
parents: 63505
diff changeset
    22
  where "cond(a,b,c) \<equiv> when(a, \<lambda>_. b, \<lambda>_. c)"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    23
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    24
lemmas bool_defs = Bool_def true_def false_def cond_def
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    25
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    26
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    27
subsection \<open>Derivation of rules for the type \<open>Bool\<close>\<close>
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    28
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    29
text \<open>Formation rule.\<close>
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    30
lemma boolF: "Bool type"
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    31
  unfolding bool_defs by typechk
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    32
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    33
text \<open>Introduction rules for \<open>true\<close>, \<open>false\<close>.\<close>
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    34
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    35
lemma boolI_true: "true : Bool"
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    36
  unfolding bool_defs by typechk
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    37
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    38
lemma boolI_false: "false : Bool"
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    39
  unfolding bool_defs by typechk
17441
5b5feca0344a converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    40
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    41
text \<open>Elimination rule: typing of \<open>cond\<close>.\<close>
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58972
diff changeset
    42
lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    43
  unfolding bool_defs
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    44
  apply (typechk; erule TE)
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    45
   apply typechk
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    46
  done
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    47
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58972
diff changeset
    48
lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
9576b510f6a2 more symbols;
wenzelm
parents: 58972
diff changeset
    49
  \<Longrightarrow> cond(p,a,b) = cond(q,c,d) : C(p)"
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    50
  unfolding bool_defs
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    51
  apply (rule PlusEL)
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    52
    apply (erule asm_rl refl_elem [THEN TEL])+
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    53
  done
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    54
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    55
text \<open>Computation rules for \<open>true\<close>, \<open>false\<close>.\<close>
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    56
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58972
diff changeset
    57
lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    58
  unfolding bool_defs
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    59
  apply (rule comp_rls)
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    60
    apply typechk
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    61
   apply (erule_tac [!] TE)
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    62
   apply typechk
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    63
  done
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents: 17441
diff changeset
    64
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58972
diff changeset
    65
lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    66
  unfolding bool_defs
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    67
  apply (rule comp_rls)
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    68
    apply typechk
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    69
   apply (erule_tac [!] TE)
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    70
   apply typechk
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
    71
  done
17441
5b5feca0344a converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    72
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
end