--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Higman2.thy Tue Aug 23 12:36:43 2011 +0000
@@ -0,0 +1,517 @@
+(* Title: HOL/Proofs/Extraction/Higman.thy
+ Author: Stefan Berghofer, TU Muenchen
+ Author: Monika Seisenberger, LMU Muenchen
+*)
+
+header {* Higman's lemma *}
+
+theory Higman2
+imports Closures
+begin
+
+text {*
+ Formalization by Stefan Berghofer and Monika Seisenberger,
+ based on Coquand and Fridlender \cite{Coquand93}.
+*}
+
+datatype letter = A | B
+
+inductive 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 :: letter
+where
+ 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 :: letter
+where
+ 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 iprover
+
+theorem 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)
+ done
+
+lemma 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)
+ done
+
+lemma 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+
+ done
+
+lemma 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+
+ done
+
+lemma 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
+ done
+
+lemma 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)
+ done
+
+lemma 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
+ done
+
+theorem 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 bar
+proof 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
+ qed
+qed
+
+theorem prop3:
+ assumes bar: "bar xs"
+ shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar
+proof 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
+ qed
+qed
+
+theorem 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)
+ qed
+qed
+
+inductive substring ("_ \<preceq> _")
+where
+ "[] \<preceq> y"
+| "x \<preceq> y \<Longrightarrow> c # x \<preceq> y"
+| "x \<preceq> y \<Longrightarrow> c # x \<preceq> c # y"
+
+lemma substring_refl:
+ "x \<preceq> x"
+apply(induct x)
+apply(auto intro: substring.intros)
+done
+
+definition
+ "SUBSEQ C \<equiv> {x. \<exists>y \<in> C. x \<preceq> y}"
+
+lemma
+ "SUBSEQ (SUBSEQ C) = SUBSEQ C"
+unfolding SUBSEQ_def
+apply(auto)
+apply(erule substring.induct)
+apply(rule_tac x="xb" in bexI)
+apply(rule substring.intros)
+apply(simp)
+apply(erule bexE)
+apply(rule_tac x="ya" in bexI)
+apply(rule substring.intros)
+apply(auto)[2]
+apply(erule bexE)
+apply(rule_tac x="ya" in bexI)
+apply(rule substring.intros)
+apply(auto)[2]
+apply(rule_tac x="x" in exI)
+apply(rule conjI)
+apply(rule_tac x="y" in bexI)
+apply(auto)[2]
+apply(rule substring_refl)
+done
+
+lemma
+ "x \<in> SUBSEQ C \<and> y \<preceq> x \<Longrightarrow> y \<in> SUBSEQ C"
+unfolding SUBSEQ_def
+apply(auto)
+
+
+definition
+ "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 L
+proof 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 iprover
+next
+ 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 iprover
+qed
+
+theorem good_idx:
+ assumes good: "good ws"
+ shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using good
+proof 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 simp
+qed
+
+theorem bar_idx:
+ assumes bar: "bar ws"
+ shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using bar
+proof 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)
+qed
+
+text {*
+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 simp
+qed
+
+text {*
+Weak version: only yield sequence containing words
+that 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 bar
+proof induct
+ case bar1
+ thus ?case by iprover
+next
+ case (bar2 ws)
+ from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp
+ thus ?case by (iprover intro: bar2)
+qed
+
+theorem 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_idx
+
+text {*
+ 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 :: default
+begin
+
+definition "default = L0 [] []"
+
+definition "default = T0 A [] [] [] R0"
+
+instance ..
+
+end
+
+function 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 auto
+termination by (relation "measure ((op -) 1001)") auto
+
+definition 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 Higman
+contains
+ higman = higman_idx
+
+ML {*
+local open Higman in
+
+val 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