## [f3dc84]: thys / Functional-Automata / MaxPrefix.thy  Maximize  Restore  History

### 92 lines (78 with data), 2.4 kB

 ``` 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91``` ```(* ID: \$Id: MaxPrefix.thy,v 1.3.2.1 2004-05-21 00:14:35 lsf37 Exp \$ Author: Tobias Nipkow Copyright 1998 TUM *) header "Maximal prefix" theory MaxPrefix = List_Prefix: constdefs is_maxpref :: "('a list => bool) => 'a list => 'a list => bool" "is_maxpref P xs ys == xs <= ys & (xs=[] | P xs) & (!zs. zs <= ys & P zs --> zs <= xs)" types 'a splitter = "'a list => 'a list * 'a list" constdefs is_maxsplitter :: "('a list => bool) => 'a splitter => bool" "is_maxsplitter P f == (!xs ps qs. f xs = (ps,qs) = (xs=ps@qs & is_maxpref P ps xs))" consts maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => 'a splitter" primrec "maxsplit P res ps [] = (if P ps then (ps,[]) else res)" "maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res) (ps@[q]) qs" declare split_if[split del] lemma maxsplit_lemma: "!!(ps::'a list) res. (maxsplit P res ps qs = (xs,ys)) = (if EX us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) else (xs,ys)=res)" apply(unfold is_maxpref_def) apply (induct "qs") apply (simp split: split_if) apply blast apply simp apply (erule thin_rl) apply clarify apply (case_tac "EX us. us <= list & P (ps @ a # us)") apply (subgoal_tac "EX us. us <= a # list & P (ps @ us)") apply simp apply (blast intro: prefix_Cons[THEN iffD2]) apply (subgoal_tac "~P(ps@[a])") prefer 2 apply blast apply (simp (no_asm_simp)) apply (case_tac "EX us. us <= a#list & P (ps @ us)") apply simp apply clarify apply (case_tac "us") apply (rule iffI) apply (simp add: prefix_Cons prefix_append) apply blast apply (simp add: prefix_Cons prefix_append) apply clarify apply (erule disjE) apply (fast dest: order_antisym) apply clarify apply (erule disjE) apply clarify apply simp apply (erule disjE) apply clarify apply simp apply blast apply simp apply (subgoal_tac "~P(ps)") apply (simp (no_asm_simp)) apply fastsimp done declare split_if[split add] lemma is_maxpref_Nil[simp]: "~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])" apply(unfold is_maxpref_def) apply blast done lemma is_maxsplitter_maxsplit: "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)" apply(unfold is_maxsplitter_def) apply (simp add: maxsplit_lemma) apply (fastsimp) done lemmas maxsplit_eq = is_maxsplitter_maxsplit[simplified is_maxsplitter_def] end ```