src/HOL/HOLCF/Lift.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42814 5af15f1e2ef6
child 49759 ecf1d5d87e5e
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41430
diff changeset
     1
(*  Title:      HOL/HOLCF/Lift.thy
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
     2
    Author:     Olaf Mueller
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     3
*)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     4
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
     5
header {* Lifting types of class type to flat pcpo's *}
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
     6
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     7
theory Lift
40086
c339c0e8fdfb minimize imports
huffman
parents: 40082
diff changeset
     8
imports Discrete Up
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     9
begin
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    10
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35948
diff changeset
    11
default_sort type
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    12
40082
f4be971c5746 pcpodef (open) 'a lift
huffman
parents: 40009
diff changeset
    13
pcpodef (open) 'a lift = "UNIV :: 'a discr u set"
29063
7619f0561cd7 pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents: 27311
diff changeset
    14
by simp_all
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    15
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    16
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    17
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19764
diff changeset
    18
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19764
diff changeset
    19
  Def :: "'a \<Rightarrow> 'a lift" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19764
diff changeset
    20
  "Def x = Abs_lift (up\<cdot>(Discr x))"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    21
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    22
subsection {* Lift as a datatype *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    23
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    24
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
    25
apply (induct y)
16755
fd02f9d06e43 renamed upE1 to upE; added simp rule cont2cont_flift1
huffman
parents: 16749
diff changeset
    26
apply (rule_tac p=y in upE)
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    27
apply (simp add: Abs_lift_strict)
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    28
apply (case_tac x)
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    29
apply (simp add: Def_def)
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    30
done
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    31
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 26963
diff changeset
    32
rep_datatype "\<bottom>\<Colon>'a lift" Def
40082
f4be971c5746 pcpodef (open) 'a lift
huffman
parents: 40009
diff changeset
    33
  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    34
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 40834
diff changeset
    35
text {* @{term bottom} and @{term Def} *}
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    36
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    37
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    38
  by (cases x) simp_all
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    39
16630
83bf468b1dc7 added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents: 16555
diff changeset
    40
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
    41
  by (cases x) simp_all
83bf468b1dc7 added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents: 16555
diff changeset
    42
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    43
text {*
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 40834
diff changeset
    44
  For @{term "x ~= \<bottom>"} in assumptions @{text defined} replaces @{text
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    45
  x} by @{text "Def a"} in conclusion. *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    46
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 29138
diff changeset
    47
method_setup defined = {*
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 29138
diff changeset
    48
  Scan.succeed (fn ctxt => SIMPLE_METHOD'
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 31076
diff changeset
    49
    (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 42151
diff changeset
    50
*}
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    51
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    52
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    53
  by simp
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    54
16748
58b9ce4fac54 define lift type using pcpodef; cleaned up
huffman
parents: 16695
diff changeset
    55
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    56
  by simp
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    57
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30607
diff changeset
    58
lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
40082
f4be971c5746 pcpodef (open) 'a lift
huffman
parents: 40009
diff changeset
    59
by (simp add: below_lift_def Def_def Abs_lift_inverse)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    60
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30607
diff changeset
    61
lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30607
diff changeset
    62
by (induct y, simp, simp add: Def_below_Def)
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    63
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    64
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    65
subsection {* Lift is flat *}
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    66
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12026
diff changeset
    67
instance lift :: (type) flat
27292
huffman
parents: 27104
diff changeset
    68
proof
huffman
parents: 27104
diff changeset
    69
  fix x y :: "'a lift"
huffman
parents: 27104
diff changeset
    70
  assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
huffman
parents: 27104
diff changeset
    71
    by (induct x) auto
huffman
parents: 27104
diff changeset
    72
qed
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 2640
diff changeset
    73
40088
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    74
subsection {* Continuity of @{const lift_case} *}
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    75
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    76
lemma lift_case_eq: "lift_case \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    77
apply (induct x, unfold lift.cases)
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    78
apply (simp add: Rep_lift_strict)
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    79
apply (simp add: Def_def Abs_lift_inverse)
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    80
done
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    81
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    82
lemma cont2cont_lift_case [simp]:
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    83
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
40834
a1249aeff5b6 change cpodef-generated cont_Rep rules to cont2cont format
huffman
parents: 40774
diff changeset
    84
unfolding lift_case_eq by (simp add: cont_Rep_lift)
40088
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
    85
16695
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
    86
subsection {* Further operations *}
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
    87
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19764
diff changeset
    88
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19764
diff changeset
    89
  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19764
diff changeset
    90
  "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
16695
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
    91
40323
4cce7c708402 add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents: 40321
diff changeset
    92
translations
4cce7c708402 add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents: 40321
diff changeset
    93
  "\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)"
4cce7c708402 add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents: 40321
diff changeset
    94
  "\<Lambda>(CONST Def x). FLIFT y. t" <= "FLIFT x y. t"
4cce7c708402 add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents: 40321
diff changeset
    95
  "\<Lambda>(CONST Def x). t" <= "FLIFT x. t"
4cce7c708402 add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents: 40321
diff changeset
    96
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19764
diff changeset
    97
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19764
diff changeset
    98
  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19764
diff changeset
    99
  "flift2 f = (FLIFT x. Def (f x))"
16695
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   100
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   101
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
40088
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   102
by (simp add: flift1_def)
16695
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   103
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   104
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   105
by (simp add: flift2_def)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   106
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   107
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
40088
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   108
by (simp add: flift1_def)
16695
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   109
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   110
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   111
by (simp add: flift2_def)
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
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
   114
by (erule lift_definedE, simp)
dc8c868e910b simplified definitions of flift1, flift2, liftpair;
huffman
parents: 16630
diff changeset
   115
40321
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40089
diff changeset
   116
lemma flift2_bottom_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
19520
873dad2d8a6d add theorem flift2_defined_iff
huffman
parents: 19440
diff changeset
   117
by (cases x, simp_all)
873dad2d8a6d add theorem flift2_defined_iff
huffman
parents: 19440
diff changeset
   118
40088
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   119
lemma FLIFT_mono:
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   120
  "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   121
by (rule cfun_belowI, case_tac x, simp_all)
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   122
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   123
lemma cont2cont_flift1 [simp, cont2cont]:
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   124
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   125
by (simp add: flift1_def cont2cont_LAM)
49b9d301fadb simplify proofs about flift; remove unneeded lemmas
huffman
parents: 40086
diff changeset
   126
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
   127
end