(* Title: HOL/Proofs/Extraction/Higman.thy
Author: Stefan Berghofer, TU Muenchen
Author: Monika Seisenberger, LMU Muenchen
*)
section ‹Higman
's lemma\
theory Higman
imports Main
begin
text ‹
Formalization
by Stefan Berghofer
and Monika Seisenberger,
based on Coquand
and Fridlender
🍋‹Coquand93
›.
›
datatype letter = A | B
inductive emb ::
"letter list \ letter list \ bool"
where
emb0 [Pure.intro]:
"emb [] bs"
| emb1 [Pure.intro]:
"emb as bs \ emb as (b # bs)"
| emb2 [Pure.intro]:
"emb as bs \ emb (a # as) (a # bs)"
inductive L ::
"letter list \ letter list list \ bool"
for v ::
"letter list"
where
L0 [Pure.intro]:
"emb w v \ L v (w # ws)"
| L1 [Pure.intro]:
"L v ws \ L v (w # ws)"
inductive good ::
"letter list list \ bool"
where
good0 [Pure.intro]:
"L w ws \ good (w # ws)"
| good1 [Pure.intro]:
"good ws \ good (w # ws)"
inductive R ::
"letter \ letter list list \ letter list list \ bool"
for a :: letter
where
R0 [Pure.intro]:
"R a [] []"
| R1 [Pure.intro]:
"R a vs ws \ R a (w # vs) ((a # w) # ws)"
inductive T ::
"letter \ letter list list \ letter list list \ bool"
for a :: letter
where
T0 [Pure.intro]:
"a \ b \ R b ws zs \ T a (w # zs) ((a # w) # zs)"
| T1 [Pure.intro]:
"T a ws zs \ T a (w # ws) ((a # w) # zs)"
| T2 [Pure.intro]:
"a \ b \ T a ws zs \ T a ws ((b # w) # zs)"
inductive bar ::
"letter list list \ bool"
where
bar1 [Pure.intro]:
"good ws \ bar ws"
| bar2 [Pure.intro]:
"(\w. bar (w # ws)) \ bar ws"
theorem prop1:
"bar ([] # ws)"
by iprover
theorem lemma1:
"L as ws \ L (a # as) ws"
by (erule L.induct) iprover+
lemma lemma2
': "R a vs ws \ L as vs \ L (a # as) ws"
supply [[simproc del: defined_all]]
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 \ good vs \ good ws"
supply [[simproc del: defined_all]]
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 \ L as vs \ L (a # as) ws"
supply [[simproc del: defined_all]]
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 \ good ws \ good zs"
supply [[simproc del: defined_all]]
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 \ ws \ [] \ T a ws zs"
supply [[simproc del: defined_all]]
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 \ b \ c \ a \ c = b" for a b c :: letter
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 = b \ a \ b" for a b :: letter
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 \ b" and bar:
"bar xs"
shows "\ys zs. bar ys \ T a xs zs \ T b ys zs \ bar zs"
using bar
proof induct
fix xs zs
assume "T a xs zs" and "good xs"
then have "good zs" by (rule lemma3)
then show "bar zs" by (rule bar1)
next
fix xs ys
assume I:
"\w ys zs. bar ys \ T a (w # xs) zs \ T b ys zs \ bar zs"
assume "bar ys"
then show "\zs. T a xs zs \ T b ys zs \ 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
': "\w zs. T a xs zs \ T b (w # ys) zs \ bar zs"
and ys:
"\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
then show ?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)
then show ?thesis
by (simp add: Cons ca)
next
assume "c \ a"
with ab
have cb:
"c = b" by (rule letter_neq)
from ab
have "bar ((b # cs) # zs)" by (iprover intro: I
' Ta Tb)
then show ?thesis
by (simp add: Cons cb)
qed
qed
qed
qed
qed
theorem prop3:
assumes bar:
"bar xs"
shows "\zs. xs \ [] \ R a xs zs \ 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:
"\w zs. w # xs \ [] \ R a (w # xs) zs \ bar zs"
and xsb:
"\w. bar (w # xs)" and xsn:
"xs \ []" 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"
then show ?thesis
by (iprover intro: I [simplified] R)
next
from R xsn
have T:
"T a xs zs" by (rule lemma4)
assume "c \ a"
then show ?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]"
then show "bar [c # cs]" by (rule prop3) (simp, iprover)
qed
qed
primrec is_prefix ::
"'a list \ (nat \ 'a) \ bool"
where
"is_prefix [] f = True"
|
"is_prefix (x # xs) f = (x = f (length xs) \ is_prefix xs f)"
theorem L_idx:
assumes L:
"L w ws"
shows "is_prefix ws f \ \i. emb (f i) w \ i < length ws"
using L
proof induct
case (L0 v ws)
then have "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
then have "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 \ \i j. emb (f i) (f j) \ i < j"
using good
proof induct
case (good0 w ws)
then have "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)
then show ?
case by simp
qed
theorem bar_idx:
assumes bar:
"bar ws"
shows "is_prefix ws f \ \i j. emb (f i) (f j) \ i < j"
using bar
proof induct
case (bar1 ws)
then show ?
case by (rule good_idx)
next
case (bar2 ws)
then have "is_prefix (f (length ws) # ws) f" by simp
then show ?
case by (rule bar2)
qed
text ‹
Strong version: yields indices of words that can be embedded into each other.
›
theorem higman_idx:
"\(i::nat) j. emb (f i) (f j) \ 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 \ \vs. is_prefix vs f \ good vs"
using bar
proof induct
case bar1
then show ?
case by iprover
next
case (bar2 ws)
from bar2.prems
have "is_prefix (f (length ws) # ws) f" by simp
then show ?
case by (iprover intro: bar2)
qed
theorem good_prefix:
"\vs. is_prefix vs f \ good vs"
using higman
by (rule good_prefix_lemma) simp+
end
