src/HOLCF/Tr.thy
author huffman
Thu, 03 Nov 2005 01:45:52 +0100
changeset 18081 fe15796b257d
parent 18070 b653e18f0a41
child 25131 2c8caac48ade
permissions -rw-r--r--
changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     1
(*  Title:      HOLCF/Tr.thy
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     2
    ID:         $Id$
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     3
    Author:     Franz Regensburger
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     4
16070
4a83dd540b88 removed LICENCE note -- everything is subject to Isabelle licence as
wenzelm
parents: 15649
diff changeset
     5
Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     6
*)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     7
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     8
header {* The type of lifted booleans *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     9
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    10
theory Tr
16228
9b5b0c92230a import Fix is unnecessary
huffman
parents: 16121
diff changeset
    11
imports Lift
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    12
begin
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    13
16631
58b4a689ae85 defaultsort pcpo
huffman
parents: 16228
diff changeset
    14
defaultsort pcpo
58b4a689ae85 defaultsort pcpo
huffman
parents: 16228
diff changeset
    15
2782
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    16
types
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    17
  tr = "bool lift"
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    18
2766
3e90c5187ce1 "bool lift" now syntax instead of type abbrev;
wenzelm
parents: 2719
diff changeset
    19
translations
2782
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    20
  "tr" <= (type) "bool lift" 
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    21
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    22
consts
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    23
  TT     :: "tr"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    24
  FF     :: "tr"
18081
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    25
  trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c"
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    26
  trand  :: "tr \<rightarrow> tr \<rightarrow> tr"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    27
  tror   :: "tr \<rightarrow> tr \<rightarrow> tr"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    28
  neg    :: "tr \<rightarrow> tr"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    29
  If2    :: "[tr, 'c, 'c] \<Rightarrow> 'c"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    30
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    31
syntax
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    32
  "@cifte"   :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60)
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    33
  "@andalso" :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ andalso _" [36,35] 35)
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    34
  "@orelse"  :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ orelse _"  [31,30] 30)
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    35
 
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    36
translations
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    37
  "x andalso y" == "trand\<cdot>x\<cdot>y"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    38
  "x orelse y"  == "tror\<cdot>x\<cdot>y"
18081
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    39
  "If b then e1 else e2 fi" == "trifte\<cdot>e1\<cdot>e2\<cdot>b"
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    40
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    41
translations
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    42
  "\<Lambda> TT. t" == "trifte\<cdot>t\<cdot>\<bottom>"
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    43
  "\<Lambda> FF. t" == "trifte\<cdot>\<bottom>\<cdot>t"
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    44
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    45
defs
18081
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    46
  TT_def:      "TT \<equiv> Def True"
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    47
  FF_def:      "FF \<equiv> Def False"
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    48
  neg_def:     "neg \<equiv> flift2 Not"
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    49
  ifte_def:    "trifte \<equiv> \<Lambda> t e. FLIFT b. if b then t else e"
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    50
  andalso_def: "trand \<equiv> \<Lambda> x y. If x then y else FF fi"
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    51
  orelse_def:  "tror \<equiv> \<Lambda> x y. If x then TT else y fi"
fe15796b257d changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman
parents: 18070
diff changeset
    52
  If2_def:     "If2 Q x y \<equiv> If Q then x else y fi"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    53
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    54
text {* Exhaustion and Elimination for type @{typ tr} *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    55
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    56
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    57
apply (unfold FF_def TT_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    58
apply (induct_tac "t")
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    59
apply fast
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    60
apply fast
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    61
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    62
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    63
lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    64
apply (rule Exh_tr [THEN disjE])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    65
apply fast
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    66
apply (erule disjE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    67
apply fast
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    68
apply fast
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    69
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    70
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    71
text {* tactic for tr-thms with case split *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    72
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    73
lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    74
(*
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    75
fun prover t =  prove_goal thy t
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    76
 (fn prems =>
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    77
        [
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    78
        (res_inst_tac [("p","y")] trE 1),
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    79
	(REPEAT(asm_simp_tac (simpset() addsimps 
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    80
		[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    81
	])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    82
*)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    83
text {* distinctness for type @{typ tr} *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    84
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    85
lemma dist_less_tr [simp]:
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    86
  "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    87
by (simp_all add: tr_defs)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    88
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    89
lemma dist_eq_tr [simp]:
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    90
  "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    91
by (simp_all add: tr_defs)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    92
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    93
text {* lemmas about andalso, orelse, neg and if *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    94
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    95
lemma ifte_thms [simp]:
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
    96
  "If \<bottom> then e1 else e2 fi = \<bottom>"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    97
  "If FF then e1 else e2 fi = e2"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    98
  "If TT then e1 else e2 fi = e1"
16756
e05c8039873a simplified proof of ifte_thms, removed ifte_simp
huffman
parents: 16631
diff changeset
    99
by (simp_all add: ifte_def TT_def FF_def)
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   100
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   101
lemma andalso_thms [simp]:
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   102
  "(TT andalso y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   103
  "(FF andalso y) = FF"
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   104
  "(\<bottom> andalso y) = \<bottom>"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   105
  "(y andalso TT) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   106
  "(y andalso y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   107
apply (unfold andalso_def, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   108
apply (rule_tac p=y in trE, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   109
apply (rule_tac p=y in trE, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   110
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   111
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   112
lemma orelse_thms [simp]:
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   113
  "(TT orelse y) = TT"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   114
  "(FF orelse y) = y"
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   115
  "(\<bottom> orelse y) = \<bottom>"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   116
  "(y orelse FF) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   117
  "(y orelse y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   118
apply (unfold orelse_def, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   119
apply (rule_tac p=y in trE, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   120
apply (rule_tac p=y in trE, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   121
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   122
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   123
lemma neg_thms [simp]:
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   124
  "neg\<cdot>TT = FF"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   125
  "neg\<cdot>FF = TT"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   126
  "neg\<cdot>\<bottom> = \<bottom>"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   127
by (simp_all add: neg_def TT_def FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   128
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   129
text {* split-tac for If via If2 because the constant has to be a constant *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   130
  
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   131
lemma split_If2: 
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   132
  "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   133
apply (unfold If2_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   134
apply (rule_tac p = "Q" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   135
apply (simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   136
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   137
16121
wenzelm
parents: 16070
diff changeset
   138
ML {*
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   139
val split_If_tac =
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   140
  simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   141
    THEN' (split_tac [thm "split_If2"])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   142
*}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   143
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   144
subsection "Rewriting of HOLCF operations to HOL functions"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   145
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   146
lemma andalso_or: 
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   147
  "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   148
apply (rule_tac p = "t" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   149
apply simp_all
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   150
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   151
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   152
lemma andalso_and:
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   153
  "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   154
apply (rule_tac p = "t" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   155
apply simp_all
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   156
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   157
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   158
lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   159
by (simp add: FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   160
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   161
lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   162
by (simp add: FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   163
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   164
lemma Def_bool3 [simp]: "(Def x = TT) = x"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   165
by (simp add: TT_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   166
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   167
lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   168
by (simp add: TT_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   169
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   170
lemma If_and_if: 
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   171
  "(If Def P then A else B fi) = (if P then A else B)"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   172
apply (rule_tac p = "Def P" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   173
apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   174
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   175
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   176
subsection {* Compactness *}
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   177
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   178
lemma compact_TT [simp]: "compact TT"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   179
by (rule compact_chfin)
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   180
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   181
lemma compact_FF [simp]: "compact FF"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   182
by (rule compact_chfin)
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   183
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   184
end