thys/PositionsExt.thy
author Chengsong
Tue, 20 Dec 2022 22:32:54 +0000
changeset 635 7ce2389dff4b
parent 286 804fbb227568
permissions -rw-r--r--
more
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
   
276
a3134f7de065 updated
cu
parents: 273
diff changeset
     2
theory PositionsExt
a3134f7de065 updated
cu
parents: 273
diff changeset
     3
  imports "SpecExt" "LexerExt" 
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
begin
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
     6
section {* Positions in Values *}
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
     7
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
fun 
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
  at :: "val \<Rightarrow> nat list \<Rightarrow> val"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
  "at v [] = v"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
| "at (Left v) (0#ps)= at v ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
| "at (Right v) (Suc 0#ps)= at v ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
| "at (Seq v1 v2) (0#ps)= at v1 ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
| "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
| "at (Stars vs) (n#ps)= at (nth vs n) ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
    18
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
    19
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
fun Pos :: "val \<Rightarrow> (nat list) set"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
  "Pos (Void) = {[]}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
| "Pos (Char c) = {[]}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
| "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
| "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
| "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" 
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
| "Pos (Stars []) = {[]}"
251
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    28
| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
    30
253
ca4e9eb8d576 polished
Christian Urban <urbanc@in.tum.de>
parents: 252
diff changeset
    31
lemma Pos_stars:
ca4e9eb8d576 polished
Christian Urban <urbanc@in.tum.de>
parents: 252
diff changeset
    32
  "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
ca4e9eb8d576 polished
Christian Urban <urbanc@in.tum.de>
parents: 252
diff changeset
    33
apply(induct vs)
267
32b222d77fa0 updated
Christian Urban <urbanc@in.tum.de>
parents: 266
diff changeset
    34
apply(auto simp add: insert_ident less_Suc_eq_0_disj)
32b222d77fa0 updated
Christian Urban <urbanc@in.tum.de>
parents: 266
diff changeset
    35
done
253
ca4e9eb8d576 polished
Christian Urban <urbanc@in.tum.de>
parents: 252
diff changeset
    36
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
lemma Pos_empty:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
  shows "[] \<in> Pos v"
251
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    39
by (induct v rule: Pos.induct)(auto)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
    41
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
    42
abbreviation
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
    43
  "intlen vs \<equiv> int (length vs)"
267
32b222d77fa0 updated
Christian Urban <urbanc@in.tum.de>
parents: 266
diff changeset
    44
255
222ed43892ea updated
Christian Urban <urbanc@in.tum.de>
parents: 254
diff changeset
    45
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
definition pflat_len :: "val \<Rightarrow> nat list => int"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
  "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
lemma pflat_len_simps:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
  shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
  and   "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
  and   "pflat_len (Left v) (0#p) = pflat_len v p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
  and   "pflat_len (Left v) (Suc 0#p) = -1"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
  and   "pflat_len (Right v) (Suc 0#p) = pflat_len v p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
  and   "pflat_len (Right v) (0#p) = -1"
251
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    57
  and   "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)"
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    58
  and   "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p"
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
  and   "pflat_len v [] = intlen (flat v)"
251
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    60
by (auto simp add: pflat_len_def Pos_empty)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
lemma pflat_len_Stars_simps:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
  assumes "n < length vs"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
  shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
267
32b222d77fa0 updated
Christian Urban <urbanc@in.tum.de>
parents: 266
diff changeset
    65
using assms
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
apply(induct vs arbitrary: n p)
251
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    67
apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
    70
lemma pflat_len_outside:
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
    71
  assumes "p \<notin> Pos v1"
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
    72
  shows "pflat_len v1 p = -1 "
267
32b222d77fa0 updated
Christian Urban <urbanc@in.tum.de>
parents: 266
diff changeset
    73
using assms by (simp add: pflat_len_def)
32b222d77fa0 updated
Christian Urban <urbanc@in.tum.de>
parents: 266
diff changeset
    74
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
    75
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
    76
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
    77
section {* Orderings *}
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
    78
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
    79
257
9deaff82e0c5 updated
Christian Urban <urbanc@in.tum.de>
parents: 256
diff changeset
    80
definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
where
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
    82
  "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2"
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
257
9deaff82e0c5 updated
Christian Urban <urbanc@in.tum.de>
parents: 256
diff changeset
    84
definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
where
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
    86
  "ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2"
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
257
9deaff82e0c5 updated
Christian Urban <urbanc@in.tum.de>
parents: 256
diff changeset
    88
inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
where
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
    90
  "[] \<sqsubset>lex (p#ps)"
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
| "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
| "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
lemma lex_irrfl:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
  fixes ps1 ps2 :: "nat list"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
  assumes "ps1 \<sqsubset>lex ps2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
  shows "ps1 \<noteq> ps2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
using assms
257
9deaff82e0c5 updated
Christian Urban <urbanc@in.tum.de>
parents: 256
diff changeset
    99
by(induct rule: lex_list.induct)(auto)
9deaff82e0c5 updated
Christian Urban <urbanc@in.tum.de>
parents: 256
diff changeset
   100
251
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   101
lemma lex_simps [simp]:
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
  fixes xs ys :: "nat list"
251
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   103
  shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   104
  and   "xs \<sqsubset>lex [] \<longleftrightarrow> False"
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   105
  and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))"
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   106
by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
lemma lex_trans:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
  fixes ps1 ps2 ps3 :: "nat list"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
  assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
  shows "ps1 \<sqsubset>lex ps3"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
using assms
264
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   113
by (induct arbitrary: ps3 rule: lex_list.induct)
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   114
   (auto elim: lex_list.cases)
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   115
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
257
9deaff82e0c5 updated
Christian Urban <urbanc@in.tum.de>
parents: 256
diff changeset
   117
lemma lex_trichotomous:
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
  fixes p q :: "nat list"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
  shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
apply(induct p arbitrary: q)
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   121
apply(auto elim: lex_list.cases)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
apply(case_tac q)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
apply(auto)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   126
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   127
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   128
286
804fbb227568 added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents: 280
diff changeset
   129
section {* POSIX Ordering of Values According to Okui \& Suzuki *}
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   130
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   132
definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   133
where
264
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   134
  "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and>
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   135
                   (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   136
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   137
lemma PosOrd_def2:
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   138
  shows "v1 \<sqsubset>val p v2 \<longleftrightarrow> 
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   139
         pflat_len v1 p > pflat_len v2 p \<and>
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   140
         (\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and>
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   141
         (\<forall>q \<in> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   142
unfolding PosOrd_def
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   143
apply(auto)
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   144
done
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   145
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   146
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   147
definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
where
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   149
  "v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2"
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   151
definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
  "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   155
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   156
lemma PosOrd_trans:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   157
  assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   158
  shows "v1 :\<sqsubset>val v3"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   159
proof -
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   160
  from assms obtain p p'
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   161
    where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   162
  then have pos: "p \<in> Pos v1" "p' \<in> Pos v2" unfolding PosOrd_def pflat_len_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   163
    by (smt not_int_zless_negative)+
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   164
  have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   165
    by (rule lex_trichotomous)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   166
  moreover
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   167
    { assume "p = p'"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   168
      with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   169
      by (smt Un_iff)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   170
      then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   171
    }   
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   172
  moreover
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   173
    { assume "p \<sqsubset>lex p'"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   174
      with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   175
      by (smt Un_iff lex_trans)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   176
      then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   177
    }
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   178
  moreover
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   179
    { assume "p' \<sqsubset>lex p"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   180
      with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   181
      by (smt Un_iff lex_trans pflat_len_def)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   182
      then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   183
    }
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   184
  ultimately show "v1 :\<sqsubset>val v3" by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   185
qed
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   186
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   187
lemma PosOrd_irrefl:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   188
  assumes "v :\<sqsubset>val v"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   189
  shows "False"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   190
using assms unfolding PosOrd_ex_def PosOrd_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   191
by auto
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   192
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   193
lemma PosOrd_assym:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   194
  assumes "v1 :\<sqsubset>val v2" 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   195
  shows "\<not>(v2 :\<sqsubset>val v1)"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   196
using assms
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   197
using PosOrd_irrefl PosOrd_trans by blast 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   198
286
804fbb227568 added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents: 280
diff changeset
   199
(*
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   200
  :\<sqsubseteq>val and :\<sqsubset>val are partial orders.
286
804fbb227568 added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents: 280
diff changeset
   201
*)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   202
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   203
lemma PosOrd_ordering:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   204
  shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   205
unfolding ordering_def PosOrd_ex_eq_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   206
apply(auto)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   207
using PosOrd_irrefl apply blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   208
using PosOrd_assym apply blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   209
using PosOrd_trans by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   210
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   211
lemma PosOrd_order:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   212
  shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   213
using PosOrd_ordering
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   214
apply(simp add: class.order_def class.preorder_def class.order_axioms_def)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   215
unfolding ordering_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   216
by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   217
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   218
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   219
lemma PosOrd_ex_eq2:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   220
  shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   221
using PosOrd_ordering 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   222
unfolding ordering_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   223
by auto
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   224
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   225
lemma PosOrdeq_trans:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   226
  assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   227
  shows "v1 :\<sqsubseteq>val v3"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   228
using assms PosOrd_ordering 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   229
unfolding ordering_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   230
by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   231
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   232
lemma PosOrdeq_antisym:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   233
  assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   234
  shows "v1 = v2"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   235
using assms PosOrd_ordering 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   236
unfolding ordering_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   237
by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   238
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   239
lemma PosOrdeq_refl:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   240
  shows "v :\<sqsubseteq>val v" 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   241
unfolding PosOrd_ex_eq_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   242
by auto
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   243
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   244
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   245
lemma PosOrd_shorterE:
255
222ed43892ea updated
Christian Urban <urbanc@in.tum.de>
parents: 254
diff changeset
   246
  assumes "v1 :\<sqsubset>val v2" 
222ed43892ea updated
Christian Urban <urbanc@in.tum.de>
parents: 254
diff changeset
   247
  shows "length (flat v2) \<le> length (flat v1)"
267
32b222d77fa0 updated
Christian Urban <urbanc@in.tum.de>
parents: 266
diff changeset
   248
using assms unfolding PosOrd_ex_def PosOrd_def
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   249
apply(auto)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   250
apply(case_tac p)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   251
apply(simp add: pflat_len_simps)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   252
apply(drule_tac x="[]" in bspec)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   253
apply(simp add: Pos_empty)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   254
apply(simp add: pflat_len_simps)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   255
done
255
222ed43892ea updated
Christian Urban <urbanc@in.tum.de>
parents: 254
diff changeset
   256
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   257
lemma PosOrd_shorterI:
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   258
  assumes "length (flat v2) < length (flat v1)"
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   259
  shows "v1 :\<sqsubset>val v2"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   260
unfolding PosOrd_ex_def PosOrd_def pflat_len_def 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   261
using assms Pos_empty by force
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   262
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   263
lemma PosOrd_spreI:
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   264
  assumes "flat v' \<sqsubset>spre flat v"
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   265
  shows "v :\<sqsubset>val v'" 
251
925232418a15 polished
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   266
using assms
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   267
apply(rule_tac PosOrd_shorterI)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   268
unfolding prefix_list_def sprefix_list_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   269
by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   270
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   271
lemma pflat_len_inside:
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   272
  assumes "pflat_len v2 p < pflat_len v1 p"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   273
  shows "p \<in> Pos v1"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   274
using assms 
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   275
unfolding pflat_len_def
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   276
by (auto split: if_splits)
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   277
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   278
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   279
lemma PosOrd_Left_Right:
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   280
  assumes "flat v1 = flat v2"
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   281
  shows "Left v1 :\<sqsubset>val Right v2" 
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   282
unfolding PosOrd_ex_def
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   283
apply(rule_tac x="[0]" in exI)
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   284
apply(auto simp add: PosOrd_def pflat_len_simps assms)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   285
done
256
146b4817aebd updated
Christian Urban <urbanc@in.tum.de>
parents: 255
diff changeset
   286
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   287
lemma PosOrd_LeftE:
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   288
  assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   289
  shows "v1 :\<sqsubset>val v2"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   290
using assms
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   291
unfolding PosOrd_ex_def PosOrd_def2
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   292
apply(auto simp add: pflat_len_simps)
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   293
apply(frule pflat_len_inside)
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   294
apply(auto simp add: pflat_len_simps)
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   295
by (metis lex_simps(3) pflat_len_simps(3))
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   296
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   297
lemma PosOrd_LeftI:
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   298
  assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   299
  shows  "Left v1 :\<sqsubset>val Left v2"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   300
using assms
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   301
unfolding PosOrd_ex_def PosOrd_def2
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   302
apply(auto simp add: pflat_len_simps)
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   303
by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3))
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   304
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   305
lemma PosOrd_Left_eq:
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   306
  assumes "flat v1 = flat v2"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   307
  shows "Left v1 :\<sqsubset>val Left v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" 
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   308
using assms PosOrd_LeftE PosOrd_LeftI
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   309
by blast
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   310
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   311
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   312
lemma PosOrd_RightE:
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   313
  assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   314
  shows "v1 :\<sqsubset>val v2"
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   315
using assms
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   316
unfolding PosOrd_ex_def PosOrd_def2
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   317
apply(auto simp add: pflat_len_simps)
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   318
apply(frule pflat_len_inside)
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   319
apply(auto simp add: pflat_len_simps)
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   320
by (metis lex_simps(3) pflat_len_simps(5))
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   321
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   322
lemma PosOrd_RightI:
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   323
  assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   324
  shows  "Right v1 :\<sqsubset>val Right v2"
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   325
using assms
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   326
unfolding PosOrd_ex_def PosOrd_def2
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   327
apply(auto simp add: pflat_len_simps)
269
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   328
by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5))
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   329
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   330
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   331
lemma PosOrd_Right_eq:
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   332
  assumes "flat v1 = flat v2"
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   333
  shows "Right v1 :\<sqsubset>val Right v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" 
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   334
using assms PosOrd_RightE PosOrd_RightI
12772d537b71 updated
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
   335
by blast
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   336
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   337
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   338
lemma PosOrd_SeqI1:
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   339
  assumes "v1 :\<sqsubset>val w1" "flat (Seq v1 v2) = flat (Seq w1 w2)"
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   340
  shows "Seq v1 v2 :\<sqsubset>val Seq w1 w2" 
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   341
using assms(1)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   342
apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   343
apply(subst (asm) PosOrd_def)
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   344
apply(clarify)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   345
apply(subst PosOrd_ex_def)
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   346
apply(rule_tac x="0#p" in exI)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   347
apply(subst PosOrd_def)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   348
apply(rule conjI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   349
apply(simp add: pflat_len_simps)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   350
apply(rule ballI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   351
apply(rule impI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   352
apply(simp only: Pos.simps)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   353
apply(auto)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   354
apply(simp add: pflat_len_simps)
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   355
apply(auto simp add: pflat_len_simps)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   356
using assms(2)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   357
apply(simp)
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   358
apply(metis length_append of_nat_add)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   359
done
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   360
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   361
lemma PosOrd_SeqI2:
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   362
  assumes "v2 :\<sqsubset>val w2" "flat v2 = flat w2"
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   363
  shows "Seq v v2 :\<sqsubset>val Seq v w2" 
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   364
using assms(1)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   365
apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   366
apply(subst (asm) PosOrd_def)
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   367
apply(clarify)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   368
apply(subst PosOrd_ex_def)
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   369
apply(rule_tac x="Suc 0#p" in exI)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   370
apply(subst PosOrd_def)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   371
apply(rule conjI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   372
apply(simp add: pflat_len_simps)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   373
apply(rule ballI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   374
apply(rule impI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   375
apply(simp only: Pos.simps)
252
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   376
apply(auto)[1]
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   377
apply(simp add: pflat_len_simps)
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   378
using assms(2)
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   379
apply(simp)
022b80503766 polished
Christian Urban <urbanc@in.tum.de>
parents: 251
diff changeset
   380
apply(auto simp add: pflat_len_simps)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   381
done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   382
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   383
lemma PosOrd_Seq_eq:
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   384
  assumes "flat v2 = flat w2"
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   385
  shows "(Seq v v2) :\<sqsubset>val (Seq v w2) \<longleftrightarrow> v2 :\<sqsubset>val w2"
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   386
using assms 
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   387
apply(auto)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   388
prefer 2
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   389
apply(simp add: PosOrd_SeqI2)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   390
apply(simp add: PosOrd_ex_def)
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   391
apply(auto)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   392
apply(case_tac p)
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   393
apply(simp add: PosOrd_def pflat_len_simps)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   394
apply(case_tac a)
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   395
apply(simp add: PosOrd_def pflat_len_simps)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   396
apply(clarify)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   397
apply(case_tac nat)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   398
prefer 2
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   399
apply(simp add: PosOrd_def pflat_len_simps pflat_len_outside)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   400
apply(rule_tac x="list" in exI)
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   401
apply(auto simp add: PosOrd_def2 pflat_len_simps)
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   402
apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   403
apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   404
done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   406
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   407
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   408
lemma PosOrd_StarsI:
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   409
  assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   410
  shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" 
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   411
using assms(1)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   412
apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   413
apply(subst (asm) PosOrd_def)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   414
apply(clarify)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   415
apply(subst PosOrd_ex_def)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   416
apply(subst PosOrd_def)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   417
apply(rule_tac x="0#p" in exI)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   418
apply(simp add: pflat_len_Stars_simps pflat_len_simps)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   419
using assms(2)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   420
apply(simp add: pflat_len_simps)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   421
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   422
by (metis length_append of_nat_add)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   423
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   424
lemma PosOrd_StarsI2:
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   425
  assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flats vs1 = flats vs2"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   426
  shows "Stars (v#vs1) :\<sqsubset>val Stars (v#vs2)" 
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   427
using assms(1)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   428
apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   429
apply(subst (asm) PosOrd_def)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   430
apply(clarify)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   431
apply(subst PosOrd_ex_def)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   432
apply(subst PosOrd_def)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   433
apply(case_tac p)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   434
apply(simp add: pflat_len_simps)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   435
apply(rule_tac x="Suc a#list" in exI)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   436
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2))
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   437
done
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   438
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   439
lemma PosOrd_Stars_appendI:
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   440
  assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   441
  shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   442
using assms
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   443
apply(induct vs)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   444
apply(simp)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   445
apply(simp add: PosOrd_StarsI2)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   446
done
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   447
276
a3134f7de065 updated
cu
parents: 273
diff changeset
   448
lemma PosOrd_eq_Stars_zipI:
a3134f7de065 updated
cu
parents: 273
diff changeset
   449
  assumes "\<forall>(v1, v2) \<in> set (zip vs1 vs2). v1 :\<sqsubseteq>val v2" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   450
     "length vs1 = length vs2" "flats vs1 = flats vs2"
a3134f7de065 updated
cu
parents: 273
diff changeset
   451
  shows "Stars vs1 :\<sqsubseteq>val Stars vs2"
a3134f7de065 updated
cu
parents: 273
diff changeset
   452
  using assms
a3134f7de065 updated
cu
parents: 273
diff changeset
   453
  apply(induct vs1 arbitrary: vs2)
a3134f7de065 updated
cu
parents: 273
diff changeset
   454
   apply(case_tac vs2)
a3134f7de065 updated
cu
parents: 273
diff changeset
   455
apply(simp add: PosOrd_ex_eq_def)    
a3134f7de065 updated
cu
parents: 273
diff changeset
   456
   apply(simp)
a3134f7de065 updated
cu
parents: 273
diff changeset
   457
  apply(case_tac vs2)
a3134f7de065 updated
cu
parents: 273
diff changeset
   458
   apply(simp)
a3134f7de065 updated
cu
parents: 273
diff changeset
   459
  apply(simp)
a3134f7de065 updated
cu
parents: 273
diff changeset
   460
  apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   461
apply(subst (asm) (2)PosOrd_ex_eq_def)
a3134f7de065 updated
cu
parents: 273
diff changeset
   462
  apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   463
   apply(subst PosOrd_ex_eq_def)
a3134f7de065 updated
cu
parents: 273
diff changeset
   464
   apply(rule disjI1)
a3134f7de065 updated
cu
parents: 273
diff changeset
   465
   apply(rule PosOrd_StarsI)
a3134f7de065 updated
cu
parents: 273
diff changeset
   466
    apply(simp)
a3134f7de065 updated
cu
parents: 273
diff changeset
   467
   apply(simp)
a3134f7de065 updated
cu
parents: 273
diff changeset
   468
  using PosOrd_StarsI2 PosOrd_ex_eq_def by fastforce
a3134f7de065 updated
cu
parents: 273
diff changeset
   469
  
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   470
lemma PosOrd_StarsE2:
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   471
  assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   472
  shows "Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   473
using assms
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   474
apply(subst (asm) PosOrd_ex_def)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   475
apply(erule exE)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   476
apply(case_tac p)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   477
apply(simp)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   478
apply(simp add: PosOrd_def pflat_len_simps)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   479
apply(subst PosOrd_ex_def)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   480
apply(rule_tac x="[]" in exI)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   481
apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   482
apply(simp)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   483
apply(case_tac a)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   484
apply(clarify)
264
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   485
apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1]
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   486
apply(clarify)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   487
apply(simp add: PosOrd_ex_def)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   488
apply(rule_tac x="nat#list" in exI)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   489
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   490
apply(case_tac q)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   491
apply(simp add: PosOrd_def pflat_len_simps)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   492
apply(clarify)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   493
apply(drule_tac x="Suc a # lista" in bspec)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   494
apply(simp)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   495
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   496
apply(case_tac q)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   497
apply(simp add: PosOrd_def pflat_len_simps)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   498
apply(clarify)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   499
apply(drule_tac x="Suc a # lista" in bspec)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   500
apply(simp)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   501
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   502
done
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   503
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   504
lemma PosOrd_Stars_appendE:
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   505
  assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   506
  shows "Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   507
using assms
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   508
apply(induct vs)
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   509
apply(simp)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   510
apply(simp add: PosOrd_StarsE2)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   511
done
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   512
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   513
lemma PosOrd_Stars_append_eq:
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   514
  assumes "flats vs1 = flats vs2"
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   515
  shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   516
using assms
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   517
apply(rule_tac iffI)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   518
apply(erule PosOrd_Stars_appendE)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   519
apply(rule PosOrd_Stars_appendI)
254
7c89d3f6923e polished
Christian Urban <urbanc@in.tum.de>
parents: 253
diff changeset
   520
apply(auto)
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   521
done  
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   522
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   523
lemma PosOrd_almost_trichotomous:
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   524
  shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (length (flat v1) = length (flat v2))"
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   525
apply(auto simp add: PosOrd_ex_def)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   526
apply(auto simp add: PosOrd_def)
256
146b4817aebd updated
Christian Urban <urbanc@in.tum.de>
parents: 255
diff changeset
   527
apply(rule_tac x="[]" in exI)
146b4817aebd updated
Christian Urban <urbanc@in.tum.de>
parents: 255
diff changeset
   528
apply(auto simp add: Pos_empty pflat_len_simps)
146b4817aebd updated
Christian Urban <urbanc@in.tum.de>
parents: 255
diff changeset
   529
apply(drule_tac x="[]" in spec)
146b4817aebd updated
Christian Urban <urbanc@in.tum.de>
parents: 255
diff changeset
   530
apply(auto simp add: Pos_empty pflat_len_simps)
146b4817aebd updated
Christian Urban <urbanc@in.tum.de>
parents: 255
diff changeset
   531
done
146b4817aebd updated
Christian Urban <urbanc@in.tum.de>
parents: 255
diff changeset
   532
146b4817aebd updated
Christian Urban <urbanc@in.tum.de>
parents: 255
diff changeset
   533
267
32b222d77fa0 updated
Christian Urban <urbanc@in.tum.de>
parents: 266
diff changeset
   534
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   535
section {* The Posix Value is smaller than any other Value *}
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   536
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   537
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   538
lemma Posix_PosOrd:
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   539
  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s" 
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   540
  shows "v1 :\<sqsubseteq>val v2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   541
using assms
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   542
proof (induct arbitrary: v2 rule: Posix.induct)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   543
  case (Posix_ONE v)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   544
  have "v \<in> LV ONE []" by fact
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   545
  then have "v = Void"
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   546
    by (simp add: LV_simps)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   547
  then show "Void :\<sqsubseteq>val v"
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   548
    by (simp add: PosOrd_ex_eq_def)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   549
next
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   550
  case (Posix_CHAR c v)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   551
  have "v \<in> LV (CHAR c) [c]" by fact
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   552
  then have "v = Char c"
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   553
    by (simp add: LV_simps)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   554
  then show "Char c :\<sqsubseteq>val v"
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   555
    by (simp add: PosOrd_ex_eq_def)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   556
next
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   557
  case (Posix_ALT1 s r1 v r2 v2)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   558
  have as1: "s \<in> r1 \<rightarrow> v" by fact
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   559
  have IH: "\<And>v2. v2 \<in> LV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   560
  have "v2 \<in> LV (ALT r1 r2) s" by fact
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   561
  then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   562
    by(auto simp add: LV_def prefix_list_def)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   563
  then consider
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   564
    (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   565
  | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   566
  by (auto elim: Prf.cases)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   567
  then show "Left v :\<sqsubseteq>val v2"
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   568
  proof(cases)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   569
     case (Left v3)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   570
     have "v3 \<in> LV r1 s" using Left(2,3) 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   571
       by (auto simp add: LV_def prefix_list_def)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   572
     with IH have "v :\<sqsubseteq>val v3" by simp
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   573
     moreover
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   574
     have "flat v3 = flat v" using as1 Left(3)
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   575
       by (simp add: Posix1(2)) 
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   576
     ultimately have "Left v :\<sqsubseteq>val Left v3"
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   577
       by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   578
     then show "Left v :\<sqsubseteq>val v2" unfolding Left .
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   579
  next
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   580
     case (Right v3)
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   581
     have "flat v3 = flat v" using as1 Right(3)
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   582
       by (simp add: Posix1(2)) 
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   583
     then have "Left v :\<sqsubseteq>val Right v3" 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   584
       unfolding PosOrd_ex_eq_def
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   585
       by (simp add: PosOrd_Left_Right)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   586
     then show "Left v :\<sqsubseteq>val v2" unfolding Right .
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   587
  qed
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   588
next
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   589
  case (Posix_ALT2 s r2 v r1 v2)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   590
  have as1: "s \<in> r2 \<rightarrow> v" by fact
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   591
  have as2: "s \<notin> L r1" by fact
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   592
  have IH: "\<And>v2. v2 \<in> LV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   593
  have "v2 \<in> LV (ALT r1 r2) s" by fact
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   594
  then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   595
    by(auto simp add: LV_def prefix_list_def)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   596
  then consider
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   597
    (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   598
  | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   599
  by (auto elim: Prf.cases)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   600
  then show "Right v :\<sqsubseteq>val v2"
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   601
  proof (cases)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   602
    case (Right v3)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   603
     have "v3 \<in> LV r2 s" using Right(2,3) 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   604
       by (auto simp add: LV_def prefix_list_def)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   605
     with IH have "v :\<sqsubseteq>val v3" by simp
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   606
     moreover
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   607
     have "flat v3 = flat v" using as1 Right(3)
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   608
       by (simp add: Posix1(2)) 
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   609
     ultimately have "Right v :\<sqsubseteq>val Right v3" 
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   610
        by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   611
     then show "Right v :\<sqsubseteq>val v2" unfolding Right .
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   612
  next
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   613
     case (Left v3)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   614
     have "v3 \<in> LV r1 s" using Left(2,3) as2  
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   615
       by (auto simp add: LV_def prefix_list_def)
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   616
     then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   617
       by (simp add: Posix1(2) LV_def) 
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   618
     then have "False" using as1 as2 Left
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   619
       by (auto simp add: Posix1(2) L_flat_Prf1)
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   620
     then show "Right v :\<sqsubseteq>val v2" by simp
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   621
  qed
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   622
next 
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   623
  case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
264
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   624
  have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   625
  then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   626
  have IH1: "\<And>v3. v3 \<in> LV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   627
  have IH2: "\<And>v3. v3 \<in> LV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   628
  have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   629
  have "v3 \<in> LV (SEQ r1 r2) (s1 @ s2)" by fact
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   630
  then obtain v3a v3b where eqs:
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   631
    "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   632
    "flat v3a @ flat v3b = s1 @ s2" 
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   633
    by (force simp add: prefix_list_def LV_def elim: Prf.cases)
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   634
  with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   635
    by (smt L_flat_Prf1 append_eq_append_conv2 append_self_conv)
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   636
  then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   637
    by (simp add: sprefix_list_def append_eq_conv_conj)
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   638
  then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" 
264
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   639
    using PosOrd_spreI as1(1) eqs by blast
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   640
  then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   641
    by (auto simp add: LV_def)
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   642
  then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   643
  then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
   644
    unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_Seq_eq) 
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   645
  then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   646
next 
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   647
  case (Posix_STAR1 s1 r v s2 vs v3) 
264
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   648
  have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   649
  then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   650
  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   651
  have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   652
  have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   653
  have cond2: "flat v \<noteq> []" by fact
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   654
  have "v3 \<in> LV (STAR r) (s1 @ s2)" by fact
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   655
  then consider 
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   656
    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   657
    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   658
    "flat (Stars (v3a # vs3)) = s1 @ s2"
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   659
  | (Empty) "v3 = Stars []"
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   660
  unfolding LV_def  
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   661
  apply(auto)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   662
  apply(erule Prf.cases)
270
462d893ecb3d updated
Christian Urban <urbanc@in.tum.de>
parents: 269
diff changeset
   663
  apply(auto)
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   664
  apply(case_tac vs)
270
462d893ecb3d updated
Christian Urban <urbanc@in.tum.de>
parents: 269
diff changeset
   665
  apply(auto intro: Prf.intros)
462d893ecb3d updated
Christian Urban <urbanc@in.tum.de>
parents: 269
diff changeset
   666
  done
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   667
  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   668
    proof (cases)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   669
      case (NonEmpty v3a vs3)
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   670
      have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   671
      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   672
        unfolding prefix_list_def
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   673
        by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7)) 
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   674
      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   675
        by (simp add: sprefix_list_def append_eq_conv_conj)
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   676
      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
264
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   677
        using PosOrd_spreI as1(1) NonEmpty(4) by blast
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   678
      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)" 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   679
        using NonEmpty(2,3) by (auto simp add: LV_def)
264
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   680
      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
e2828c4a1e23 updated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
   681
      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   682
         unfolding PosOrd_ex_eq_def by auto     
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   683
      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   684
        unfolding  PosOrd_ex_eq_def
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   685
        using PosOrd_StarsI PosOrd_StarsI2 by auto 
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   686
      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   687
    next 
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   688
      case Empty
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   689
      have "v3 = Stars []" by fact
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   690
      then show "Stars (v # vs) :\<sqsubseteq>val v3"
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
   691
      unfolding PosOrd_ex_eq_def using cond2
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   692
      by (simp add: PosOrd_shorterI)
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   693
    qed      
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   694
next 
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   695
  case (Posix_STAR2 r v2)
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   696
  have "v2 \<in> LV (STAR r) []" by fact
262
45ad887fa6aa isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 261
diff changeset
   697
  then have "v2 = Stars []" 
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   698
    unfolding LV_def by (auto elim: Prf.cases) 
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
   699
  then show "Stars [] :\<sqsubseteq>val v2"
276
a3134f7de065 updated
cu
parents: 273
diff changeset
   700
    by (simp add: PosOrd_ex_eq_def)
a3134f7de065 updated
cu
parents: 273
diff changeset
   701
next 
a3134f7de065 updated
cu
parents: 273
diff changeset
   702
  case (Posix_NTIMES1 s1 r v s2 n vs v3) 
a3134f7de065 updated
cu
parents: 273
diff changeset
   703
  have "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs" by fact+
a3134f7de065 updated
cu
parents: 273
diff changeset
   704
  then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2))
a3134f7de065 updated
cu
parents: 273
diff changeset
   705
  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   706
  have IH2: "\<And>v3. v3 \<in> LV (NTIMES r (n - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   707
  have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   708
  have cond2: "flat v \<noteq> []" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   709
  have "v3 \<in> LV (NTIMES r n) (s1 @ s2)" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   710
  then consider 
a3134f7de065 updated
cu
parents: 273
diff changeset
   711
    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   712
    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : NTIMES r (n - 1)"
a3134f7de065 updated
cu
parents: 273
diff changeset
   713
    "flats (v3a # vs3) = s1 @ s2"
a3134f7de065 updated
cu
parents: 273
diff changeset
   714
  | (Empty) "v3 = Stars []"
a3134f7de065 updated
cu
parents: 273
diff changeset
   715
  unfolding LV_def  
a3134f7de065 updated
cu
parents: 273
diff changeset
   716
  apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   717
  apply(erule Prf.cases)
a3134f7de065 updated
cu
parents: 273
diff changeset
   718
             apply(auto)  
a3134f7de065 updated
cu
parents: 273
diff changeset
   719
  apply(case_tac vs1)
a3134f7de065 updated
cu
parents: 273
diff changeset
   720
   apply(auto intro: Prf.intros)
a3134f7de065 updated
cu
parents: 273
diff changeset
   721
   apply(case_tac vs2)
a3134f7de065 updated
cu
parents: 273
diff changeset
   722
    apply(auto intro: Prf.intros)
a3134f7de065 updated
cu
parents: 273
diff changeset
   723
  apply (simp add: as1(1) cond2 flats_empty)
a3134f7de065 updated
cu
parents: 273
diff changeset
   724
  by (simp add: Prf.intros(8))
a3134f7de065 updated
cu
parents: 273
diff changeset
   725
  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   726
    proof (cases)
a3134f7de065 updated
cu
parents: 273
diff changeset
   727
      case (NonEmpty v3a vs3)
a3134f7de065 updated
cu
parents: 273
diff changeset
   728
      have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . 
a3134f7de065 updated
cu
parents: 273
diff changeset
   729
      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
a3134f7de065 updated
cu
parents: 273
diff changeset
   730
        unfolding prefix_list_def
a3134f7de065 updated
cu
parents: 273
diff changeset
   731
        by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7) flat_Stars)
a3134f7de065 updated
cu
parents: 273
diff changeset
   732
      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
a3134f7de065 updated
cu
parents: 273
diff changeset
   733
        by (simp add: sprefix_list_def append_eq_conv_conj)
a3134f7de065 updated
cu
parents: 273
diff changeset
   734
      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   735
        using PosOrd_spreI as1(1) NonEmpty(4) by blast
a3134f7de065 updated
cu
parents: 273
diff changeset
   736
      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (NTIMES r (n - 1)) s2)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   737
        using NonEmpty(2,3) by (auto simp add: LV_def)
a3134f7de065 updated
cu
parents: 273
diff changeset
   738
      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
a3134f7de065 updated
cu
parents: 273
diff changeset
   739
      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   740
         unfolding PosOrd_ex_eq_def by auto     
a3134f7de065 updated
cu
parents: 273
diff changeset
   741
      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
a3134f7de065 updated
cu
parents: 273
diff changeset
   742
        unfolding  PosOrd_ex_eq_def
a3134f7de065 updated
cu
parents: 273
diff changeset
   743
        using PosOrd_StarsI PosOrd_StarsI2 by auto 
a3134f7de065 updated
cu
parents: 273
diff changeset
   744
      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
a3134f7de065 updated
cu
parents: 273
diff changeset
   745
    next 
a3134f7de065 updated
cu
parents: 273
diff changeset
   746
      case Empty
a3134f7de065 updated
cu
parents: 273
diff changeset
   747
      have "v3 = Stars []" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   748
      then show "Stars (v # vs) :\<sqsubseteq>val v3"
a3134f7de065 updated
cu
parents: 273
diff changeset
   749
      unfolding PosOrd_ex_eq_def using cond2
a3134f7de065 updated
cu
parents: 273
diff changeset
   750
      by (simp add: PosOrd_shorterI)
a3134f7de065 updated
cu
parents: 273
diff changeset
   751
  qed 
a3134f7de065 updated
cu
parents: 273
diff changeset
   752
next
a3134f7de065 updated
cu
parents: 273
diff changeset
   753
  case (Posix_NTIMES2 vs r n v2) 
a3134f7de065 updated
cu
parents: 273
diff changeset
   754
  then show "Stars vs :\<sqsubseteq>val v2"
a3134f7de065 updated
cu
parents: 273
diff changeset
   755
    apply(simp add: LV_def)
a3134f7de065 updated
cu
parents: 273
diff changeset
   756
    apply(auto)  
a3134f7de065 updated
cu
parents: 273
diff changeset
   757
    apply(erule Prf_elims)
a3134f7de065 updated
cu
parents: 273
diff changeset
   758
    apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   759
    apply(rule PosOrd_eq_Stars_zipI) 
a3134f7de065 updated
cu
parents: 273
diff changeset
   760
      prefer 2
a3134f7de065 updated
cu
parents: 273
diff changeset
   761
      apply(simp)
a3134f7de065 updated
cu
parents: 273
diff changeset
   762
     prefer 2
a3134f7de065 updated
cu
parents: 273
diff changeset
   763
     apply (metis Posix1(2) flats_empty)
a3134f7de065 updated
cu
parents: 273
diff changeset
   764
    apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   765
    by (meson in_set_zipE)
a3134f7de065 updated
cu
parents: 273
diff changeset
   766
next
a3134f7de065 updated
cu
parents: 273
diff changeset
   767
  case (Posix_UPNTIMES2 r n v2)
a3134f7de065 updated
cu
parents: 273
diff changeset
   768
    then show "Stars [] :\<sqsubseteq>val v2"
a3134f7de065 updated
cu
parents: 273
diff changeset
   769
    apply(simp add: LV_def)
a3134f7de065 updated
cu
parents: 273
diff changeset
   770
      apply(auto)  
a3134f7de065 updated
cu
parents: 273
diff changeset
   771
    apply(erule Prf_elims)
a3134f7de065 updated
cu
parents: 273
diff changeset
   772
      apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   773
      unfolding PosOrd_ex_eq_def by simp
a3134f7de065 updated
cu
parents: 273
diff changeset
   774
next 
a3134f7de065 updated
cu
parents: 273
diff changeset
   775
  case (Posix_UPNTIMES1 s1 r v s2 n vs v3)
a3134f7de065 updated
cu
parents: 273
diff changeset
   776
  have "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (n - 1) \<rightarrow> Stars vs" by fact+
a3134f7de065 updated
cu
parents: 273
diff changeset
   777
  then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
a3134f7de065 updated
cu
parents: 273
diff changeset
   778
  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   779
  have IH2: "\<And>v3. v3 \<in> LV (UPNTIMES r (n - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   780
  have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (n - 1)))" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   781
  have cond2: "flat v \<noteq> []" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   782
  have "v3 \<in> LV (UPNTIMES r n) (s1 @ s2)" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   783
  then consider 
a3134f7de065 updated
cu
parents: 273
diff changeset
   784
    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   785
    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : UPNTIMES r (n - 1)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   786
    "flats (v3a # vs3) = s1 @ s2"
a3134f7de065 updated
cu
parents: 273
diff changeset
   787
  | (Empty) "v3 = Stars []"
a3134f7de065 updated
cu
parents: 273
diff changeset
   788
  unfolding LV_def  
a3134f7de065 updated
cu
parents: 273
diff changeset
   789
  apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   790
  apply(erule Prf.cases)
a3134f7de065 updated
cu
parents: 273
diff changeset
   791
  apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   792
  apply(case_tac vs)
a3134f7de065 updated
cu
parents: 273
diff changeset
   793
   apply(auto intro: Prf.intros)
a3134f7de065 updated
cu
parents: 273
diff changeset
   794
  by (simp add: Prf.intros(7) as1(1) cond2)
a3134f7de065 updated
cu
parents: 273
diff changeset
   795
  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   796
    proof (cases)
a3134f7de065 updated
cu
parents: 273
diff changeset
   797
      case (NonEmpty v3a vs3)
a3134f7de065 updated
cu
parents: 273
diff changeset
   798
      have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . 
a3134f7de065 updated
cu
parents: 273
diff changeset
   799
      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
a3134f7de065 updated
cu
parents: 273
diff changeset
   800
        unfolding prefix_list_def
a3134f7de065 updated
cu
parents: 273
diff changeset
   801
        apply(simp)
a3134f7de065 updated
cu
parents: 273
diff changeset
   802
        apply(simp add: append_eq_append_conv2)
a3134f7de065 updated
cu
parents: 273
diff changeset
   803
        apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   804
        by (metis L_flat_Prf1 One_nat_def cond flat_Stars)
a3134f7de065 updated
cu
parents: 273
diff changeset
   805
      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
a3134f7de065 updated
cu
parents: 273
diff changeset
   806
        by (simp add: sprefix_list_def append_eq_conv_conj)
a3134f7de065 updated
cu
parents: 273
diff changeset
   807
      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   808
        using PosOrd_spreI as1(1) NonEmpty(4) by blast
a3134f7de065 updated
cu
parents: 273
diff changeset
   809
      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (UPNTIMES r (n - 1)) s2)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   810
        using NonEmpty(2,3) by (auto simp add: LV_def)
a3134f7de065 updated
cu
parents: 273
diff changeset
   811
      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
a3134f7de065 updated
cu
parents: 273
diff changeset
   812
      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   813
         unfolding PosOrd_ex_eq_def by auto     
a3134f7de065 updated
cu
parents: 273
diff changeset
   814
      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
a3134f7de065 updated
cu
parents: 273
diff changeset
   815
        unfolding  PosOrd_ex_eq_def
a3134f7de065 updated
cu
parents: 273
diff changeset
   816
        using PosOrd_StarsI PosOrd_StarsI2 by auto 
a3134f7de065 updated
cu
parents: 273
diff changeset
   817
      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
a3134f7de065 updated
cu
parents: 273
diff changeset
   818
    next 
a3134f7de065 updated
cu
parents: 273
diff changeset
   819
      case Empty
a3134f7de065 updated
cu
parents: 273
diff changeset
   820
      have "v3 = Stars []" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   821
      then show "Stars (v # vs) :\<sqsubseteq>val v3"
a3134f7de065 updated
cu
parents: 273
diff changeset
   822
      unfolding PosOrd_ex_eq_def using cond2
a3134f7de065 updated
cu
parents: 273
diff changeset
   823
      by (simp add: PosOrd_shorterI)
a3134f7de065 updated
cu
parents: 273
diff changeset
   824
  qed        
a3134f7de065 updated
cu
parents: 273
diff changeset
   825
next
a3134f7de065 updated
cu
parents: 273
diff changeset
   826
  case (Posix_FROMNTIMES2 vs r n v2)
a3134f7de065 updated
cu
parents: 273
diff changeset
   827
    then show "Stars vs :\<sqsubseteq>val v2"
a3134f7de065 updated
cu
parents: 273
diff changeset
   828
    apply(simp add: LV_def)
a3134f7de065 updated
cu
parents: 273
diff changeset
   829
      apply(auto)  
a3134f7de065 updated
cu
parents: 273
diff changeset
   830
    apply(erule Prf_elims)
a3134f7de065 updated
cu
parents: 273
diff changeset
   831
       apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   832
        apply(rule PosOrd_eq_Stars_zipI) 
a3134f7de065 updated
cu
parents: 273
diff changeset
   833
      prefer 2
a3134f7de065 updated
cu
parents: 273
diff changeset
   834
      apply(simp)
a3134f7de065 updated
cu
parents: 273
diff changeset
   835
     prefer 2
a3134f7de065 updated
cu
parents: 273
diff changeset
   836
     apply (metis Posix1(2) flats_empty)
a3134f7de065 updated
cu
parents: 273
diff changeset
   837
    apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   838
      by (meson in_set_zipE)
a3134f7de065 updated
cu
parents: 273
diff changeset
   839
next 
a3134f7de065 updated
cu
parents: 273
diff changeset
   840
  case (Posix_FROMNTIMES1 s1 r v s2 n vs v3) 
a3134f7de065 updated
cu
parents: 273
diff changeset
   841
  have "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs" by fact+
a3134f7de065 updated
cu
parents: 273
diff changeset
   842
  then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2))
a3134f7de065 updated
cu
parents: 273
diff changeset
   843
  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   844
  have IH2: "\<And>v3. v3 \<in> LV (FROMNTIMES r (n - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   845
  have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   846
  have cond2: "flat v \<noteq> []" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   847
  have "v3 \<in> LV (FROMNTIMES r n) (s1 @ s2)" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   848
  then consider 
a3134f7de065 updated
cu
parents: 273
diff changeset
   849
    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   850
    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : FROMNTIMES r (n - 1)"
a3134f7de065 updated
cu
parents: 273
diff changeset
   851
    "flats (v3a # vs3) = s1 @ s2"
a3134f7de065 updated
cu
parents: 273
diff changeset
   852
  | (Empty) "v3 = Stars []" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   853
  unfolding LV_def  
a3134f7de065 updated
cu
parents: 273
diff changeset
   854
  apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   855
  apply(erule Prf.cases)
a3134f7de065 updated
cu
parents: 273
diff changeset
   856
             apply(auto)  
a3134f7de065 updated
cu
parents: 273
diff changeset
   857
  apply(case_tac vs1)
a3134f7de065 updated
cu
parents: 273
diff changeset
   858
   apply(auto intro: Prf.intros)
a3134f7de065 updated
cu
parents: 273
diff changeset
   859
   apply(case_tac vs2)
a3134f7de065 updated
cu
parents: 273
diff changeset
   860
    apply(auto intro: Prf.intros)
a3134f7de065 updated
cu
parents: 273
diff changeset
   861
    apply (simp add: as1(1) cond2 flats_empty)
a3134f7de065 updated
cu
parents: 273
diff changeset
   862
  apply (simp add: Prf.intros)
a3134f7de065 updated
cu
parents: 273
diff changeset
   863
  apply(case_tac vs)
a3134f7de065 updated
cu
parents: 273
diff changeset
   864
   apply(auto)
a3134f7de065 updated
cu
parents: 273
diff changeset
   865
  using Posix_FROMNTIMES1.hyps(6) Prf.intros(10) by auto
a3134f7de065 updated
cu
parents: 273
diff changeset
   866
  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   867
    proof (cases)
a3134f7de065 updated
cu
parents: 273
diff changeset
   868
      case (NonEmpty v3a vs3)
a3134f7de065 updated
cu
parents: 273
diff changeset
   869
      have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . 
a3134f7de065 updated
cu
parents: 273
diff changeset
   870
      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
a3134f7de065 updated
cu
parents: 273
diff changeset
   871
        unfolding prefix_list_def
a3134f7de065 updated
cu
parents: 273
diff changeset
   872
        by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7) flat_Stars)
a3134f7de065 updated
cu
parents: 273
diff changeset
   873
      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
a3134f7de065 updated
cu
parents: 273
diff changeset
   874
        by (simp add: sprefix_list_def append_eq_conv_conj)
a3134f7de065 updated
cu
parents: 273
diff changeset
   875
      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   876
        using PosOrd_spreI as1(1) NonEmpty(4) by blast
a3134f7de065 updated
cu
parents: 273
diff changeset
   877
      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (FROMNTIMES r (n - 1)) s2)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   878
        using NonEmpty(2,3) by (auto simp add: LV_def)
a3134f7de065 updated
cu
parents: 273
diff changeset
   879
      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
a3134f7de065 updated
cu
parents: 273
diff changeset
   880
      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
a3134f7de065 updated
cu
parents: 273
diff changeset
   881
         unfolding PosOrd_ex_eq_def by auto     
a3134f7de065 updated
cu
parents: 273
diff changeset
   882
      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
a3134f7de065 updated
cu
parents: 273
diff changeset
   883
        unfolding  PosOrd_ex_eq_def
a3134f7de065 updated
cu
parents: 273
diff changeset
   884
        using PosOrd_StarsI PosOrd_StarsI2 by auto 
a3134f7de065 updated
cu
parents: 273
diff changeset
   885
      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
a3134f7de065 updated
cu
parents: 273
diff changeset
   886
    next 
a3134f7de065 updated
cu
parents: 273
diff changeset
   887
      case Empty
a3134f7de065 updated
cu
parents: 273
diff changeset
   888
      have "v3 = Stars []" by fact
a3134f7de065 updated
cu
parents: 273
diff changeset
   889
      then show "Stars (v # vs) :\<sqsubseteq>val v3"
a3134f7de065 updated
cu
parents: 273
diff changeset
   890
      unfolding PosOrd_ex_eq_def using cond2
a3134f7de065 updated
cu
parents: 273
diff changeset
   891
      by (simp add: PosOrd_shorterI)
277
42268a284ea6 updated
cu
parents: 276
diff changeset
   892
  qed        
42268a284ea6 updated
cu
parents: 276
diff changeset
   893
next    
42268a284ea6 updated
cu
parents: 276
diff changeset
   894
  case (Posix_FROMNTIMES3 s1 r v s2 vs v3)
42268a284ea6 updated
cu
parents: 276
diff changeset
   895
      have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
42268a284ea6 updated
cu
parents: 276
diff changeset
   896
  then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
42268a284ea6 updated
cu
parents: 276
diff changeset
   897
  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
42268a284ea6 updated
cu
parents: 276
diff changeset
   898
  have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
42268a284ea6 updated
cu
parents: 276
diff changeset
   899
  have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
42268a284ea6 updated
cu
parents: 276
diff changeset
   900
  have cond2: "flat v \<noteq> []" by fact
42268a284ea6 updated
cu
parents: 276
diff changeset
   901
  have "v3 \<in> LV (FROMNTIMES r 0) (s1 @ s2)" by fact
42268a284ea6 updated
cu
parents: 276
diff changeset
   902
  then consider 
42268a284ea6 updated
cu
parents: 276
diff changeset
   903
    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
42268a284ea6 updated
cu
parents: 276
diff changeset
   904
    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
42268a284ea6 updated
cu
parents: 276
diff changeset
   905
    "flat (Stars (v3a # vs3)) = s1 @ s2"
42268a284ea6 updated
cu
parents: 276
diff changeset
   906
  | (Empty) "v3 = Stars []" 
42268a284ea6 updated
cu
parents: 276
diff changeset
   907
  unfolding LV_def  
42268a284ea6 updated
cu
parents: 276
diff changeset
   908
  apply(auto)
42268a284ea6 updated
cu
parents: 276
diff changeset
   909
  apply(erule Prf.cases)
42268a284ea6 updated
cu
parents: 276
diff changeset
   910
  apply(auto)
42268a284ea6 updated
cu
parents: 276
diff changeset
   911
  apply(case_tac vs)
42268a284ea6 updated
cu
parents: 276
diff changeset
   912
  apply(auto intro: Prf.intros)
42268a284ea6 updated
cu
parents: 276
diff changeset
   913
  done
42268a284ea6 updated
cu
parents: 276
diff changeset
   914
  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
42268a284ea6 updated
cu
parents: 276
diff changeset
   915
    proof (cases)
42268a284ea6 updated
cu
parents: 276
diff changeset
   916
      case (NonEmpty v3a vs3)
42268a284ea6 updated
cu
parents: 276
diff changeset
   917
      have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
42268a284ea6 updated
cu
parents: 276
diff changeset
   918
      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
42268a284ea6 updated
cu
parents: 276
diff changeset
   919
        unfolding prefix_list_def
42268a284ea6 updated
cu
parents: 276
diff changeset
   920
        by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7)) 
42268a284ea6 updated
cu
parents: 276
diff changeset
   921
      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
42268a284ea6 updated
cu
parents: 276
diff changeset
   922
        by (simp add: sprefix_list_def append_eq_conv_conj)
42268a284ea6 updated
cu
parents: 276
diff changeset
   923
      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
42268a284ea6 updated
cu
parents: 276
diff changeset
   924
        using PosOrd_spreI as1(1) NonEmpty(4) by blast
42268a284ea6 updated
cu
parents: 276
diff changeset
   925
      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)" 
42268a284ea6 updated
cu
parents: 276
diff changeset
   926
        using NonEmpty(2,3) by (auto simp add: LV_def)
42268a284ea6 updated
cu
parents: 276
diff changeset
   927
      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
42268a284ea6 updated
cu
parents: 276
diff changeset
   928
      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
42268a284ea6 updated
cu
parents: 276
diff changeset
   929
         unfolding PosOrd_ex_eq_def by auto     
42268a284ea6 updated
cu
parents: 276
diff changeset
   930
      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
42268a284ea6 updated
cu
parents: 276
diff changeset
   931
        unfolding  PosOrd_ex_eq_def
42268a284ea6 updated
cu
parents: 276
diff changeset
   932
        using PosOrd_StarsI PosOrd_StarsI2 by auto 
42268a284ea6 updated
cu
parents: 276
diff changeset
   933
      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
42268a284ea6 updated
cu
parents: 276
diff changeset
   934
    next 
42268a284ea6 updated
cu
parents: 276
diff changeset
   935
      case Empty
42268a284ea6 updated
cu
parents: 276
diff changeset
   936
      have "v3 = Stars []" by fact
42268a284ea6 updated
cu
parents: 276
diff changeset
   937
      then show "Stars (v # vs) :\<sqsubseteq>val v3"
42268a284ea6 updated
cu
parents: 276
diff changeset
   938
      unfolding PosOrd_ex_eq_def using cond2
42268a284ea6 updated
cu
parents: 276
diff changeset
   939
      by (simp add: PosOrd_shorterI)
42268a284ea6 updated
cu
parents: 276
diff changeset
   940
    qed      
276
a3134f7de065 updated
cu
parents: 273
diff changeset
   941
next
a3134f7de065 updated
cu
parents: 273
diff changeset
   942
  case (Posix_NMTIMES2 vs r n m v2) 
278
424bdcd01016 updated
cu
parents: 277
diff changeset
   943
  then show "Stars vs :\<sqsubseteq>val v2" 
424bdcd01016 updated
cu
parents: 277
diff changeset
   944
    apply(auto simp add: LV_def)
424bdcd01016 updated
cu
parents: 277
diff changeset
   945
    apply(erule Prf_elims)
424bdcd01016 updated
cu
parents: 277
diff changeset
   946
     apply(simp)
424bdcd01016 updated
cu
parents: 277
diff changeset
   947
     apply(rule PosOrd_eq_Stars_zipI) 
424bdcd01016 updated
cu
parents: 277
diff changeset
   948
       apply(auto)
424bdcd01016 updated
cu
parents: 277
diff changeset
   949
     apply (meson in_set_zipE)
424bdcd01016 updated
cu
parents: 277
diff changeset
   950
    by (metis Posix1(2) flats_empty)
276
a3134f7de065 updated
cu
parents: 273
diff changeset
   951
next
278
424bdcd01016 updated
cu
parents: 277
diff changeset
   952
  case (Posix_NMTIMES1 s1 r v s2 n m vs v3) 
424bdcd01016 updated
cu
parents: 277
diff changeset
   953
  have "s1 \<in> r \<rightarrow> v" "s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs" by fact+
424bdcd01016 updated
cu
parents: 277
diff changeset
   954
  then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2))
424bdcd01016 updated
cu
parents: 277
diff changeset
   955
  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
   956
  have IH2: "\<And>v3. v3 \<in> LV (NMTIMES r (n - 1) (m - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
   957
  have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
   958
  have cond2: "flat v \<noteq> []" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
   959
  have "v3 \<in> LV (NMTIMES r n m) (s1 @ s2)" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
   960
  then consider 
424bdcd01016 updated
cu
parents: 277
diff changeset
   961
    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
424bdcd01016 updated
cu
parents: 277
diff changeset
   962
    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : NMTIMES r (n - 1) (m - 1)"
424bdcd01016 updated
cu
parents: 277
diff changeset
   963
    "flats (v3a # vs3) = s1 @ s2"
424bdcd01016 updated
cu
parents: 277
diff changeset
   964
  | (Empty) "v3 = Stars []" 
424bdcd01016 updated
cu
parents: 277
diff changeset
   965
  unfolding LV_def  
424bdcd01016 updated
cu
parents: 277
diff changeset
   966
  apply(auto)
424bdcd01016 updated
cu
parents: 277
diff changeset
   967
  apply(erule Prf.cases)
424bdcd01016 updated
cu
parents: 277
diff changeset
   968
             apply(auto)  
424bdcd01016 updated
cu
parents: 277
diff changeset
   969
  apply(case_tac n)
424bdcd01016 updated
cu
parents: 277
diff changeset
   970
    apply(auto intro: Prf.intros)
424bdcd01016 updated
cu
parents: 277
diff changeset
   971
   apply(case_tac vs1)
424bdcd01016 updated
cu
parents: 277
diff changeset
   972
    apply(auto intro: Prf.intros)
424bdcd01016 updated
cu
parents: 277
diff changeset
   973
   apply (simp add: as1(1) cond2 flats_empty)
424bdcd01016 updated
cu
parents: 277
diff changeset
   974
   apply (simp add: Prf.intros(11))
424bdcd01016 updated
cu
parents: 277
diff changeset
   975
  apply(case_tac n)
424bdcd01016 updated
cu
parents: 277
diff changeset
   976
   apply(simp)
424bdcd01016 updated
cu
parents: 277
diff changeset
   977
  using Posix_NMTIMES1.hyps(6) apply blast
424bdcd01016 updated
cu
parents: 277
diff changeset
   978
  apply(simp)
424bdcd01016 updated
cu
parents: 277
diff changeset
   979
  apply(case_tac vs)
424bdcd01016 updated
cu
parents: 277
diff changeset
   980
   apply(auto)
424bdcd01016 updated
cu
parents: 277
diff changeset
   981
  by (simp add: Prf.intros(12))
424bdcd01016 updated
cu
parents: 277
diff changeset
   982
  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
424bdcd01016 updated
cu
parents: 277
diff changeset
   983
    proof (cases)
424bdcd01016 updated
cu
parents: 277
diff changeset
   984
      case (NonEmpty v3a vs3)
424bdcd01016 updated
cu
parents: 277
diff changeset
   985
      have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . 
424bdcd01016 updated
cu
parents: 277
diff changeset
   986
      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
424bdcd01016 updated
cu
parents: 277
diff changeset
   987
        unfolding prefix_list_def
424bdcd01016 updated
cu
parents: 277
diff changeset
   988
        by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7) flat_Stars)
424bdcd01016 updated
cu
parents: 277
diff changeset
   989
      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
424bdcd01016 updated
cu
parents: 277
diff changeset
   990
        by (simp add: sprefix_list_def append_eq_conv_conj)
424bdcd01016 updated
cu
parents: 277
diff changeset
   991
      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
424bdcd01016 updated
cu
parents: 277
diff changeset
   992
        using PosOrd_spreI as1(1) NonEmpty(4) by blast
424bdcd01016 updated
cu
parents: 277
diff changeset
   993
      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (NMTIMES r (n - 1) (m - 1)) s2)" 
424bdcd01016 updated
cu
parents: 277
diff changeset
   994
        using NonEmpty(2,3) by (auto simp add: LV_def)
424bdcd01016 updated
cu
parents: 277
diff changeset
   995
      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
424bdcd01016 updated
cu
parents: 277
diff changeset
   996
      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
424bdcd01016 updated
cu
parents: 277
diff changeset
   997
         unfolding PosOrd_ex_eq_def by auto     
424bdcd01016 updated
cu
parents: 277
diff changeset
   998
      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
424bdcd01016 updated
cu
parents: 277
diff changeset
   999
        unfolding  PosOrd_ex_eq_def
424bdcd01016 updated
cu
parents: 277
diff changeset
  1000
        using PosOrd_StarsI PosOrd_StarsI2 by auto 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1001
      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
424bdcd01016 updated
cu
parents: 277
diff changeset
  1002
    next 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1003
      case Empty
424bdcd01016 updated
cu
parents: 277
diff changeset
  1004
      have "v3 = Stars []" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
  1005
      then show "Stars (v # vs) :\<sqsubseteq>val v3"
424bdcd01016 updated
cu
parents: 277
diff changeset
  1006
      unfolding PosOrd_ex_eq_def using cond2
424bdcd01016 updated
cu
parents: 277
diff changeset
  1007
      by (simp add: PosOrd_shorterI)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1008
  qed        
424bdcd01016 updated
cu
parents: 277
diff changeset
  1009
next
424bdcd01016 updated
cu
parents: 277
diff changeset
  1010
  case (Posix_NMTIMES3 s1 r v s2 m vs v3) 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1011
  have "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" by fact+
424bdcd01016 updated
cu
parents: 277
diff changeset
  1012
  then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
424bdcd01016 updated
cu
parents: 277
diff changeset
  1013
  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
  1014
  have IH2: "\<And>v3. v3 \<in> LV (UPNTIMES r (m - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
  1015
  have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
  1016
  have cond2: "flat v \<noteq> []" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
  1017
  have "v3 \<in> LV (NMTIMES r 0 m) (s1 @ s2)" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
  1018
  then consider 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1019
    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1020
    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : UPNTIMES r (m - 1)" 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1021
    "flats (v3a # vs3) = s1 @ s2"
424bdcd01016 updated
cu
parents: 277
diff changeset
  1022
  | (Empty) "v3 = Stars []"
424bdcd01016 updated
cu
parents: 277
diff changeset
  1023
  unfolding LV_def  
424bdcd01016 updated
cu
parents: 277
diff changeset
  1024
  apply(auto)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1025
  apply(erule Prf.cases)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1026
  apply(auto)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1027
  apply(case_tac vs)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1028
   apply(auto intro: Prf.intros)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1029
  by (simp add: Prf.intros(7) as1(1) cond2)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1030
  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1031
    proof (cases)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1032
      case (NonEmpty v3a vs3)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1033
      have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1034
      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1035
        unfolding prefix_list_def
424bdcd01016 updated
cu
parents: 277
diff changeset
  1036
        apply(simp)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1037
        apply(simp add: append_eq_append_conv2)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1038
        apply(auto)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1039
        by (metis L_flat_Prf1 One_nat_def cond flat_Stars)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1040
      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1041
        by (simp add: sprefix_list_def append_eq_conv_conj)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1042
      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1043
        using PosOrd_spreI as1(1) NonEmpty(4) by blast
424bdcd01016 updated
cu
parents: 277
diff changeset
  1044
      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (UPNTIMES r (m - 1)) s2)" 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1045
        using NonEmpty(2,3) by (auto simp add: LV_def)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1046
      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
424bdcd01016 updated
cu
parents: 277
diff changeset
  1047
      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1048
         unfolding PosOrd_ex_eq_def by auto     
424bdcd01016 updated
cu
parents: 277
diff changeset
  1049
      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
424bdcd01016 updated
cu
parents: 277
diff changeset
  1050
        unfolding  PosOrd_ex_eq_def
424bdcd01016 updated
cu
parents: 277
diff changeset
  1051
        using PosOrd_StarsI PosOrd_StarsI2 by auto 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1052
      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
424bdcd01016 updated
cu
parents: 277
diff changeset
  1053
    next 
424bdcd01016 updated
cu
parents: 277
diff changeset
  1054
      case Empty
424bdcd01016 updated
cu
parents: 277
diff changeset
  1055
      have "v3 = Stars []" by fact
424bdcd01016 updated
cu
parents: 277
diff changeset
  1056
      then show "Stars (v # vs) :\<sqsubseteq>val v3"
424bdcd01016 updated
cu
parents: 277
diff changeset
  1057
      unfolding PosOrd_ex_eq_def using cond2
424bdcd01016 updated
cu
parents: 277
diff changeset
  1058
      by (simp add: PosOrd_shorterI)
424bdcd01016 updated
cu
parents: 277
diff changeset
  1059
  qed          
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
  1060
qed
253
ca4e9eb8d576 polished
Christian Urban <urbanc@in.tum.de>
parents: 252
diff changeset
  1061
263
00c9a95d492e isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 262
diff changeset
  1062
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
  1063
lemma Posix_PosOrd_reverse:
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1064
  assumes "s \<in> r \<rightarrow> v1" 
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1065
  shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)"
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1066
using assms
267
32b222d77fa0 updated
Christian Urban <urbanc@in.tum.de>
parents: 266
diff changeset
  1067
by (metis Posix_PosOrd less_irrefl PosOrd_def 
265
d36be1e356c0 changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents: 264
diff changeset
  1068
    PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1069
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
  1070
lemma PosOrd_Posix:
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1071
  assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1072
  shows "s \<in> r \<rightarrow> v1" 
272
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1073
proof -
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1074
  have "s \<in> L r" using assms(1) unfolding LV_def
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1075
    using L_flat_Prf1 by blast 
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1076
  then obtain vposix where vp: "s \<in> r \<rightarrow> vposix"
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1077
    using lexer_correct_Some by blast 
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1078
  with assms(1) have "vposix :\<sqsubseteq>val v1" by (simp add: Posix_PosOrd) 
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1079
  then have "vposix = v1 \<or> vposix :\<sqsubset>val v1" unfolding PosOrd_ex_eq2 by auto
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
  1080
  moreover
272
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1081
    { assume "vposix :\<sqsubset>val v1"
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1082
      moreover
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1083
      have "vposix \<in> LV r s" using vp 
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1084
         using Posix_LV by blast 
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1085
      ultimately have "False" using assms(2) by blast
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1086
    }
f16019b11179 simplified proof
Christian Urban <urbanc@in.tum.de>
parents: 270
diff changeset
  1087
  ultimately show "s \<in> r \<rightarrow> v1" using vp by blast
261
247fc5dd4943 isar proofs
Christian Urban <urbanc@in.tum.de>
parents: 257
diff changeset
  1088
qed
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1089
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1090
lemma Least_existence:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1091
  assumes "LV r s \<noteq> {}"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1092
  shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1093
proof -
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1094
  from assms
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1095
  obtain vposix where "s \<in> r \<rightarrow> vposix"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1096
  unfolding LV_def 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1097
  using L_flat_Prf1 lexer_correct_Some by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1098
  then have "\<forall>v \<in> LV r s. vposix :\<sqsubseteq>val v"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1099
    by (simp add: Posix_PosOrd)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1100
  then show "\<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1101
    using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1102
qed 
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1103
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1104
lemma Least_existence1:
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1105
  assumes "LV r s \<noteq> {}"
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
  1106
  shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
  1107
using Least_existence[OF assms] assms
276
a3134f7de065 updated
cu
parents: 273
diff changeset
  1108
  using PosOrdeq_antisym by blast
273
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
  1109
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
  1110
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
  1111
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
  1112
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
  1113
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
  1114
lemma Least_existence1_pre:
e85099ac4c6c updated
Christian Urban <urbanc@in.tum.de>
parents: 272
diff changeset
  1115
  assumes "LV r s \<noteq> {}"
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1116
  shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1117
using Least_existence[OF assms] assms
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1118
apply -
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1119
apply(erule bexE)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1120
apply(rule_tac a="vmin" in ex1I)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1121
apply(auto)[1]
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1122
apply (metis PosOrd_Posix PosOrd_ex_eq2 PosOrd_spreI PosOrdeq_antisym Posix1(2))
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1123
apply(auto)[1]
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1124
apply(simp add: PosOrdeq_antisym)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1125
done
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1126
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1127
lemma
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1128
  shows "partial_order_on UNIV {(v1, v2). v1 :\<sqsubseteq>val v2}"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1129
apply(simp add: partial_order_on_def)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1130
apply(simp add: preorder_on_def refl_on_def)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1131
apply(simp add: PosOrdeq_refl)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1132
apply(auto)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1133
apply(rule transI)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1134
apply(auto intro: PosOrdeq_trans)[1]
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1135
apply(rule antisymI)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1136
apply(simp add: PosOrdeq_antisym)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1137
done
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1138
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1139
lemma
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1140
 "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}"
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1141
apply(rule finite_acyclic_wf)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1142
prefer 2
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1143
apply(simp add: acyclic_def)
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1144
apply(induct_tac rule: trancl.induct)
280
c840a99a3e05 updated
cu
parents: 278
diff changeset
  1145
     apply(auto)[1]
c840a99a3e05 updated
cu
parents: 278
diff changeset
  1146
    prefer 3
c840a99a3e05 updated
cu
parents: 278
diff changeset
  1147
268
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1148
oops
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1149
6746f5e1f1f8 updated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
  1150
249
256484ef4be4 updated
Christian Urban <urbanc@in.tum.de>
parents: 248
diff changeset
  1151
unused_thms
256484ef4be4 updated
Christian Urban <urbanc@in.tum.de>
parents: 248
diff changeset
  1152
248
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1153
end