src/HOL/HOLCF/Algebraic.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41959 b460124855b8
child 49834 b27bbb021df1
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 41430
diff changeset
     1
(*  Title:      HOL/HOLCF/Algebraic.thy
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
     3
*)
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
     4
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39984
diff changeset
     5
header {* Algebraic deflations *}
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
     6
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
     7
theory Algebraic
40502
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents: 40327
diff changeset
     8
imports Universal Map_Functions
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
     9
begin
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    10
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    11
default_sort bifinite
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    12
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    13
subsection {* Type constructor for finite deflations *}
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    14
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    15
typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41394
diff changeset
    16
by (fast intro: finite_deflation_bottom)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    17
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    18
instantiation fin_defl :: (bifinite) below
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    19
begin
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    20
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    21
definition below_fin_defl_def:
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    22
  "below \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    23
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    24
instance ..
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    25
end
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    26
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    27
instance fin_defl :: (bifinite) po
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    28
using type_definition_fin_defl below_fin_defl_def
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    29
by (rule typedef_po)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    30
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    31
lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    32
using Rep_fin_defl by simp
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    33
31164
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
    34
lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
    35
using finite_deflation_Rep_fin_defl
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
    36
by (rule finite_deflation_imp_deflation)
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
    37
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29252
diff changeset
    38
interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    39
by (rule finite_deflation_Rep_fin_defl)
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    40
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    41
lemma fin_defl_belowI:
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    42
  "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    43
unfolding below_fin_defl_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    44
by (rule Rep_fin_defl.belowI)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    45
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    46
lemma fin_defl_belowD:
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    47
  "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    48
unfolding below_fin_defl_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    49
by (rule Rep_fin_defl.belowD)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    50
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    51
lemma fin_defl_eqI:
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    52
  "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    53
apply (rule below_antisym)
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    54
apply (rule fin_defl_belowI, simp)
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    55
apply (rule fin_defl_belowI, simp)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    56
done
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    57
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    58
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    59
unfolding below_fin_defl_def .
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    60
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    61
lemma Abs_fin_defl_mono:
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    62
  "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    63
    \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    64
unfolding below_fin_defl_def
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    65
by (simp add: Abs_fin_defl_inverse)
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    66
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    67
lemma (in finite_deflation) compact_belowI:
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    68
  assumes "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    69
by (rule belowI, rule assms, erule subst, rule compact)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    70
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    71
lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    72
using finite_deflation_Rep_fin_defl
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    73
by (rule finite_deflation_imp_compact)
33586
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
    74
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    75
subsection {* Defining algebraic deflations by ideal completion *}
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    76
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    77
typedef (open) 'a defl = "{S::'a fin_defl set. below.ideal S}"
40888
28cd51cff70c reformulate lemma preorder.ex_ideal, and use it for typedefs
huffman
parents: 40774
diff changeset
    78
by (rule below.ex_ideal)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    79
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    80
instantiation defl :: (bifinite) below
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    81
begin
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    82
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    83
definition
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
    84
  "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    85
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    86
instance ..
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    87
end
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    88
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    89
instance defl :: (bifinite) po
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
    90
using type_definition_defl below_defl_def
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    91
by (rule below.typedef_ideal_po)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    92
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    93
instance defl :: (bifinite) cpo
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
    94
using type_definition_defl below_defl_def
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
    95
by (rule below.typedef_ideal_cpo)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    96
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
    97
definition
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    98
  defl_principal :: "'a fin_defl \<Rightarrow> 'a defl" where
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
    99
  "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   100
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
   101
lemma fin_defl_countable: "\<exists>f::'a fin_defl \<Rightarrow> nat. inj f"
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 40888
diff changeset
   102
proof -
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
   103
  obtain f :: "'a compact_basis \<Rightarrow> nat" where inj_f: "inj f"
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 40888
diff changeset
   104
    using compact_basis.countable ..
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 40888
diff changeset
   105
  have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   106
    apply (rule finite_imageI)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   107
    apply (rule finite_vimageI)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   108
    apply (rule Rep_fin_defl.finite_fixes)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   109
    apply (simp add: inj_on_def Rep_compact_basis_inject)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   110
    done
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   111
  have range_eq: "range Rep_compact_basis = {x. compact x}"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   112
    using type_definition_compact_basis by (rule type_definition.Rep_range)
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 40888
diff changeset
   113
  have "inj (\<lambda>d. set_encode
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 40888
diff changeset
   114
    (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   115
    apply (rule inj_onI)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   116
    apply (simp only: set_encode_eq *)
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 40888
diff changeset
   117
    apply (simp only: inj_image_eq_iff inj_f)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   118
    apply (drule_tac f="image Rep_compact_basis" in arg_cong)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   119
    apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   120
    apply (rule Rep_fin_defl_inject [THEN iffD1])
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   121
    apply (rule below_antisym)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   122
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   123
    apply (drule_tac x=z in spec, simp)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   124
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   125
    apply (drule_tac x=z in spec, simp)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   126
    done
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 40888
diff changeset
   127
  thus ?thesis by - (rule exI)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   128
qed
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   129
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   130
interpretation defl: ideal_completion below defl_principal Rep_defl
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   131
using type_definition_defl below_defl_def
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   132
using defl_principal_def fin_defl_countable
39984
0300d5170622 add lemma typedef_ideal_completion
huffman
parents: 39974
diff changeset
   133
by (rule below.typedef_ideal_completion)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   134
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   135
text {* Algebraic deflations are pointed *}
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   136
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   137
lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   138
apply (induct x rule: defl.principal_induct, simp)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   139
apply (rule defl.principal_mono)
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   140
apply (simp add: below_fin_defl_def)
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41394
diff changeset
   141
apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   142
done
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   143
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
   144
instance defl :: (bifinite) pcpo
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   145
by intro_classes (fast intro: defl_minimal)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   146
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   147
lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41394
diff changeset
   148
by (rule defl_minimal [THEN bottomI, symmetric])
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   149
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   150
subsection {* Applying algebraic deflations *}
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   151
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   152
definition
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
   153
  cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   154
where
41394
51c866d1b53b rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents: 41290
diff changeset
   155
  "cast = defl.extension Rep_fin_defl"
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   156
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   157
lemma cast_defl_principal:
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   158
  "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   159
unfolding cast_def
41394
51c866d1b53b rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents: 41290
diff changeset
   160
apply (rule defl.extension_principal)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
   161
apply (simp only: below_fin_defl_def)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   162
done
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   163
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   164
lemma deflation_cast: "deflation (cast\<cdot>d)"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   165
apply (induct d rule: defl.principal_induct)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   166
apply (rule adm_subst [OF _ adm_deflation], simp)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   167
apply (simp add: cast_defl_principal)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   168
apply (rule finite_deflation_imp_deflation)
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   169
apply (rule finite_deflation_Rep_fin_defl)
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   170
done
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   171
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   172
lemma finite_deflation_cast:
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   173
  "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   174
apply (drule defl.compact_imp_principal, clarify)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   175
apply (simp add: cast_defl_principal)
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   176
apply (rule finite_deflation_Rep_fin_defl)
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   177
done
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   178
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29252
diff changeset
   179
interpretation cast: deflation "cast\<cdot>d"
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   180
by (rule deflation_cast)
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   181
33586
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   182
declare cast.idem [simp]
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   183
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   184
lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   185
apply (rule finite_deflation_imp_compact)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   186
apply (erule finite_deflation_cast)
31164
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
   187
done
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
   188
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   189
lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   190
apply (induct A rule: defl.principal_induct, simp)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   191
apply (induct B rule: defl.principal_induct, simp)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   192
apply (simp add: cast_defl_principal below_fin_defl_def)
31164
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
   193
done
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
   194
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   195
lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   196
apply (rule iffI)
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   197
apply (simp only: compact_def cast_below_cast [symmetric])
40327
1dfdbd66093a renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman
parents: 40038
diff changeset
   198
apply (erule adm_subst [OF cont_Rep_cfun2])
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   199
apply (erule compact_cast)
39972
4244ff4f9649 add lemmas finite_deflation_imp_compact, cast_below_cast_iff
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   200
done
4244ff4f9649 add lemmas finite_deflation_imp_compact, cast_below_cast_iff
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   201
31164
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
   202
lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39972
diff changeset
   203
by (simp only: cast_below_cast)
31164
f550c4cf3f3a continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman
parents: 31076
diff changeset
   204
33586
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   205
lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   206
by (simp add: below_antisym cast_below_imp_below)
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   207
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   208
lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   209
apply (subst inst_defl_pcpo)
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39985
diff changeset
   210
apply (subst cast_defl_principal)
33586
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   211
apply (rule Abs_fin_defl_inverse)
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41394
diff changeset
   212
apply (simp add: finite_deflation_bottom)
33586
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   213
done
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   214
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   215
lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41394
diff changeset
   216
by (rule cast.below [THEN bottomI])
33586
0e745228d605 add in_deflation relation, more lemmas about cast
huffman
parents: 31164
diff changeset
   217
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   218
subsection {* Deflation combinators *}
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   219
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   220
definition
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   221
  "defl_fun1 e p f =
41394
51c866d1b53b rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents: 41290
diff changeset
   222
    defl.extension (\<lambda>a.
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   223
      defl_principal (Abs_fin_defl
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   224
        (e oo f\<cdot>(Rep_fin_defl a) oo p)))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   225
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   226
definition
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   227
  "defl_fun2 e p f =
41394
51c866d1b53b rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents: 41290
diff changeset
   228
    defl.extension (\<lambda>a.
51c866d1b53b rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents: 41290
diff changeset
   229
      defl.extension (\<lambda>b.
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   230
        defl_principal (Abs_fin_defl
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   231
          (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   232
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   233
lemma cast_defl_fun1:
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   234
  assumes ep: "ep_pair e p"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   235
  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   236
  shows "cast\<cdot>(defl_fun1 e p f\<cdot>A) = e oo f\<cdot>(cast\<cdot>A) oo p"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   237
proof -
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   238
  have 1: "\<And>a. finite_deflation (e oo f\<cdot>(Rep_fin_defl a) oo p)"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   239
    apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   240
    apply (rule f, rule finite_deflation_Rep_fin_defl)
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   241
    done
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   242
  show ?thesis
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   243
    by (induct A rule: defl.principal_induct, simp)
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   244
       (simp only: defl_fun1_def
41394
51c866d1b53b rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents: 41290
diff changeset
   245
                   defl.extension_principal
51c866d1b53b rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents: 41290
diff changeset
   246
                   defl.extension_mono
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   247
                   defl.principal_mono
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   248
                   Abs_fin_defl_mono [OF 1 1]
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   249
                   monofun_cfun below_refl
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   250
                   Rep_fin_defl_mono
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   251
                   cast_defl_principal
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   252
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   253
qed
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   254
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   255
lemma cast_defl_fun2:
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   256
  assumes ep: "ep_pair e p"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   257
  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   258
                finite_deflation (f\<cdot>a\<cdot>b)"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   259
  shows "cast\<cdot>(defl_fun2 e p f\<cdot>A\<cdot>B) = e oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo p"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   260
proof -
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   261
  have 1: "\<And>a b. finite_deflation
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   262
      (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   263
    apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   264
    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   265
    done
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   266
  show ?thesis
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   267
    apply (induct A rule: defl.principal_induct, simp)
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   268
    apply (induct B rule: defl.principal_induct, simp)
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   269
    by (simp only: defl_fun2_def
41394
51c866d1b53b rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents: 41290
diff changeset
   270
                   defl.extension_principal
51c866d1b53b rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents: 41290
diff changeset
   271
                   defl.extension_mono
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   272
                   defl.principal_mono
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   273
                   Abs_fin_defl_mono [OF 1 1]
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   274
                   monofun_cfun below_refl
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   275
                   Rep_fin_defl_mono
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   276
                   cast_defl_principal
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   277
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   278
qed
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   279
27409
f65a889f97f9 theory of algebraic deflations
huffman
parents:
diff changeset
   280
end