src/HOLCF/Pcpodef.thy
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 23152 9497234a2743
child 25827 c2adeb1bae5c
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/Pcpodef.thy
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
     2
    ID:         $Id$
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
     3
    Author:     Brian Huffman
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
     4
*)
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
     5
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
     6
header {* Subtypes of pcpos *}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
     7
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
     8
theory Pcpodef
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
     9
imports Adm
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19519
diff changeset
    10
uses ("Tools/pcpodef_package.ML")
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    11
begin
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    12
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    13
subsection {* Proving a subtype is a partial order *}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    14
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    15
text {*
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    16
  A subtype of a partial order is itself a partial order,
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    17
  if the ordering is defined in the standard way.
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    18
*}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    19
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    20
theorem typedef_po:
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    21
  fixes Abs :: "'a::po \<Rightarrow> 'b::sq_ord"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    22
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    23
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    24
  shows "OFCLASS('b, po_class)"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    25
 apply (intro_classes, unfold less)
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    26
   apply (rule refl_less)
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    27
  apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    28
  apply (erule (1) antisym_less)
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    29
 apply (erule (1) trans_less)
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    30
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    31
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    32
17812
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    33
subsection {* Proving a subtype is chain-finite *}
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    34
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    35
lemma monofun_Rep:
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    36
  assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    37
  shows "monofun Rep"
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    38
by (rule monofunI, unfold less)
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    39
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    40
lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep]
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    41
lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep]
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    42
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    43
theorem typedef_chfin:
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    44
  fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    45
  assumes type: "type_definition Rep Abs A"
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    46
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    47
  shows "OFCLASS('b, chfin_class)"
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    48
 apply (intro_classes, clarify)
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    49
 apply (drule ch2ch_Rep [OF less])
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    50
 apply (drule chfin [rule_format])
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    51
 apply (unfold max_in_chain_def)
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    52
 apply (simp add: type_definition.Rep_inject [OF type])
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    53
done
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    54
703005988cfe added theorem typedef_chfin
huffman
parents: 16918
diff changeset
    55
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    56
subsection {* Proving a subtype is complete *}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    57
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    58
text {*
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    59
  A subtype of a cpo is itself a cpo if the ordering is
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    60
  defined in the standard way, and the defining subset
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    61
  is closed with respect to limits of chains.  A set is
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    62
  closed if and only if membership in the set is an
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    63
  admissible predicate.
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    64
*}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    65
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    66
lemma Abs_inverse_lub_Rep:
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    67
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    68
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    69
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    70
    and adm:  "adm (\<lambda>x. x \<in> A)"
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    71
  shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    72
 apply (rule type_definition.Abs_inverse [OF type])
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    73
 apply (erule admD [OF adm ch2ch_Rep [OF less], rule_format])
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    74
 apply (rule type_definition.Rep [OF type])
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    75
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    76
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    77
theorem typedef_lub:
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    78
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    79
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    80
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    81
    and adm: "adm (\<lambda>x. x \<in> A)"
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    82
  shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    83
 apply (frule ch2ch_Rep [OF less])
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    84
 apply (rule is_lubI)
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    85
  apply (rule ub_rangeI)
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    86
  apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    87
  apply (erule is_ub_thelub)
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    88
 apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    89
 apply (erule is_lub_thelub)
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    90
 apply (erule ub2ub_Rep [OF less])
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    91
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    92
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    93
lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
    94
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    95
theorem typedef_cpo:
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    96
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    97
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    98
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
    99
    and adm: "adm (\<lambda>x. x \<in> A)"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   100
  shows "OFCLASS('b, cpo_class)"
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   101
proof
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   102
  fix S::"nat \<Rightarrow> 'b" assume "chain S"
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   103
  hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   104
    by (rule typedef_lub [OF type less adm])
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   105
  thus "\<exists>x. range S <<| x" ..
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   106
qed
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   107
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   108
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   109
subsubsection {* Continuity of @{term Rep} and @{term Abs} *}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   110
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   111
text {* For any sub-cpo, the @{term Rep} function is continuous. *}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   112
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   113
theorem typedef_cont_Rep:
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   114
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   115
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   116
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   117
    and adm: "adm (\<lambda>x. x \<in> A)"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   118
  shows "cont Rep"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   119
 apply (rule contI)
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   120
 apply (simp only: typedef_thelub [OF type less adm])
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   121
 apply (simp only: Abs_inverse_lub_Rep [OF type less adm])
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   122
 apply (rule thelubE [OF _ refl])
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   123
 apply (erule ch2ch_Rep [OF less])
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   124
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   125
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   126
text {*
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   127
  For a sub-cpo, we can make the @{term Abs} function continuous
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   128
  only if we restrict its domain to the defining subset by
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   129
  composing it with another continuous function.
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   130
*}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   131
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   132
theorem typedef_is_lubI:
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   133
  assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   134
  shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   135
 apply (rule is_lubI)
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   136
  apply (rule ub_rangeI)
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   137
  apply (subst less)
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   138
  apply (erule is_ub_lub)
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   139
 apply (subst less)
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   140
 apply (erule is_lub_lub)
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   141
 apply (erule ub2ub_Rep [OF less])
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   142
done
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   143
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   144
theorem typedef_cont_Abs:
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   145
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   146
  fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   147
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   148
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   149
    and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   150
    and f_in_A: "\<And>x. f x \<in> A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   151
    and cont_f: "cont f"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   152
  shows "cont (\<lambda>x. Abs (f x))"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   153
 apply (rule contI)
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   154
 apply (rule typedef_is_lubI [OF less])
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   155
 apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   156
 apply (erule cont_f [THEN contE])
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   157
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   158
17833
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   159
subsection {* Proving subtype elements are compact *}
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   160
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   161
theorem typedef_compact:
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   162
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   163
  assumes type: "type_definition Rep Abs A"
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   164
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   165
    and adm: "adm (\<lambda>x. x \<in> A)"
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   166
  shows "compact (Rep k) \<Longrightarrow> compact k"
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   167
proof (unfold compact_def)
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   168
  have cont_Rep: "cont Rep"
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   169
    by (rule typedef_cont_Rep [OF type less adm])
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   170
  assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   171
  with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   172
  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold less)
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   173
qed
8631dfe017a8 added theorem typedef_compact
huffman
parents: 17812
diff changeset
   174
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   175
subsection {* Proving a subtype is pointed *}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   176
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   177
text {*
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   178
  A subtype of a cpo has a least element if and only if
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   179
  the defining subset has a least element.
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   180
*}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   181
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   182
theorem typedef_pcpo_generic:
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   183
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   184
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   185
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   186
    and z_in_A: "z \<in> A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   187
    and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   188
  shows "OFCLASS('b, pcpo_class)"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   189
 apply (intro_classes)
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   190
 apply (rule_tac x="Abs z" in exI, rule allI)
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   191
 apply (unfold less)
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   192
 apply (subst type_definition.Abs_inverse [OF type z_in_A])
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   193
 apply (rule z_least [OF type_definition.Rep [OF type]])
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   194
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   195
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   196
text {*
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   197
  As a special case, a subtype of a pcpo has a least element
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   198
  if the defining subset contains @{term \<bottom>}.
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   199
*}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   200
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   201
theorem typedef_pcpo:
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   202
  fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   203
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   204
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   205
    and UU_in_A: "\<bottom> \<in> A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   206
  shows "OFCLASS('b, pcpo_class)"
16918
d0fdc7b9a33f cleaned up; renamed some theorems
huffman
parents: 16738
diff changeset
   207
by (rule typedef_pcpo_generic [OF type less UU_in_A], rule minimal)
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   208
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   209
subsubsection {* Strictness of @{term Rep} and @{term Abs} *}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   210
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   211
text {*
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   212
  For a sub-pcpo where @{term \<bottom>} is a member of the defining
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   213
  subset, @{term Rep} and @{term Abs} are both strict.
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   214
*}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   215
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   216
theorem typedef_Abs_strict:
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   217
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   218
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   219
    and UU_in_A: "\<bottom> \<in> A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   220
  shows "Abs \<bottom> = \<bottom>"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   221
 apply (rule UU_I, unfold less)
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   222
 apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   223
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   224
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   225
theorem typedef_Rep_strict:
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   226
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   227
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   228
    and UU_in_A: "\<bottom> \<in> A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   229
  shows "Rep \<bottom> = \<bottom>"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   230
 apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   231
 apply (rule type_definition.Abs_inverse [OF type UU_in_A])
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   232
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   233
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   234
theorem typedef_Abs_defined:
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   235
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   236
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   237
    and UU_in_A: "\<bottom> \<in> A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   238
  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   239
 apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   240
 apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   241
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   242
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   243
theorem typedef_Rep_defined:
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   244
  assumes type: "type_definition Rep Abs A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   245
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   246
    and UU_in_A: "\<bottom> \<in> A"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   247
  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   248
 apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   249
 apply (simp add: type_definition.Rep_inject [OF type])
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   250
done
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   251
19519
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   252
subsection {* Proving a subtype is flat *}
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   253
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   254
theorem typedef_flat:
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   255
  fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   256
  assumes type: "type_definition Rep Abs A"
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   257
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   258
    and UU_in_A: "\<bottom> \<in> A"
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   259
  shows "OFCLASS('b, flat_class)"
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   260
 apply (intro_classes)
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   261
 apply (unfold less)
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   262
 apply (simp add: type_definition.Rep_inject [OF type, symmetric])
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   263
 apply (simp add: typedef_Rep_strict [OF type less UU_in_A])
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   264
 apply (simp add: ax_flat)
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   265
done
8134024166b8 add theorem typdef_flat
huffman
parents: 17833
diff changeset
   266
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   267
subsection {* HOLCF type definition package *}
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   268
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19519
diff changeset
   269
use "Tools/pcpodef_package.ML"
16697
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   270
007f4caab6c1 renamed from TypedefPcpo.thy;
huffman
parents:
diff changeset
   271
end