src/HOL/HOLCF/Lift.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62175 8ffc4d0e652d
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Lift.thy
wenzelm@12026
     2
    Author:     Olaf Mueller
slotosch@2640
     3
*)
slotosch@2640
     4
wenzelm@62175
     5
section \<open>Lifting types of class type to flat pcpo's\<close>
wenzelm@12026
     6
huffman@15577
     7
theory Lift
huffman@40086
     8
imports Discrete Up
huffman@15577
     9
begin
wenzelm@12026
    10
wenzelm@36452
    11
default_sort type
wenzelm@12026
    12
huffman@49759
    13
pcpodef 'a lift = "UNIV :: 'a discr u set"
wenzelm@29063
    14
by simp_all
wenzelm@12026
    15
huffman@16748
    16
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
wenzelm@12026
    17
wenzelm@25131
    18
definition
wenzelm@25131
    19
  Def :: "'a \<Rightarrow> 'a lift" where
wenzelm@25131
    20
  "Def x = Abs_lift (up\<cdot>(Discr x))"
wenzelm@12026
    21
wenzelm@62175
    22
subsection \<open>Lift as a datatype\<close>
wenzelm@12026
    23
huffman@16748
    24
lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
huffman@16748
    25
apply (induct y)
huffman@16755
    26
apply (rule_tac p=y in upE)
huffman@16748
    27
apply (simp add: Abs_lift_strict)
huffman@16748
    28
apply (case_tac x)
huffman@16748
    29
apply (simp add: Def_def)
huffman@16748
    30
done
wenzelm@12026
    31
wenzelm@61076
    32
old_rep_datatype "\<bottom>::'a lift" Def
huffman@40082
    33
  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
wenzelm@12026
    34
wenzelm@62175
    35
text \<open>@{term bottom} and @{term Def}\<close>
wenzelm@12026
    36
huffman@16748
    37
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
wenzelm@12026
    38
  by (cases x) simp_all
wenzelm@12026
    39
huffman@16630
    40
lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
huffman@16630
    41
  by (cases x) simp_all
huffman@16630
    42
wenzelm@62175
    43
text \<open>
wenzelm@62175
    44
  For @{term "x ~= \<bottom>"} in assumptions \<open>defined\<close> replaces \<open>x\<close> by \<open>Def a\<close> in conclusion.\<close>
wenzelm@12026
    45
wenzelm@62175
    46
method_setup defined = \<open>
wenzelm@30607
    47
  Scan.succeed (fn ctxt => SIMPLE_METHOD'
wenzelm@60754
    48
    (eresolve_tac ctxt @{thms lift_definedE} THEN' asm_simp_tac ctxt))
wenzelm@62175
    49
\<close>
wenzelm@12026
    50
huffman@16748
    51
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
huffman@16748
    52
  by simp
wenzelm@12026
    53
huffman@16748
    54
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
wenzelm@12026
    55
  by simp
wenzelm@12026
    56
huffman@31076
    57
lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
huffman@40082
    58
by (simp add: below_lift_def Def_def Abs_lift_inverse)
wenzelm@12026
    59
huffman@31076
    60
lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
huffman@31076
    61
by (induct y, simp, simp add: Def_below_Def)
wenzelm@12026
    62
wenzelm@12026
    63
wenzelm@62175
    64
subsection \<open>Lift is flat\<close>
wenzelm@12026
    65
wenzelm@12338
    66
instance lift :: (type) flat
huffman@27292
    67
proof
huffman@27292
    68
  fix x y :: "'a lift"
huffman@27292
    69
  assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
huffman@27292
    70
    by (induct x) auto
huffman@27292
    71
qed
wenzelm@12026
    72
wenzelm@62175
    73
subsection \<open>Continuity of @{const case_lift}\<close>
huffman@40088
    74
blanchet@55417
    75
lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
blanchet@55642
    76
apply (induct x, unfold lift.case)
huffman@40088
    77
apply (simp add: Rep_lift_strict)
huffman@40088
    78
apply (simp add: Def_def Abs_lift_inverse)
huffman@40088
    79
done
huffman@40088
    80
blanchet@55417
    81
lemma cont2cont_case_lift [simp]:
blanchet@55417
    82
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. case_lift \<bottom> (f x) (g x))"
blanchet@55417
    83
unfolding case_lift_eq by (simp add: cont_Rep_lift)
huffman@40088
    84
wenzelm@62175
    85
subsection \<open>Further operations\<close>
huffman@16695
    86
wenzelm@25131
    87
definition
wenzelm@25131
    88
  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
blanchet@55417
    89
  "flift1 = (\<lambda>f. (\<Lambda> x. case_lift \<bottom> f x))"
huffman@16695
    90
huffman@40323
    91
translations
huffman@40323
    92
  "\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)"
huffman@40323
    93
  "\<Lambda>(CONST Def x). FLIFT y. t" <= "FLIFT x y. t"
huffman@40323
    94
  "\<Lambda>(CONST Def x). t" <= "FLIFT x. t"
huffman@40323
    95
wenzelm@25131
    96
definition
wenzelm@25131
    97
  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
wenzelm@25131
    98
  "flift2 f = (FLIFT x. Def (f x))"
huffman@16695
    99
huffman@16695
   100
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
huffman@40088
   101
by (simp add: flift1_def)
huffman@16695
   102
huffman@16695
   103
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
huffman@16695
   104
by (simp add: flift2_def)
huffman@16695
   105
huffman@16695
   106
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
huffman@40088
   107
by (simp add: flift1_def)
huffman@16695
   108
huffman@16695
   109
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
huffman@16695
   110
by (simp add: flift2_def)
huffman@16695
   111
huffman@16695
   112
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
huffman@16695
   113
by (erule lift_definedE, simp)
huffman@16695
   114
huffman@40321
   115
lemma flift2_bottom_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
huffman@19520
   116
by (cases x, simp_all)
huffman@19520
   117
huffman@40088
   118
lemma FLIFT_mono:
huffman@40088
   119
  "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
huffman@40088
   120
by (rule cfun_belowI, case_tac x, simp_all)
huffman@40088
   121
huffman@40088
   122
lemma cont2cont_flift1 [simp, cont2cont]:
huffman@40088
   123
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
huffman@40088
   124
by (simp add: flift1_def cont2cont_LAM)
huffman@40088
   125
slotosch@2640
   126
end