src/HOL/Cardinals/Wellfounded_More.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 66453 cc19f7ca2ed6
child 67006 b1278ed3cd46
permissions -rw-r--r--
more permissive;
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
wenzelm@63167
     8
section \<open>More on Well-Founded Relations\<close>
blanchet@48975
     9
blanchet@48975
    10
theory Wellfounded_More
wenzelm@66453
    11
imports HOL.Wellfounded Order_Relation_More
blanchet@48975
    12
begin
blanchet@48975
    13
wenzelm@63167
    14
subsection \<open>Well-founded recursion via genuine fixpoints\<close>
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