src/HOL/IMP/Complete_Lattice.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58889 5b7a9633cfa8
child 67613 ce654b0e6d69
permissions -rw-r--r--
Lots of new material for multivariate analysis
wenzelm@58889
     1
section "Abstract Interpretation"
nipkow@49487
     2
nipkow@48759
     3
theory Complete_Lattice
nipkow@48759
     4
imports Main
nipkow@48759
     5
begin
nipkow@48759
     6
nipkow@48759
     7
locale Complete_Lattice =
nipkow@48759
     8
fixes L :: "'a::order set" and Glb :: "'a set \<Rightarrow> 'a"
nipkow@48759
     9
assumes Glb_lower: "A \<subseteq> L \<Longrightarrow> a \<in> A \<Longrightarrow> Glb A \<le> a"
nipkow@48759
    10
and Glb_greatest: "b : L \<Longrightarrow> \<forall>a\<in>A. b \<le> a \<Longrightarrow> b \<le> Glb A"
nipkow@48759
    11
and Glb_in_L: "A \<subseteq> L \<Longrightarrow> Glb A : L"
nipkow@48759
    12
begin
nipkow@48759
    13
nipkow@48759
    14
definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
nipkow@48759
    15
"lfp f = Glb {a : L. f a \<le> a}"
nipkow@48759
    16
nipkow@48759
    17
lemma index_lfp: "lfp f : L"
nipkow@48759
    18
by(auto simp: lfp_def intro: Glb_in_L)
nipkow@48759
    19
nipkow@48759
    20
lemma lfp_lowerbound:
nipkow@48759
    21
  "\<lbrakk> a : L;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp f \<le> a"
nipkow@48759
    22
by (auto simp add: lfp_def intro: Glb_lower)
nipkow@48759
    23
nipkow@48759
    24
lemma lfp_greatest:
nipkow@48759
    25
  "\<lbrakk> a : L;  \<And>u. \<lbrakk> u : L; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp f"
nipkow@48759
    26
by (auto simp add: lfp_def intro: Glb_greatest)
nipkow@48759
    27
nipkow@48759
    28
lemma lfp_unfold: assumes "\<And>x. f x : L \<longleftrightarrow> x : L"
nipkow@48759
    29
and mono: "mono f" shows "lfp f = f (lfp f)"
nipkow@48759
    30
proof-
nipkow@48759
    31
  note assms(1)[simp] index_lfp[simp]
nipkow@48759
    32
  have 1: "f (lfp f) \<le> lfp f"
nipkow@48759
    33
    apply(rule lfp_greatest)
nipkow@48759
    34
    apply simp
nipkow@48759
    35
    by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
nipkow@48759
    36
  have "lfp f \<le> f (lfp f)"
nipkow@48759
    37
    by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)
nipkow@48759
    38
  with 1 show ?thesis by(blast intro: order_antisym)
nipkow@48759
    39
qed
nipkow@48759
    40
nipkow@48759
    41
end
nipkow@48759
    42
nipkow@48759
    43
end
nipkow@48759
    44