src/HOL/Proofs/Extraction/Higman.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 40359 84388bba911d
child 43973 a907e541b127
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (*  Title:      HOL/Proofs/Extraction/Higman.thy
     2     Author:     Stefan Berghofer, TU Muenchen
     3     Author:     Monika Seisenberger, LMU Muenchen
     4 *)
     5 
     6 header {* Higman's lemma *}
     7 
     8 theory Higman
     9 imports Main "~~/src/HOL/Library/State_Monad" Random
    10 begin
    11 
    12 text {*
    13   Formalization by Stefan Berghofer and Monika Seisenberger,
    14   based on Coquand and Fridlender \cite{Coquand93}.
    15 *}
    16 
    17 datatype letter = A | B
    18 
    19 inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
    20 where
    21    emb0 [Pure.intro]: "emb [] bs"
    22  | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
    23  | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
    24 
    25 inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"
    26   for v :: "letter list"
    27 where
    28    L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"
    29  | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"
    30 
    31 inductive good :: "letter list list \<Rightarrow> bool"
    32 where
    33     good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"
    34   | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"
    35 
    36 inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
    37   for a :: letter
    38 where
    39     R0 [Pure.intro]: "R a [] []"
    40   | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"
    41 
    42 inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
    43   for a :: letter
    44 where
    45     T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"
    46   | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"
    47   | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"
    48 
    49 inductive bar :: "letter list list \<Rightarrow> bool"
    50 where
    51     bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"
    52   | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"
    53 
    54 theorem prop1: "bar ([] # ws)" by iprover
    55 
    56 theorem lemma1: "L as ws \<Longrightarrow> L (a # as) ws"
    57   by (erule L.induct, iprover+)
    58 
    59 lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"
    60   apply (induct set: R)
    61   apply (erule L.cases)
    62   apply simp+
    63   apply (erule L.cases)
    64   apply simp_all
    65   apply (rule L0)
    66   apply (erule emb2)
    67   apply (erule L1)
    68   done
    69 
    70 lemma lemma2: "R a vs ws \<Longrightarrow> good vs \<Longrightarrow> good ws"
    71   apply (induct set: R)
    72   apply iprover
    73   apply (erule good.cases)
    74   apply simp_all
    75   apply (rule good0)
    76   apply (erule lemma2')
    77   apply assumption
    78   apply (erule good1)
    79   done
    80 
    81 lemma lemma3': "T a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"
    82   apply (induct set: T)
    83   apply (erule L.cases)
    84   apply simp_all
    85   apply (rule L0)
    86   apply (erule emb2)
    87   apply (rule L1)
    88   apply (erule lemma1)
    89   apply (erule L.cases)
    90   apply simp_all
    91   apply iprover+
    92   done
    93 
    94 lemma lemma3: "T a ws zs \<Longrightarrow> good ws \<Longrightarrow> good zs"
    95   apply (induct set: T)
    96   apply (erule good.cases)
    97   apply simp_all
    98   apply (rule good0)
    99   apply (erule lemma1)
   100   apply (erule good1)
   101   apply (erule good.cases)
   102   apply simp_all
   103   apply (rule good0)
   104   apply (erule lemma3')
   105   apply iprover+
   106   done
   107 
   108 lemma lemma4: "R a ws zs \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> T a ws zs"
   109   apply (induct set: R)
   110   apply iprover
   111   apply (case_tac vs)
   112   apply (erule R.cases)
   113   apply simp
   114   apply (case_tac a)
   115   apply (rule_tac b=B in T0)
   116   apply simp
   117   apply (rule R0)
   118   apply (rule_tac b=A in T0)
   119   apply simp
   120   apply (rule R0)
   121   apply simp
   122   apply (rule T1)
   123   apply simp
   124   done
   125 
   126 lemma letter_neq: "(a::letter) \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b"
   127   apply (case_tac a)
   128   apply (case_tac b)
   129   apply (case_tac c, simp, simp)
   130   apply (case_tac c, simp, simp)
   131   apply (case_tac b)
   132   apply (case_tac c, simp, simp)
   133   apply (case_tac c, simp, simp)
   134   done
   135 
   136 lemma letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b"
   137   apply (case_tac a)
   138   apply (case_tac b)
   139   apply simp
   140   apply simp
   141   apply (case_tac b)
   142   apply simp
   143   apply simp
   144   done
   145 
   146 theorem prop2:
   147   assumes ab: "a \<noteq> b" and bar: "bar xs"
   148   shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar
   149 proof induct
   150   fix xs zs assume "T a xs zs" and "good xs"
   151   hence "good zs" by (rule lemma3)
   152   then show "bar zs" by (rule bar1)
   153 next
   154   fix xs ys
   155   assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
   156   assume "bar ys"
   157   thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
   158   proof induct
   159     fix ys zs assume "T b ys zs" and "good ys"
   160     then have "good zs" by (rule lemma3)
   161     then show "bar zs" by (rule bar1)
   162   next
   163     fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"
   164     and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"
   165     show "bar zs"
   166     proof (rule bar2)
   167       fix w
   168       show "bar (w # zs)"
   169       proof (cases w)
   170         case Nil
   171         thus ?thesis by simp (rule prop1)
   172       next
   173         case (Cons c cs)
   174         from letter_eq_dec show ?thesis
   175         proof
   176           assume ca: "c = a"
   177           from ab have "bar ((a # cs) # zs)" by (iprover intro: I ys Ta Tb)
   178           thus ?thesis by (simp add: Cons ca)
   179         next
   180           assume "c \<noteq> a"
   181           with ab have cb: "c = b" by (rule letter_neq)
   182           from ab have "bar ((b # cs) # zs)" by (iprover intro: I' Ta Tb)
   183           thus ?thesis by (simp add: Cons cb)
   184         qed
   185       qed
   186     qed
   187   qed
   188 qed
   189 
   190 theorem prop3:
   191   assumes bar: "bar xs"
   192   shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar
   193 proof induct
   194   fix xs zs
   195   assume "R a xs zs" and "good xs"
   196   then have "good zs" by (rule lemma2)
   197   then show "bar zs" by (rule bar1)
   198 next
   199   fix xs zs
   200   assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs"
   201   and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs"
   202   show "bar zs"
   203   proof (rule bar2)
   204     fix w
   205     show "bar (w # zs)"
   206     proof (induct w)
   207       case Nil
   208       show ?case by (rule prop1)
   209     next
   210       case (Cons c cs)
   211       from letter_eq_dec show ?case
   212       proof
   213         assume "c = a"
   214         thus ?thesis by (iprover intro: I [simplified] R)
   215       next
   216         from R xsn have T: "T a xs zs" by (rule lemma4)
   217         assume "c \<noteq> a"
   218         thus ?thesis by (iprover intro: prop2 Cons xsb xsn R T)
   219       qed
   220     qed
   221   qed
   222 qed
   223 
   224 theorem higman: "bar []"
   225 proof (rule bar2)
   226   fix w
   227   show "bar [w]"
   228   proof (induct w)
   229     show "bar [[]]" by (rule prop1)
   230   next
   231     fix c cs assume "bar [cs]"
   232     thus "bar [c # cs]" by (rule prop3) (simp, iprover)
   233   qed
   234 qed
   235 
   236 primrec
   237   is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
   238 where
   239     "is_prefix [] f = True"
   240   | "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"
   241 
   242 theorem L_idx:
   243   assumes L: "L w ws"
   244   shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws" using L
   245 proof induct
   246   case (L0 v ws)
   247   hence "emb (f (length ws)) w" by simp
   248   moreover have "length ws < length (v # ws)" by simp
   249   ultimately show ?case by iprover
   250 next
   251   case (L1 ws v)
   252   then obtain i where emb: "emb (f i) w" and "i < length ws"
   253     by simp iprover
   254   hence "i < length (v # ws)" by simp
   255   with emb show ?case by iprover
   256 qed
   257 
   258 theorem good_idx:
   259   assumes good: "good ws"
   260   shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using good
   261 proof induct
   262   case (good0 w ws)
   263   hence "w = f (length ws)" and "is_prefix ws f" by simp_all
   264   with good0 show ?case by (iprover dest: L_idx)
   265 next
   266   case (good1 ws w)
   267   thus ?case by simp
   268 qed
   269 
   270 theorem bar_idx:
   271   assumes bar: "bar ws"
   272   shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using bar
   273 proof induct
   274   case (bar1 ws)
   275   thus ?case by (rule good_idx)
   276 next
   277   case (bar2 ws)
   278   hence "is_prefix (f (length ws) # ws) f" by simp
   279   thus ?case by (rule bar2)
   280 qed
   281 
   282 text {*
   283 Strong version: yields indices of words that can be embedded into each other.
   284 *}
   285 
   286 theorem higman_idx: "\<exists>(i::nat) j. emb (f i) (f j) \<and> i < j"
   287 proof (rule bar_idx)
   288   show "bar []" by (rule higman)
   289   show "is_prefix [] f" by simp
   290 qed
   291 
   292 text {*
   293 Weak version: only yield sequence containing words
   294 that can be embedded into each other.
   295 *}
   296 
   297 theorem good_prefix_lemma:
   298   assumes bar: "bar ws"
   299   shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> good vs" using bar
   300 proof induct
   301   case bar1
   302   thus ?case by iprover
   303 next
   304   case (bar2 ws)
   305   from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp
   306   thus ?case by (iprover intro: bar2)
   307 qed
   308 
   309 theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> good vs"
   310   using higman
   311   by (rule good_prefix_lemma) simp+
   312 
   313 subsection {* Extracting the program *}
   314 
   315 declare R.induct [ind_realizer]
   316 declare T.induct [ind_realizer]
   317 declare L.induct [ind_realizer]
   318 declare good.induct [ind_realizer]
   319 declare bar.induct [ind_realizer]
   320 
   321 extract higman_idx
   322 
   323 text {*
   324   Program extracted from the proof of @{text higman_idx}:
   325   @{thm [display] higman_idx_def [no_vars]}
   326   Corresponding correctness theorem:
   327   @{thm [display] higman_idx_correctness [no_vars]}
   328   Program extracted from the proof of @{text higman}:
   329   @{thm [display] higman_def [no_vars]}
   330   Program extracted from the proof of @{text prop1}:
   331   @{thm [display] prop1_def [no_vars]}
   332   Program extracted from the proof of @{text prop2}:
   333   @{thm [display] prop2_def [no_vars]}
   334   Program extracted from the proof of @{text prop3}:
   335   @{thm [display] prop3_def [no_vars]}
   336 *}
   337 
   338 
   339 subsection {* Some examples *}
   340 
   341 instantiation LT and TT :: default
   342 begin
   343 
   344 definition "default = L0 [] []"
   345 
   346 definition "default = T0 A [] [] [] R0"
   347 
   348 instance ..
   349 
   350 end
   351 
   352 function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
   353   "mk_word_aux k = exec {
   354      i \<leftarrow> Random.range 10;
   355      (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
   356      else exec {
   357        let l = (if i mod 2 = 0 then A else B);
   358        ls \<leftarrow> mk_word_aux (Suc k);
   359        Pair (l # ls)
   360      })}"
   361 by pat_completeness auto
   362 termination by (relation "measure ((op -) 1001)") auto
   363 
   364 definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
   365   "mk_word = mk_word_aux 0"
   366 
   367 primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
   368   "mk_word_s 0 = mk_word"
   369   | "mk_word_s (Suc n) = exec {
   370        _ \<leftarrow> mk_word;
   371        mk_word_s n
   372      }"
   373 
   374 definition g1 :: "nat \<Rightarrow> letter list" where
   375   "g1 s = fst (mk_word_s s (20000, 1))"
   376 
   377 definition g2 :: "nat \<Rightarrow> letter list" where
   378   "g2 s = fst (mk_word_s s (50000, 1))"
   379 
   380 fun f1 :: "nat \<Rightarrow> letter list" where
   381   "f1 0 = [A, A]"
   382   | "f1 (Suc 0) = [B]"
   383   | "f1 (Suc (Suc 0)) = [A, B]"
   384   | "f1 _ = []"
   385 
   386 fun f2 :: "nat \<Rightarrow> letter list" where
   387   "f2 0 = [A, A]"
   388   | "f2 (Suc 0) = [B]"
   389   | "f2 (Suc (Suc 0)) = [B, A]"
   390   | "f2 _ = []"
   391 
   392 ML {*
   393 local
   394   val higman_idx = @{code higman_idx};
   395   val g1 = @{code g1};
   396   val g2 = @{code g2};
   397   val f1 = @{code f1};
   398   val f2 = @{code f2};
   399 in
   400   val (i1, j1) = higman_idx g1;
   401   val (v1, w1) = (g1 i1, g1 j1);
   402   val (i2, j2) = higman_idx g2;
   403   val (v2, w2) = (g2 i2, g2 j2);
   404   val (i3, j3) = higman_idx f1;
   405   val (v3, w3) = (f1 i3, f1 j3);
   406   val (i4, j4) = higman_idx f2;
   407   val (v4, w4) = (f2 i4, f2 j4);
   408 end;
   409 *}
   410 
   411 code_module Higman
   412 contains
   413   higman = higman_idx
   414 
   415 ML {*
   416 local open Higman in
   417 
   418 val a = 16807.0;
   419 val m = 2147483647.0;
   420 
   421 fun nextRand seed =
   422   let val t = a*seed
   423   in  t - m * real (Real.floor(t/m)) end;
   424 
   425 fun mk_word seed l =
   426   let
   427     val r = nextRand seed;
   428     val i = Real.round (r / m * 10.0);
   429   in if i > 7 andalso l > 2 then (r, []) else
   430     apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
   431   end;
   432 
   433 fun f s zero = mk_word s 0
   434   | f s (Suc n) = f (fst (mk_word s 0)) n;
   435 
   436 val g1 = snd o (f 20000.0);
   437 
   438 val g2 = snd o (f 50000.0);
   439 
   440 fun f1 zero = [A,A]
   441   | f1 (Suc zero) = [B]
   442   | f1 (Suc (Suc zero)) = [A,B]
   443   | f1 _ = [];
   444 
   445 fun f2 zero = [A,A]
   446   | f2 (Suc zero) = [B]
   447   | f2 (Suc (Suc zero)) = [B,A]
   448   | f2 _ = [];
   449 
   450 val (i1, j1) = higman g1;
   451 val (v1, w1) = (g1 i1, g1 j1);
   452 val (i2, j2) = higman g2;
   453 val (v2, w2) = (g2 i2, g2 j2);
   454 val (i3, j3) = higman f1;
   455 val (v3, w3) = (f1 i3, f1 j3);
   456 val (i4, j4) = higman f2;
   457 val (v4, w4) = (f2 i4, f2 j4);
   458 
   459 end;
   460 *}
   461 
   462 end