# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1452083069 0
# Node ID 030939b7d4755846be7ccf0a7d141a667796a1fd
# Parent  56dd3d1d479b70de6f15820f71a0cd322c66b5e3
added type inference paper and updated Re.thy

diff -r 56dd3d1d479b -r 030939b7d475 Literature/type-pattern-match.pdf
Binary file Literature/type-pattern-match.pdf has changed
diff -r 56dd3d1d479b -r 030939b7d475 thys/Re.thy
--- a/thys/Re.thy	Sat Dec 19 23:51:31 2015 +0000
+++ b/thys/Re.thy	Wed Jan 06 12:24:29 2016 +0000
@@ -826,6 +826,12 @@
 apply (metis v3_proj v4_proj2)
 done
 
+lemma 
+  "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
+apply(simp)
+done
+
+
 section {* Sulzmann's Ordering of values *}
 
 thm PMatch.intros
@@ -870,6 +876,12 @@
 apply(auto intro: ValOrd.intros elim: Prf.cases)
 done
 
+section {* Posix definition *}
+
+definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
+where
+  "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v' \<sqsubseteq> flat v) \<longrightarrow> v \<succ>r v'))"
+
 lemma ValOrd_refl:
   assumes "\<turnstile> v : r"
   shows "v \<succ>r v"
@@ -975,6 +987,102 @@
 apply(simp_all)[8]
 done
 
+lemma POSIX_ALT_I1:
+  assumes "POSIX v1 r1" 
+  shows "POSIX (Left v1) (ALT r1 r2)"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply (metis Prf.intros(2))
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rule ValOrd.intros)
+apply(auto)
+apply(rule ValOrd.intros)
+by (metis le_eq_less_or_eq length_sprefix sprefix_def)
+
+lemma POSIX_ALT_I2:
+  assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
+  shows "POSIX (Right v2) (ALT r1 r2)"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply (metis Prf.intros)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rule ValOrd.intros)
+apply metis
+apply(rule ValOrd.intros)
+apply metis
+done
+
+thm PMatch.intros[no_vars]
+
+lemma POSIX_PMatch:
+  assumes "s \<in> r \<rightarrow> v" "\<turnstile> v' : r"
+  shows "length (flat v') \<le> length (flat v)" 
+using assms
+apply(induct arbitrary: s v v' rule: rexp.induct)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+defer
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(simp add: L_flat_Prf)
+
+apply(clarify)
+apply (metis ValOrd.intros(8))
+apply (metis POSIX_ALT_I1)
+apply(rule POSIX_ALT_I2)
+apply(simp)
+apply(auto)[1]
+apply(simp add: POSIX_def)
+apply(frule PMatch1(1))
+apply(frule PMatch1(2))
+apply(simp)
+
+
+lemma POSIX_PMatch:
+  assumes "s \<in> r \<rightarrow> v" 
+  shows "POSIX v r" 
+using assms
+apply(induct arbitrary: rule: PMatch.induct)
+apply(auto)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply (metis Prf.intros(4))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply (metis Prf.intros(5))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply (metis POSIX_ALT_I1)
+apply(rule POSIX_ALT_I2)
+apply(simp)
+apply(auto)[1]
+apply(simp add: POSIX_def)
+apply(frule PMatch1(1))
+apply(frule PMatch1(2))
+apply(simp)
+
+
 
 lemma ValOrd_PMatch:
   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 = s"
@@ -998,6 +1106,7 @@
 apply(clarify)
 apply (metis Prf_flat_L)
 apply (metis ValOrd.intros(5))
+(* Seq case *)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(auto)
@@ -1006,6 +1115,20 @@
 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
 apply(rule ValOrd.intros(2))
 apply(auto)
+apply(drule_tac x="v1a" in meta_spec)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(drule_tac meta_mp)
+prefer 2
+apply(simp)
+apply(simp add: append_eq_append_conv2)
+apply(auto)
+apply (metis Prf_flat_L)
+apply(case_tac "us = []")
+apply(simp)
+apply(drule_tac x="us" in spec)
+apply(drule mp)
+
 thm L_flat_Prf
 apply(simp add: L_flat_Prf)
 thm append_eq_append_conv2
@@ -1017,6 +1140,10 @@
 apply (metis append_Nil2)
 apply(case_tac "us = []")
 apply(auto)
+apply(drule_tac x="s2" in spec)
+apply(drule mp)
+
+apply(auto)[1]
 apply(drule_tac x="v1a" in meta_spec)
 apply(simp)