min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
authorkrauss
Wed Nov 12 17:23:22 2008 +0100 (2008-11-12)
changeset 28735bed31381e6b6
parent 28734 19277c7a160c
child 28736 b1fd60fee652
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
src/HOL/Wellfounded.thy
     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"