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