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

Download this file

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

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:

JavaScript is required for this form.





No, thanks