equal
deleted
inserted
replaced
40 | "L (EMPTY) = {[]}" |
40 | "L (EMPTY) = {[]}" |
41 | "L (CHAR c) = {[c]}" |
41 | "L (CHAR c) = {[c]}" |
42 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
42 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
43 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
43 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
44 |
44 |
|
45 value "L(CHAR c)" |
|
46 value "L(SEQ(CHAR c)(CHAR b))" |
|
47 |
45 |
48 |
46 section {* Values *} |
49 section {* Values *} |
47 |
50 |
48 datatype val = |
51 datatype val = |
49 Void |
52 Void |
70 | "flat(Char c) = [c]" |
73 | "flat(Char c) = [c]" |
71 | "flat(Left v) = flat(v)" |
74 | "flat(Left v) = flat(v)" |
72 | "flat(Right v) = flat(v)" |
75 | "flat(Right v) = flat(v)" |
73 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)" |
76 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)" |
74 |
77 |
|
78 value "flat(Seq(Char c)(Char b))" |
|
79 value "flat(Right(Void))" |
|
80 |
75 fun flats :: "val \<Rightarrow> string list" |
81 fun flats :: "val \<Rightarrow> string list" |
76 where |
82 where |
77 "flats(Void) = [[]]" |
83 "flats(Void) = [[]]" |
78 | "flats(Char c) = [[c]]" |
84 | "flats(Char c) = [[c]]" |
79 | "flats(Left v) = flats(v)" |
85 | "flats(Left v) = flats(v)" |
80 | "flats(Right v) = flats(v)" |
86 | "flats(Right v) = flats(v)" |
81 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)" |
87 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)" |
|
88 |
|
89 value "flats(Seq(Char c)(Char b))" |
82 |
90 |
83 lemma Prf_flat_L: |
91 lemma Prf_flat_L: |
84 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
92 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
85 using assms |
93 using assms |
86 apply(induct) |
94 apply(induct) |
98 apply (metis Prf.intros(3) flat.simps(4)) |
106 apply (metis Prf.intros(3) flat.simps(4)) |
99 apply(erule Prf.cases) |
107 apply(erule Prf.cases) |
100 apply(auto) |
108 apply(auto) |
101 done |
109 done |
102 |
110 |
103 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100) |
111 definition definition prefix :: :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100) |
104 where |
112 where |
105 "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2" |
113 "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2" |
106 |
114 |
107 section {* Ordering of values *} |
115 section {* Ordering of values *} |
108 |
116 |