(* Title: HOL/Extraction/Higman.thy ID: $Id: Higman.thy,v 1.9 2005/09/23 14:05:42 nipkow Exp $ Author: Stefan Berghofer, TU Muenchen Monika Seisenberger, LMU Muenchen *) header {* Higman's lemma *} theory Higman imports Main begin text {* Formalization by Stefan Berghofer and Monika Seisenberger, based on Coquand and Fridlender \cite{Coquand93}. *} datatype letter = A | B consts emb :: "(letter list × letter list) set" inductive emb intros emb0 [Pure.intro]: "([], bs) ∈ emb" emb1 [Pure.intro]: "(as, bs) ∈ emb ==> (as, b # bs) ∈ emb" emb2 [Pure.intro]: "(as, bs) ∈ emb ==> (a # as, a # bs) ∈ emb" consts L :: "letter list => letter list list set" inductive "L v" intros L0 [Pure.intro]: "(w, v) ∈ emb ==> w # ws ∈ L v" L1 [Pure.intro]: "ws ∈ L v ==> w # ws ∈ L v" consts good :: "letter list list set" inductive good intros good0 [Pure.intro]: "ws ∈ L w ==> w # ws ∈ good" good1 [Pure.intro]: "ws ∈ good ==> w # ws ∈ good" consts R :: "letter => (letter list list × letter list list) set" inductive "R a" intros R0 [Pure.intro]: "([], []) ∈ R a" R1 [Pure.intro]: "(vs, ws) ∈ R a ==> (w # vs, (a # w) # ws) ∈ R a" consts T :: "letter => (letter list list × letter list list) set" inductive "T a" intros T0 [Pure.intro]: "a ≠ b ==> (ws, zs) ∈ R b ==> (w # zs, (a # w) # zs) ∈ T a" T1 [Pure.intro]: "(ws, zs) ∈ T a ==> (w # ws, (a # w) # zs) ∈ T a" T2 [Pure.intro]: "a ≠ b ==> (ws, zs) ∈ T a ==> (ws, (b # w) # zs) ∈ T a" consts bar :: "letter list list set" inductive bar intros bar1 [Pure.intro]: "ws ∈ good ==> ws ∈ bar" bar2 [Pure.intro]: "(!!w. w # ws ∈ bar) ==> ws ∈ bar" theorem prop1: "([] # ws) ∈ bar" by iprover theorem lemma1: "ws ∈ L as ==> ws ∈ L (a # as)" by (erule L.induct, iprover+) lemma lemma2': "(vs, ws) ∈ R a ==> vs ∈ L as ==> ws ∈ L (a # as)" apply (induct set: R) apply (erule L.elims) apply simp+ apply (erule L.elims) apply simp_all apply (rule L0) apply (erule emb2) apply (erule L1) done lemma lemma2: "(vs, ws) ∈ R a ==> vs ∈ good ==> ws ∈ good" apply (induct set: R) apply iprover apply (erule good.elims) apply simp_all apply (rule good0) apply (erule lemma2') apply assumption apply (erule good1) done lemma lemma3': "(vs, ws) ∈ T a ==> vs ∈ L as ==> ws ∈ L (a # as)" apply (induct set: T) apply (erule L.elims) apply simp_all apply (rule L0) apply (erule emb2) apply (rule L1) apply (erule lemma1) apply (erule L.elims) apply simp_all apply iprover+ done lemma lemma3: "(ws, zs) ∈ T a ==> ws ∈ good ==> zs ∈ good" apply (induct set: T) apply (erule good.elims) apply simp_all apply (rule good0) apply (erule lemma1) apply (erule good1) apply (erule good.elims) apply simp_all apply (rule good0) apply (erule lemma3') apply iprover+ done lemma lemma4: "(ws, zs) ∈ R a ==> ws ≠ [] ==> (ws, zs) ∈ T a" apply (induct set: R) apply iprover apply (case_tac vs) apply (erule R.elims) 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) ≠ b ==> c ≠ a ==> 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 ∨ a ≠ 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 ≠ b" and bar: "xs ∈ bar" shows "!!ys zs. ys ∈ bar ==> (xs, zs) ∈ T a ==> (ys, zs) ∈ T b ==> zs ∈ bar" using bar proof induct fix xs zs assume "xs ∈ good" and "(xs, zs) ∈ T a" show "zs ∈ bar" by (rule bar1) (rule lemma3) next fix xs ys assume I: "!!w ys zs. ys ∈ bar ==> (w # xs, zs) ∈ T a ==> (ys, zs) ∈ T b ==> zs ∈ bar" assume "ys ∈ bar" thus "!!zs. (xs, zs) ∈ T a ==> (ys, zs) ∈ T b ==> zs ∈ bar" proof induct fix ys zs assume "ys ∈ good" and "(ys, zs) ∈ T b" show "zs ∈ bar" by (rule bar1) (rule lemma3) next fix ys zs assume I': "!!w zs. (xs, zs) ∈ T a ==> (w # ys, zs) ∈ T b ==> zs ∈ bar" and ys: "!!w. w # ys ∈ bar" and Ta: "(xs, zs) ∈ T a" and Tb: "(ys, zs) ∈ T b" show "zs ∈ bar" proof (rule bar2) fix w show "w # zs ∈ bar" 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 "(a # cs) # zs ∈ bar" by (iprover intro: I ys Ta Tb) thus ?thesis by (simp add: Cons ca) next assume "c ≠ a" with ab have cb: "c = b" by (rule letter_neq) from ab have "(b # cs) # zs ∈ bar" by (iprover intro: I' Ta Tb) thus ?thesis by (simp add: Cons cb) qed qed qed qed qed theorem prop3: assumes bar: "xs ∈ bar" shows "!!zs. xs ≠ [] ==> (xs, zs) ∈ R a ==> zs ∈ bar" using bar proof induct fix xs zs assume "xs ∈ good" and "(xs, zs) ∈ R a" show "zs ∈ bar" by (rule bar1) (rule lemma2) next fix xs zs assume I: "!!w zs. w # xs ≠ [] ==> (w # xs, zs) ∈ R a ==> zs ∈ bar" and xsb: "!!w. w # xs ∈ bar" and xsn: "xs ≠ []" and R: "(xs, zs) ∈ R a" show "zs ∈ bar" proof (rule bar2) fix w show "w # zs ∈ bar" 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: "(xs, zs) ∈ T a" by (rule lemma4) assume "c ≠ 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 "[w] ∈ bar" proof (induct w) show "[[]] ∈ bar" by (rule prop1) next fix c cs assume "[cs] ∈ bar" thus "[c # cs] ∈ bar" by (rule prop3) (simp, iprover) qed qed consts is_prefix :: "'a list => (nat => 'a) => bool" primrec "is_prefix [] f = True" "is_prefix (x # xs) f = (x = f (length xs) ∧ is_prefix xs f)" theorem good_prefix_lemma: assumes bar: "ws ∈ bar" shows "is_prefix ws f ==> ∃vs. is_prefix vs f ∧ vs ∈ good" using bar proof induct case bar1 thus ?case by iprover next case (bar2 ws) have "is_prefix (f (length ws) # ws) f" by simp thus ?case by (iprover intro: bar2) qed theorem good_prefix: "∃vs. is_prefix vs f ∧ vs ∈ good" using higman by (rule good_prefix_lemma) simp+ subsection {* Extracting the program *} declare bar.induct [ind_realizer] extract good_prefix text {* Program extracted from the proof of @{text good_prefix}: @{thm [display] good_prefix_def [no_vars]} Corresponding correctness theorem: @{thm [display] good_prefix_correctness [no_vars]} Program extracted from the proof of @{text good_prefix_lemma}: @{thm [display] good_prefix_lemma_def [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]} *} code_module Higman contains test = good_prefix 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 id_0 = 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 id_0 = [A,A] | f1 (Suc id_0) = [B] | f1 (Suc (Suc id_0)) = [A,B] | f1 _ = []; fun f2 id_0 = [A,A] | f2 (Suc id_0) = [B] | f2 (Suc (Suc id_0)) = [B,A] | f2 _ = []; val xs1 = test g1; val xs2 = test g2; val xs3 = test f1; val xs4 = test f2; end; *} end
theorem prop1:
[] # ws ∈ bar
theorem lemma1:
ws ∈ L as ==> ws ∈ L (a # as)
lemma lemma2':
[| (vs, ws) ∈ R a; vs ∈ L as |] ==> ws ∈ L (a # as)
lemma lemma2:
[| (vs, ws) ∈ R a; vs ∈ good |] ==> ws ∈ good
lemma lemma3':
[| (vs, ws) ∈ T a; vs ∈ L as |] ==> ws ∈ L (a # as)
lemma lemma3:
[| (ws, zs) ∈ T a; ws ∈ good |] ==> zs ∈ good
lemma lemma4:
[| (ws, zs) ∈ R a; ws ≠ [] |] ==> (ws, zs) ∈ T a
lemma letter_neq:
[| a ≠ b; c ≠ a |] ==> c = b
lemma letter_eq_dec:
a = b ∨ a ≠ b
theorem prop2:
[| a ≠ b; xs ∈ bar; ys ∈ bar; (xs, zs) ∈ T a; (ys, zs) ∈ T b |] ==> zs ∈ bar
theorem prop3:
[| xs ∈ bar; xs ≠ []; (xs, zs) ∈ R a |] ==> zs ∈ bar
theorem higman:
[] ∈ bar
theorem good_prefix_lemma:
[| ws ∈ bar; is_prefix ws f |] ==> ∃vs. is_prefix vs f ∧ vs ∈ good
theorem good_prefix:
∃vs. is_prefix vs f ∧ vs ∈ good