(* Title: HOL/Proofs/Extraction/Higman.thy Author: Stefan Berghofer, TU Muenchen Author: Monika Seisenberger, LMU Muenchen*)header {* Higman's lemma *}theory Higman2imports Mainbegintext {* Formalization by Stefan Berghofer and Monika Seisenberger, based on Coquand and Fridlender \cite{Coquand93}.*}datatype letter = A | Binductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"where emb0 [Pure.intro]: "emb [] bs" | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)" | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool" for v :: "letter list"where L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)" | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"inductive good :: "letter list list \<Rightarrow> bool"where good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)" | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool" for a :: letterwhere R0 [Pure.intro]: "R a [] []" | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool" for a :: letterwhere T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)" | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)" | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"inductive bar :: "letter list list \<Rightarrow> bool"where bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws" | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"theorem prop1: "bar ([] # ws)" by iprovertheorem lemma1: "L as ws \<Longrightarrow> L (a # as) ws" by (erule L.induct, iprover+)lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws" apply (induct set: R) apply (erule L.cases) apply simp+ apply (erule L.cases) apply simp_all apply (rule L0) apply (erule emb2) apply (erule L1) donelemma lemma2: "R a vs ws \<Longrightarrow> good vs \<Longrightarrow> good ws" apply (induct set: R) apply iprover apply (erule good.cases) apply simp_all apply (rule good0) apply (erule lemma2') apply assumption apply (erule good1) donelemma lemma3': "T a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws" apply (induct set: T) apply (erule L.cases) apply simp_all apply (rule L0) apply (erule emb2) apply (rule L1) apply (erule lemma1) apply (erule L.cases) apply simp_all apply iprover+ donelemma lemma3: "T a ws zs \<Longrightarrow> good ws \<Longrightarrow> good zs" apply (induct set: T) apply (erule good.cases) apply simp_all apply (rule good0) apply (erule lemma1) apply (erule good1) apply (erule good.cases) apply simp_all apply (rule good0) apply (erule lemma3') apply iprover+ donelemma lemma4: "R a ws zs \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> T a ws zs" apply (induct set: R) apply iprover apply (case_tac vs) apply (erule R.cases) apply simp apply (case_tac a) apply (rule_tac b=B in T0) apply simp apply (rule R0) apply (rule_tac b=A in T0) apply simp apply (rule R0) apply simp apply (rule T1) apply simp donelemma letter_neq: "(a::letter) \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b" apply (case_tac a) apply (case_tac b) apply (case_tac c, simp, simp) apply (case_tac c, simp, simp) apply (case_tac b) apply (case_tac c, simp, simp) apply (case_tac c, simp, simp) donelemma letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b" apply (case_tac a) apply (case_tac b) apply simp apply simp apply (case_tac b) apply simp apply simp donetheorem prop2: assumes ab: "a \<noteq> b" and bar: "bar xs" shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using barproof induct fix xs zs assume "T a xs zs" and "good xs" hence "good zs" by (rule lemma3) then show "bar zs" by (rule bar1)next fix xs ys assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" assume "bar ys" thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" proof induct fix ys zs assume "T b ys zs" and "good ys" then have "good zs" by (rule lemma3) then show "bar zs" by (rule bar1) next fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs" and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs" show "bar zs" proof (rule bar2) fix w show "bar (w # zs)" proof (cases w) case Nil thus ?thesis by simp (rule prop1) next case (Cons c cs) from letter_eq_dec show ?thesis proof assume ca: "c = a" from ab have "bar ((a # cs) # zs)" by (iprover intro: I ys Ta Tb) thus ?thesis by (simp add: Cons ca) next assume "c \<noteq> a" with ab have cb: "c = b" by (rule letter_neq) from ab have "bar ((b # cs) # zs)" by (iprover intro: I' Ta Tb) thus ?thesis by (simp add: Cons cb) qed qed qed qedqedtheorem prop3: assumes bar: "bar xs" shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using barproof induct fix xs zs assume "R a xs zs" and "good xs" then have "good zs" by (rule lemma2) then show "bar zs" by (rule bar1)next fix xs zs assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs" and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs" show "bar zs" proof (rule bar2) fix w show "bar (w # zs)" proof (induct w) case Nil show ?case by (rule prop1) next case (Cons c cs) from letter_eq_dec show ?case proof assume "c = a" thus ?thesis by (iprover intro: I [simplified] R) next from R xsn have T: "T a xs zs" by (rule lemma4) assume "c \<noteq> a" thus ?thesis by (iprover intro: prop2 Cons xsb xsn R T) qed qed qedqedtheorem higman: "bar []"proof (rule bar2) fix w show "bar [w]" proof (induct w) show "bar [[]]" by (rule prop1) next fix c cs assume "bar [cs]" thus "bar [c # cs]" by (rule prop3) (simp, iprover) qedqednotation emb ("_ \<preceq> _")lemma substring_refl: "x \<preceq> x"apply(induct x)apply(auto intro: emb.intros)donelemma substring_trans: assumes a: "x1 \<preceq> x2" and b: "x2 \<preceq> x3" shows "x1 \<preceq> x3"using a bapply(induct arbitrary: x3)apply(auto intro: emb.intros)apply(rotate_tac 2)apply(erule emb.cases)apply(simp_all)sorry definition "SUBSEQ C \<equiv> {x. \<exists>y \<in> C. x \<preceq> y}"lemma "SUBSEQ (SUBSEQ C) = SUBSEQ C"unfolding SUBSEQ_defapply(auto)apply(erule emb.induct)apply(rule_tac x="xb" in bexI)apply(rule emb.intros)apply(simp)apply(erule bexE)apply(rule_tac x="y" in bexI)apply(auto)[2]apply(erule bexE)sorrylemma substring_closed: "x \<in> SUBSEQ C \<and> y \<preceq> x \<Longrightarrow> y \<in> SUBSEQ C"unfolding SUBSEQ_defapply(auto)apply(rule_tac x="xa" in bexI)apply(rule substring_trans)apply(auto)donelemma "SUBSEQ C \<subseteq> UNIV"unfolding SUBSEQ_defapply(auto)doneML {*@{term "UNIV - (C::string set)"}*}lemma assumes "finite S" shows "finite (UNIV - {y. \<forall>z \<in> S. \<not>(z \<preceq> y)})"oopslemma a: "\<forall>x \<in> SUBSEQ C. \<exists>y \<in> C. x \<preceq> y"unfolding SUBSEQ_def apply(auto)donelemma b: shows "\<exists>S \<subseteq> SUBSEQ C. S \<noteq>{} \<and> (y \<in> C \<longleftrightarrow> (\<forall>z \<in> S. \<not>(z \<preceq> y)))"sorrylemma "False"using b aapply(blast)donedefinition "CLOSED C \<equiv> C = SUBSEQ C"primrec is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"where "is_prefix [] f = True" | "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"theorem L_idx: assumes L: "L w ws" shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws" using Lproof induct case (L0 v ws) hence "emb (f (length ws)) w" by simp moreover have "length ws < length (v # ws)" by simp ultimately show ?case by iprovernext case (L1 ws v) then obtain i where emb: "emb (f i) w" and "i < length ws" by simp iprover hence "i < length (v # ws)" by simp with emb show ?case by iproverqedtheorem good_idx: assumes good: "good ws" shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using goodproof induct case (good0 w ws) hence "w = f (length ws)" and "is_prefix ws f" by simp_all with good0 show ?case by (iprover dest: L_idx)next case (good1 ws w) thus ?case by simpqedtheorem bar_idx: assumes bar: "bar ws" shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using barproof induct case (bar1 ws) thus ?case by (rule good_idx)next case (bar2 ws) hence "is_prefix (f (length ws) # ws) f" by simp thus ?case by (rule bar2)qedtext {*Strong version: yields indices of words that can be embedded into each other.*}theorem higman_idx: "\<exists>(i::nat) j. emb (f i) (f j) \<and> i < j"proof (rule bar_idx) show "bar []" by (rule higman) show "is_prefix [] f" by simpqeddefinition myeq ("~~")where "~~ \<equiv> {(x, y). x \<preceq> y \<and> y \<preceq> x}"abbreviation myeq_applied ("_ ~~~ _")where "x ~~~ y \<equiv> (x, y) \<in> ~~"definition "minimal x Y \<equiv> (x \<in> Y \<and> (\<forall>y \<in> Y. y \<preceq> x \<longrightarrow> x \<preceq> y))"definition "downclosed Y \<equiv> (\<forall>x \<in> Y. \<forall>y. y \<preceq> x \<longrightarrow> y \<in> Y)" lemma g: assumes "minimal x Y" "y ~~~ x" "downclosed Y" shows "minimal y Y"using assmsapply(simp add: minimal_def)apply(rule conjI)apply(simp add: downclosed_def)apply(simp add: myeq_def)apply(auto)[1]apply(rule ballI)apply(rule impI)apply(simp add: downclosed_def)apply(simp add: myeq_def)apply(erule conjE)apply(rotate_tac 5)apply(drule_tac x="ya" in bspec)apply(auto)[1]apply(drule mp)apply(erule conjE)apply(rule substring_trans)apply(auto)[2]apply(rule substring_trans)apply(auto)[2]donethm Least_lelemma assumes a: "\<exists>(i::nat) j. (f i) \<preceq> (f j) \<and> i < j" and "downclosed Y" shows "\<exists>S. finite S \<and> (\<forall>x \<in> Y. \<exists>y \<in> S. \<not> (y \<preceq> x))"proof - def Ymin \<equiv> "{x. minimal x Y}" have "downclosed Ymin" unfolding Ymin_def downclosed_def apply(auto) apply(simp add: minimal_def) apply(rule conjI) using assms(2) apply(simp add: downclosed_def) apply(auto)[1] apply(rule ballI) apply(rule impI) apply(erule conjE) apply(drule_tac x="ya" in bspec) apply(simp) apply(drule mp) apply(rule substring_trans) apply(auto)[2] apply(rule substring_trans) apply(auto)[2] done def Yeq \<equiv> "Ymin // ~~" def Ypick \<equiv> "(\<lambda>X. SOME x. x \<in> X) ` Yeq" have "finite Ypick" sorry moreover thm LeastI_ex have "(\<forall>x \<in> Y. \<exists>y \<in> Ypick. (\<not> (y \<preceq> x)))" apply(rule ballI) apply(subgoal_tac "\<exists>y. y \<in> Ypick") apply(erule exE) apply(rule_tac x="y" in bexI) apply(subgoal_tac "y \<in> Ymin") apply(simp add: Ymin_def minimal_def) apply(subgoal_tac "~~ `` {y} \<in> Yeq") apply(simp add: Yeq_def quotient_def Image_def) apply(erule bexE) apply(simp add: Ymin_def) apply(subgoal_tac "y ~~~ xa") apply(drule g) apply(assumption) apply(rule assms(2)) apply(simp add: minimal_def) apply(erule conjE) apply(drule_tac x="x" in bspec) apply(assumption)lemma assumes a: "\<exists>(i::nat) j. (f i) \<preceq> (f j) \<and> i < j" and b: "downclosed Y" and c: "Y \<noteq> {}" shows "\<exists>S. finite S \<and> (Y = {y. (\<forall>z \<in> S. \<not>(z \<preceq> y))})"proof - def Ybar \<equiv> "- Y" def M \<equiv> "{x \<in> Ybar. minimal x Ybar}" def Cpre \<equiv> "M // ~~" def C \<equiv> "(\<lambda>X. SOME x. x \<in> X) ` Cpre" have "finite C" sorry moreover have "\<forall>x \<in> Y. \<exists>y \<in> C. y \<preceq> x" sorry then have "\<forall>x. (x \<in> Ybar) \<longleftrightarrow> (\<exists>z \<in> C. z \<preceq> x)" apply(auto simp add: Ybar_def) apply(rule allI) apply(rule iffI) prefer 2 apply(erule bexE) apply(case_tac "x \<in> Y") prefer 2 apply(simp add: Ybar_def) apply(subgoal_tac "z \<in> Y") apply(simp add: C_def) apply(simp add: Cpre_def) apply(simp add: M_def Ybar_def) apply(simp add: quotient_def) apply(simp add: myeq_def) apply(simp add: image_def) apply(rule_tac x="x" in exI) apply(simp) apply(rule conjI) apply(simp add: minimal_def) apply(rule ballI) apply(simp) apply(rule impI) prefer 3 apply(simp add: Ybar_def) apply(rule notI) apply(simp add: C_def Cpre_def M_def Ybar_def quotient_def) prefer 2 apply(rule someI2_ex) apply(rule_tac x="x" in exI) apply(simp add: substring_refl) apply(auto)[1] using b apply - sorry ultimately have "\<exists>S. finite S \<and> (\<forall>y. y \<in> Y = (\<forall>z \<in> S. \<not>(z \<preceq> y)))" apply - apply(rule_tac x="C" in exI) apply(simp) apply(rule allI) apply(rule iffI) apply(drule_tac x="y" in spec) apply(simp add: Ybar_def) apply(simp add: Ybar_def) apply(case_tac "y \<in> Y") apply(simp) apply(drule_tac x="y" in spec) apply(simp) done then show ?thesis by (auto)qed thm higman_idxtext {*Weak version: only yield sequence containing wordsthat can be embedded into each other.*}theorem good_prefix_lemma: assumes bar: "bar ws" shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> good vs" using barproof induct case bar1 thus ?case by iprovernext case (bar2 ws) from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp thus ?case by (iprover intro: bar2)qedtheorem good_prefix: "\<exists>vs. is_prefix vs f \<and> good vs" using higman by (rule good_prefix_lemma) simp+subsection {* Extracting the program *}declare R.induct [ind_realizer]declare T.induct [ind_realizer]declare L.induct [ind_realizer]declare good.induct [ind_realizer]declare bar.induct [ind_realizer]extract higman_idxtext {* Program extracted from the proof of @{text higman_idx}: @{thm [display] higman_idx_def [no_vars]} Corresponding correctness theorem: @{thm [display] higman_idx_correctness [no_vars]} Program extracted from the proof of @{text higman}: @{thm [display] higman_def [no_vars]} Program extracted from the proof of @{text prop1}: @{thm [display] prop1_def [no_vars]} Program extracted from the proof of @{text prop2}: @{thm [display] prop2_def [no_vars]} Program extracted from the proof of @{text prop3}: @{thm [display] prop3_def [no_vars]}*}subsection {* Some examples *}instantiation LT and TT :: defaultbegindefinition "default = L0 [] []"definition "default = T0 A [] [] [] R0"instance ..endfunction mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where "mk_word_aux k = exec { i \<leftarrow> Random.range 10; (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair [] else exec { let l = (if i mod 2 = 0 then A else B); ls \<leftarrow> mk_word_aux (Suc k); Pair (l # ls) })}"by pat_completeness autotermination by (relation "measure ((op -) 1001)") autodefinition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where "mk_word = mk_word_aux 0"primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where "mk_word_s 0 = mk_word" | "mk_word_s (Suc n) = exec { _ \<leftarrow> mk_word; mk_word_s n }"definition g1 :: "nat \<Rightarrow> letter list" where "g1 s = fst (mk_word_s s (20000, 1))"definition g2 :: "nat \<Rightarrow> letter list" where "g2 s = fst (mk_word_s s (50000, 1))"fun f1 :: "nat \<Rightarrow> letter list" where "f1 0 = [A, A]" | "f1 (Suc 0) = [B]" | "f1 (Suc (Suc 0)) = [A, B]" | "f1 _ = []"fun f2 :: "nat \<Rightarrow> letter list" where "f2 0 = [A, A]" | "f2 (Suc 0) = [B]" | "f2 (Suc (Suc 0)) = [B, A]" | "f2 _ = []"ML {*local val higman_idx = @{code higman_idx}; val g1 = @{code g1}; val g2 = @{code g2}; val f1 = @{code f1}; val f2 = @{code f2};in val (i1, j1) = higman_idx g1; val (v1, w1) = (g1 i1, g1 j1); val (i2, j2) = higman_idx g2; val (v2, w2) = (g2 i2, g2 j2); val (i3, j3) = higman_idx f1; val (v3, w3) = (f1 i3, f1 j3); val (i4, j4) = higman_idx f2; val (v4, w4) = (f2 i4, f2 j4);end;*}text {* The same story with the legacy SML code generator,this can be removed once the code generator is removed. *}code_module Higmancontains higman = higman_idxML {*local open Higman inval a = 16807.0;val m = 2147483647.0;fun nextRand seed = let val t = a*seed in t - m * real (Real.floor(t/m)) end;fun mk_word seed l = let val r = nextRand seed; val i = Real.round (r / m * 10.0); in if i > 7 andalso l > 2 then (r, []) else apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1)) end;fun f s zero = mk_word s 0 | f s (Suc n) = f (fst (mk_word s 0)) n;val g1 = snd o (f 20000.0);val g2 = snd o (f 50000.0);fun f1 zero = [A,A] | f1 (Suc zero) = [B] | f1 (Suc (Suc zero)) = [A,B] | f1 _ = [];fun f2 zero = [A,A] | f2 (Suc zero) = [B] | f2 (Suc (Suc zero)) = [B,A] | f2 _ = [];val (i1, j1) = higman g1;val (v1, w1) = (g1 i1, g1 j1);val (i2, j2) = higman g2;val (v2, w2) = (g2 i2, g2 j2);val (i3, j3) = higman f1;val (v3, w3) = (f1 i3, f1 j3);val (i4, j4) = higman f2;val (v4, w4) = (f2 i4, f2 j4);end;*}end