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