src/HOLCF/ex/Domain_Proofs.thy
author huffman
Tue, 10 Nov 2009 06:47:55 -0800
changeset 33591 51091e1041a7
child 33679 331712879666
permissions -rw-r--r--
HOLCF example: domain package proofs done manually
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
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    11
defaultsort rep
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")
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    19
   and 'a bar = Bar (lazy 'a) (lazy "'a baz")
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    20
   and 'a baz = Baz (lazy 'a) (lazy "'a foo convex_pd")
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
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    31
  foo_bar_baz_typF ::
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    32
    "TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    33
where
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    34
  "foo_bar_baz_typF = (\<Lambda> a (t1, t2, t3). 
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    35
    ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2))
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    36
    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t3)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    37
    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1))))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    38
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    39
lemma foo_bar_baz_typF_beta:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    40
  "foo_bar_baz_typF\<cdot>a\<cdot>t =
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    41
    ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(fst (snd t))))
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    42
    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(snd (snd t)))
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    43
    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(fst t))))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    44
unfolding foo_bar_baz_typF_def
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    45
by (simp add: csplit_def cfst_def csnd_def)
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
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    49
definition foo_typ :: "TypeRep \<rightarrow> TypeRep"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    50
where "foo_typ = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_typF\<cdot>a)))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    51
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    52
definition bar_typ :: "TypeRep \<rightarrow> TypeRep"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    53
where "bar_typ = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    54
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    55
definition baz_typ :: "TypeRep \<rightarrow> TypeRep"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    56
where "baz_typ = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    57
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    58
text {* Unfold rules for each combinator. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    59
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    60
lemma foo_typ_unfold:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    61
  "foo_typ\<cdot>a = ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(bar_typ\<cdot>a)))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    62
unfolding foo_typ_def bar_typ_def baz_typ_def
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    63
by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    64
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    65
lemma bar_typ_unfold: "bar_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(baz_typ\<cdot>a))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    66
unfolding foo_typ_def bar_typ_def baz_typ_def
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    67
by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    68
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    69
lemma baz_typ_unfold: "baz_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(foo_typ\<cdot>a)))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    70
unfolding foo_typ_def bar_typ_def baz_typ_def
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    71
by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    72
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    73
text "The automation for the previous steps will be quite similar to
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    74
how the fixrec package works."
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
(********************************************************************)
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
subsection {* Step 2: Define types, prove class instances *}
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
text {* Use @{text pcpodef} with the appropriate type combinator. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    81
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    82
pcpodef (open) 'a foo = "{x. x ::: foo_typ\<cdot>REP('a)}"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    83
by (simp_all add: adm_in_deflation)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    84
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    85
pcpodef (open) 'a bar = "{x. x ::: bar_typ\<cdot>REP('a)}"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    86
by (simp_all add: adm_in_deflation)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    87
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    88
pcpodef (open) 'a baz = "{x. x ::: baz_typ\<cdot>REP('a)}"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    89
by (simp_all add: adm_in_deflation)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    90
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    91
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    92
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    93
instantiation foo :: (rep) rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    94
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    95
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    96
definition emb_foo :: "'a foo \<rightarrow> udom"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
    97
where "emb_foo = (\<Lambda> x. Rep_foo x)"
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 prj_foo :: "udom \<rightarrow> 'a foo"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   100
where "prj_foo = (\<Lambda> y. Abs_foo (cast\<cdot>(foo_typ\<cdot>REP('a))\<cdot>y))"
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 approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   103
where "approx_foo = (\<lambda>i. prj oo cast\<cdot>(approx i\<cdot>(foo_typ\<cdot>REP('a))) oo emb)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   104
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   105
instance
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   106
apply (rule typedef_rep_class)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   107
apply (rule type_definition_foo)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   108
apply (rule below_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   109
apply (rule emb_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   110
apply (rule prj_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   111
apply (rule approx_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   112
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   113
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   114
end
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   115
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   116
instantiation bar :: (rep) rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   117
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   118
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   119
definition emb_bar :: "'a bar \<rightarrow> udom"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   120
where "emb_bar = (\<Lambda> x. Rep_bar x)"
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 prj_bar :: "udom \<rightarrow> 'a bar"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   123
where "prj_bar = (\<Lambda> y. Abs_bar (cast\<cdot>(bar_typ\<cdot>REP('a))\<cdot>y))"
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 approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   126
where "approx_bar = (\<lambda>i. prj oo cast\<cdot>(approx i\<cdot>(bar_typ\<cdot>REP('a))) oo emb)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   127
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   128
instance
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   129
apply (rule typedef_rep_class)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   130
apply (rule type_definition_bar)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   131
apply (rule below_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   132
apply (rule emb_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   133
apply (rule prj_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   134
apply (rule approx_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   135
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   136
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   137
end
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   138
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   139
instantiation baz :: (rep) rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   140
begin
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   141
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   142
definition emb_baz :: "'a baz \<rightarrow> udom"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   143
where "emb_baz = (\<Lambda> x. Rep_baz x)"
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 prj_baz :: "udom \<rightarrow> 'a baz"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   146
where "prj_baz = (\<Lambda> y. Abs_baz (cast\<cdot>(baz_typ\<cdot>REP('a))\<cdot>y))"
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 approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   149
where "approx_baz = (\<lambda>i. prj oo cast\<cdot>(approx i\<cdot>(baz_typ\<cdot>REP('a))) oo emb)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   150
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   151
instance
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   152
apply (rule typedef_rep_class)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   153
apply (rule type_definition_baz)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   154
apply (rule below_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   155
apply (rule emb_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   156
apply (rule prj_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   157
apply (rule approx_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   158
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   159
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   160
end
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
text {* Prove REP rules using lemma @{text typedef_REP}. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   163
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   164
lemma REP_foo: "REP('a foo) = foo_typ\<cdot>REP('a)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   165
apply (rule typedef_REP)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   166
apply (rule type_definition_foo)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   167
apply (rule below_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   168
apply (rule emb_foo_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   169
apply (rule prj_foo_def)
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
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   172
lemma REP_bar: "REP('a bar) = bar_typ\<cdot>REP('a)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   173
apply (rule typedef_REP)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   174
apply (rule type_definition_bar)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   175
apply (rule below_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   176
apply (rule emb_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   177
apply (rule prj_bar_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   178
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   179
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   180
lemma REP_baz: "REP('a baz) = baz_typ\<cdot>REP('a)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   181
apply (rule typedef_REP)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   182
apply (rule type_definition_baz)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   183
apply (rule below_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   184
apply (rule emb_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   185
apply (rule prj_baz_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   186
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   187
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   188
text {* Prove REP equations using type combinator unfold lemmas. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   189
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   190
lemma REP_foo': "REP('a foo) = REP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   191
unfolding REP_foo REP_bar REP_baz REP_simps
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   192
by (rule foo_typ_unfold)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   193
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   194
lemma REP_bar': "REP('a bar) = REP('a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   195
unfolding REP_foo REP_bar REP_baz REP_simps
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   196
by (rule bar_typ_unfold)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   197
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   198
lemma REP_baz': "REP('a baz) = REP('a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   199
unfolding REP_foo REP_bar REP_baz REP_simps
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   200
by (rule baz_typ_unfold)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   201
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
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   204
subsection {* Step 3: Define rep and abs functions *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   205
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   206
text {* Define them all using @{text coerce}! *}
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_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   209
where "foo_rep = coerce"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   210
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   211
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   212
where "foo_abs = coerce"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   213
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   214
definition bar_rep :: "'a bar \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   215
where "bar_rep = coerce"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   216
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   217
definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   218
where "bar_abs = coerce"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   219
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   220
definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   221
where "baz_rep = coerce"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   222
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   223
definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   224
where "baz_abs = coerce"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   225
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   226
text {* Prove isodefl rules using @{text isodefl_coerce}. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   227
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   228
lemma isodefl_foo_abs:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   229
  "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   230
unfolding foo_abs_def foo_rep_def
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   231
by (rule isodefl_coerce [OF REP_foo'])
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   232
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   233
lemma isodefl_bar_abs:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   234
  "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   235
unfolding bar_abs_def bar_rep_def
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   236
by (rule isodefl_coerce [OF REP_bar'])
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   237
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   238
lemma isodefl_baz_abs:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   239
  "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   240
unfolding baz_abs_def baz_rep_def
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   241
by (rule isodefl_coerce [OF REP_baz'])
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 {* TODO: prove iso predicate for rep and abs. *}
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
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   246
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   247
subsection {* Step 4: Define map functions, prove isodefl property *}
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
text {* Start with the one-step non-recursive version. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   250
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   251
text {* Note that the type of the map function depends on which
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   252
variables are used in positive and negative positions. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   253
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   254
definition
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   255
  foo_bar_baz_mapF ::
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   256
  "('a \<rightarrow> 'b)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   257
     \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   258
     \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   259
where
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   260
  "foo_bar_baz_mapF = (\<Lambda> f (d1, d2, d3).
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   261
    (
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   262
      foo_abs oo
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   263
        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
   264
          oo foo_rep
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
      bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   267
    ,
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   268
      baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   269
    ))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   270
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   271
lemma foo_bar_baz_mapF_beta:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   272
  "foo_bar_baz_mapF\<cdot>f\<cdot>d =
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>(fst (snd d))))
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
    ,
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   278
      bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(snd (snd d))) oo bar_rep
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
      baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   281
    )"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   282
unfolding foo_bar_baz_mapF_def
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   283
by (simp add: csplit_def cfst_def csnd_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   284
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   285
text {* Individual map functions are projected from the fixed point. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   286
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   287
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   288
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
   289
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   290
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   291
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
   292
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   293
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a baz \<rightarrow> 'b baz)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   294
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
   295
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   296
text {* Prove isodefl rules for all map functions simultaneously. *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   297
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   298
lemma isodefl_foo_bar_baz:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   299
  assumes isodefl_d: "isodefl d t"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   300
  shows
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   301
  "isodefl (foo_map\<cdot>d) (foo_typ\<cdot>t) \<and>
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   302
  isodefl (bar_map\<cdot>d) (bar_typ\<cdot>t) \<and>
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   303
  isodefl (baz_map\<cdot>d) (baz_typ\<cdot>t)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   304
 apply (simp add: foo_map_def bar_map_def baz_map_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   305
 apply (simp add: foo_typ_def bar_typ_def baz_typ_def)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   306
 apply (rule parallel_fix_ind
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   307
  [where F="foo_bar_baz_typF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"])
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   308
   apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   309
  apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   310
 apply (simp only: foo_bar_baz_mapF_beta
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   311
                   foo_bar_baz_typF_beta
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   312
                   fst_conv snd_conv)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   313
 apply (elim conjE)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   314
 apply (intro
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   315
  conjI
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   316
  isodefl_foo_abs
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   317
  isodefl_bar_abs
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   318
  isodefl_baz_abs
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   319
  isodefl_ssum isodefl_sprod isodefl_one isodefl_u isodefl_convex
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   320
  isodefl_d
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   321
 )
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   322
 apply assumption+
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   323
done
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
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1]
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   326
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   327
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   328
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   329
text {* Prove map ID lemmas, using isodefl_REP_imp_ID *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   330
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   331
lemma foo_map_ID: "foo_map\<cdot>ID = ID"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   332
apply (rule isodefl_REP_imp_ID)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   333
apply (subst REP_foo)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   334
apply (rule isodefl_foo)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   335
apply (rule isodefl_ID_REP)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   336
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   337
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   338
lemma bar_map_ID: "bar_map\<cdot>ID = ID"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   339
apply (rule isodefl_REP_imp_ID)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   340
apply (subst REP_bar)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   341
apply (rule isodefl_bar)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   342
apply (rule isodefl_ID_REP)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   343
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   344
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   345
lemma baz_map_ID: "baz_map\<cdot>ID = ID"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   346
apply (rule isodefl_REP_imp_ID)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   347
apply (subst REP_baz)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   348
apply (rule isodefl_baz)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   349
apply (rule isodefl_ID_REP)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   350
done
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   351
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   352
(********************************************************************)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   353
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   354
subsection {* Step 5: Define copy functions, prove reach lemmas *}
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   355
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   356
definition "foo_bar_baz_copy = foo_bar_baz_mapF\<cdot>ID"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   357
definition "foo_copy = (\<Lambda> f. fst (foo_bar_baz_copy\<cdot>f))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   358
definition "bar_copy = (\<Lambda> f. fst (snd (foo_bar_baz_copy\<cdot>f)))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   359
definition "baz_copy = (\<Lambda> f. snd (snd (foo_bar_baz_copy\<cdot>f)))"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   360
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   361
lemma fix_foo_bar_baz_copy:
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   362
  "fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   363
unfolding foo_bar_baz_copy_def foo_map_def bar_map_def baz_map_def
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   364
by simp
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   365
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   366
lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   367
unfolding fix_foo_bar_baz_copy by (simp add: foo_map_ID)
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
lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   370
unfolding fix_foo_bar_baz_copy by (simp add: bar_map_ID)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   371
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   372
lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   373
unfolding fix_foo_bar_baz_copy by (simp add: baz_map_ID)
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   374
51091e1041a7 HOLCF example: domain package proofs done manually
huffman
parents:
diff changeset
   375
end