src/HOL/Wfrec.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63572 c0cbfd2b5a45
child 69593 3dda49e08b9d
permissions -rw-r--r--
executable domain membership checks
wenzelm@55210
     1
(*  Title:      HOL/Wfrec.thy
krauss@44014
     2
    Author:     Tobias Nipkow
krauss@44014
     3
    Author:     Lawrence C Paulson
krauss@44014
     4
    Author:     Konrad Slind
krauss@44014
     5
*)
krauss@44014
     6
wenzelm@60758
     7
section \<open>Well-Founded Recursion Combinator\<close>
krauss@44014
     8
krauss@44014
     9
theory Wfrec
wenzelm@63572
    10
  imports Wellfounded
krauss@44014
    11
begin
krauss@44014
    12
wenzelm@63572
    13
inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F
wenzelm@63572
    14
  where wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
krauss@44014
    15
wenzelm@63572
    16
definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
wenzelm@63572
    17
  where "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
hoelzl@58184
    18
wenzelm@63572
    19
definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool"
wenzelm@63572
    20
  where "adm_wf R F \<longleftrightarrow> (\<forall>f g x. (\<forall>z. (z, x) \<in> R \<longrightarrow> f z = g z) \<longrightarrow> F f x = F g x)"
krauss@44014
    21
wenzelm@63572
    22
definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)"
wenzelm@63572
    23
  where "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
krauss@44014
    24
hoelzl@58184
    25
lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
hoelzl@58184
    26
  by (simp add: fun_eq_iff cut_def)
krauss@44014
    27
hoelzl@58184
    28
lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
hoelzl@58184
    29
  by (simp add: cut_def)
krauss@44014
    30
wenzelm@63572
    31
text \<open>
wenzelm@63572
    32
  Inductive characterization of \<open>wfrec\<close> combinator; for details see:
wenzelm@63572
    33
  John Harrison, "Inductive definitions: automation and application".
wenzelm@63572
    34
\<close>
krauss@44014
    35
hoelzl@58184
    36
lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
hoelzl@58184
    37
  by (auto intro: the_equality[symmetric] theI)
krauss@44014
    38
wenzelm@63572
    39
lemma wfrec_unique:
wenzelm@63572
    40
  assumes "adm_wf R F" "wf R"
wenzelm@63572
    41
  shows "\<exists>!y. wfrec_rel R F x y"
wenzelm@60758
    42
  using \<open>wf R\<close>
hoelzl@58184
    43
proof induct
wenzelm@63040
    44
  define f where "f y = (THE z. wfrec_rel R F y z)" for y
hoelzl@58184
    45
  case (less x)
hoelzl@58184
    46
  then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y"
hoelzl@58184
    47
    unfolding f_def by (rule theI_unique)
wenzelm@60758
    48
  with \<open>adm_wf R F\<close> show ?case
hoelzl@58184
    49
    by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
hoelzl@58184
    50
qed
krauss@44014
    51
hoelzl@58184
    52
lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
wenzelm@63572
    53
  by (auto simp: adm_wf_def intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
hoelzl@58184
    54
hoelzl@58184
    55
lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
wenzelm@63572
    56
  apply (simp add: wfrec_def)
wenzelm@63572
    57
  apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality])
wenzelm@63572
    58
   apply assumption
wenzelm@63572
    59
  apply (rule wfrec_rel.wfrecI)
wenzelm@63572
    60
  apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
wenzelm@63572
    61
  done
krauss@44014
    62
krauss@44014
    63
wenzelm@63572
    64
text \<open>This form avoids giant explosions in proofs.  NOTE USE OF \<open>\<equiv>\<close>.\<close>
hoelzl@58184
    65
lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
wenzelm@63572
    66
  by (auto intro: wfrec)
hoelzl@58184
    67
hoelzl@58184
    68
wenzelm@60758
    69
subsubsection \<open>Well-founded recursion via genuine fixpoints\<close>
krauss@44014
    70
hoelzl@58184
    71
lemma wfrec_fixpoint:
wenzelm@63572
    72
  assumes wf: "wf R"
wenzelm@63572
    73
    and adm: "adm_wf R F"
hoelzl@58184
    74
  shows "wfrec R F = F (wfrec R F)"
hoelzl@58184
    75
proof (rule ext)
hoelzl@58184
    76
  fix x
hoelzl@58184
    77
  have "wfrec R F x = F (cut (wfrec R F) R x) x"
wenzelm@63572
    78
    using wfrec[of R F] wf by simp
hoelzl@58184
    79
  also
wenzelm@63572
    80
  have "\<And>y. (y, x) \<in> R \<Longrightarrow> cut (wfrec R F) R x y = wfrec R F y"
wenzelm@63572
    81
    by (auto simp add: cut_apply)
wenzelm@63572
    82
  then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
wenzelm@63572
    83
    using adm adm_wf_def[of R F] by auto
hoelzl@58184
    84
  finally show "wfrec R F x = F (wfrec R F) x" .
hoelzl@58184
    85
qed
krauss@44014
    86
wenzelm@63572
    87
wenzelm@61799
    88
subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
krauss@44014
    89
wenzelm@63572
    90
definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
wenzelm@63572
    91
  where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
wenzelm@63572
    92
   \<comment> \<open>For @{const wfrec} declarations where the first n parameters
wenzelm@60758
    93
       stay unchanged in the recursive call.\<close>
krauss@44014
    94
hoelzl@58184
    95
lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
hoelzl@58184
    96
  by (simp add: same_fst_def)
krauss@44014
    97
krauss@44014
    98
lemma wf_same_fst:
hoelzl@58184
    99
  assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
hoelzl@58184
   100
  shows "wf (same_fst P R)"
wenzelm@63572
   101
  apply (simp cong del: imp_cong add: wf_def same_fst_def)
wenzelm@63572
   102
  apply (intro strip)
wenzelm@63572
   103
  apply (rename_tac a b)
wenzelm@63572
   104
  apply (case_tac "wf (R a)")
wenzelm@63572
   105
   apply (erule_tac a = b in wf_induct)
wenzelm@63572
   106
   apply blast
wenzelm@63572
   107
  apply (blast intro: prem)
wenzelm@63572
   108
  done
krauss@44014
   109
krauss@44014
   110
end