| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Sun, 13 Mar 2016 01:07:34 +0000 | |
| changeset 148 | 702ed601349b |
| child 154 | 2de3cf684ba0 |
| permissions | -rw-r--r-- |
|
148
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
theory Sulzmann |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
imports "ReStar" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
begin |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
section {* Sulzmann's "Ordering" of Values *}
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ >_ _" [100, 100, 100] 100)
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
where |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
C2: "v1 >r1 v1' \<Longrightarrow> (Seq v1 v2) >(SEQ r1 r2) (Seq v1' v2')" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
| C1: "v2 >r2 v2' \<Longrightarrow> (Seq v1 v2) >(SEQ r1 r2) (Seq v1 v2')" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
| A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) >(ALT r1 r2) (Left v1)" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
| A2: "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) >(ALT r1 r2) (Right v2)" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
| A3: "v2 >r2 v2' \<Longrightarrow> (Right v2) >(ALT r1 r2) (Right v2')" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
| A4: "v1 >r1 v1' \<Longrightarrow> (Left v1) >(ALT r1 r2) (Left v1')" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
| K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) >(STAR r) (Stars (v # vs))" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
| K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) >(STAR r) (Stars [])" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
| K3: "v1 >r v2 \<Longrightarrow> (Stars (v1 # vs1)) >(STAR r) (Stars (v2 # vs2))" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
| K4: "(Stars vs1) >(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) >(STAR r) (Stars (v # vs2))" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
definition ValOrdEq :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<ge>_ _" [100, 100, 100] 100)
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
where |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
"v\<^sub>1 \<ge>r v\<^sub>2 \<equiv> v\<^sub>1 = v\<^sub>2 \<or> (v\<^sub>1 >r v\<^sub>2 \<and> flat v\<^sub>1 = flat v\<^sub>2)" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
(* |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
where |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
"v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
| "Void \<succ>EMPTY Void" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
| "(Char c) \<succ>(CHAR c) (Char c)" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
| "(Stars []) \<succ>(STAR r) (Stars [])" |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
*) |
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
|
|
702ed601349b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
end |