--- a/thys2/PDerivs.thy	Thu Nov 04 13:52:17 2021 +0000
+++ b/thys2/PDerivs.thy	Tue Dec 14 16:06:42 2021 +0000
@@ -17,7 +17,7 @@
 where
   "pder c ZERO = {}"
 | "pder c ONE = {}"
-| "pder c (CHAR d) = (if c = d then {ONE} else {})"
+| "pder c (CH d) = (if c = d then {ONE} else {})"
 | "pder c (ALT r1 r2) = (pder c r1) \<union> (pder c r2)"
 | "pder c (SEQ r1 r2) = 
     (if nullable r1 then SEQs (pder c r1) r2 \<union> pder c r2 else SEQs (pder c r1) r2)"
@@ -54,7 +54,7 @@
 by (induct s) (simp_all)
 
 lemma pders_CHAR:
-  shows "pders s (CHAR c) \<subseteq> {CHAR c, ONE}"
+  shows "pders s (CH c) \<subseteq> {CH c, ONE}"
 by (induct s) (simp_all)
 
 subsection \<open>Relating left-quotients and partial derivatives\<close>
@@ -127,7 +127,7 @@
 unfolding UNIV1_def pders_Set_def by (auto split: if_splits)
 
 lemma pders_Set_CHAR [simp]:
-  shows "pders_Set UNIV1 (CHAR c) = {ONE}"
+  shows "pders_Set UNIV1 (CH c) = {ONE}"
 unfolding UNIV1_def pders_Set_def
 apply(auto)
 apply(frule rev_subsetD)
@@ -282,7 +282,7 @@
 fun awidth :: "rexp \<Rightarrow> nat" where
 "awidth ZERO = 0" |
 "awidth ONE = 0" |
-"awidth (CHAR a) = 1" |
+"awidth (CH a) = 1" |
 "awidth (ALT r1 r2) = awidth r1 + awidth r2" |
 "awidth (SEQ r1 r2) = awidth r1 + awidth r2" |
 "awidth (STAR r1) = awidth r1"
@@ -364,7 +364,7 @@
 fun subs :: "rexp \<Rightarrow> rexp set" where
 "subs ZERO = {ZERO}" |
 "subs ONE = {ONE}" |
-"subs (CHAR a) = {CHAR a, ONE}" |
+"subs (CH a) = {CH a, ONE}" |
 "subs (ALT r1 r2) = (subs r1 \<union> subs r2 \<union> {ALT r1 r2})" |
 "subs (SEQ r1 r2) = (subs r1 \<union> subs r2 \<union> {SEQ r1 r2} \<union>  SEQs (subs r1) r2)" |
 "subs (STAR r1) = (subs r1 \<union> {STAR r1} \<union> SEQs (subs r1) (STAR r1))"
@@ -411,7 +411,7 @@
 fun size2 :: "rexp \<Rightarrow> nat" where
   "size2 ZERO = 1" |
   "size2 ONE = 1" |
-  "size2 (CHAR c) = 1" |
+  "size2 (CH c) = 1" |
   "size2 (ALT r1 r2) = Suc (size2 r1 + size2 r2)" |
   "size2 (SEQ r1 r2) = Suc (size2 r1 + size2 r2)" |
   "size2 (STAR r1) = Suc (size2 r1)" 
@@ -425,6 +425,7 @@
   apply(simp_all)
   done
 
+(*
 lemma subs_card:
   shows "card (subs r) \<le> Suc (size2 r + size2 r)"
   apply(induct r)
@@ -433,6 +434,7 @@
      apply(simp add: subs_finite)
     apply(simp add: subs_finite)
   oops
+*)
 
 lemma subs_size2:
   shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)"
@@ -532,7 +534,7 @@
 fun height :: "rexp \<Rightarrow> nat" where
   "height ZERO = 1" |
   "height ONE = 1" |
-  "height (CHAR c) = 1" |
+  "height (CH c) = 1" |
   "height (ALT r1 r2) = Suc (max (height r1) (height r2))" |
   "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" |
   "height (STAR r1) = Suc (height r1)" 
@@ -555,7 +557,56 @@
   apply(induct r)
   apply(auto)+
   done  
-  
-  
+
+fun lin_concat :: "(char \<times> rexp) \<Rightarrow> rexp \<Rightarrow> (char \<times> rexp)" (infixl "[.]" 91)
+  where
+"(c, ZERO) [.] t = (c, ZERO)"
+| "(c, ONE) [.] t = (c, t)"
+| "(c, p) [.] t = (c, SEQ p t)"
+
+
+fun circle_concat :: "(char \<times> rexp ) set \<Rightarrow> rexp \<Rightarrow> (char \<times> rexp) set" ( infixl "\<circle>" 90)
+  where
+"l \<circle> ZERO = {}"
+| "l \<circle> ONE = l"
+| "l \<circle> t  = ( (\<lambda>p.  p [.] t) ` l ) "
+
+
+
+fun linear_form :: "rexp \<Rightarrow>( char \<times> rexp ) set" 
+  where
+  "linear_form ZERO = {}"
+| "linear_form ONE = {}"
+| "linear_form (CH c)  = {(c, ONE)}"
+| "linear_form (ALT r1 r2) = (linear_form) r1 \<union> (linear_form r2)"
+| "linear_form (SEQ r1 r2) = (if (nullable r1) then (linear_form r1) \<circle> r2 \<union> linear_form r2 else  (linear_form r1) \<circle> r2) "
+| "linear_form (STAR r ) = (linear_form r) \<circle> (STAR r)"
+
+
+value "linear_form (SEQ (STAR (CH x)) (STAR (ALT (SEQ (CH x) (CH x)) (CH y)  ))  )"
+
+
+value "linear_form  (STAR (ALT (SEQ (CH x) (CH x)) (CH y)  ))  "
+
+fun pdero :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"
+  where
+"pdero c t  = \<Union> ((\<lambda>(d, p). if d = c then {p} else {}) ` (linear_form t) )"
+
+fun pderso :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set"
+  where
+  "pderso [] r = {r}"
+|  "pderso (c # s) r = \<Union> ( pderso s ` (pdero c r) )"
+
+lemma alternative_pder: 
+  shows "pderso s r = pders s r"
+  sledgehammer
+  oops
+
+
+export_code height pders subs pderso in Scala module_name Pders 
+export_code pdero pderso in Scala module_name Pderso
+export_code pdero pderso in Scala module_name Pderso
+
+
 
 end
\ No newline at end of file