src/HOLCF/Tr.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16121 a80aa66d2271
child 16228 9b5b0c92230a
permissions -rw-r--r--
New theory with lemmas for the fixrec package
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
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    11
imports Lift Fix
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
2782
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    14
types
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    15
  tr = "bool lift"
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    16
2766
3e90c5187ce1 "bool lift" now syntax instead of type abbrev;
wenzelm
parents: 2719
diff changeset
    17
translations
2782
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    18
  "tr" <= (type) "bool lift" 
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    19
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    20
consts
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    21
	TT              :: "tr"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    22
	FF              :: "tr"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    23
        Icifte          :: "tr -> 'c -> 'c -> 'c"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    24
        trand           :: "tr -> tr -> tr"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    25
        tror            :: "tr -> tr -> tr"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    26
        neg             :: "tr -> tr"
3036
5aa3bb94b729 deleted definitions for blift and plift
mueller
parents: 2782
diff changeset
    27
        If2             :: "tr=>'c=>'c=>'c"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    28
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    29
syntax  "@cifte"        :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    30
        "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    31
        "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    32
 
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    33
translations 
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 3842
diff changeset
    34
	     "x andalso y" == "trand$x$y"
a7897aebbffc *** empty log message ***
nipkow
parents: 3842
diff changeset
    35
             "x orelse y"  == "tror$x$y"
a7897aebbffc *** empty log message ***
nipkow
parents: 3842
diff changeset
    36
             "If b then e1 else e2 fi" == "Icifte$b$e1$e2"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    37
defs
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    38
  TT_def:      "TT==Def True"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    39
  FF_def:      "FF==Def False"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    40
  neg_def:     "neg == flift2 Not"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    41
  ifte_def:    "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    42
  andalso_def: "trand == (LAM x y. If x then y else FF fi)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    43
  orelse_def:  "tror == (LAM x y. If x then TT else y fi)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    44
  If2_def:     "If2 Q x y == If Q then x else y fi"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    45
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    46
text {* Exhaustion and Elimination for type @{typ tr} *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    47
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    48
lemma Exh_tr: "t=UU | t = TT | t = FF"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    49
apply (unfold FF_def TT_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    50
apply (induct_tac "t")
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    51
apply fast
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    52
apply fast
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    53
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    54
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    55
lemma trE: "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    56
apply (rule Exh_tr [THEN disjE])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    57
apply fast
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    58
apply (erule disjE)
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
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    63
text {* tactic for tr-thms with case split *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    64
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    65
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
    66
(*
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    67
fun prover t =  prove_goal thy t
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    68
 (fn prems =>
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    69
        [
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    70
        (res_inst_tac [("p","y")] trE 1),
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    71
	(REPEAT(asm_simp_tac (simpset() addsimps 
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    72
		[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    73
	])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    74
*)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    75
text {* distinctness for type @{typ tr} *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    76
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    77
lemma dist_less_tr [simp]: "~TT << UU" "~FF << UU" "~TT << FF" "~FF << TT"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    78
by (simp_all add: tr_defs)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    79
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    80
lemma dist_eq_tr [simp]: "TT~=UU" "FF~=UU" "TT~=FF" "UU~=TT" "UU~=FF" "FF~=TT"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    81
by (simp_all add: tr_defs)
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 {* lemmas about andalso, orelse, neg and if *}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    84
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    85
lemma ifte_simp:
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    86
  "If x then e1 else e2 fi =
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    87
    flift1 (%b. if b then e1 else e2)$x"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    88
apply (unfold ifte_def TT_def FF_def flift1_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    89
apply (simp add: cont_flift1_arg cont_if)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    90
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    91
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    92
lemma ifte_thms [simp]:
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    93
  "If UU then e1 else e2 fi = UU"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    94
  "If FF then e1 else e2 fi = e2"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    95
  "If TT then e1 else e2 fi = e1"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    96
by (simp_all add: ifte_simp TT_def FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    97
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    98
lemma andalso_thms [simp]:
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    99
  "(TT andalso y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   100
  "(FF andalso y) = FF"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   101
  "(UU andalso y) = UU"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   102
  "(y andalso TT) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   103
  "(y andalso y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   104
apply (unfold andalso_def, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   105
apply (rule_tac p=y in trE, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   106
apply (rule_tac p=y in trE, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   107
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   108
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   109
lemma orelse_thms [simp]:
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   110
  "(TT orelse y) = TT"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   111
  "(FF orelse y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   112
  "(UU orelse y) = UU"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   113
  "(y orelse FF) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   114
  "(y orelse y) = y"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   115
apply (unfold orelse_def, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   116
apply (rule_tac p=y in trE, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   117
apply (rule_tac p=y in trE, simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   118
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   119
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   120
lemma neg_thms [simp]:
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   121
  "neg$TT = FF"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   122
  "neg$FF = TT"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   123
  "neg$UU = UU"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   124
by (simp_all add: neg_def TT_def FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   125
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   126
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
   127
  
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   128
lemma split_If2: 
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   129
  "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))"  
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   130
apply (unfold If2_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   131
apply (rule_tac p = "Q" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   132
apply (simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   133
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   134
16121
wenzelm
parents: 16070
diff changeset
   135
ML {*
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   136
val split_If_tac =
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   137
  simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   138
    THEN' (split_tac [thm "split_If2"])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   139
*}
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   140
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   141
subsection "Rewriting of HOLCF operations to HOL functions"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   142
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   143
lemma andalso_or: 
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   144
"!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   145
apply (rule_tac p = "t" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   146
apply simp_all
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   147
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   148
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   149
lemma andalso_and: "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   150
apply (rule_tac p = "t" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   151
apply simp_all
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   152
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   153
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   154
lemma Def_bool1 [simp]: "(Def x ~= FF) = x"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   155
by (simp add: FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   156
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   157
lemma Def_bool2 [simp]: "(Def x = FF) = (~x)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   158
by (simp add: FF_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   159
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   160
lemma Def_bool3 [simp]: "(Def x = TT) = x"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   161
by (simp add: TT_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   162
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   163
lemma Def_bool4 [simp]: "(Def x ~= TT) = (~x)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   164
by (simp add: TT_def)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   165
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   166
lemma If_and_if: 
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   167
  "(If Def P then A else B fi)= (if P then A else B)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   168
apply (rule_tac p = "Def P" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   169
apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   170
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   171
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   172
subsection "admissibility"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   173
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   174
text {*
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   175
   The following rewrite rules for admissibility should in the future be 
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   176
   replaced by a more general admissibility test that also checks 
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   177
   chain-finiteness, of which these lemmata are specific examples
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   178
*}
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 adm_trick_1: "(x~=FF) = (x=TT|x=UU)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   181
apply (rule_tac p = "x" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   182
apply (simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   183
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   184
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   185
lemma adm_trick_2: "(x~=TT) = (x=FF|x=UU)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   186
apply (rule_tac p = "x" in trE)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   187
apply (simp_all)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   188
done
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   189
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   190
lemmas adm_tricks = adm_trick_1 adm_trick_2
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   191
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   192
lemma adm_nTT [simp]: "cont(f) ==> adm (%x. (f x)~=TT)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   193
by (simp add: adm_tricks)
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   194
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   195
lemma adm_nFF [simp]: "cont(f) ==> adm (%x. (f x)~=FF)"
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
   196
by (simp add: adm_tricks)
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   197
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   198
end