src/HOL/Wellfounded.thy

     Author:     Konrad Slind
     Author:     Alexander Krauss
     Author:     Andrei Popescu, TU Muenchen
 *)
 
-section {*Well-founded Recursion*}
+section \<open>Well-founded Recursion\<close>
 
 theory Wellfounded
 imports Transitive_Closure
 begin
 
-subsection {* Basic Definitions *}
+subsection \<open>Basic Definitions\<close>
 
 definition wf :: "('a * 'a) set => bool" where
   "wf r \<longleftrightarrow> (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
 
 definition wfP :: "('a => 'a => bool) => bool" where

    "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"
   unfolding wf_def by blast
 
 lemmas wfPUNIVI = wfUNIVI [to_pred]
 
-text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is
-    well-founded over their intersection, then @{term "wf r"}*}
+text\<open>Restriction to domain @{term A} and range @{term B}.  If @{term r} is
+    well-founded over their intersection, then @{term "wf r"}\<close>
 lemma wfI: 
  "[| r \<subseteq> A <*> B; 
      !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
   ==>  wf r"
   unfolding wf_def by blast

 lemma (in wellorder) wf:
   "wf {(x, y). x < y}"
 unfolding wf_def by (blast intro: less_induct)
 
 
-subsection {* Basic Results *}
-
-text {* Point-free characterization of well-foundedness *}
+subsection \<open>Basic Results\<close>
+
+text \<open>Point-free characterization of well-foundedness\<close>
 
 lemma wfE_pf:
   assumes wf: "wf R"
   assumes a: "A \<subseteq> R `` A"
   shows "A = {}"

   assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x"
   then have "?A \<subseteq> R `` ?A" by blast
   with a show "P x" by blast
 qed
 
-text{*Minimal-element characterization of well-foundedness*}
+text\<open>Minimal-element characterization of well-foundedness\<close>
 
 lemma wfE_min:
   assumes wf: "wf R" and Q: "x \<in> Q"
   obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
   using Q wfE_pf[OF wf, of Q] by blast

 apply (rule wfI_min, auto)
 done
 
 lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
 
-text{* Well-foundedness of transitive closure *}
+text\<open>Well-foundedness of transitive closure\<close>
 
 lemma wf_trancl:
   assumes "wf r"
   shows "wf (r^+)"
 proof -

     fix P and x
     assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x"
     have "P x"
     proof (rule induct_step)
       fix y assume "(y, x) : r^+"
-      with `wf r` show "P y"
+      with \<open>wf r\<close> show "P y"
       proof (induct x arbitrary: y)
         case (less x)
-        note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'`
-        from `(y, x) : r^+` show "P y"
+        note hyp = \<open>\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'\<close>
+        from \<open>(y, x) : r^+\<close> show "P y"
         proof cases
           case base
           show "P y"
           proof (rule induct_step)
             fix y' assume "(y', y) : r^+"
-            with `(y, x) : r` show "P y'" by (rule hyp [of y y'])
+            with \<open>(y, x) : r\<close> show "P y'" by (rule hyp [of y y'])
           qed
         next
           case step
           then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp
           then show "P y" by (rule hyp [of x' y])

 lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"
   apply (subst trancl_converse [symmetric])
   apply (erule wf_trancl)
   done
 
-text {* Well-foundedness of subsets *}
+text \<open>Well-foundedness of subsets\<close>
 
 lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
   apply (simp (no_asm_use) add: wf_eq_minimal)
   apply fast
   done
 
 lemmas wfP_subset = wf_subset [to_pred]
 
-text {* Well-foundedness of the empty relation *}
+text \<open>Well-foundedness of the empty relation\<close>
 
 lemma wf_empty [iff]: "wf {}"
   by (simp add: wf_def)
 
 lemma wfP_empty [iff]:

 lemma wf_Int2: "wf r ==> wf (r' Int r)"
   apply (erule wf_subset)
   apply (rule Int_lower2)
   done  
 
-text {* Exponentiation *}
+text \<open>Exponentiation\<close>
 
 lemma wf_exp:
   assumes "wf (R ^^ n)"
   shows "wf R"
 proof (rule wfI_pf)
   fix A assume "A \<subseteq> R `` A"
   then have "A \<subseteq> (R ^^ n) `` A" by (induct n) force+
-  with `wf (R ^^ n)`
+  with \<open>wf (R ^^ n)\<close>
   show "A = {}" by (rule wfE_pf)
 qed
 
-text {* Well-foundedness of insert *}
+text \<open>Well-foundedness of insert\<close>
 
 lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
 apply (rule iffI)
  apply (blast elim: wf_trancl [THEN wf_irrefl]
               intro: rtrancl_into_trancl1 wf_subset 

 apply (case_tac "y:Q")
  prefer 2 apply blast
 apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
  apply assumption
 apply (erule_tac V = "ALL Q. (EX x. x : Q) --> P Q" for P in thin_rl) 
-  --{*essential for speed*}
-txt{*Blast with new substOccur fails*}
+  --\<open>essential for speed\<close>
+txt\<open>Blast with new substOccur fails\<close>
 apply (fast intro: converse_rtrancl_into_rtrancl)
 done
 
-text{*Well-foundedness of image*}
+text\<open>Well-foundedness of image\<close>
 
 lemma wf_map_prod_image: "[| wf r; inj f |] ==> wf (map_prod f f ` r)"
 apply (simp only: wf_eq_minimal, clarify)
 apply (case_tac "EX p. f p : Q")
 apply (erule_tac x = "{p. f p : Q}" in allE)
 apply (fast dest: inj_onD, blast)
 done
 
 
-subsection {* Well-Foundedness Results for Unions *}
+subsection \<open>Well-Foundedness Results for Unions\<close>
 
 lemma wf_union_compatible:
   assumes "wf R" "wf S"
   assumes "R O S \<subseteq> R"
   shows "wf (R \<union> S)"
 proof (rule wfI_min)
   fix x :: 'a and Q 
   let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}"
   assume "x \<in> Q"
   obtain a where "a \<in> ?Q'"
-    by (rule wfE_min [OF `wf R` `x \<in> Q`]) blast
-  with `wf S`
+    by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast
+  with \<open>wf S\<close>
   obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min)
   { 
     fix y assume "(y, z) \<in> S"
     then have "y \<notin> ?Q'" by (rule zmin)
 
     have "y \<notin> Q"
     proof 
       assume "y \<in> Q"
-      with `y \<notin> ?Q'` 
+      with \<open>y \<notin> ?Q'\<close> 
       obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
-      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule relcompI)
-      with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
-      with `z \<in> ?Q'` have "w \<notin> Q" by blast 
-      with `w \<in> Q` show False by contradiction
+      from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI)
+      with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" ..
+      with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast 
+      with \<open>w \<in> Q\<close> show False by contradiction
     qed
   }
-  with `z \<in> ?Q'` show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
-qed
-
-
-text {* Well-foundedness of indexed union with disjoint domains and ranges *}
+  with \<open>z \<in> ?Q'\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
+qed
+
+
+text \<open>Well-foundedness of indexed union with disjoint domains and ranges\<close>
 
 lemma wf_UN: "[| ALL i:I. wf(r i);  
          ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {}  
       |] ==> wf(UN i:I. r i)"
 apply (simp only: wf_eq_minimal, clarify)

   show "wf ?A"
   proof (rule wfI_min)
     fix Q :: "'a set" and x 
     assume "x \<in> Q"
 
-    with `wf ?B`
+    with \<open>wf ?B\<close>
     obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
       by (erule wfE_min)
     then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
       and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
       and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
       by auto
     
     show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"
     proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")
       case True
-      with `z \<in> Q` A3 show ?thesis by blast
+      with \<open>z \<in> Q\<close> A3 show ?thesis by blast
     next
       case False 
       then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
 
       have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q"
       proof (intro allI impI)
         fix y assume "(y, z') \<in> ?A"
         then show "y \<notin> Q"
         proof
           assume "(y, z') \<in> R" 
-          then have "(y, z) \<in> R O R" using `(z', z) \<in> R` ..
+          then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> ..
           with A1 show "y \<notin> Q" .
         next
           assume "(y, z') \<in> S" 
-          then have "(y, z) \<in> S O R" using  `(z', z) \<in> R` ..
+          then have "(y, z) \<in> S O R" using  \<open>(z', z) \<in> R\<close> ..
           with A2 show "y \<notin> Q" .
         qed
       qed
-      with `z' \<in> Q` show ?thesis ..
+      with \<open>z' \<in> Q\<close> show ?thesis ..
     qed
   qed
 qed
 
-lemma wf_comp_self: "wf R = wf (R O R)"  -- {* special case *}
+lemma wf_comp_self: "wf R = wf (R O R)"  -- \<open>special case\<close>
   by (rule wf_union_merge [where S = "{}", simplified])
 
 
-subsection {* Well-Foundedness of Composition *}
+subsection \<open>Well-Foundedness of Composition\<close>
 
 text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close>
 
 lemma qc_wf_relto_iff:
   assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" -- \<open>R quasi-commutes over S\<close>

   then show ?thesis
     by (rule Wellfounded.wf_subset) blast
 qed
 
 
-subsection {* Acyclic relations *}
+subsection \<open>Acyclic relations\<close>
 
 lemma wf_acyclic: "wf r ==> acyclic r"
 apply (simp add: acyclic_def)
 apply (blast elim: wf_trancl [THEN wf_irrefl])
 done
 
 lemmas wfP_acyclicP = wf_acyclic [to_pred]
 
-text{* Wellfoundedness of finite acyclic relations*}
+text\<open>Wellfoundedness of finite acyclic relations\<close>
 
 lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
 apply (erule finite_induct, blast)
 apply (simp (no_asm_simp) only: split_tupled_all)
 apply simp

 
 lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
 by (blast intro: finite_acyclic_wf wf_acyclic)
 
 
-subsection {* @{typ nat} is well-founded *}
+subsection \<open>@{typ nat} is well-founded\<close>
 
 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
 proof (rule ext, rule ext, rule iffI)
   fix n m :: nat
   assume "m < n"

 
 lemma wf_less: "wf {(x, y::nat). x < y}"
   by (rule Wellfounded.wellorder_class.wf)
 
 
-subsection {* Accessible Part *}
-
-text {*
+subsection \<open>Accessible Part\<close>
+
+text \<open>
  Inductive definition of the accessible part @{term "acc r"} of a
  relation; see also @{cite "paulin-tlca"}.
-*}
+\<close>
 
 inductive_set
   acc :: "('a * 'a) set => 'a set"
   for r :: "('a * 'a) set"
   where

 lemma accp_eq_acc [code]:
   "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})"
   by (simp add: acc_def)
 
 
-text {* Induction rules *}
+text \<open>Induction rules\<close>
 
 theorem accp_induct:
   assumes major: "accp r a"
   assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x"
   shows "P a"

 theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
   apply (blast intro: accp_wfPI dest: accp_wfPD)
   done
 
 
-text {* Smaller relations have bigger accessible parts: *}
+text \<open>Smaller relations have bigger accessible parts:\<close>
 
 lemma accp_subset:
   assumes sub: "R1 \<le> R2"
   shows "accp R2 \<le> accp R1"
 proof (rule predicate1I)

       by (blast intro: accp.accI)
   qed
 qed
 
 
-text {* This is a generalized induction theorem that works on
-  subsets of the accessible part. *}
+text \<open>This is a generalized induction theorem that works on
+  subsets of the accessible part.\<close>
 
 lemma accp_subset_induct:
   assumes subset: "D \<le> accp R"
     and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
     and "D x"
     and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   shows "P x"
 proof -
-  from subset and `D x`
+  from subset and \<open>D x\<close>
   have "accp R x" ..
-  then show "P x" using `D x`
+  then show "P x" using \<open>D x\<close>
   proof (induct x)
     fix x
     assume "D x"
       and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
     with dcl and istep show "P x" by blast
   qed
 qed
 
 
-text {* Set versions of the above theorems *}
+text \<open>Set versions of the above theorems\<close>
 
 lemmas acc_induct = accp_induct [to_set]
 
 lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
 

 lemmas acc_subset = accp_subset [to_set]
 
 lemmas acc_subset_induct = accp_subset_induct [to_set]
 
 
-subsection {* Tools for building wellfounded relations *}
-
-text {* Inverse Image *}
+subsection \<open>Tools for building wellfounded relations\<close>
+
+text \<open>Inverse Image\<close>
 
 lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
 apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
 apply clarify
 apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")

 apply (erule allE)
 apply (erule (1) notE impE)
 apply blast
 done
 
-text {* Measure functions into @{typ nat} *}
+text \<open>Measure functions into @{typ nat}\<close>
 
 definition measure :: "('a => nat) => ('a * 'a)set"
 where "measure = inv_image less_than"
 
 lemma in_measure[simp, code_unfold]: "((x,y) : measure f) = (f x < f y)"

 apply(erule wf_subset)
 apply auto
 done
 
 
-text{* Lexicographic combinations *}
+text\<open>Lexicographic combinations\<close>
 
 definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
   "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
 
 lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"

 
 lemma in_lex_prod[simp]: 
   "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
   by (auto simp:lex_prod_def)
 
-text{* @{term "op <*lex*>"} preserves transitivity *}
+text\<open>@{term "op <*lex*>"} preserves transitivity\<close>
 
 lemma trans_lex_prod [intro!]: 
     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
 by (unfold trans_def lex_prod_def, blast) 
 
-text {* lexicographic combinations with measure functions *}
+text \<open>lexicographic combinations with measure functions\<close>
 
 definition 
   mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
 where
   "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"

 unfolding mlex_prod_def by simp
 
 lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
 unfolding mlex_prod_def by auto
 
-text {* proper subset relation on finite sets *}
+text \<open>proper subset relation on finite sets\<close>
 
 definition finite_psubset  :: "('a set * 'a set) set"
 where "finite_psubset = {(A,B). A < B & finite B}"
 
 lemma wf_finite_psubset[simp]: "wf(finite_psubset)"

 by (simp add: finite_psubset_def less_le trans_def, blast)
 
 lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset = (A < B & finite B)"
 unfolding finite_psubset_def by auto
 
-text {* max- and min-extension of order to finite sets *}
+text \<open>max- and min-extension of order to finite sets\<close>
 
 inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
 for R :: "('a \<times> 'a) set"
 where
   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"

             from asm1 have "?N2 = {}" by auto
             with Mw show "?N2 \<in> ?W" by (simp only:)
           next
             assume "M \<noteq> {}"
             from asm1 finites have N2: "(?N2, M) \<in> max_ext r" 
-              by (rule_tac max_extI[OF _ _ `M \<noteq> {}`]) auto
-
-            with `M \<in> ?W` show "?N2 \<in> ?W" by (rule acc_downward)
+              by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
+
+            with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
           qed
           with finites have "?N1 \<union> ?N2 \<in> ?W" 
             by (rule add_less) simp
           then show "N \<in> ?W" by (simp only: N)
         qed

   next
     assume "Q \<noteq> {{}}"
     with nonempty
     obtain e x where "x \<in> Q" "e \<in> x" by force
     then have eU: "e \<in> \<Union>Q" by auto
-    with `wf r` 
+    with \<open>wf r\<close> 
     obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" 
       by (erule wfE_min)
     from z obtain m where "m \<in> Q" "z \<in> m" by auto
-    from `m \<in> Q`
+    from \<open>m \<in> Q\<close>
     show ?thesis
     proof (rule, intro bexI allI impI)
       fix n
       assume smaller: "(n, m) \<in> min_ext r"
-      with `z \<in> m` obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def)
+      with \<open>z \<in> m\<close> obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def)
       then show "n \<notin> Q" using z(2) by auto
     qed      
   qed
 qed
 
-text{* Bounded increase must terminate: *}
+text\<open>Bounded increase must terminate:\<close>
 
 lemma wf_bounded_measure:
 fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat"
 assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a \<ge> f b & f b > f a"
 shows "wf r"