src/HOLCF/Lift.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16216 279ab2e02089
child 16388 1ff571813848
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/Lift.thy
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     2
    ID:         $Id$
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
     3
    Author:     Olaf Mueller
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     4
*)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     5
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
     6
header {* Lifting types of class type to flat pcpo's *}
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
     7
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     8
theory Lift
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     9
imports Cprod
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    10
begin
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    11
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
    12
defaultsort type
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    13
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    14
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    15
typedef 'a lift = "UNIV :: 'a option set" ..
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    16
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    17
constdefs
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    18
  Undef :: "'a lift"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    19
  "Undef == Abs_lift None"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    20
  Def :: "'a => 'a lift"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    21
  "Def x == Abs_lift (Some x)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    22
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
    23
instance lift :: (type) sq_ord ..
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    24
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    25
defs (overloaded)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    26
  less_lift_def: "x << y == (x=y | x=Undef)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    27
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
    28
instance lift :: (type) po
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    29
proof
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    30
  fix x y z :: "'a lift"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    31
  show "x << x" by (unfold less_lift_def) blast
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    32
  { assume "x << y" and "y << x" thus "x = y" by (unfold less_lift_def) blast }
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    33
  { assume "x << y" and "y << z" thus "x << z" by (unfold less_lift_def) blast }
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    34
qed
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    35
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    36
lemma inst_lift_po: "(op <<) = (\<lambda>x y. x = y | x = Undef)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    37
  -- {* For compatibility with old HOLCF-Version. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    38
  by (simp only: less_lift_def [symmetric])
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    39
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    40
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    41
subsection {* Type lift is pointed *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    42
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    43
lemma minimal_lift [iff]: "Undef << x"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    44
  by (simp add: inst_lift_po)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    45
15930
145651bc64a8 Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents: 15651
diff changeset
    46
lemma UU_lift_def: "(THE u. \<forall>y. u \<sqsubseteq> y) = Undef"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    47
  apply (rule minimal2UU [symmetric])
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    48
  apply (rule minimal_lift)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    49
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    50
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    51
lemma least_lift: "EX x::'a lift. ALL y. x << y"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    52
  apply (rule_tac x = Undef in exI)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    53
  apply (rule minimal_lift [THEN allI])
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    54
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    55
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    56
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    57
subsection {* Type lift is a cpo *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    58
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    59
text {*
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    60
  The following lemmas have already been proved in @{text Pcpo.ML} and
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    61
  @{text Fix.ML}, but there class @{text pcpo} is assumed, although
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    62
  only @{text po} is necessary and a least element. Therefore they are
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    63
  redone here for the @{text po} lift with least element @{text
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    64
  Undef}.
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    65
*}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    66
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    67
lemma flat_imp_chfin_poo: "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    68
  -- {* Tailoring @{text flat_imp_chfin} of @{text Fix.ML} to @{text lift} *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    69
  apply (unfold max_in_chain_def)
16067
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    70
  apply clarify
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    71
  apply (case_tac "ALL i. Y i = Undef")
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    72
   apply simp
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    73
  apply simp
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    74
  apply (erule exE)
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    75
  apply (rule_tac x=i in exI)
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    76
  apply clarify
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    77
  apply (drule chain_mono3, assumption)
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    78
  apply (simp add: less_lift_def)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    79
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    80
16067
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    81
instance lift :: (type) chfin
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    82
  apply intro_classes
c57725e8055a shorted proof that lift is chfin
huffman
parents: 16054
diff changeset
    83
  apply (rule flat_imp_chfin_poo)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    84
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    85
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
    86
instance lift :: (type) pcpo
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    87
  apply intro_classes
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    88
  apply (rule least_lift)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    89
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    90
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    91
lemma inst_lift_pcpo: "UU = Undef"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    92
  -- {* For compatibility with old HOLCF-Version. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    93
  by (simp add: UU_def UU_lift_def)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    94
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    95
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    96
subsection {* Lift as a datatype *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    97
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    98
lemma lift_distinct1: "UU ~= Def x"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    99
  by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   100
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   101
lemma lift_distinct2: "Def x ~= UU"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   102
  by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   103
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   104
lemma Def_inject: "(Def x = Def x') = (x = x')"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   105
  by (simp add: Def_def Abs_lift_inject lift_def)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   106
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   107
lemma lift_induct: "P UU ==> (!!x. P (Def x)) ==> P y"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   108
  apply (induct y)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   109
  apply (induct_tac y)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   110
   apply (simp_all add: Undef_def Def_def inst_lift_pcpo)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   111
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   112
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   113
rep_datatype lift
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   114
  distinct lift_distinct1 lift_distinct2
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   115
  inject Def_inject
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   116
  induction lift_induct
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   117
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   118
lemma Def_not_UU: "Def a ~= UU"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   119
  by simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   120
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   121
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   122
subsection {* Further operations *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   123
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   124
consts
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   125
 flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   126
 flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
   127
 liftpair    ::"'a::type lift * 'b::type lift => ('a * 'b) lift"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   128
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   129
defs
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   130
 flift1_def:
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   131
  "flift1 f == (LAM x. (case x of
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   132
                   UU => UU
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   133
                 | Def y => (f y)))"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   134
 flift2_def:
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   135
  "flift2 f == (LAM x. (case x of
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   136
                   UU => UU
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   137
                 | Def y => Def (f y)))"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   138
 liftpair_def:
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   139
  "liftpair x  == (case (cfst$x) of
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   140
                  UU  => UU
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   141
                | Def x1 => (case (csnd$x) of
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   142
                               UU => UU
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   143
                             | Def x2 => Def (x1,x2)))"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   144
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   145
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   146
declare inst_lift_pcpo [symmetric, simp]
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   147
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   148
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   149
lemma less_lift: "(x::'a lift) << y = (x=y | x=UU)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   150
  by (simp add: inst_lift_po)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   151
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   152
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   153
text {* @{text UU} and @{text Def} *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   154
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   155
lemma Lift_exhaust: "x = UU | (EX y. x = Def y)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   156
  by (induct x) simp_all
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   157
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   158
lemma Lift_cases: "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   159
  by (insert Lift_exhaust) blast
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   160
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   161
lemma not_Undef_is_Def: "(x ~= UU) = (EX y. x = Def y)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   162
  by (cases x) simp_all
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   163
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   164
text {*
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   165
  For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   166
  x} by @{text "Def a"} in conclusion. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   167
16121
wenzelm
parents: 16067
diff changeset
   168
ML {*
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   169
  local val not_Undef_is_Def = thm "not_Undef_is_Def"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   170
  in val def_tac = SIMPSET' (fn ss =>
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   171
    etac (not_Undef_is_Def RS iffD1 RS exE) THEN' asm_simp_tac ss)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   172
  end;
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   173
*}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   174
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   175
lemma Undef_eq_UU: "Undef = UU"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   176
  by (rule inst_lift_pcpo [symmetric])
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   177
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   178
lemma DefE: "Def x = UU ==> R"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   179
  by simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   180
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   181
lemma DefE2: "[| x = Def s; x = UU |] ==> R"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   182
  by simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   183
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   184
lemma Def_inject_less_eq: "Def x << Def y = (x = y)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   185
  by (simp add: less_lift_def)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   186
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   187
lemma Def_less_is_eq [simp]: "Def x << y = (Def x = y)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   188
  by (simp add: less_lift)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   189
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   190
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   191
subsection {* Lift is flat *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   192
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
   193
instance lift :: (type) flat
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   194
proof
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   195
  show "ALL x y::'a lift. x << y --> x = UU | x = y"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   196
    by (simp add: less_lift)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   197
qed
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   198
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   199
defaultsort pcpo
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   200
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   201
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   202
text {*
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   203
  \medskip Two specific lemmas for the combination of LCF and HOL
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   204
  terms.
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   205
*}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   206
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   207
lemma cont_Rep_CFun_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   208
  apply (rule cont2cont_CF1L)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   209
  apply (tactic "resolve_tac cont_lemmas1 1")+
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   210
   apply auto
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   211
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   212
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   213
lemma cont_Rep_CFun_app_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   214
  apply (rule cont2cont_CF1L)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   215
  apply (erule cont_Rep_CFun_app)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   216
  apply assumption
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   217
  done
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   218
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   219
text {* Continuity of if-then-else. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   220
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   221
lemma cont_if: "[| cont f1; cont f2 |] ==> cont (%x. if b then f1 x else f2 x)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   222
  by (cases b) simp_all
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   223
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   224
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   225
subsection {* Continuity Proofs for flift1, flift2, if *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   226
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   227
text {* Need the instance of @{text flat}. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   228
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   229
lemma cont_flift1_arg: "cont (lift_case UU f)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   230
  -- {* @{text flift1} is continuous in its argument itself. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   231
  apply (rule flatdom_strict2cont)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   232
  apply simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   233
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   234
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   235
lemma cont_flift1_not_arg: "!!f. [| !! a. cont (%y. (f y) a) |] ==>
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   236
           cont (%y. lift_case UU (f y))"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   237
  -- {* @{text flift1} is continuous in a variable that occurs only
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   238
    in the @{text Def} branch. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   239
  apply (rule cont2cont_CF1L_rev)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   240
  apply (intro strip)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   241
  apply (case_tac y)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   242
   apply simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   243
  apply simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   244
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   245
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   246
lemma cont_flift1_arg_and_not_arg: "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==>
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   247
    cont (%y. lift_case UU (f y) (g y))"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   248
  -- {* @{text flift1} is continuous in a variable that occurs either
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   249
    in the @{text Def} branch or in the argument. *}
16216
279ab2e02089 renamed variable in cont2cont_app
huffman
parents: 16121
diff changeset
   250
  apply (rule_tac t=g in cont2cont_app)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   251
    apply (rule cont_flift1_not_arg)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   252
    apply auto
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   253
  apply (rule cont_flift1_arg)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   254
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   255
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   256
lemma cont_flift2_arg: "cont (lift_case UU (%y. Def (f y)))"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   257
  -- {* @{text flift2} is continuous in its argument itself. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   258
  apply (rule flatdom_strict2cont)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   259
  apply simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   260
  done
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   261
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   262
text {*
14096
f79d139c7e46 corrected markup text
oheimb
parents: 12338
diff changeset
   263
  \medskip Extension of @{text cont_tac} and installation of simplifier.
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   264
*}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   265
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   266
lemmas cont_lemmas_ext [simp] =
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   267
  cont_flift1_arg cont_flift2_arg
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   268
  cont_flift1_arg_and_not_arg cont2cont_CF1L_rev2
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   269
  cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   270
16121
wenzelm
parents: 16067
diff changeset
   271
ML {*
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   272
val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   273
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   274
fun cont_tac  i = resolve_tac cont_lemmas2 i;
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   275
fun cont_tacR i = REPEAT (cont_tac i);
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   276
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   277
local val flift1_def = thm "flift1_def" and flift2_def = thm "flift2_def"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   278
in fun cont_tacRs i =
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   279
  simp_tac (simpset() addsimps [flift1_def, flift2_def]) i THEN
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   280
  REPEAT (cont_tac i)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   281
end;
15651
4b393520846e Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
huffman
parents: 15577
diff changeset
   282
*}
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   283
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   284
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   285
subsection {* flift1, flift2 *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   286
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   287
lemma flift1_Def [simp]: "flift1 f$(Def x) = (f x)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   288
  by (simp add: flift1_def)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   289
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   290
lemma flift2_Def [simp]: "flift2 f$(Def x) = Def (f x)"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   291
  by (simp add: flift2_def)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   292
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   293
lemma flift1_UU [simp]: "flift1 f$UU = UU"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   294
  by (simp add: flift1_def)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   295
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   296
lemma flift2_UU [simp]: "flift2 f$UU = UU"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   297
  by (simp add: flift2_def)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   298
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   299
lemma flift2_nUU [simp]: "x~=UU ==> (flift2 f)$x~=UU"
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   300
  by (tactic "def_tac 1")
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   301
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   302
end