59 apply(induct xs arbitrary: ys) |
59 apply(induct xs arbitrary: ys) |
60 apply(auto) |
60 apply(auto) |
61 apply(case_tac ys) |
61 apply(case_tac ys) |
62 apply(simp_all) |
62 apply(simp_all) |
63 apply (smt intlen_bigger) |
63 apply (smt intlen_bigger) |
64 (* HERE *) |
64 apply (smt Suc_mono intlen.simps(2) length_Suc_conv less_antisym) |
65 oops |
|
66 |
|
67 |
|
68 lemma intlen_length: |
|
69 assumes "length xs < length ys" |
|
70 shows "intlen xs < intlen ys" |
|
71 using assms |
|
72 apply(induct xs arbitrary: ys) |
|
73 apply(auto) |
|
74 apply(case_tac ys) |
|
75 apply(simp_all) |
|
76 apply (smt intlen_bigger) |
|
77 by (smt Suc_lessE intlen.simps(2) length_Suc_conv) |
65 by (smt Suc_lessE intlen.simps(2) length_Suc_conv) |
78 |
66 |
79 lemma length_intlen: |
|
80 assumes "intlen xs < intlen ys" |
|
81 shows "length xs < length ys" |
|
82 using assms |
|
83 apply(induct xs arbitrary: ys) |
|
84 apply(auto) |
|
85 apply(case_tac ys) |
|
86 apply(simp_all) |
|
87 by (smt intlen_bigger) |
|
88 |
67 |
89 |
68 |
90 definition pflat_len :: "val \<Rightarrow> nat list => int" |
69 definition pflat_len :: "val \<Rightarrow> nat list => int" |
91 where |
70 where |
92 "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)" |
71 "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)" |
118 |
97 |
119 |
98 |
120 section {* Orderings *} |
99 section {* Orderings *} |
121 |
100 |
122 |
101 |
123 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _") |
102 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60) |
124 where |
103 where |
125 "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2" |
104 "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2" |
126 |
105 |
127 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _") |
106 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60) |
128 where |
107 where |
129 "ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2" |
108 "ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2" |
130 |
109 |
131 inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _") |
110 inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60) |
132 where |
111 where |
133 "[] \<sqsubset>lex (p#ps)" |
112 "[] \<sqsubset>lex (p#ps)" |
134 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)" |
113 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)" |
135 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)" |
114 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)" |
136 |
115 |
137 lemma lex_irrfl: |
116 lemma lex_irrfl: |
138 fixes ps1 ps2 :: "nat list" |
117 fixes ps1 ps2 :: "nat list" |
139 assumes "ps1 \<sqsubset>lex ps2" |
118 assumes "ps1 \<sqsubset>lex ps2" |
140 shows "ps1 \<noteq> ps2" |
119 shows "ps1 \<noteq> ps2" |
141 using assms |
120 using assms |
142 apply(induct rule: lex_list.induct) |
121 by(induct rule: lex_list.induct)(auto) |
143 apply(auto) |
122 |
144 done |
|
145 |
123 |
146 lemma lex_simps [simp]: |
124 lemma lex_simps [simp]: |
147 fixes xs ys :: "nat list" |
125 fixes xs ys :: "nat list" |
148 shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []" |
126 shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []" |
149 and "xs \<sqsubset>lex [] \<longleftrightarrow> False" |
127 and "xs \<sqsubset>lex [] \<longleftrightarrow> False" |
194 |
171 |
195 definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _") |
172 definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _") |
196 where |
173 where |
197 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
174 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
198 |
175 |
199 |
|
200 |
|
201 |
|
202 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _") |
176 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _") |
203 where |
177 where |
204 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
178 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
205 |
179 |
206 lemma val_ord_shorterE: |
180 lemma val_ord_shorterE: |
208 shows "length (flat v2) \<le> length (flat v1)" |
182 shows "length (flat v2) \<le> length (flat v1)" |
209 using assms |
183 using assms |
210 apply(auto simp add: val_ord_ex_def val_ord_def) |
184 apply(auto simp add: val_ord_ex_def val_ord_def) |
211 apply(case_tac p) |
185 apply(case_tac p) |
212 apply(simp add: pflat_len_simps) |
186 apply(simp add: pflat_len_simps) |
213 apply(drule length_intlen) |
187 apply(simp add: intlen_length) |
214 apply(simp) |
188 apply(simp) |
215 apply(drule_tac x="[]" in bspec) |
189 apply(drule_tac x="[]" in bspec) |
216 apply(simp add: Pos_empty) |
190 apply(simp add: Pos_empty) |
217 apply(simp add: pflat_len_simps) |
191 apply(simp add: pflat_len_simps) |
218 by (metis intlen_length le_less less_irrefl linear) |
192 by (metis intlen_length le_less less_irrefl linear) |
491 using assms |
465 using assms |
492 unfolding val_ord_ex_def |
466 unfolding val_ord_ex_def |
493 apply(clarify) |
467 apply(clarify) |
494 apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p") |
468 apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p") |
495 prefer 2 |
469 prefer 2 |
496 apply(rule trichotomous) |
470 apply(rule lex_trichotomous) |
497 apply(erule disjE) |
471 apply(erule disjE) |
498 apply(simp) |
472 apply(simp) |
499 apply(rule_tac x="pa" in exI) |
473 apply(rule_tac x="pa" in exI) |
500 apply(subst val_ord_def) |
474 apply(subst val_ord_def) |
501 apply(rule conjI) |
475 apply(rule conjI) |
883 apply(simp) |
857 apply(simp) |
884 apply(simp add: val_ord_ex_def) |
858 apply(simp add: val_ord_ex_def) |
885 apply(simp (no_asm) add: val_ord_def) |
859 apply(simp (no_asm) add: val_ord_def) |
886 apply(rule_tac x="[]" in exI) |
860 apply(rule_tac x="[]" in exI) |
887 apply(simp add: pflat_len_simps) |
861 apply(simp add: pflat_len_simps) |
888 apply(rule intlen_length) |
862 apply(simp only: intlen_length) |
889 apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le) |
863 apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le) |
890 apply(subgoal_tac "length (flat v1a) \<le> length s1") |
864 apply(subgoal_tac "length (flat v1a) \<le> length s1") |
891 prefer 2 |
865 prefer 2 |
892 apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_take_drop_id drop_eq_Nil) |
866 apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_take_drop_id drop_eq_Nil) |
893 apply(subst (asm) append_eq_append_conv_if) |
867 apply(subst (asm) append_eq_append_conv_if) |