equal
deleted
inserted
replaced
11 | "at (Right v) (Suc 0#ps)= at v ps" |
11 | "at (Right v) (Suc 0#ps)= at v ps" |
12 | "at (Seq v1 v2) (0#ps)= at v1 ps" |
12 | "at (Seq v1 v2) (0#ps)= at v1 ps" |
13 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps" |
13 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps" |
14 | "at (Stars vs) (n#ps)= at (nth vs n) ps" |
14 | "at (Stars vs) (n#ps)= at (nth vs n) ps" |
15 |
15 |
16 (* |
|
17 fun |
|
18 ato :: "val \<Rightarrow> nat list \<Rightarrow> val option" |
|
19 where |
|
20 "ato v [] = Some v" |
|
21 | "ato (Left v) (0#ps)= ato v ps" |
|
22 | "ato (Right v) (Suc 0#ps)= ato v ps" |
|
23 | "ato (Seq v1 v2) (0#ps)= ato v1 ps" |
|
24 | "ato (Seq v1 v2) (Suc 0#ps)= ato v2 ps" |
|
25 | "ato (Stars vs) (n#ps)= (if (n < length vs) then ato (nth vs n) ps else None)" |
|
26 | "ato v p = None" |
|
27 *) |
|
28 |
|
29 |
|
30 fun Pos :: "val \<Rightarrow> (nat list) set" |
16 fun Pos :: "val \<Rightarrow> (nat list) set" |
31 where |
17 where |
32 "Pos (Void) = {[]}" |
18 "Pos (Void) = {[]}" |
33 | "Pos (Char c) = {[]}" |
19 | "Pos (Char c) = {[]}" |
34 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}" |
20 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}" |
41 shows "[] \<in> Pos v" |
27 shows "[] \<in> Pos v" |
42 apply(induct v rule: Pos.induct) |
28 apply(induct v rule: Pos.induct) |
43 apply(auto) |
29 apply(auto) |
44 done |
30 done |
45 |
31 |
46 lemma Pos_finite_aux: |
|
47 assumes "\<forall>v \<in> set vs. finite (Pos v)" |
|
48 shows "finite (Pos (Stars vs))" |
|
49 using assms |
|
50 apply(induct vs) |
|
51 apply(simp) |
|
52 apply(simp) |
|
53 apply(subgoal_tac "finite (Pos (Stars vs) - {[]})") |
|
54 apply(rule_tac f="\<lambda>l. Suc (hd l) # tl l" in finite_surj) |
|
55 apply(assumption) |
|
56 back |
|
57 apply(auto simp add: image_def) |
|
58 apply(rule_tac x="n#ps" in bexI) |
|
59 apply(simp) |
|
60 apply(simp) |
|
61 done |
|
62 |
|
63 lemma Pos_finite: |
|
64 shows "finite (Pos v)" |
|
65 apply(induct v rule: val.induct) |
|
66 apply(auto) |
|
67 apply(simp add: Pos_finite_aux) |
|
68 done |
|
69 |
|
70 (* |
|
71 lemma ato_test: |
|
72 assumes "p \<in> Pos v" |
|
73 shows "\<exists>v'. ato v p = Some v'" |
|
74 using assms |
|
75 apply(induct v arbitrary: p rule: Pos.induct) |
|
76 apply(auto) |
|
77 apply force |
|
78 by (metis ato.simps(6) option.distinct(1)) |
|
79 *) |
|
80 |
|
81 |
|
82 definition pflat :: "val \<Rightarrow> nat list => string option" |
|
83 where |
|
84 "pflat v p \<equiv> (if p \<in> Pos v then Some (flat (at v p)) else None)" |
|
85 |
|
86 fun intlen :: "'a list \<Rightarrow> int" |
32 fun intlen :: "'a list \<Rightarrow> int" |
87 where |
33 where |
88 "intlen [] = 0" |
34 "intlen [] = 0" |
89 | "intlen (x#xs) = 1 + intlen xs" |
35 | "intlen (x#xs) = 1 + intlen xs" |
90 |
36 |
155 apply(simp add: pflat_len_def) |
101 apply(simp add: pflat_len_def) |
156 apply(auto split: if_splits) |
102 apply(auto split: if_splits) |
157 apply (smt inlen_bigger)+ |
103 apply (smt inlen_bigger)+ |
158 done |
104 done |
159 |
105 |
160 lemma Two_to_Three: |
|
161 assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat v1 p = pflat v2 p" |
|
162 shows "Pos v1 = Pos v2" |
|
163 using assms |
|
164 by (metis Un_iff option.distinct(1) pflat_def subsetI subset_antisym) |
|
165 |
106 |
166 lemma Two_to_Three_orig: |
107 lemma Two_to_Three_orig: |
167 assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p" |
108 assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p" |
168 shows "Pos v1 = Pos v2" |
109 shows "Pos v1 = Pos v2" |
169 using assms |
110 using assms |
170 by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym) |
111 by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym) |
171 |
|
172 lemma set_eq1: |
|
173 assumes "insert [] A = insert [] B" "[] \<notin> A" "[] \<notin> B" |
|
174 shows "A = B" |
|
175 using assms |
|
176 by (simp add: insert_ident) |
|
177 |
|
178 lemma set_eq2: |
|
179 assumes "A \<union> B = A \<union> C" |
|
180 and "A \<inter> B = {}" "A \<inter> C = {}" |
|
181 shows "B = C" |
|
182 using assms |
|
183 using Un_Int_distrib sup_bot.left_neutral sup_commute by blast |
|
184 |
|
185 |
112 |
186 |
113 |
187 lemma Three_to_One: |
114 lemma Three_to_One: |
188 assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" |
115 assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" |
189 and "Pos v1 = Pos v2" |
116 and "Pos v1 = Pos v2" |
1845 apply(drule_tac x="0#p" in spec) |
1772 apply(drule_tac x="0#p" in spec) |
1846 apply (simp add: val_ord_STARI) |
1773 apply (simp add: val_ord_STARI) |
1847 apply(auto simp add: PT_def) |
1774 apply(auto simp add: PT_def) |
1848 done |
1775 done |
1849 |
1776 |
|
1777 unused_thms |
|
1778 |
1850 end |
1779 end |