4 begin |
4 begin |
5 |
5 |
6 |
6 |
7 section {* Sulzmann's "Ordering" of Values *} |
7 section {* Sulzmann's "Ordering" of Values *} |
8 |
8 |
|
9 inductive ValOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ \<prec> _" [100, 100] 100) |
|
10 where |
|
11 MY0: "length (flat v2) < length (flat v1) \<Longrightarrow> v1 \<prec> v2" |
|
12 | C2: "\<lbrakk>v1 \<prec> v1'; flat (Seq v1 v2) = flat (Seq v1' v2')\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1' v2')" |
|
13 | C1: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1 v2')" |
|
14 | A2: "flat v1 = flat v2 \<Longrightarrow> (Left v1) \<prec> (Right v2)" |
|
15 | A3: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Right v2) \<prec> (Right v2')" |
|
16 | A4: "\<lbrakk>v1 \<prec> v1'; flat v1 = flat v1'\<rbrakk> \<Longrightarrow> (Left v1) \<prec> (Left v1')" |
|
17 | K1: "flat (Stars (v#vs)) = [] \<Longrightarrow> (Stars []) \<prec> (Stars (v#vs))" |
|
18 | K3: "\<lbrakk>v1 \<prec> v2; flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))\<rbrakk> \<Longrightarrow> (Stars (v1#vs1)) \<prec> (Stars (v2#vs2))" |
|
19 | K4: "\<lbrakk>(Stars vs1) \<prec> (Stars vs2); flat (Stars vs1) = flat (Stars vs2)\<rbrakk> \<Longrightarrow> (Stars (v#vs1)) \<prec> (Stars (v#vs2))" |
|
20 |
|
21 |
|
22 (* |
9 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100) |
23 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100) |
10 where |
24 where |
11 C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" |
25 C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" |
12 | C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" |
26 | C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" |
13 | A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Left v1)" |
27 | A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Left v1)" |
16 | A4: "v1 \<preceq>r1 v1' \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Left v1')" |
30 | A4: "v1 \<preceq>r1 v1' \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Left v1')" |
17 | K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<preceq>(STAR r) (Stars (v # vs))" |
31 | K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<preceq>(STAR r) (Stars (v # vs))" |
18 | K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<preceq>(STAR r) (Stars [])" |
32 | K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<preceq>(STAR r) (Stars [])" |
19 | K3: "v1 \<preceq>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<preceq>(STAR r) (Stars (v2 # vs2))" |
33 | K3: "v1 \<preceq>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<preceq>(STAR r) (Stars (v2 # vs2))" |
20 | K4: "(Stars vs1) \<preceq>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<preceq>(STAR r) (Stars (v # vs2))" |
34 | K4: "(Stars vs1) \<preceq>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<preceq>(STAR r) (Stars (v # vs2))" |
|
35 *) |
21 (*| MY1: "Void \<preceq>ONE Void" |
36 (*| MY1: "Void \<preceq>ONE Void" |
22 | MY2: "(Char c) \<preceq>(CHAR c) (Char c)" |
37 | MY2: "(Char c) \<preceq>(CHAR c) (Char c)" |
23 | MY3: "(Stars []) \<preceq>(STAR r) (Stars [])" |
38 | MY3: "(Stars []) \<preceq>(STAR r) (Stars [])" |
24 *) |
39 *) |
25 |
40 |
70 done |
85 done |
71 |
86 |
72 |
87 |
73 |
88 |
74 lemma Posix_CPT2: |
89 lemma Posix_CPT2: |
75 assumes "v1 \<preceq>r v2" "flat v2 \<sqsubseteq>pre s" "flat v1 \<sqsubseteq>pre s" |
90 assumes "v1 \<prec> v2" |
76 shows "v1 :\<sqsubset>val v2" |
91 shows "v1 :\<sqsubset>val v2" |
77 using assms |
92 using assms |
78 apply(induct v1 r v2 arbitrary: s rule: ValOrd.induct) |
93 apply(induct v1 v2 arbitrary: rule: ValOrd.induct) |
79 prefer 3 |
|
80 apply(simp) |
|
81 apply(rule val_ord_shorterI) |
94 apply(rule val_ord_shorterI) |
82 apply(simp) |
95 apply(simp) |
83 apply(subst (asm) (3) prefix_list_def) |
96 apply(rule val_ord_SeqI1) |
84 apply(subst (asm) (3) prefix_list_def) |
97 apply(simp) |
85 apply(clarify) |
98 apply(simp) |
86 apply(simp) |
99 apply(rule val_ord_SeqI2) |
|
100 apply(simp) |
|
101 apply(simp) |
|
102 apply(simp add: val_ord_ex_def) |
|
103 apply(rule_tac x="[0]" in exI) |
|
104 apply(auto simp add: val_ord_def Pos_empty pflat_len_simps)[1] |
|
105 apply(smt inlen_bigger) |
|
106 apply(rule val_ord_RightI) |
|
107 apply(simp) |
|
108 apply(simp) |
|
109 apply(rule val_ord_LeftI) |
|
110 apply(simp) |
|
111 apply(simp) |
|
112 defer |
|
113 apply(rule val_ord_StarsI) |
|
114 apply(simp) |
|
115 apply(simp) |
|
116 apply(rule val_ord_StarsI2) |
|
117 apply(simp) |
|
118 apply(simp) |
|
119 oops |
|
120 |
|
121 lemma Posix_CPT2: |
|
122 assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPTpre r s" "v2 \<in> CPTpre r s" |
|
123 shows "v1 \<prec> v2" |
|
124 using assms |
|
125 apply(induct r arbitrary: v1 v2 s) |
|
126 apply(auto simp add: CPTpre_def)[1] |
|
127 apply(erule CPrf.cases) |
|
128 apply(simp_all)[7] |
|
129 apply(auto simp add: CPTpre_def)[1] |
|
130 apply(erule CPrf.cases) |
|
131 apply(simp_all)[7] |
|
132 apply(auto simp add: CPTpre_def)[1] |
|
133 apply(erule CPrf.cases) |
|
134 apply(simp_all)[7] |
|
135 apply(simp add: val_ord_ex_def) |
|
136 apply(auto simp add: val_ord_def)[1] |
|
137 apply(auto simp add: CPTpre_def)[1] |
|
138 apply(erule CPrf.cases) |
|
139 apply(simp_all)[7] |
|
140 apply(erule CPrf.cases) |
|
141 apply(simp_all)[7] |
|
142 apply(auto simp add: val_ord_ex_def val_ord_def)[1] |
|
143 (* SEQ case *) |
|
144 apply(subst (asm) (5) CPTpre_def) |
|
145 apply(subst (asm) (5) CPTpre_def) |
|
146 apply(auto)[1] |
|
147 apply(erule CPrf.cases) |
|
148 apply(simp_all)[7] |
|
149 apply(erule CPrf.cases) |
|
150 apply(simp_all)[7] |
|
151 apply(clarify) |
|
152 apply(drule val_ord_SeqE) |
|
153 apply(erule disjE) |
|
154 apply(drule_tac x="v1a" in meta_spec) |
|
155 apply(rotate_tac 7) |
|
156 apply(drule_tac x="v1b" in meta_spec) |
|
157 apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec) |
|
158 apply(simp) |
|
159 apply(drule meta_mp) |
|
160 apply(auto simp add: CPTpre_def)[1] |
|
161 apply(drule meta_mp) |
|
162 apply(auto simp add: CPTpre_def)[1] |
|
163 apply(rule ValOrd.intros) |
|
164 apply(subst (asm) (3) CPTpre_def) |
|
165 apply(subst (asm) (3) CPTpre_def) |
|
166 apply(auto)[1] |
|
167 apply(drule_tac meta_mp) |
|
168 apply(auto simp add: CPTpre_def)[1] |
|
169 apply(erule CPrf.cases) |
|
170 apply(simp_all)[7] |
|
171 apply(erule CPrf.cases) |
|
172 apply(simp_all)[7] |
|
173 apply(clarify) |
|
174 apply(drule val_ord_SeqE) |
|
175 apply(erule disjE) |
87 apply(simp add: append_eq_append_conv2) |
176 apply(simp add: append_eq_append_conv2) |
88 apply(auto)[1] |
177 apply(auto) |
89 apply(drule_tac x="flat v1' @ flat v2' @ usa" in meta_spec) |
178 prefer 2 |
90 apply(simp add: prefix_list_def) |
179 apply(rule ValOrd.intros(2)) |
91 apply(rule val_ord_SeqI1) |
180 prefer 2 |
92 apply(simp) |
181 apply(simp) |
93 apply(simp) |
182 thm ValOrd.intros |
|
183 apply(case_tac "flat v1b = flat v1a") |
|
184 apply(rule ValOrd.intros) |
|
185 apply(simp) |
|
186 apply(simp) |
|
187 |
|
188 |
94 |
189 |
95 |
190 |
96 lemma Posix_CPT: |
191 lemma Posix_CPT: |
97 assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPT r s" "v2 \<in> CPT r s" |
192 assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPT r s" "v2 \<in> CPT r s" |
98 shows "v1 \<preceq>r v2" |
193 shows "v1 \<preceq>r v2" |