src/HOL/HOLCF/Tr.thy
author wenzelm
Mon, 19 Jan 2015 20:39:01 +0100
changeset 59409 b7cfe12acf2e
parent 58956 a816aa3ff391
child 62175 8ffc4d0e652d
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41295
diff changeset
     1
(*  Title:      HOL/HOLCF/Tr.thy
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     2
    Author:     Franz Regensburger
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     3
*)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     4
58880
0baae4311a9f modernized header;
wenzelm
parents: 51717
diff changeset
     5
section {* The type of lifted booleans *}
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     6
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     7
theory Tr
16228
9b5b0c92230a import Fix is unnecessary
huffman
parents: 16121
diff changeset
     8
imports Lift
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     9
begin
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    10
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    11
subsection {* Type definition and constructors *}
16631
58b4a689ae85 defaultsort pcpo
huffman
parents: 16228
diff changeset
    12
41295
5b5388d4ccc9 types -> type_synonym
huffman
parents: 41182
diff changeset
    13
type_synonym
2782
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    14
  tr = "bool lift"
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    15
2766
3e90c5187ce1 "bool lift" now syntax instead of type abbrev;
wenzelm
parents: 2719
diff changeset
    16
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 31076
diff changeset
    17
  (type) "tr" <= (type) "bool lift"
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    18
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    19
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    20
  TT :: "tr" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    21
  "TT = Def True"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    22
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    23
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    24
  FF :: "tr" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    25
  "FF = Def False"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    26
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    27
text {* Exhaustion and Elimination for type @{typ tr} *}
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    28
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    29
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    30
unfolding FF_def TT_def by (induct t) auto
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    31
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
    32
lemma trE [case_names bottom TT FF, cases type: tr]:
35783
38538bfe9ca6 declare case_names for various induction rules
huffman
parents: 35431
diff changeset
    33
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    34
unfolding FF_def TT_def by (induct p) auto
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    35
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
    36
lemma tr_induct [case_names bottom TT FF, induct type: tr]:
35783
38538bfe9ca6 declare case_names for various induction rules
huffman
parents: 35431
diff changeset
    37
  "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
    38
by (cases x) simp_all
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    39
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    40
text {* distinctness for type @{typ tr} *}
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    41
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    42
lemma dist_below_tr [simp]:
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
    43
  "TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT"
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    44
unfolding TT_def FF_def by simp_all
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    45
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    46
lemma dist_eq_tr [simp]:
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    47
  "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    48
unfolding TT_def FF_def by simp_all
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    49
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    50
lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
    51
by (induct x) simp_all
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    52
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    53
lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
    54
by (induct x) simp_all
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    55
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
    56
lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF"
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
    57
by (induct x) simp_all
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    58
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
    59
lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT"
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
    60
by (induct x) simp_all
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    61
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    62
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    63
subsection {* Case analysis *}
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    64
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35783
diff changeset
    65
default_sort pcpo
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    66
40324
b5e1ab22198a rename constant trifte to tr_case
huffman
parents: 40322
diff changeset
    67
definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a" where
b5e1ab22198a rename constant trifte to tr_case
huffman
parents: 40322
diff changeset
    68
  "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
    69
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18081
diff changeset
    70
abbreviation
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
    71
  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
    72
where
40324
b5e1ab22198a rename constant trifte to tr_case
huffman
parents: 40322
diff changeset
    73
  "If b then e1 else e2 == tr_case\<cdot>e1\<cdot>e2\<cdot>b"
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18081
diff changeset
    74
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    75
translations
40324
b5e1ab22198a rename constant trifte to tr_case
huffman
parents: 40322
diff changeset
    76
  "\<Lambda> (XCONST TT). t" == "CONST tr_case\<cdot>t\<cdot>\<bottom>"
b5e1ab22198a rename constant trifte to tr_case
huffman
parents: 40322
diff changeset
    77
  "\<Lambda> (XCONST FF). t" == "CONST tr_case\<cdot>\<bottom>\<cdot>t"
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    78
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    79
lemma ifte_thms [simp]:
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
    80
  "If \<bottom> then e1 else e2 = \<bottom>"
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
    81
  "If FF then e1 else e2 = e2"
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
    82
  "If TT then e1 else e2 = e1"
40324
b5e1ab22198a rename constant trifte to tr_case
huffman
parents: 40322
diff changeset
    83
by (simp_all add: tr_case_def TT_def FF_def)
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    84
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    85
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    86
subsection {* Boolean connectives *}
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
    87
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    88
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    89
  trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
    90
  andalso_def: "trand = (\<Lambda> x y. If x then y else FF)"
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18081
diff changeset
    91
abbreviation
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18081
diff changeset
    92
  andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18081
diff changeset
    93
  "x andalso y == trand\<cdot>x\<cdot>y"
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18081
diff changeset
    94
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    95
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
    96
  tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
    97
  orelse_def: "tror = (\<Lambda> x y. If x then TT else y)"
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18081
diff changeset
    98
abbreviation
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18081
diff changeset
    99
  orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18081
diff changeset
   100
  "x orelse y == tror\<cdot>x\<cdot>y"
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   101
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   102
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   103
  neg :: "tr \<rightarrow> tr" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   104
  "neg = flift2 Not"
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   105
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   106
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   107
  If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
   108
  "If2 Q x y = (If Q then x else y)"
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   109
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   110
text {* tactic for tr-thms with case split *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   111
40324
b5e1ab22198a rename constant trifte to tr_case
huffman
parents: 40322
diff changeset
   112
lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def
27148
5b78e50adc49 removed dead code;
wenzelm
parents: 25135
diff changeset
   113
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   114
text {* lemmas about andalso, orelse, neg and if *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   115
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   116
lemma andalso_thms [simp]:
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   117
  "(TT andalso y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   118
  "(FF andalso y) = FF"
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   119
  "(\<bottom> andalso y) = \<bottom>"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   120
  "(y andalso TT) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   121
  "(y andalso y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   122
apply (unfold andalso_def, simp_all)
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
   123
apply (cases y, simp_all)
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
   124
apply (cases y, simp_all)
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   125
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   126
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   127
lemma orelse_thms [simp]:
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   128
  "(TT orelse y) = TT"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   129
  "(FF orelse y) = y"
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   130
  "(\<bottom> orelse y) = \<bottom>"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   131
  "(y orelse FF) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   132
  "(y orelse y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   133
apply (unfold orelse_def, simp_all)
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
   134
apply (cases y, simp_all)
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
   135
apply (cases y, simp_all)
15649
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
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   138
lemma neg_thms [simp]:
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   139
  "neg\<cdot>TT = FF"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   140
  "neg\<cdot>FF = TT"
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   141
  "neg\<cdot>\<bottom> = \<bottom>"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   142
by (simp_all add: neg_def TT_def FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   143
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   144
text {* split-tac for If via If2 because the constant has to be a constant *}
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   145
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   146
lemma split_If2:
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   147
  "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
   148
apply (unfold If2_def)
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
   149
apply (cases Q)
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   150
apply (simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   151
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   152
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 48659
diff changeset
   153
(* FIXME unused!? *)
16121
wenzelm
parents: 16070
diff changeset
   154
ML {*
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 48659
diff changeset
   155
fun split_If_tac ctxt =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 48659
diff changeset
   156
  simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym])
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 58880
diff changeset
   157
    THEN' (split_tac ctxt [@{thm split_If2}])
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   158
*}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   159
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   160
subsection "Rewriting of HOLCF operations to HOL functions"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   161
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   162
lemma andalso_or:
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   163
  "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
   164
apply (cases t)
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   165
apply simp_all
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   166
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   167
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   168
lemma andalso_and:
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   169
  "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
   170
apply (cases t)
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   171
apply simp_all
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   172
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   173
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   174
lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   175
by (simp add: FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   176
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   177
lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   178
by (simp add: FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   179
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   180
lemma Def_bool3 [simp]: "(Def x = TT) = x"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   181
by (simp add: TT_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   182
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   183
lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   184
by (simp add: TT_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   185
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 25131
diff changeset
   186
lemma If_and_if:
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 36452
diff changeset
   187
  "(If Def P then A else B) = (if P then A else B)"
48659
40a87b4dac19 declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents: 42151
diff changeset
   188
apply (cases "Def P")
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   189
apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   190
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   191
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   192
subsection {* Compactness *}
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   193
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
   194
lemma compact_TT: "compact TT"
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   195
by (rule compact_chfin)
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   196
27294
c11e716fafeb added some lemmas; reorganized into sections; tuned proofs
huffman
parents: 27148
diff changeset
   197
lemma compact_FF: "compact FF"
18070
b653e18f0a41 cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents: 16756
diff changeset
   198
by (rule compact_chfin)
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   199
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   200
end