src/HOLCF/Lift.thy
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 19764 372065f34795
child 25131 2c8caac48ade
permissions -rw-r--r--
moved lfp_induct2 here
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
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
     9
imports Discrete Up Cprod
15577
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
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    14
pcpodef 'a lift = "UNIV :: 'a discr u set"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    15
by simp
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    16
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    17
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    18
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    19
constdefs
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    20
  Def :: "'a \<Rightarrow> 'a lift"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    21
  "Def x \<equiv> Abs_lift (up\<cdot>(Discr x))"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    22
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    23
subsection {* Lift as a datatype *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    24
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    25
lemma lift_distinct1: "\<bottom> \<noteq> Def x"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    26
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    27
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    28
lemma lift_distinct2: "Def x \<noteq> \<bottom>"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    29
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    30
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    31
lemma Def_inject: "(Def x = Def y) = (x = y)"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    32
by (simp add: Def_def Abs_lift_inject lift_def)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    33
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    34
lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    35
apply (induct y)
16755
fd02f9d06e43 renamed upE1 to upE; added simp rule cont2cont_flift1
huffman
parents: 16749
diff changeset
    36
apply (rule_tac p=y in upE)
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    37
apply (simp add: Abs_lift_strict)
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    38
apply (case_tac x)
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    39
apply (simp add: Def_def)
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    40
done
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    41
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    42
rep_datatype lift
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    43
  distinct lift_distinct1 lift_distinct2
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    44
  inject Def_inject
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    45
  induction lift_induct
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    46
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    47
lemma Def_not_UU: "Def a \<noteq> UU"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    48
  by simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    49
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    50
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    51
text {* @{term UU} and @{term Def} *}
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    52
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    53
lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    54
  by (induct x) simp_all
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    55
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    56
lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    57
  by (insert Lift_exhaust) blast
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    58
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    59
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    60
  by (cases x) simp_all
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    61
16630
83bf468b1dc7 added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents: 16555
diff changeset
    62
lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
83bf468b1dc7 added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents: 16555
diff changeset
    63
  by (cases x) simp_all
83bf468b1dc7 added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents: 16555
diff changeset
    64
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    65
text {*
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    66
  For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    67
  x} by @{text "Def a"} in conclusion. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    68
16121
wenzelm
parents: 16067
diff changeset
    69
ML {*
16630
83bf468b1dc7 added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents: 16555
diff changeset
    70
  local val lift_definedE = thm "lift_definedE"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    71
  in val def_tac = SIMPSET' (fn ss =>
16630
83bf468b1dc7 added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents: 16555
diff changeset
    72
    etac lift_definedE THEN' asm_simp_tac ss)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    73
  end;
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    74
*}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    75
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    76
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    77
  by simp
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    78
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    79
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    80
  by simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    81
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    82
lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y = (x = y)"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    83
by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    84
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    85
lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y = (Def x = y)"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    86
apply (induct y)
19440
b2877e230b07 add lemma less_UU_iff as default simp rule
huffman
parents: 18092
diff changeset
    87
apply simp
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    88
apply (simp add: Def_inject_less_eq)
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    89
done
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    90
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    91
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    92
subsection {* Lift is flat *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    93
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    94
lemma less_lift: "(x::'a lift) \<sqsubseteq> y = (x = y \<or> x = \<bottom>)"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    95
by (induct x, simp_all)
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    96
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
    97
instance lift :: (type) flat
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    98
by (intro_classes, simp add: less_lift)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    99
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   100
text {*
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   101
  \medskip Two specific lemmas for the combination of LCF and HOL
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   102
  terms.
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   103
*}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   104
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
   105
lemma cont_Rep_CFun_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
18092
2c5d5da79a1e renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents: 17612
diff changeset
   106
by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   107
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
   108
lemma cont_Rep_CFun_app_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
18092
2c5d5da79a1e renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents: 17612
diff changeset
   109
by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   110
16695
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   111
subsection {* Further operations *}
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   112
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   113
constdefs
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   114
  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   115
  "flift1 \<equiv> \<lambda>f. (\<Lambda> x. lift_case \<bottom> f x)"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   116
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   117
  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   118
  "flift2 f \<equiv> FLIFT x. Def (f x)"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   119
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   120
  liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   121
  "liftpair x \<equiv> csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   122
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   123
subsection {* Continuity Proofs for flift1, flift2 *}
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   124
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   125
text {* Need the instance of @{text flat}. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   126
16695
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   127
lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   128
apply (induct x)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   129
apply simp
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   130
apply simp
18092
2c5d5da79a1e renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents: 17612
diff changeset
   131
apply (rule cont_id [THEN cont2cont_fun])
16695
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   132
done
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   133
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   134
lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   135
apply (rule flatdom_strict2cont)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   136
apply simp
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   137
done
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   138
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   139
lemma cont_flift1: "cont flift1"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   140
apply (unfold flift1_def)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   141
apply (rule cont2cont_LAM)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   142
apply (rule cont_lift_case2)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   143
apply (rule cont_lift_case1)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   144
done
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   145
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   146
lemma cont2cont_flift1:
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   147
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   148
apply (rule cont_flift1 [THEN cont2cont_app3])
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   149
apply (simp add: cont2cont_lambda)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   150
done
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   151
16757
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   152
lemma cont2cont_lift_case:
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   153
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))"
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   154
apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))")
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   155
apply (simp add: flift1_def cont_lift_case2)
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   156
apply (simp add: cont2cont_flift1)
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   157
done
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   158
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   159
text {* rewrites for @{term flift1}, @{term flift2} *}
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   160
16695
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   161
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   162
by (simp add: flift1_def cont_lift_case2)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   163
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   164
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   165
by (simp add: flift2_def)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   166
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   167
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   168
by (simp add: flift1_def cont_lift_case2)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   169
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   170
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   171
by (simp add: flift2_def)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   172
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   173
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   174
by (erule lift_definedE, simp)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   175
19520
873dad2d8a6d add theorem flift2_defined_iff
huffman
parents: 19440
diff changeset
   176
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
873dad2d8a6d add theorem flift2_defined_iff
huffman
parents: 19440
diff changeset
   177
by (cases x, simp_all)
873dad2d8a6d add theorem flift2_defined_iff
huffman
parents: 19440
diff changeset
   178
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   179
text {*
14096
f79d139c7e46 corrected markup text
oheimb
parents: 12338
diff changeset
   180
  \medskip Extension of @{text cont_tac} and installation of simplifier.
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   181
*}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   182
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   183
lemmas cont_lemmas_ext [simp] =
16757
b8bfd086f7d4 replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents: 16755
diff changeset
   184
  cont2cont_flift1 cont2cont_lift_case cont2cont_lambda
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   185
  cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   186
16121
wenzelm
parents: 16067
diff changeset
   187
ML {*
19764
372065f34795 removed obsolete ML files;
wenzelm
parents: 19520
diff changeset
   188
local
372065f34795 removed obsolete ML files;
wenzelm
parents: 19520
diff changeset
   189
  val cont_lemmas2 = thms "cont_lemmas1" @ thms "cont_lemmas_ext";
372065f34795 removed obsolete ML files;
wenzelm
parents: 19520
diff changeset
   190
  val flift1_def = thm "flift1_def";
372065f34795 removed obsolete ML files;
wenzelm
parents: 19520
diff changeset
   191
in
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   192
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   193
fun cont_tac  i = resolve_tac cont_lemmas2 i;
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   194
fun cont_tacR i = REPEAT (cont_tac i);
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   195
19764
372065f34795 removed obsolete ML files;
wenzelm
parents: 19520
diff changeset
   196
fun cont_tacRs ss i =
17612
5b37787d2d9e adm_tac/cont_tacRs: proper simpset;
wenzelm
parents: 16757
diff changeset
   197
  simp_tac ss i THEN
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   198
  REPEAT (cont_tac i)
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   199
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
   200
*}
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
   201
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   202
end