src/HOL/HOLCF/ex/Domain_Proofs.thy
author wenzelm
Wed, 13 Jan 2016 23:07:06 +0100
changeset 62175 8ffc4d0e652d
parent 61424 c3658c18b7bc
permissions -rw-r--r--
isabelle update_cartouches -c -t;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41437
diff changeset
     1
(*  Title:      HOL/HOLCF/ex/Domain_Proofs.thy
33591
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
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
     5
section \<open>Internal domain package proofs done manually\<close>
33591
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
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    11
(*
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
The definitions and proofs below are for the following recursive
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    14
datatypes:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    15
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    16
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
    17
   and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
    18
   and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    19
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    20
*)
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
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
    24
subsection \<open>Step 1: Define the new type combinators\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    25
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
    26
text \<open>Start with the one-step non-recursive version\<close>
33591
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
definition
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    29
  foo_bar_baz_deflF ::
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 40774
diff changeset
    30
    "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    31
where
40327
1dfdbd66093a renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman
parents: 40038
diff changeset
    32
  "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
    33
    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
    34
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
    35
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    36
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    37
lemma foo_bar_baz_deflF_beta:
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    38
  "foo_bar_baz_deflF\<cdot>a\<cdot>t =
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
    39
    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
    40
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
    41
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    42
unfolding foo_bar_baz_deflF_def
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
    43
by (simp add: split_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    44
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
    45
text \<open>Individual type combinators are projected from the fixed point.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    46
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 40774
diff changeset
    47
definition foo_defl :: "udom defl \<rightarrow> udom defl"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    48
where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    49
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 40774
diff changeset
    50
definition bar_defl :: "udom defl \<rightarrow> udom defl"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    51
where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    52
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 40774
diff changeset
    53
definition baz_defl :: "udom defl \<rightarrow> udom defl"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    54
where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    55
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
    56
lemma defl_apply_thms:
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    57
  "foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))"
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    58
  "bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    59
  "baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    60
unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
    61
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
    62
text \<open>Unfold rules for each combinator.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    63
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    64
lemma foo_defl_unfold:
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
    65
  "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    66
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    67
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
    68
lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    69
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    70
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
    71
lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
    72
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    73
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    74
text "The automation for the previous steps will be quite similar to
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    75
how the fixrec package works."
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    76
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    77
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    78
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
    79
subsection \<open>Step 2: Define types, prove class instances\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    80
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
    81
text \<open>Use \<open>pcpodef\<close> with the appropriate type combinator.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    82
49759
ecf1d5d87e5e removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents: 44066
diff changeset
    83
pcpodef 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
40038
9d061b3d8f46 replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents: 40037
diff changeset
    84
by (rule defl_set_bottom, rule adm_defl_set)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    85
49759
ecf1d5d87e5e removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents: 44066
diff changeset
    86
pcpodef 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
40038
9d061b3d8f46 replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents: 40037
diff changeset
    87
by (rule defl_set_bottom, rule adm_defl_set)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    88
49759
ecf1d5d87e5e removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents: 44066
diff changeset
    89
pcpodef 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
40038
9d061b3d8f46 replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents: 40037
diff changeset
    90
by (rule defl_set_bottom, rule adm_defl_set)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    91
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
    92
text \<open>Prove rep instance using lemma \<open>typedef_rep_class\<close>.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    93
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    94
instantiation foo :: ("domain") "domain"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    95
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    96
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    97
definition emb_foo :: "'a foo \<rightarrow> udom"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33591
diff changeset
    98
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    99
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   100
definition prj_foo :: "udom \<rightarrow> 'a foo"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   101
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   102
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 40774
diff changeset
   103
definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   104
where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   105
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   106
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   107
  "(liftemb :: 'a foo u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   108
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   109
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   110
  "(liftprj :: udom u \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   111
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   112
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41292
diff changeset
   113
  "liftdefl \<equiv> \<lambda>(t::'a foo itself). liftdefl_of\<cdot>DEFL('a foo)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   114
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   115
instance
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   116
apply (rule typedef_domain_class)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   117
apply (rule type_definition_foo)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   118
apply (rule below_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   119
apply (rule emb_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   120
apply (rule prj_foo_def)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   121
apply (rule defl_foo_def)
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   122
apply (rule liftemb_foo_def)
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   123
apply (rule liftprj_foo_def)
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   124
apply (rule liftdefl_foo_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   125
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   126
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   127
end
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   128
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   129
instantiation bar :: ("domain") "domain"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   130
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   131
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   132
definition emb_bar :: "'a bar \<rightarrow> udom"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33591
diff changeset
   133
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   134
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   135
definition prj_bar :: "udom \<rightarrow> 'a bar"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   136
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   137
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 40774
diff changeset
   138
definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   139
where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   140
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   141
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   142
  "(liftemb :: 'a bar u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   143
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   144
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   145
  "(liftprj :: udom u \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   146
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   147
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41292
diff changeset
   148
  "liftdefl \<equiv> \<lambda>(t::'a bar itself). liftdefl_of\<cdot>DEFL('a bar)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   149
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   150
instance
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   151
apply (rule typedef_domain_class)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   152
apply (rule type_definition_bar)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   153
apply (rule below_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   154
apply (rule emb_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   155
apply (rule prj_bar_def)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   156
apply (rule defl_bar_def)
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   157
apply (rule liftemb_bar_def)
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   158
apply (rule liftprj_bar_def)
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   159
apply (rule liftdefl_bar_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   160
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   161
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   162
end
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   163
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   164
instantiation baz :: ("domain") "domain"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   165
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   166
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   167
definition emb_baz :: "'a baz \<rightarrow> udom"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33591
diff changeset
   168
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   169
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   170
definition prj_baz :: "udom \<rightarrow> 'a baz"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   171
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   172
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 40774
diff changeset
   173
definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   174
where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   175
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   176
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   177
  "(liftemb :: 'a baz u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   178
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   179
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   180
  "(liftprj :: udom u \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   181
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   182
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41292
diff changeset
   183
  "liftdefl \<equiv> \<lambda>(t::'a baz itself). liftdefl_of\<cdot>DEFL('a baz)"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   184
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   185
instance
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   186
apply (rule typedef_domain_class)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   187
apply (rule type_definition_baz)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   188
apply (rule below_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   189
apply (rule emb_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   190
apply (rule prj_baz_def)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   191
apply (rule defl_baz_def)
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   192
apply (rule liftemb_baz_def)
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   193
apply (rule liftprj_baz_def)
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   194
apply (rule liftdefl_baz_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   195
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   196
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   197
end
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   198
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   199
text \<open>Prove DEFL rules using lemma \<open>typedef_DEFL\<close>.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   200
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   201
lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   202
apply (rule typedef_DEFL)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   203
apply (rule defl_foo_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   204
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   205
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   206
lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   207
apply (rule typedef_DEFL)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   208
apply (rule defl_bar_def)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   209
done
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 36452
diff changeset
   210
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   211
lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   212
apply (rule typedef_DEFL)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   213
apply (rule defl_baz_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   214
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   215
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   216
text \<open>Prove DEFL equations using type combinator unfold lemmas.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   217
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   218
lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   219
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   220
by (rule foo_defl_unfold)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   221
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   222
lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   223
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   224
by (rule bar_defl_unfold)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   225
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   226
lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   227
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   228
by (rule baz_defl_unfold)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   229
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   230
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   231
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   232
subsection \<open>Step 3: Define rep and abs functions\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   233
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   234
text \<open>Define them all using \<open>prj\<close> and \<open>emb\<close>!\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   235
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   236
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
40037
81e6b89d8f58 eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents: 39989
diff changeset
   237
where "foo_rep \<equiv> prj oo emb"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   238
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   239
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
40037
81e6b89d8f58 eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents: 39989
diff changeset
   240
where "foo_abs \<equiv> prj oo emb"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   241
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   242
definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
40037
81e6b89d8f58 eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents: 39989
diff changeset
   243
where "bar_rep \<equiv> prj oo emb"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   244
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   245
definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
40037
81e6b89d8f58 eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents: 39989
diff changeset
   246
where "bar_abs \<equiv> prj oo emb"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   247
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   248
definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
40037
81e6b89d8f58 eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents: 39989
diff changeset
   249
where "baz_rep \<equiv> prj oo emb"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   250
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   251
definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
40037
81e6b89d8f58 eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents: 39989
diff changeset
   252
where "baz_abs \<equiv> prj oo emb"
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   253
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   254
text \<open>Prove isomorphism rules.\<close>
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   255
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   256
lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   257
by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   258
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   259
lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   260
by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   261
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   262
lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   263
by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   264
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   265
lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   266
by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   267
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   268
lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   269
by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   270
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   271
lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   272
by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   273
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   274
text \<open>Prove isodefl rules using \<open>isodefl_coerce\<close>.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   275
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   276
lemma isodefl_foo_abs:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   277
  "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   278
by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def])
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   279
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   280
lemma isodefl_bar_abs:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   281
  "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   282
by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def])
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   283
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   284
lemma isodefl_baz_abs:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   285
  "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   286
by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   287
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   288
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   289
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   290
subsection \<open>Step 4: Define map functions, prove isodefl property\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   291
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   292
text \<open>Start with the one-step non-recursive version.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   293
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   294
text \<open>Note that the type of the map function depends on which
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   295
variables are used in positive and negative positions.\<close>
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
definition
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   298
  foo_bar_baz_mapF ::
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   299
    "('a \<rightarrow> 'b) \<rightarrow>
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   300
     ('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
   301
     ('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
   302
where
40327
1dfdbd66093a renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman
parents: 40038
diff changeset
   303
  "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
   304
    (
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   305
      foo_abs oo
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   306
        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
   307
          oo foo_rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   308
    ,
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   309
      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
   310
    ,
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   311
      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
   312
    )))"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   313
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   314
lemma foo_bar_baz_mapF_beta:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   315
  "foo_bar_baz_mapF\<cdot>f\<cdot>d =
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   316
    (
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   317
      foo_abs oo
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   318
        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
   319
          oo foo_rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   320
    ,
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   321
      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
   322
    ,
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   323
      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
   324
    )"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   325
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
   326
by (simp add: split_def)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   327
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   328
text \<open>Individual map functions are projected from the fixed point.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   329
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   330
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   331
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
   332
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   333
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   334
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
   335
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   336
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
   337
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
   338
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   339
lemma map_apply_thms:
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   340
  "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
   341
  "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
   342
  "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
   343
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
   344
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   345
text \<open>Prove isodefl rules for all map functions simultaneously.\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   346
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   347
lemma isodefl_foo_bar_baz:
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   348
  assumes isodefl_d: "isodefl d t"
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   349
  shows
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   350
  "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   351
  isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   352
  isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   353
unfolding map_apply_thms defl_apply_thms
33787
71a675065128 change example to use recursion with continuous function space
huffman
parents: 33784
diff changeset
   354
 apply (rule parallel_fix_ind)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   355
   apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   356
  apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   357
 apply (simp only: foo_bar_baz_mapF_beta
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   358
                   foo_bar_baz_deflF_beta
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   359
                   fst_conv snd_conv)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   360
 apply (elim conjE)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   361
 apply (intro
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   362
  conjI
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   363
  isodefl_foo_abs
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   364
  isodefl_bar_abs
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   365
  isodefl_baz_abs
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   366
  domain_isodefl
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40327
diff changeset
   367
  isodefl_ID_DEFL isodefl_LIFTDEFL
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   368
  isodefl_d
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
 apply assumption+
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   371
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   372
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   373
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1]
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   374
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   375
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   376
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   377
text \<open>Prove map ID lemmas, using isodefl_DEFL_imp_ID\<close>
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   378
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   379
lemma foo_map_ID: "foo_map\<cdot>ID = ID"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   380
apply (rule isodefl_DEFL_imp_ID)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   381
apply (subst DEFL_foo)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   382
apply (rule isodefl_foo)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   383
apply (rule isodefl_ID_DEFL)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   384
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   385
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   386
lemma bar_map_ID: "bar_map\<cdot>ID = ID"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   387
apply (rule isodefl_DEFL_imp_ID)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   388
apply (subst DEFL_bar)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   389
apply (rule isodefl_bar)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   390
apply (rule isodefl_ID_DEFL)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   391
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   392
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   393
lemma baz_map_ID: "baz_map\<cdot>ID = ID"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   394
apply (rule isodefl_DEFL_imp_ID)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39986
diff changeset
   395
apply (subst DEFL_baz)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   396
apply (rule isodefl_baz)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   397
apply (rule isodefl_ID_DEFL)
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   398
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   399
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   400
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   401
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   402
subsection \<open>Step 5: Define take functions, prove lub-take lemmas\<close>
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   403
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   404
definition
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   405
  foo_bar_baz_takeF ::
33781
c7d32e726bb9 avoid using csplit; define copy functions exactly like the current domain package
huffman
parents: 33779
diff changeset
   406
    "('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
   407
     ('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
   408
where
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   409
  "foo_bar_baz_takeF = (\<Lambda> p.
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   410
    ( foo_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   411
        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
   412
          oo foo_rep
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   413
    , bar_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   414
        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
   415
    , baz_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   416
        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
   417
    ))"
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 foo_bar_baz_takeF_beta:
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   420
  "foo_bar_baz_takeF\<cdot>p =
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   421
    ( foo_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   422
        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
   423
          oo foo_rep
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   424
    , bar_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   425
        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
   426
    , baz_abs oo
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   427
        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
   428
    )"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   429
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
   430
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   431
definition
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   432
  foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   433
where
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   434
  "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
   435
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   436
definition
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   437
  bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   438
where
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   439
  "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
   440
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   441
definition
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   442
  baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   443
where
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   444
  "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
   445
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   446
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
   447
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
   448
by (intro ch2ch_fst ch2ch_snd chain_iterate)+
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   449
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   450
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
   451
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
   452
by (simp only: iterate_0 fst_strict snd_strict)+
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   453
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   454
lemma take_Suc_thms:
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   455
  "foo_take (Suc n) =
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   456
    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
   457
  "bar_take (Suc n) =
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   458
    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
   459
  "baz_take (Suc n) =
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   460
    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
   461
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
   462
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
   463
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   464
lemma lub_take_lemma:
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   465
  "(\<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
   466
    = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40592
diff changeset
   467
apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 58880
diff changeset
   468
apply (simp only: map_apply_thms prod.collapse)
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   469
apply (simp only: fix_def2)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   470
apply (rule lub_eq)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   471
apply (rule nat.induct)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   472
apply (simp only: iterate_0 Pair_strict take_0_thms)
44066
d74182c93f04 rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents: 42151
diff changeset
   473
apply (simp only: iterate_Suc prod_eq_iff fst_conv snd_conv
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   474
                  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
   475
done
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   476
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   477
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
   478
apply (rule trans [OF _ foo_map_ID])
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   479
using lub_take_lemma
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   480
apply (elim Pair_inject)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   481
apply assumption
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   482
done
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   483
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   484
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
   485
apply (rule trans [OF _ bar_map_ID])
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   486
using lub_take_lemma
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   487
apply (elim Pair_inject)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   488
apply assumption
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   489
done
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   490
36132
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   491
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
   492
apply (rule trans [OF _ baz_map_ID])
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   493
using lub_take_lemma
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   494
apply (elim Pair_inject)
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   495
apply assumption
6afa012a8f5c bring HOLCF/ex/Domain_Proofs.thy up to date
huffman
parents: 35493
diff changeset
   496
done
33591
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   497
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   498
end