Quelle Higman.thy Sprache: Isabelle

(*  Title:      HOL/Proofs/Extraction/Higman.thy
    Author:     Stefan Berghofer, TU Muenchen
    Author:     Monika Seisenberger, LMU Muenchen
*)

section \<open>Higman's lemma\<close>

theory Higman
imports Main
begin

text \<open>
  Formalization by Stefan Berghofer and Monika Seisenberger,
  based on Coquand and Fridlender \<^cite>\<open>Coquand93\<close>.
\<close>

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 \<open>
  Strong version: yields indices of words that can be embedded into each other.
\<close>

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 \<open>
  Weak version: only yield sequence containing words
  that can be embedded into each other.
\<close>

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

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

über den Urheber dieser Seite

Die Firma ist wie angegeben erreichbar.

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

diese Dinge liegen außhalb unserer Verantwortung

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.