src/HOLCF/ex/Domain_Proofs.thy
author huffman
Fri, 08 Oct 2010 07:39:50 -0700
changeset 39986 38677db30cad
parent 39974 b525988432e9
child 39989 ad60d7311f43
permissions -rw-r--r--
rename class 'sfp' to 'bifinite'
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/ex/Domain_Proofs.thy
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
     3
*)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
     4
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
     5
header {* Internal domain package proofs done manually *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
     6
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
     7
theory Domain_Proofs
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
     8
imports HOLCF
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
     9
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    10
39986
38677db30cad rename class 'sfp' to 'bifinite'
huffman
parents: 39974
diff changeset
    11
default_sort bifinite
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    12
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    13
(*
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    14
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    15
The definitions and proofs below are for the following recursive
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    16
datatypes:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    17
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    18
domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
    19
   and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
    20
   and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    21
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    22
*)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    23
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    24
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    25
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    26
subsection {* Step 1: Define the new type combinators *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    27
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    28
text {* Start with the one-step non-recursive version *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    29
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    30
definition
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    31
  foo_bar_baz_sfpF ::
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    32
    "sfp \<rightarrow> sfp \<times> sfp \<times> sfp \<rightarrow> sfp \<times> sfp \<times> sfp"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    33
where
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    34
  "foo_bar_baz_sfpF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    35
    ( ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>t2))
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    36
    , u_sfp\<cdot>(cfun_sfp\<cdot>t3\<cdot>SFP(tr))
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    37
    , u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>t1)\<cdot>SFP(tr)))))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    38
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    39
lemma foo_bar_baz_sfpF_beta:
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    40
  "foo_bar_baz_sfpF\<cdot>a\<cdot>t =
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    41
    ( ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>(fst (snd t))))
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    42
    , u_sfp\<cdot>(cfun_sfp\<cdot>(snd (snd t))\<cdot>SFP(tr))
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    43
    , u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>(fst t))\<cdot>SFP(tr)))"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    44
unfolding foo_bar_baz_sfpF_def
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
    45
by (simp add: split_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    46
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    47
text {* Individual type combinators are projected from the fixed point. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    48
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    49
definition foo_sfp :: "sfp \<rightarrow> sfp"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    50
where "foo_sfp = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    51
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    52
definition bar_sfp :: "sfp \<rightarrow> sfp"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    53
where "bar_sfp = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    54
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    55
definition baz_sfp :: "sfp \<rightarrow> sfp"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    56
where "baz_sfp = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    57
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
    58
lemma defl_apply_thms:
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    59
  "foo_sfp\<cdot>a = fst (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    60
  "bar_sfp\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    61
  "baz_sfp\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    62
unfolding foo_sfp_def bar_sfp_def baz_sfp_def by simp_all
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
    63
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    64
text {* Unfold rules for each combinator. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    65
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    66
lemma foo_sfp_unfold:
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    67
  "foo_sfp\<cdot>a = ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>(bar_sfp\<cdot>a)))"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    68
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    69
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    70
lemma bar_sfp_unfold: "bar_sfp\<cdot>a = u_sfp\<cdot>(cfun_sfp\<cdot>(baz_sfp\<cdot>a)\<cdot>SFP(tr))"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    71
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    72
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    73
lemma baz_sfp_unfold: "baz_sfp\<cdot>a = u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>(foo_sfp\<cdot>a))\<cdot>SFP(tr))"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    74
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    75
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    76
text "The automation for the previous steps will be quite similar to
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    77
how the fixrec package works."
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    78
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    79
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    80
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    81
subsection {* Step 2: Define types, prove class instances *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    82
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    83
text {* Use @{text pcpodef} with the appropriate type combinator. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    84
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    85
pcpodef (open) 'a foo = "{x. x ::: foo_sfp\<cdot>SFP('a)}"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    86
by (simp_all add: adm_in_sfp)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    87
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    88
pcpodef (open) 'a bar = "{x. x ::: bar_sfp\<cdot>SFP('a)}"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    89
by (simp_all add: adm_in_sfp)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    90
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    91
pcpodef (open) 'a baz = "{x. x ::: baz_sfp\<cdot>SFP('a)}"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
    92
by (simp_all add: adm_in_sfp)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    93
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    94
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    95
39986
38677db30cad rename class 'sfp' to 'bifinite'
huffman
parents: 39974
diff changeset
    96
instantiation foo :: (bifinite) bifinite
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    97
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    98
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    99
definition emb_foo :: "'a foo \<rightarrow> udom"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33591
diff changeset
   100
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   101
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   102
definition prj_foo :: "udom \<rightarrow> 'a foo"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   103
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_sfp\<cdot>SFP('a))\<cdot>y))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   104
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   105
definition sfp_foo :: "'a foo itself \<Rightarrow> sfp"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   106
where "sfp_foo \<equiv> \<lambda>a. foo_sfp\<cdot>SFP('a)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   107
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   108
instance
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   109
apply (rule typedef_rep_class)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   110
apply (rule type_definition_foo)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   111
apply (rule below_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   112
apply (rule emb_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   113
apply (rule prj_foo_def)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   114
apply (rule sfp_foo_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   115
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   116
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   117
end
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   118
39986
38677db30cad rename class 'sfp' to 'bifinite'
huffman
parents: 39974
diff changeset
   119
instantiation bar :: (bifinite) bifinite
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   120
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   121
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   122
definition emb_bar :: "'a bar \<rightarrow> udom"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33591
diff changeset
   123
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   124
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   125
definition prj_bar :: "udom \<rightarrow> 'a bar"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   126
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_sfp\<cdot>SFP('a))\<cdot>y))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   127
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   128
definition sfp_bar :: "'a bar itself \<Rightarrow> sfp"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   129
where "sfp_bar \<equiv> \<lambda>a. bar_sfp\<cdot>SFP('a)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   130
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   131
instance
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   132
apply (rule typedef_rep_class)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   133
apply (rule type_definition_bar)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   134
apply (rule below_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   135
apply (rule emb_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   136
apply (rule prj_bar_def)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   137
apply (rule sfp_bar_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   138
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   139
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   140
end
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   141
39986
38677db30cad rename class 'sfp' to 'bifinite'
huffman
parents: 39974
diff changeset
   142
instantiation baz :: (bifinite) bifinite
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   143
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   144
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   145
definition emb_baz :: "'a baz \<rightarrow> udom"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33591
diff changeset
   146
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   147
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   148
definition prj_baz :: "udom \<rightarrow> 'a baz"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   149
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_sfp\<cdot>SFP('a))\<cdot>y))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   150
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   151
definition sfp_baz :: "'a baz itself \<Rightarrow> sfp"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   152
where "sfp_baz \<equiv> \<lambda>a. baz_sfp\<cdot>SFP('a)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   153
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   154
instance
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   155
apply (rule typedef_rep_class)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   156
apply (rule type_definition_baz)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   157
apply (rule below_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   158
apply (rule emb_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   159
apply (rule prj_baz_def)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   160
apply (rule sfp_baz_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   161
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   162
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   163
end
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   164
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   165
text {* Prove SFP rules using lemma @{text typedef_SFP}. *}
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   166
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   167
lemma SFP_foo: "SFP('a foo) = foo_sfp\<cdot>SFP('a)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   168
apply (rule typedef_SFP)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   169
apply (rule sfp_foo_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   170
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   171
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   172
lemma SFP_bar: "SFP('a bar) = bar_sfp\<cdot>SFP('a)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   173
apply (rule typedef_SFP)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   174
apply (rule sfp_bar_def)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   175
done
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   176
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   177
lemma SFP_baz: "SFP('a baz) = baz_sfp\<cdot>SFP('a)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   178
apply (rule typedef_SFP)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   179
apply (rule sfp_baz_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   180
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   181
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   182
text {* Prove SFP equations using type combinator unfold lemmas. *}
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   183
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   184
lemmas SFP_simps =
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   185
  SFP_ssum SFP_sprod SFP_u SFP_cfun
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   186
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   187
lemma SFP_foo': "SFP('a foo) = SFP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   188
unfolding SFP_foo SFP_bar SFP_baz SFP_simps
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   189
by (rule foo_sfp_unfold)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   190
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   191
lemma SFP_bar': "SFP('a bar) = SFP(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   192
unfolding SFP_foo SFP_bar SFP_baz SFP_simps
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   193
by (rule bar_sfp_unfold)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   194
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   195
lemma SFP_baz': "SFP('a baz) = SFP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   196
unfolding SFP_foo SFP_bar SFP_baz SFP_simps SFP_convex
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   197
by (rule baz_sfp_unfold)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   198
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   199
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   200
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   201
subsection {* Step 3: Define rep and abs functions *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   202
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   203
text {* Define them all using @{text coerce}! *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   204
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   205
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   206
where "foo_rep \<equiv> coerce"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   207
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   208
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   209
where "foo_abs \<equiv> coerce"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   210
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   211
definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   212
where "bar_rep \<equiv> coerce"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   213
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   214
definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   215
where "bar_abs \<equiv> coerce"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   216
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   217
definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   218
where "baz_rep \<equiv> coerce"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   219
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   220
definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   221
where "baz_abs \<equiv> coerce"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   222
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   223
text {* Prove isomorphism rules. *}
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   224
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   225
lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   226
by (rule domain_abs_iso [OF SFP_foo' foo_abs_def foo_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   227
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   228
lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   229
by (rule domain_rep_iso [OF SFP_foo' foo_abs_def foo_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   230
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   231
lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   232
by (rule domain_abs_iso [OF SFP_bar' bar_abs_def bar_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   233
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   234
lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   235
by (rule domain_rep_iso [OF SFP_bar' bar_abs_def bar_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   236
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   237
lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   238
by (rule domain_abs_iso [OF SFP_baz' baz_abs_def baz_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   239
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   240
lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   241
by (rule domain_rep_iso [OF SFP_baz' baz_abs_def baz_rep_def])
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   242
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   243
text {* Prove isodefl rules using @{text isodefl_coerce}. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   244
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   245
lemma isodefl_foo_abs:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   246
  "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   247
by (rule isodefl_abs_rep [OF SFP_foo' foo_abs_def foo_rep_def])
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   248
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   249
lemma isodefl_bar_abs:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   250
  "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   251
by (rule isodefl_abs_rep [OF SFP_bar' bar_abs_def bar_rep_def])
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   252
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   253
lemma isodefl_baz_abs:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   254
  "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   255
by (rule isodefl_abs_rep [OF SFP_baz' baz_abs_def baz_rep_def])
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   256
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   257
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   258
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   259
subsection {* Step 4: Define map functions, prove isodefl property *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   260
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   261
text {* Start with the one-step non-recursive version. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   262
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   263
text {* Note that the type of the map function depends on which
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   264
variables are used in positive and negative positions. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   265
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   266
definition
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   267
  foo_bar_baz_mapF ::
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   268
    "('a \<rightarrow> 'b) \<rightarrow>
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   269
     ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   270
     ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   271
where
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   272
  "foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3).
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   273
    (
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   274
      foo_abs oo
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   275
        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   276
          oo foo_rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   277
    ,
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   278
      bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   279
    ,
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   280
      baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   281
    )))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   282
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   283
lemma foo_bar_baz_mapF_beta:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   284
  "foo_bar_baz_mapF\<cdot>f\<cdot>d =
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   285
    (
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   286
      foo_abs oo
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   287
        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d))))
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   288
          oo foo_rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   289
    ,
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   290
      bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   291
    ,
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   292
      baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   293
    )"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   294
unfolding foo_bar_baz_mapF_def
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   295
by (simp add: split_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   296
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   297
text {* Individual map functions are projected from the fixed point. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   298
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   299
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   300
where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   301
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   302
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   303
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   304
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   305
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   306
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   307
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   308
lemma map_apply_thms:
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   309
  "foo_map\<cdot>f = fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   310
  "bar_map\<cdot>f = fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   311
  "baz_map\<cdot>f = snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   312
unfolding foo_map_def bar_map_def baz_map_def by simp_all
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   313
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   314
text {* Prove isodefl rules for all map functions simultaneously. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   315
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   316
lemma isodefl_foo_bar_baz:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   317
  assumes isodefl_d: "isodefl d t"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   318
  shows
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   319
  "isodefl (foo_map\<cdot>d) (foo_sfp\<cdot>t) \<and>
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   320
  isodefl (bar_map\<cdot>d) (bar_sfp\<cdot>t) \<and>
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   321
  isodefl (baz_map\<cdot>d) (baz_sfp\<cdot>t)"
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   322
unfolding map_apply_thms defl_apply_thms
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   323
 apply (rule parallel_fix_ind)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   324
   apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   325
  apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   326
 apply (simp only: foo_bar_baz_mapF_beta
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   327
                   foo_bar_baz_sfpF_beta
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   328
                   fst_conv snd_conv)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   329
 apply (elim conjE)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   330
 apply (intro
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   331
  conjI
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   332
  isodefl_foo_abs
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   333
  isodefl_bar_abs
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   334
  isodefl_baz_abs
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   335
  isodefl_ssum isodefl_sprod isodefl_ID_SFP
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   336
  isodefl_u isodefl_convex isodefl_cfun
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   337
  isodefl_d
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   338
 )
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   339
 apply assumption+
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   340
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   341
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   342
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1]
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   343
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   344
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   345
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   346
text {* Prove map ID lemmas, using isodefl_SFP_imp_ID *}
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   347
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   348
lemma foo_map_ID: "foo_map\<cdot>ID = ID"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   349
apply (rule isodefl_SFP_imp_ID)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   350
apply (subst SFP_foo)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   351
apply (rule isodefl_foo)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   352
apply (rule isodefl_ID_SFP)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   353
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   354
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   355
lemma bar_map_ID: "bar_map\<cdot>ID = ID"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   356
apply (rule isodefl_SFP_imp_ID)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   357
apply (subst SFP_bar)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   358
apply (rule isodefl_bar)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   359
apply (rule isodefl_ID_SFP)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   360
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   361
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   362
lemma baz_map_ID: "baz_map\<cdot>ID = ID"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   363
apply (rule isodefl_SFP_imp_ID)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   364
apply (subst SFP_baz)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   365
apply (rule isodefl_baz)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   366
apply (rule isodefl_ID_SFP)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   367
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   368
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   369
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   370
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   371
subsection {* Step 5: Define take functions, prove lub-take lemmas *}
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   372
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   373
definition
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   374
  foo_bar_baz_takeF ::
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   375
    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   376
     ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   377
where
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   378
  "foo_bar_baz_takeF = (\<Lambda> p.
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   379
    ( foo_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   380
        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   381
          oo foo_rep
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   382
    , bar_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   383
        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   384
    , baz_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   385
        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   386
    ))"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   387
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   388
lemma foo_bar_baz_takeF_beta:
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   389
  "foo_bar_baz_takeF\<cdot>p =
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   390
    ( foo_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   391
        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   392
          oo foo_rep
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   393
    , bar_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   394
        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   395
    , baz_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   396
        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   397
    )"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   398
unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   399
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   400
definition
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   401
  foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   402
where
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   403
  "foo_take = (\<lambda>n. fst (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>))"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   404
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   405
definition
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   406
  bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   407
where
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   408
  "bar_take = (\<lambda>n. fst (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   409
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   410
definition
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   411
  baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   412
where
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   413
  "baz_take = (\<lambda>n. snd (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   414
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   415
lemma chain_take_thms: "chain foo_take" "chain bar_take" "chain baz_take"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   416
unfolding foo_take_def bar_take_def baz_take_def
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   417
by (intro ch2ch_fst ch2ch_snd chain_iterate)+
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   418
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   419
lemma take_0_thms: "foo_take 0 = \<bottom>" "bar_take 0 = \<bottom>" "baz_take 0 = \<bottom>"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   420
unfolding foo_take_def bar_take_def baz_take_def
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   421
by (simp only: iterate_0 fst_strict snd_strict)+
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   422
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   423
lemma take_Suc_thms:
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   424
  "foo_take (Suc n) =
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   425
    foo_abs oo ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(bar_take n))) oo foo_rep"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   426
  "bar_take (Suc n) =
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   427
    bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   428
  "baz_take (Suc n) =
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   429
    baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(foo_take n))\<cdot>ID) oo baz_rep"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   430
unfolding foo_take_def bar_take_def baz_take_def
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   431
by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   432
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   433
lemma lub_take_lemma:
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   434
  "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   435
    = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   436
apply (simp only: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   437
apply (simp only: map_apply_thms pair_collapse)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   438
apply (simp only: fix_def2)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   439
apply (rule lub_eq)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   440
apply (rule nat.induct)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   441
apply (simp only: iterate_0 Pair_strict take_0_thms)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   442
apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   443
                  foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   444
done
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   445
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   446
lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   447
apply (rule trans [OF _ foo_map_ID])
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   448
using lub_take_lemma
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   449
apply (elim Pair_inject)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   450
apply assumption
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   451
done
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   452
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   453
lemma lub_bar_take: "(\<Squnion>n. bar_take n) = ID"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   454
apply (rule trans [OF _ bar_map_ID])
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   455
using lub_take_lemma
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   456
apply (elim Pair_inject)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   457
apply assumption
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   458
done
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   459
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   460
lemma lub_baz_take: "(\<Squnion>n. baz_take n) = ID"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   461
apply (rule trans [OF _ baz_map_ID])
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   462
using lub_take_lemma
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   463
apply (elim Pair_inject)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   464
apply assumption
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   465
done
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   466
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   467
end