# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1454932488 0
# Node ID f76c250906d51bf0315c6bebf2c2ba309cd7deca
# Parent  8b4c8cdd0b51d8b75b000744ad7a3964141bf5cb
updated

diff -r 8b4c8cdd0b51 -r f76c250906d5 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Mon Feb 08 09:56:32 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Feb 08 11:54:48 2016 +0000
@@ -134,7 +134,7 @@
   @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 
       @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
   @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
-      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "c" "v\<^sub>1" "v\<^sub>2"]}\\
+      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
   @{thm (lhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
       & @{thm (rhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
   @{thm (lhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 
@@ -260,6 +260,16 @@
 
 text {*
   \noindent
+  Things we have proved about our version of the Sulzmann ordering
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=IfThen] ValOrd_refl[of "v" "r"]}\medskip\\
+  @{thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]}
+  \end{tabular}
+  \end{center}\bigskip  
+
+  \noindent
   Things we like to prove, but cannot:\bigskip
 
   If @{term "s \<in> r \<rightarrow> v\<^sub>1"}, @{term "\<turnstile> v\<^sub>2 : r"}, then @{term "v\<^sub>1 \<succ>r v\<^sub>2"}
diff -r 8b4c8cdd0b51 -r f76c250906d5 thys/ReStar.thy
--- a/thys/ReStar.thy	Mon Feb 08 09:56:32 2016 +0000
+++ b/thys/ReStar.thy	Mon Feb 08 11:54:48 2016 +0000
@@ -1249,21 +1249,6 @@
 
 section {* Sulzmann's Ordering of values *}
 
-thm PMatch.intros
-
-(*
-inductive ValOrd :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_ _" [100, 100, 100, 100] 100)
-where
-  "\<lbrakk>s2 \<turnstile> v2 \<succ>r2 v2'; flat v1 = s1\<rbrakk> \<Longrightarrow> (s1 @ s2) \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
-| "\<lbrakk>s1 \<turnstile> v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
-| "\<lbrakk>flat v1 \<sqsubseteq> s; flat v2 \<sqsubseteq> flat v1\<rbrakk> \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
-| "\<lbrakk>flat v2 \<sqsubseteq> s; flat v1 \<sqsubset>  flat v2\<rbrakk> \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
-| "s \<turnstile> v2 \<succ>r2 v2' \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
-| "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
-| "s \<turnstile> Void \<succ>EMPTY Void"
-| "(c#s) \<turnstile> (Char c) \<succ>(CHAR c) (Char c)"
-*)
-
 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 where
   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
@@ -1280,6 +1265,170 @@
 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
 | "(Stars []) \<succ>(STAR r) (Stars [])"
 
+lemma ValOrd_refl:
+  assumes "\<turnstile> v : r"
+  shows "v \<succ>r v"
+using assms
+apply(induct)
+apply(auto intro: ValOrd.intros)
+done
+
+lemma ValOrd_total:
+  shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk>  \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"
+apply(induct r arbitrary: v1 v2)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis ValOrd.intros(7))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis ValOrd.intros(8))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(case_tac "v1a = v1b")
+apply(simp)
+apply(rule ValOrd.intros(1))
+apply (metis ValOrd.intros(1))
+apply(rule ValOrd.intros(2))
+apply(auto)[2]
+apply(erule contrapos_np)
+apply(rule ValOrd.intros(2))
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply (metis ValOrd.intros(6))
+apply(rule ValOrd.intros)
+apply(erule contrapos_np)
+apply(rule ValOrd.intros)
+apply (metis le_eq_less_or_eq neq_iff)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule ValOrd.intros)
+apply(erule contrapos_np)
+apply(rule ValOrd.intros)
+apply (metis le_eq_less_or_eq neq_iff)
+apply(rule ValOrd.intros)
+apply(erule contrapos_np)
+apply(rule ValOrd.intros)
+apply(metis)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)
+apply (metis ValOrd.intros(13))
+apply (metis ValOrd.intros(10) ValOrd.intros(9))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)
+apply (metis ValOrd.intros(10) ValOrd.intros(9))
+by (metis ValOrd.intros(11))
+
+lemma ValOrd_anti:
+  shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
+  and   "\<lbrakk>\<turnstile> Stars vs1 : r; \<turnstile> Stars vs2 : r; Stars vs1 \<succ>r Stars vs2; Stars vs2 \<succ>r Stars vs1\<rbrakk>  \<Longrightarrow> vs1 = vs2"
+apply(induct v1 and vs1 arbitrary: r v2 and r vs2 rule: val.inducts)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(auto)[1]
+prefer 2
+apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
+prefer 2
+apply(auto)[1]
+apply(rotate_tac 5)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply (metis (no_types) Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
+apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
+apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
+apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
+apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
+apply (metis Prf.intros(7) ValOrd.intros(11) ValOrd_refl not_Cons_self2)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+
+
+oops
+
+
 (*
 
 lemma ValOrd_PMatch:
diff -r 8b4c8cdd0b51 -r f76c250906d5 thys/paper.pdf
Binary file thys/paper.pdf has changed