equal
deleted
inserted
replaced
1 |
1 |
2 theory Positions |
2 theory Positions |
3 imports "Spec" "Lexer" |
3 imports "Spec" "Lexer" |
4 begin |
4 begin |
5 |
5 |
6 chapter {* An alternative definition for POSIX values *} |
6 chapter \<open>An alternative definition for POSIX values\<close> |
7 |
7 |
8 section {* Positions in Values *} |
8 section \<open>Positions in Values\<close> |
9 |
9 |
10 fun |
10 fun |
11 at :: "val \<Rightarrow> nat list \<Rightarrow> val" |
11 at :: "val \<Rightarrow> nat list \<Rightarrow> val" |
12 where |
12 where |
13 "at v [] = v" |
13 "at v [] = v" |
74 shows "pflat_len v1 p = -1 " |
74 shows "pflat_len v1 p = -1 " |
75 using assms by (simp add: pflat_len_def) |
75 using assms by (simp add: pflat_len_def) |
76 |
76 |
77 |
77 |
78 |
78 |
79 section {* Orderings *} |
79 section \<open>Orderings\<close> |
80 |
80 |
81 |
81 |
82 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60) |
82 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60) |
83 where |
83 where |
84 "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2" |
84 "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2" |
126 done |
126 done |
127 |
127 |
128 |
128 |
129 |
129 |
130 |
130 |
131 section {* POSIX Ordering of Values According to Okui \& Suzuki *} |
131 section \<open>POSIX Ordering of Values According to Okui \& Suzuki\<close> |
132 |
132 |
133 |
133 |
134 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
134 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
135 where |
135 where |
136 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
136 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
510 apply(auto simp add: Pos_empty pflat_len_simps) |
510 apply(auto simp add: Pos_empty pflat_len_simps) |
511 done |
511 done |
512 |
512 |
513 |
513 |
514 |
514 |
515 section {* The Posix Value is smaller than any other Value *} |
515 section \<open>The Posix Value is smaller than any other Value\<close> |
516 |
516 |
517 |
517 |
518 lemma Posix_PosOrd: |
518 lemma Posix_PosOrd: |
519 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s" |
519 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s" |
520 shows "v1 :\<sqsubseteq>val v2" |
520 shows "v1 :\<sqsubseteq>val v2" |