(* Title: HOL/Proofs/Extraction/Higman.thy
Author: Stefan Berghofer, TU Muenchen
Author: Monika Seisenberger, LMU Muenchen
*)
header {* Higman's lemma *}
theory Higman2
imports Main
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
notation
emb ("_ \<preceq> _")
lemma substring_refl:
"x \<preceq> x"
apply(induct x)
apply(auto intro: emb.intros)
done
lemma substring_trans:
assumes a: "x1 \<preceq> x2" and b: "x2 \<preceq> x3"
shows "x1 \<preceq> x3"
using a b
apply(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_def
apply(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)
sorry
lemma substring_closed:
"x \<in> SUBSEQ C \<and> y \<preceq> x \<Longrightarrow> y \<in> SUBSEQ C"
unfolding SUBSEQ_def
apply(auto)
apply(rule_tac x="xa" in bexI)
apply(rule substring_trans)
apply(auto)
done
lemma "SUBSEQ C \<subseteq> UNIV"
unfolding SUBSEQ_def
apply(auto)
done
ML {*
@{term "UNIV - (C::string set)"}
*}
lemma
assumes "finite S"
shows "finite (UNIV - {y. \<forall>z \<in> S. \<not>(z \<preceq> y)})"
oops
lemma a: "\<forall>x \<in> SUBSEQ C. \<exists>y \<in> C. x \<preceq> y"
unfolding SUBSEQ_def
apply(auto)
done
lemma b:
shows "\<exists>S \<subseteq> SUBSEQ C. S \<noteq>{} \<and> (y \<in> C \<longleftrightarrow> (\<forall>z \<in> S. \<not>(z \<preceq> y)))"
sorry
lemma "False"
using b a
apply(blast)
done
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
definition
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 assms
apply(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]
done
thm Least_le
lemma
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_idx
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