src/HOL/Cardinals/Wellfounded_More.thy
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55066 4e5ddf3162ac
parent 55027 a74ea6d75571
child 58889 5b7a9633cfa8
permissions -rw-r--r--
tuning
blanchet@49310
     1
(*  Title:      HOL/Cardinals/Wellfounded_More.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
More on well-founded relations.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* More on Well-Founded Relations *}
blanchet@48975
     9
blanchet@48975
    10
theory Wellfounded_More
blanchet@55027
    11
imports Wellfounded Order_Relation_More
blanchet@48975
    12
begin
blanchet@48975
    13
blanchet@48975
    14
subsection {* Well-founded recursion via genuine fixpoints *}
blanchet@48975
    15
blanchet@48975
    16
(*2*)lemma adm_wf_unique_fixpoint:
blanchet@48975
    17
fixes r :: "('a * 'a) set" and
blanchet@48975
    18
      H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" and
blanchet@48975
    19
      f :: "'a \<Rightarrow> 'b" and g :: "'a \<Rightarrow> 'b"
blanchet@48975
    20
assumes WF: "wf r" and ADM: "adm_wf r H" and fFP: "f = H f" and gFP: "g = H g"
blanchet@48975
    21
shows "f = g"
blanchet@48975
    22
proof-
blanchet@48975
    23
  {fix x
blanchet@48975
    24
   have "f x = g x"
blanchet@48975
    25
   proof(rule wf_induct[of r "(\<lambda>x. f x = g x)"],
blanchet@48975
    26
         auto simp add: WF)
blanchet@48975
    27
     fix x assume "\<forall>y. (y, x) \<in> r \<longrightarrow> f y = g y"
blanchet@48975
    28
     hence "H f x = H g x" using ADM adm_wf_def[of r H] by auto
blanchet@48975
    29
     thus "f x = g x" using fFP and gFP by simp
blanchet@48975
    30
   qed
blanchet@48975
    31
  }
blanchet@48975
    32
  thus ?thesis by (simp add: ext)
blanchet@48975
    33
qed
blanchet@48975
    34
blanchet@48975
    35
(*2*)lemma wfrec_unique_fixpoint:
blanchet@48975
    36
fixes r :: "('a * 'a) set" and
blanchet@48975
    37
      H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" and
blanchet@48975
    38
      f :: "'a \<Rightarrow> 'b"
blanchet@48975
    39
assumes WF: "wf r" and ADM: "adm_wf r H" and
blanchet@48975
    40
        fp: "f = H f"
blanchet@48975
    41
shows "f = wfrec r H"
blanchet@48975
    42
proof-
blanchet@48975
    43
  have "H (wfrec r H) = wfrec r H"
blanchet@48975
    44
  using assms wfrec_fixpoint[of r H] by simp
blanchet@48975
    45
  thus ?thesis
blanchet@48975
    46
  using assms adm_wf_unique_fixpoint[of r H "wfrec r H"] by simp
blanchet@48975
    47
qed
blanchet@48975
    48
blanchet@48975
    49
end