src/HOLCF/Tr.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 31076 99fe356cbbc2
child 35431 8758fe1fc9f8
permissions -rw-r--r--
merged
slotosch@2640
     1
(*  Title:      HOLCF/Tr.thy
slotosch@2640
     2
    Author:     Franz Regensburger
slotosch@2640
     3
*)
slotosch@2640
     4
huffman@15649
     5
header {* The type of lifted booleans *}
huffman@15649
     6
huffman@15649
     7
theory Tr
huffman@16228
     8
imports Lift
huffman@15649
     9
begin
slotosch@2640
    10
huffman@27294
    11
subsection {* Type definition and constructors *}
huffman@16631
    12
wenzelm@2782
    13
types
wenzelm@2782
    14
  tr = "bool lift"
wenzelm@2782
    15
wenzelm@2766
    16
translations
wenzelm@25135
    17
  "tr" <= (type) "bool lift"
wenzelm@25135
    18
wenzelm@25135
    19
definition
wenzelm@25135
    20
  TT :: "tr" where
wenzelm@25135
    21
  "TT = Def True"
slotosch@2640
    22
wenzelm@25135
    23
definition
wenzelm@25135
    24
  FF :: "tr" where
wenzelm@25135
    25
  "FF = Def False"
slotosch@2640
    26
huffman@27294
    27
text {* Exhaustion and Elimination for type @{typ tr} *}
huffman@27294
    28
huffman@27294
    29
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
huffman@27294
    30
unfolding FF_def TT_def by (induct t) auto
huffman@27294
    31
huffman@27294
    32
lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@27294
    33
unfolding FF_def TT_def by (induct p) auto
huffman@27294
    34
huffman@27294
    35
lemma tr_induct: "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
huffman@27294
    36
by (cases x rule: trE) simp_all
huffman@27294
    37
huffman@27294
    38
text {* distinctness for type @{typ tr} *}
huffman@27294
    39
huffman@31076
    40
lemma dist_below_tr [simp]:
huffman@27294
    41
  "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
huffman@27294
    42
unfolding TT_def FF_def by simp_all
huffman@27294
    43
huffman@27294
    44
lemma dist_eq_tr [simp]:
huffman@27294
    45
  "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
huffman@27294
    46
unfolding TT_def FF_def by simp_all
huffman@27294
    47
huffman@31076
    48
lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
huffman@27294
    49
by (induct x rule: tr_induct) simp_all
huffman@27294
    50
huffman@31076
    51
lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
huffman@27294
    52
by (induct x rule: tr_induct) simp_all
huffman@27294
    53
huffman@31076
    54
lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
huffman@27294
    55
by (induct x rule: tr_induct) simp_all
huffman@27294
    56
huffman@31076
    57
lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
huffman@27294
    58
by (induct x rule: tr_induct) simp_all
huffman@27294
    59
huffman@27294
    60
huffman@27294
    61
subsection {* Case analysis *}
huffman@27294
    62
huffman@27294
    63
defaultsort pcpo
huffman@27294
    64
wenzelm@25135
    65
definition
wenzelm@25135
    66
  trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
wenzelm@25135
    67
  ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"
wenzelm@25131
    68
abbreviation
wenzelm@25131
    69
  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(3If _/ (then _/ else _) fi)" 60)  where
wenzelm@25131
    70
  "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
wenzelm@25131
    71
huffman@27294
    72
translations
huffman@27294
    73
  "\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
huffman@27294
    74
  "\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
huffman@27294
    75
huffman@27294
    76
lemma ifte_thms [simp]:
huffman@27294
    77
  "If \<bottom> then e1 else e2 fi = \<bottom>"
huffman@27294
    78
  "If FF then e1 else e2 fi = e2"
huffman@27294
    79
  "If TT then e1 else e2 fi = e1"
huffman@27294
    80
by (simp_all add: ifte_def TT_def FF_def)
huffman@27294
    81
huffman@27294
    82
huffman@27294
    83
subsection {* Boolean connectives *}
huffman@27294
    84
wenzelm@25135
    85
definition
wenzelm@25135
    86
  trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
wenzelm@25135
    87
  andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)"
wenzelm@25131
    88
abbreviation
wenzelm@25131
    89
  andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
wenzelm@25131
    90
  "x andalso y == trand\<cdot>x\<cdot>y"
wenzelm@25131
    91
wenzelm@25135
    92
definition
wenzelm@25135
    93
  tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
wenzelm@25135
    94
  orelse_def: "tror = (\<Lambda> x y. If x then TT else y fi)"
wenzelm@25131
    95
abbreviation
wenzelm@25131
    96
  orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
wenzelm@25131
    97
  "x orelse y == tror\<cdot>x\<cdot>y"
wenzelm@25135
    98
wenzelm@25135
    99
definition
wenzelm@25135
   100
  neg :: "tr \<rightarrow> tr" where
wenzelm@25135
   101
  "neg = flift2 Not"
huffman@18070
   102
wenzelm@25135
   103
definition
wenzelm@25135
   104
  If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
wenzelm@25135
   105
  "If2 Q x y = (If Q then x else y fi)"
wenzelm@25135
   106
huffman@15649
   107
text {* tactic for tr-thms with case split *}
huffman@15649
   108
huffman@15649
   109
lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
wenzelm@27148
   110
huffman@15649
   111
text {* lemmas about andalso, orelse, neg and if *}
huffman@15649
   112
huffman@15649
   113
lemma andalso_thms [simp]:
huffman@15649
   114
  "(TT andalso y) = y"
huffman@15649
   115
  "(FF andalso y) = FF"
huffman@18070
   116
  "(\<bottom> andalso y) = \<bottom>"
huffman@15649
   117
  "(y andalso TT) = y"
huffman@15649
   118
  "(y andalso y) = y"
huffman@15649
   119
apply (unfold andalso_def, simp_all)
huffman@27294
   120
apply (cases y rule: trE, simp_all)
huffman@27294
   121
apply (cases y rule: trE, simp_all)
huffman@15649
   122
done
huffman@15649
   123
huffman@15649
   124
lemma orelse_thms [simp]:
huffman@15649
   125
  "(TT orelse y) = TT"
huffman@15649
   126
  "(FF orelse y) = y"
huffman@18070
   127
  "(\<bottom> orelse y) = \<bottom>"
huffman@15649
   128
  "(y orelse FF) = y"
huffman@15649
   129
  "(y orelse y) = y"
huffman@15649
   130
apply (unfold orelse_def, simp_all)
huffman@27294
   131
apply (cases y rule: trE, simp_all)
huffman@27294
   132
apply (cases y rule: trE, simp_all)
huffman@15649
   133
done
huffman@15649
   134
huffman@15649
   135
lemma neg_thms [simp]:
huffman@18070
   136
  "neg\<cdot>TT = FF"
huffman@18070
   137
  "neg\<cdot>FF = TT"
huffman@18070
   138
  "neg\<cdot>\<bottom> = \<bottom>"
huffman@15649
   139
by (simp_all add: neg_def TT_def FF_def)
huffman@15649
   140
huffman@15649
   141
text {* split-tac for If via If2 because the constant has to be a constant *}
wenzelm@25135
   142
wenzelm@25135
   143
lemma split_If2:
huffman@18070
   144
  "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
huffman@15649
   145
apply (unfold If2_def)
huffman@15649
   146
apply (rule_tac p = "Q" in trE)
huffman@15649
   147
apply (simp_all)
huffman@15649
   148
done
huffman@15649
   149
wenzelm@16121
   150
ML {*
huffman@15649
   151
val split_If_tac =
wenzelm@25135
   152
  simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym])
wenzelm@25135
   153
    THEN' (split_tac [@{thm split_If2}])
huffman@15649
   154
*}
huffman@15649
   155
huffman@15649
   156
subsection "Rewriting of HOLCF operations to HOL functions"
huffman@15649
   157
wenzelm@25135
   158
lemma andalso_or:
huffman@18070
   159
  "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
huffman@15649
   160
apply (rule_tac p = "t" in trE)
huffman@15649
   161
apply simp_all
huffman@15649
   162
done
huffman@15649
   163
huffman@18070
   164
lemma andalso_and:
huffman@18070
   165
  "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
huffman@15649
   166
apply (rule_tac p = "t" in trE)
huffman@15649
   167
apply simp_all
huffman@15649
   168
done
huffman@15649
   169
huffman@18070
   170
lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x"
huffman@15649
   171
by (simp add: FF_def)
huffman@15649
   172
huffman@18070
   173
lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)"
huffman@15649
   174
by (simp add: FF_def)
huffman@15649
   175
huffman@15649
   176
lemma Def_bool3 [simp]: "(Def x = TT) = x"
huffman@15649
   177
by (simp add: TT_def)
huffman@15649
   178
huffman@18070
   179
lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
huffman@15649
   180
by (simp add: TT_def)
huffman@15649
   181
wenzelm@25135
   182
lemma If_and_if:
huffman@18070
   183
  "(If Def P then A else B fi) = (if P then A else B)"
huffman@15649
   184
apply (rule_tac p = "Def P" in trE)
huffman@15649
   185
apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
huffman@15649
   186
done
huffman@15649
   187
huffman@18070
   188
subsection {* Compactness *}
huffman@15649
   189
huffman@27294
   190
lemma compact_TT: "compact TT"
huffman@18070
   191
by (rule compact_chfin)
huffman@15649
   192
huffman@27294
   193
lemma compact_FF: "compact FF"
huffman@18070
   194
by (rule compact_chfin)
slotosch@2640
   195
slotosch@2640
   196
end