src/HOL/Wellfounded.thy
 changeset 28735 bed31381e6b6 parent 28562 4e74209f113e child 28845 cdfc8ef54a99
```     1.1 --- a/src/HOL/Wellfounded.thy	Mon Nov 10 19:42:22 2008 +0100
1.2 +++ b/src/HOL/Wellfounded.thy	Wed Nov 12 17:23:22 2008 +0100
1.3 @@ -769,6 +769,114 @@
1.4  lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset = (A < B & finite B)"
1.5  unfolding finite_psubset_def by auto
1.6
1.7 +text {* max- and min-extension of order to finite sets *}
1.8 +
1.9 +inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
1.10 +for R :: "('a \<times> 'a) set"
1.11 +where
1.12 +  max_extI[intro]: "finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R"
1.13 +
1.14 +lemma max_ext_wf:
1.15 +  assumes wf: "wf r"
1.16 +  shows "wf (max_ext r)"
1.17 +proof (rule acc_wfI, intro allI)
1.18 +  fix M show "M \<in> acc (max_ext r)" (is "_ \<in> ?W")
1.19 +  proof cases
1.20 +    assume "finite M"
1.21 +    thus ?thesis
1.22 +    proof (induct M)
1.23 +      show "{} \<in> ?W"
1.24 +        by (rule accI) (auto elim: max_ext.cases)
1.25 +    next
1.26 +      fix M a assume "M \<in> ?W" "finite M"
1.27 +      with wf show "insert a M \<in> ?W"
1.28 +      proof (induct arbitrary: M)
1.29 +        fix M a
1.30 +        assume "M \<in> ?W"  and  [intro]: "finite M"
1.31 +        assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W"
1.32 +        {
1.33 +          fix N M :: "'a set"
1.34 +          assume "finite N" "finite M"
1.35 +          then
1.36 +          have "\<lbrakk>M \<in> ?W ; (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r)\<rbrakk> \<Longrightarrow>  N \<union> M \<in> ?W"
1.37 +            by (induct N arbitrary: M) (auto simp: hyp)
1.38 +        }
1.39 +        note add_less = this
1.40 +
1.41 +        show "insert a M \<in> ?W"
1.42 +        proof (rule accI)
1.43 +          fix N assume Nless: "(N, insert a M) \<in> max_ext r"
1.44 +          hence asm1: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)"
1.45 +            by (auto elim!: max_ext.cases)
1.46 +
1.47 +          let ?N1 = "{ n \<in> N. (n, a) \<in> r }"
1.48 +          let ?N2 = "{ n \<in> N. (n, a) \<notin> r }"
1.49 +          have N: "?N1 \<union> ?N2 = N" by (rule set_ext) auto
1.50 +          from Nless have "finite N" by (auto elim: max_ext.cases)
1.51 +          then have finites: "finite ?N1" "finite ?N2" by auto
1.52 +
1.53 +          have "?N2 \<in> ?W"
1.54 +          proof cases
1.55 +            assume [simp]: "M = {}"
1.56 +            have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases)
1.57 +
1.58 +            from asm1 have "?N2 = {}" by auto
1.59 +            with Mw show "?N2 \<in> ?W" by (simp only:)
1.60 +          next
1.61 +            assume "M \<noteq> {}"
1.62 +            have N2: "(?N2, M) \<in> max_ext r"
1.63 +              by (rule max_extI[OF _ _ `M \<noteq> {}`]) (insert asm1, auto intro: finites)
1.64 +
1.65 +            with `M \<in> ?W` show "?N2 \<in> ?W" by (rule acc_downward)
1.66 +          qed
1.67 +          with finites have "?N1 \<union> ?N2 \<in> ?W"
1.68 +            by (rule add_less) simp
1.69 +          then show "N \<in> ?W" by (simp only: N)
1.70 +        qed
1.71 +      qed
1.72 +    qed
1.73 +  next
1.74 +    assume [simp]: "\<not> finite M"
1.75 +    show ?thesis
1.76 +      by (rule accI) (auto elim: max_ext.cases)
1.77 +  qed
1.78 +qed
1.79 +
1.80 +
1.81 +definition
1.82 +  min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
1.83 +where
1.84 +  [code del]: "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
1.85 +
1.86 +lemma min_ext_wf:
1.87 +  assumes "wf r"
1.88 +  shows "wf (min_ext r)"
1.89 +proof (rule wfI_min)
1.90 +  fix Q :: "'a set set"
1.91 +  fix x
1.92 +  assume nonempty: "x \<in> Q"
1.93 +  show "\<exists>m \<in> Q. (\<forall> n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)"
1.94 +  proof cases
1.95 +    assume "Q = {{}}" thus ?thesis by (simp add: min_ext_def)
1.96 +  next
1.97 +    assume "Q \<noteq> {{}}"
1.98 +    with nonempty
1.99 +    obtain e x where "x \<in> Q" "e \<in> x" by force
1.100 +    then have eU: "e \<in> \<Union>Q" by auto
1.101 +    with `wf r`
1.102 +    obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q"
1.103 +      by (erule wfE_min)
1.104 +    from z obtain m where "m \<in> Q" "z \<in> m" by auto
1.105 +    from `m \<in> Q`
1.106 +    show ?thesis
1.107 +    proof (rule, intro bexI allI impI)
1.108 +      fix n
1.109 +      assume smaller: "(n, m) \<in> min_ext r"
1.110 +      with `z \<in> m` obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def)
1.111 +      then show "n \<notin> Q" using z(2) by auto
1.112 +    qed
1.113 +  qed
1.114 +qed
1.115
1.116  text {*Wellfoundedness of @{text same_fst}*}
1.117
1.118 @@ -777,8 +885,7 @@
1.119  where
1.120      "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
1.121     --{*For @{text rec_def} declarations where the first n parameters
1.122 -       stay unchanged in the recursive call.
1.123 -       See @{text "Library/While_Combinator.thy"} for an application.*}
1.124 +       stay unchanged in the recursive call. *}
1.125
1.126  lemma same_fstI [intro!]:
1.127       "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
```