diff --git a/theories/utp_circus_time.thy b/theories/utp_circus_time.thy
new file mode 100644
index 000000000..a6f2b8a95
--- /dev/null
+++ b/theories/utp_circus_time.thy
@@ -0,0 +1,517 @@
+section {* Circus Time model *}
+
+theory utp_circus_time
+  imports 
+    utp_cml
+    "../utils/Library_extra/Terminated_lists"
+    "~~/src/HOL/Library/Prefix_Order"
+begin
+
+no_adhoc_overloading uconj conj
+no_adhoc_overloading udisj disj
+no_adhoc_overloading unot Not
+  
+text {* TODO: Move these into the theory of Terminated_lists. *}
+    
+lemma stlist_last_concat:
+  fixes s z :: "'a::plus stlist"
+  shows "last (s + (x#\<^sub>tz)) = last z"
+  unfolding plus_stlist_def
+  apply (induct s)
+  by auto
+    
+lemma stlist_last_concat2:
+  fixes s :: "'a::plus stlist"
+  shows "last (x#\<^sub>t(s + [;z])) = last s + z"
+  unfolding plus_stlist_def
+  apply (induct s)
+  by auto
+    
+lemma stlist_last_concat3:
+  fixes s :: "'a::plus stlist"
+  shows "last ((x#\<^sub>ts) + [;z]) = last s + z"
+  unfolding plus_stlist_def
+  apply (induct s)
+  by auto
+   
+lemma monoid_le_stlist2:
+  "(xs :: 'a::monoid_add stlist) \<le>\<^sub>m ys \<longleftrightarrow> xs \<le> ys"
+  by (simp add: less_eq_stlist_def)
+    
+lemma stlist_eq_nil:
+  fixes a b :: "'a::ordered_cancel_monoid_diff"
+  shows "a = b \<longleftrightarrow> [;a] = [;b]"
+  by simp
+    
+lemma stlist_le_nil:
+  fixes a b :: "'a::ordered_cancel_monoid_diff"
+  shows "\<not> a < a"
+  by simp   
+  
+lemma monoid_plus_prefix_iff_zero:
+  fixes a b :: "'a::ordered_cancel_monoid_diff"
+  shows "a + x \<le> a \<longleftrightarrow> x = 0"
+  by (metis add.right_neutral antisym le_add left_cancel_monoid_class.add_left_imp_eq)
+    
+lemma stlist_le_nil_imp_le_elements:
+  fixes a b :: "'a::ordered_cancel_monoid_diff"
+  shows "[;a] \<le> [;b] \<Longrightarrow> a \<le> b"
+  apply (simp add: less_eq_stlist_def monoid_le_def)
+  apply auto
+  apply (case_tac c)
+  apply auto
+  apply (simp add: plus_stlist_def)
+  by (simp add: stlist_nil_concat_cons)
+    
+lemma stlist_le_nil_iff_le_elements:
+  fixes a b :: "'a::ordered_cancel_monoid_diff"
+  shows "[;a] \<le> [;b] \<longleftrightarrow> a \<le> b"
+  by (metis concat_stlist.simps(1) ordered_cancel_monoid_diff_class.le_iff_add plus_stlist_def stlist_le_nil_imp_le_elements)
+    
+lemma stlist_plus_nils:
+  fixes a b :: "'a::ordered_cancel_monoid_diff"
+  shows "a + b = c \<longleftrightarrow> [;a] + [;b] = [;c]"
+  by (simp add: plus_stlist_def)      
+    
+lemma stlist_nil_minus:
+  fixes a b :: "'a::ordered_cancel_monoid_diff"
+  shows "[;a] - [;b] = [;a-b]"
+  apply (case_tac "b \<le> a")
+  apply auto
+  apply (metis add_monoid_diff_cancel_left concat_stlist.simps(1) diff_add_cancel_left' minus_stlist_def plus_stlist_def)
+  apply (simp add:stlist_le_nil_iff_le_elements)
+  by (simp add:zero_stlist_def)
+    
+lemma stlist_minus_cons:
+  fixes xs ys :: "'a::ordered_cancel_monoid_diff"
+  assumes "x \<le> y" "xs \<le> ys"
+  shows "(y + ys) - (x + xs) = (y-x) + (ys-xs)"
+  using assms
+  apply (simp add:le_is_monoid_le)
+  apply (simp add:minus_def monoid_subtract_def)
+  apply auto
+  
+  oops
+    
+lemma listconsconcat:
+  fixes xs ys :: "'a::ordered_cancel_monoid_diff list"
+  assumes "x \<le> y" "xs \<le> ys"
+  shows "(y#ys) - (x#xs) = [y]-[x]+(ys-xs)"
+  using assms
+  apply (simp add:le_is_monoid_le minus_def monoid_subtract_def)
+  apply auto
+  oops
+        
+lemma stlist_nil_le_cons_imp_le:
+  fixes xs :: "'a::ordered_cancel_monoid_diff stlist"
+  shows "[;a] \<le> (x#\<^sub>txs) \<Longrightarrow> a \<le> x"
+  apply (simp add:le_is_monoid_le monoid_le_def)
+  apply auto
+  apply (case_tac c)
+  apply (simp add: plus_stlist_def)
+  by (metis stlist.inject(2) stlist_nil_concat_cons)
+
+lemma stlist_cons_minus_nil_eq:
+  fixes xs :: "'a::ordered_cancel_monoid_diff stlist"
+  assumes "[;a] \<le> (x#\<^sub>txs)"
+  shows "(x#\<^sub>txs) - [;a] = (x-a)#\<^sub>txs" 
+  using assms
+  apply (simp add:minus_stlist_def minus_def le_is_monoid_le)
+  by (smt Terminated_lists.last.simps(1) add.assoc add.right_neutral assms concat_stlist.simps(2) diff_add_cancel_left' front.simps(1) left_cancel_monoid_class.add_left_imp_eq minus_def stlist_front_concat_last stlist_nil_concat_cons stlist_nil_le_cons_imp_le stlist_plus_follow_concat zero_stlist_def)
+    
+subsection {* Types *}
+
+text {* A trace of events is a list. *}  
+  
+type_synonym '\<alpha> trace = "'\<alpha> list"
+  
+text {* We define a separate type for refusals, a set of events, so that
+        we can instantiate it with specific type classes, separate from
+        the generic set type. *}  
+  
+typedef      '\<alpha> refusal = "{x::'\<alpha> set. True}" 
+  morphisms refusal2set set2refusal
+  by auto
+
+text {* Two morphisms are defined between this type and that of generic sets,
+        refusal2set from refusal to set, and set2refusal in the opposite
+        direction. *}
+    
+text {* We set-up the lifting package to provide support for lifting on the
+        new declared type refusal. Furthermore we also enable default coercion
+        from sets to this refusal type below. *}  
+  
+setup_lifting type_definition_refusal    
+declare [[coercion_enabled]]
+        [[coercion set2refusal]]
+        
+text {* We now define the zero for refusals as the empty set by lifting
+        from sets. *}
+   
+instantiation refusal :: (type) zero
+begin
+   lift_definition zero_refusal :: "'a refusal" is "{}" ..
+   instance by (intro_classes)
+end  
+ 
+text {* As for the difference operator, we actually have a choice between 
+        lifting to set difference, or using the monoid_subtract. If we use
+        monoid_subtract then we need to instantiate refusals as monoid_add,
+        where plus is lifted from set union.*}  
+ 
+instantiation refusal :: (type) monoid_add
+begin
+   lift_definition plus_refusal :: "'a refusal \<Rightarrow> 'a refusal \<Rightarrow> 'a refusal" is "op \<union>" .
+
+   instance by (intro_classes,(transfer,auto)+)
+end
+
+instantiation refusal :: (type) minus
+begin
+  definition minus_refusal :: "'a refusal \<Rightarrow> 'a refusal \<Rightarrow> 'a refusal" where "minus_refusal == monoid_subtract"
+  
+(*lift_definition minus_refusal :: "'a refusal \<Rightarrow> 'a refusal \<Rightarrow> 'a refusal" is "op -" .
+
+  lemma refusal_zero_minus_zero:
+  "(0::'a refusal) - 0 = 0"
+  by (simp add:minus_refusal_def zero_refusal_def)*)
+      
+  lemma refusal_zero_minus_zero:
+  "(0::'a refusal) - 0 = 0"
+    apply (simp add:minus_refusal_def zero_refusal_def monoid_subtract_def)
+    by (metis (mono_tags, lifting) add.left_neutral the_equality zero_refusal.abs_eq)
+    
+  instance by (intro_classes)
+end
+  
+text {* The point with these instantiations is that we can then define
+        the type ttrace as an stlist of pairs (trace \<times> refusal) below.
+        
+        We observe that in general this does not yield an ordered
+        cancelative monoid, as there is no injective function from 
+        two sets to sets. *}
+  
+type_synonym '\<alpha> ttrace = "('\<alpha> trace \<times> '\<alpha> refusal) stlist"  
+  
+text {* To achieve a trace algebra, we define the type of circus
+        time traces (cttrace) as a ttrace, where the refusal of the 
+        ttrace is always empty (the zero). *}
+  
+typedef '\<alpha> cttrace = "{ct::'\<alpha> ttrace. snd(last(ct)) = 0}"
+morphisms ct2ttrace ttrace2ct
+  by (auto, metis Terminated_lists.last.simps(1) prod.sel(2))
+ 
+text {* Just as before, we have two morphisms, ct2ttrace from cttrace
+        to ttrace and ttrace2ct in the opposite direction. *}    
+    
+value ct2ttrace  
+value ttrace2ct
+
+declare [[coercion ttrace2ct]]
+    
+setup_lifting type_definition_cttrace
+
+  (*
+lemma cttrace_snd_last_0_minus:
+  fixes s z :: "('a list \<times> 'a refusal) stlist"
+  shows "snd (last s) = 0 \<and> snd (last z) = 0 \<Longrightarrow> snd ((last z) - (last s)) = 0"
+  apply auto
+  by (simp add:refusal_zero_minus_zero)
+    
+lemma cttrace_snd_last_0_minus2:
+  fixes s z :: "('a list \<times> 'a refusal) stlist"
+  shows "\<forall> (s::('a list \<times> 'a refusal) stlist) z. snd (last s) = 0 \<and> snd (last z) = 0 \<longrightarrow> snd ((last z) - (last s)) = 0"
+  apply auto
+  by (simp add:refusal_zero_minus_zero)
+    
+lemma stlist_last_minus_property:
+  fixes s z :: "'a::ordered_cancel_monoid_diff stlist"
+  assumes "s < z"
+  and "\<forall>x y. P (last x) \<and> P (last y) \<longrightarrow> P ((last x) - (last y))" 
+  shows "P (last z) \<and> P (last s) \<Longrightarrow> P (last (z - s))"
+  unfolding minus_stlist_def
+  using assms
+  apply (induct z s rule:stlist_induct_cons)
+  apply (metis Terminated_lists.last.simps(1) minus_stlist_def stlist_nil_minus)
+  apply simp_all
+  apply (metis Terminated_lists.last.simps(2) less_imp_le minus_stlist_def stlist_cons_minus_nil_eq) 
+  apply (metis concat_stlist.simps(3) diff_add_cancel_left' less_imp_le plus_stlist_def stlist.distinct(1))
+  by (metis add_monoid_diff_cancel_left concat_stlist.simps(3) diff_add_cancel_left' le_add less_stlist_def plus_stlist_def stlist.inject(2))
+  *)
+
+text {* We now show that cttrace is an additive monoid with any parametrised
+        type by lifting the definition of zero and plus from stlist. *}
+
+instantiation cttrace :: (type) monoid_add
+begin
+  
+  lift_definition zero_cttrace :: "'a cttrace" is "0"
+    by (simp add: zero_stlist_def)
+  
+  text {* The lifting of plus relies on proving closure of cttrace under plus,
+          that is, the second component of nil is empty. *}
+    
+  lift_definition plus_cttrace :: "'a cttrace \<Rightarrow> 'a cttrace \<Rightarrow> 'a cttrace" is "op +"
+    apply (case_tac stlist2)
+    apply (case_tac stlist1)
+    apply (simp add: plus_stlist_def)
+    apply (simp add: stlist_last_concat3)
+    by (simp add: stlist_last_concat)
+  
+  instance 
+    apply (intro_classes)
+    apply (metis (mono_tags, lifting) ct2ttrace_inject plus_cttrace.rep_eq plus_seq_assoc)
+    using ct2ttrace_inject plus_cttrace.rep_eq zero_cttrace.rep_eq apply fastforce
+    using ct2ttrace_inject plus_cttrace.rep_eq zero_cttrace.rep_eq by fastforce
+end
+  
+text {* To show that cttrace forms a trace algebra we need to show that
+        ttrace satisfies the monoid laws under the assumption that the 
+        second component of the nil element is empty. *}
+  
+lemma ct2ttrace_ttrace2ct_eq:
+  fixes a :: "'a ttrace"
+  assumes "snd(last a) = 0"
+  shows "ct2ttrace (ttrace2ct a) = a"
+  using assms
+  apply (induct a)
+  apply auto
+  apply (simp add: ttrace2ct_inverse)
+  by (simp add: ttrace2ct_inverse)
+  
+lemma ttrace2ct_dist_plus:
+  assumes "snd(last a) = 0" and "snd(last b) = 0"
+  shows "ttrace2ct (a + b) = ttrace2ct a + ttrace2ct b"
+  using assms
+  apply (simp add:plus_stlist_def plus_cttrace_def)
+  by (simp add:ct2ttrace_ttrace2ct_eq)
+
+thm cttrace.ct2ttrace_inject    
+
+text {* Below we reprove the left cancelative monoid lemmas for ttrace. *}
+  
+lemma ttrace_left_zero_cancel:
+  fixes a :: "'\<alpha> ttrace"
+  assumes "snd(last a) = 0"
+  and "snd(b) = 0"
+  and "snd(c) = 0"
+  shows "a + [;b] = a + [;c] \<Longrightarrow> [;b] = [;c]"
+  using assms
+  unfolding plus_stlist_def
+  apply (induct a)
+  apply auto
+  by (metis fst_add left_cancel_monoid_class.add_left_imp_eq prod.collapse)
+
+lemma ttrace_left_cancel_monoid0:
+  fixes b c :: "'\<alpha> ttrace"
+  assumes "snd(a) = 0"
+  and "snd(last b) = 0"
+  and "snd(last c) = 0"
+  shows "[;a] + b = [;a] + c \<Longrightarrow> b = c"
+  using assms
+  unfolding plus_stlist_def
+  apply (induct rule:stlist_induct_cons)
+  apply auto
+  apply (metis fst_add fst_conv left_cancel_monoid_class.add_left_imp_eq)
+  apply (metis fst_add fst_conv left_cancel_monoid_class.add_left_imp_eq)
+  by (metis add.left_neutral snd_add snd_conv)        
+
+lemma ttrace_left_cancel_monoid:
+  fixes a b c :: "'\<alpha> ttrace"
+  assumes "snd(last a) = 0"
+  and "snd(last b) = 0"
+  and "snd(last c) = 0"
+  shows "a + b = a + c \<Longrightarrow> b = c"
+  using assms
+  apply (induct a rule:stlist.induct)
+  using ttrace_left_cancel_monoid0 apply auto[1]
+  by (simp add: plus_stlist_def)
+    
+text {* Below we reprove the right cancelative monoid lemmas for ttrace. *}
+
+lemma ttrace_right_cancel_monoid0:
+  fixes b c :: "'\<alpha> ttrace"
+  assumes "snd(a) = 0"
+  and "snd(last b) = 0"
+  and "snd(last c) = 0"
+  shows "(b + [;a] = c + [;a]) \<Longrightarrow> b = c"
+  using assms
+  unfolding plus_stlist_def
+  apply (induct b c rule:stlist_induct_cons, auto)
+  by (metis fst_add fst_conv right_cancel_monoid_class.add_right_imp_eq)
+
+lemma ttrace_right_cancel_monoid1:
+  fixes b c :: "'\<alpha> ttrace"
+  assumes  "snd(d) = 0"
+  and "snd(last b) = 0"
+  and "snd(last c) = 0"
+  shows "(b + [a;d] = c + [a;d]) \<Longrightarrow> b = c"
+  using assms
+  unfolding plus_stlist_def
+  apply (induct b c rule:stlist_induct_cons, auto)
+  apply (metis fst_add fst_conv right_cancel_monoid_class.add_right_imp_eq)
+  apply (case_tac "xs", simp+)
+  by (case_tac "ys", simp+)
+    
+lemma ttrace_right_cancel_monoid2:
+  fixes a :: "'\<alpha> ttrace"
+  shows "(b#\<^sub>ta) = (c#\<^sub>ta) \<Longrightarrow> b = c"  
+  by auto
+    
+lemma ttrace_zero_monoid_sum:
+  fixes a :: "'\<alpha> ttrace"
+  assumes "snd(last a) = 0"
+  and "snd(last b) = 0"
+  shows "a + b = 0 \<Longrightarrow> a = 0"
+  using assms
+  apply (induct a b rule:stlist_induct_cons)
+  apply (smt Terminated_lists.last.simps(1) add.right_neutral concat_stlist.simps(1) fst_add fst_zero plus_prod_def plus_stlist_def snd_zero zero_sum_right)
+  by (simp add: plus_stlist_def zero_stlist_def zero_sum_left)+     
+    
+lemma ttrace_plus_follow_concat:
+  fixes a c :: "'\<alpha> ttrace"
+  shows "a + (b #\<^sub>t c) = a + [b;0] + c"
+  by (metis concat_stlist.simps(3) plus_seq_assoc plus_stlist_def stlist_concat_zero_left)
+
+lemma last_concat_pair:
+  shows "last (b + [x1a; 0]) = 0"
+  by (simp add: stlist_last_concat)
+
+lemma snd_last_concat_pair:
+  shows "snd(last (b + [x1a; 0])) = 0"
+  by (simp add: stlist_last_concat)    
+    
+lemma ttrace_plus_closure:
+  fixes a b :: "'\<alpha> ttrace"
+  assumes "snd(last a) = 0"
+  and "snd(last b) = 0"
+  shows "snd(last (a+b)) = 0"
+  using assms
+  apply (induct a b rule:stlist_induct_cons)
+  apply auto
+  apply (simp add: plus_stlist_def)
+  apply (simp add: stlist_last_concat3)
+  by (simp add: stlist_last_concat)+
+
+lemma trace_refusal_right_cancel:
+  fixes b1 :: "'\<alpha> trace" and b2 :: "'\<alpha> refusal"
+  assumes "b2 = 0" and "c2 = 0"
+  shows "(b1, b2) + a = (c1, c2) + a \<Longrightarrow> b1 = c1 \<and> b2 = c2"
+  using assms
+  by (metis fst_add fst_conv right_cancel_monoid_class.add_right_imp_eq)
+    
+lemma ttrace_right_cancel_monoid3:
+  fixes c :: "'\<alpha> ttrace"
+  shows "[;(a, 0)] + c = [;(b, 0)] + c \<Longrightarrow> a = b"
+  apply (induct c)
+  apply (metis (mono_tags, lifting) Terminated_lists.last.simps(1) concat_stlist.simps(1) fstI fst_add plus_stlist_def right_cancel_monoid_class.add_right_imp_eq)
+  by (metis (no_types, lifting) fst_add fst_conv right_cancel_monoid_class.add_right_imp_eq stlist_nil_concat_cons ttrace_right_cancel_monoid2)
+
+lemma ttrace_right_cancel_monoid:
+  fixes b c :: "'\<alpha> ttrace"
+  assumes "snd(last a) = 0"
+  and "snd(last b) = 0"
+  and "snd(last c) = 0"
+  shows "b+a = c+a \<Longrightarrow> b = c"
+  using assms
+  apply (induct a arbitrary:b c rule:stlist.induct, auto)
+  apply (meson snd_conv ttrace_right_cancel_monoid0)
+  by (metis (mono_tags, lifting) snd_last_concat_pair ttrace_plus_follow_concat ttrace_right_cancel_monoid1)
+ 
+(*  (* alternative step-by-step proof below *)
+proof (induct a arbitrary: b c rule:stlist.induct)
+  case (Nil x)
+  then show ?case by (simp add: ttrace_right_cancel_monoid0)
+next
+  case a:(Cons x1a x2)
+      
+  then show ?case
+    proof -
+      from a
+      have c:"b + [x1a;0] + x2 = c + [x1a;0] + x2"
+        by (metis ttrace_plus_follow_concat)
+      
+      then have "(b + [x1a;0]) + x2 = (c + [x1a;0]) + x2"
+        by auto
+      
+      have c:"snd(last(b + [x1a;0])) = 0"
+        by (metis snd_last_concat_pair)
+          
+      have d:"snd(last(c + [x1a;0])) = 0"
+        by (metis snd_last_concat_pair)
+          
+      from a and c and d 
+      have "b + [x1a;0] = c + [x1a;0]"
+        by (metis Terminated_lists.last.simps(2) \<open>b + [x1a; 0] + x2 = c + [x1a; 0] + x2\<close>)
+      then have "b = c"
+        using ttrace_right_cancel_monoid1
+        using a.prems(3) a.prems(4) snd_zero by blast
+  
+    qed*)
+    
+text {* We then instantiate cttrace as a cancelative monoid, which relies
+        on the lemmas we have just proved. *}
+    
+instantiation cttrace :: (type) cancel_monoid
+begin
+instance 
+  apply intro_classes
+  apply (metis (mono_tags, lifting) ct2ttrace ct2ttrace_inject mem_Collect_eq plus_cttrace.rep_eq ttrace_left_cancel_monoid)
+  apply (metis (mono_tags, lifting) ct2ttrace ct2ttrace_inject mem_Collect_eq plus_cttrace.rep_eq ttrace_zero_monoid_sum zero_cttrace.rep_eq)
+  using ttrace_right_cancel_monoid
+  by (metis (mono_tags, lifting) ct2ttrace ct2ttrace_inject mem_Collect_eq plus_cttrace.rep_eq) (* can't complete because have not proved right cancellative monoid for type *)
+end
+
+text {* Finally to show that we have a trace algebra we define less_eq, less
+        and minus directly in terms of the monoid definitions. The proof is
+        now trivial. *}  
+  
+instantiation cttrace :: (type) ordered_cancel_monoid_diff
+begin
+  
+  definition less_eq_cttrace :: "'a cttrace \<Rightarrow> 'a cttrace \<Rightarrow> bool" where "less_eq_cttrace == monoid_le"
+  definition less_cttrace :: "'a cttrace \<Rightarrow> 'a cttrace \<Rightarrow> bool" where "less_cttrace x y == x \<le> y \<and> \<not> (y \<le> x)"
+  definition minus_cttrace :: "'a cttrace \<Rightarrow> 'a cttrace \<Rightarrow> 'a cttrace" where "minus_cttrace == monoid_subtract"
+  
+instance
+  apply intro_classes
+  apply (simp add: less_eq_cttrace_def)
+  apply (simp add: less_cttrace_def)
+  by (simp add: minus_cttrace_def)
+
+(* REVISED UP TO HERE *)
+  
+text {* What is the meaning of "empty" refusals in the CML trace?
+  That is, a trace like [Event a, Event b] should have an unrestricted
+  trace, rather than being empty? *}
+  
+fun ccut :: "'\<theta> tevent list \<Rightarrow> (('\<theta> trace \<times> '\<theta> refusal) \<times> '\<theta> tevent list)" where
+"ccut [] = (([],{}),[])" |
+"ccut (Tock T # t) = (([],T), t)" |
+"ccut (Event e # t) = ((e # fst (fst (ccut t)), snd (fst (ccut t))),snd (ccut t))"
+  
+function c2ct :: "'\<theta> tevent list \<Rightarrow> '\<theta> timedtrace" where 
+"c2ct T = (fst (ccut T)) # (c2ct (snd (ccut T)))"
+by auto
+
+value "ccut []"
+value "ccut [Event a, Event b]"
+value "ccut [Event a, Event b, Tock {d}, Event e, Event f, Tock {g}]"
+(*
+
+fun cml2ct :: "'\<theta> tevent list \<Rightarrow> '\<theta> timedtrace" where
+"cml2ct [] = [([],{})]" |
+"cml2ct (Tock T # t) = (([],T), t)"
+
+"c2ct (Tock T # t) = [fst (ccut (Tock T # t))] # c2ct t" |
+"c2ct (Event e # t) = [fst (ccut (Event e # t))] # "
+*)
+text {* Could we really reuse the generalised reactive designs
+        with the trace model of Circus Time? I don't think so
+        for several reasons:
+    
+        1. Traces are non-empty.
+        2. Zero element cannot just be empty trace.
+        3. R2 as defined would not apply?  *}
+
+end
\ No newline at end of file
diff --git a/theories/utp_cml.thy b/theories/utp_cml.thy
index 898c31af4..f858d8bbe 100644
--- a/theories/utp_cml.thy
+++ b/theories/utp_cml.thy
@@ -22,7 +22,14 @@ lemma events_append [simp]: "events (xs @ ys) = events(xs) @ events(ys)"
   apply (rename_tac x xs)
   apply (case_tac x)
   apply (simp_all)
-done
+  done
+    
+lemma events_mono: "(P \<le> Q) \<Longrightarrow> (events(P) \<le> events(Q))"
+  apply (induct P rule:events.induct)
+  apply simp+
+  apply auto
+  apply (metis (no_types, lifting) Prefix_Order.prefixE Prefix_Order.prefix_prefix events.simps(2) events_append order_refl)
+  by (metis (mono_tags, lifting) Prefix_Order.prefixE Prefix_Order.prefix_prefix events.simps(3) events_append order_refl)    
 
 fun tocks :: "'\<theta> tevent list \<Rightarrow> '\<theta> tevent list" where
 "tocks [] = []" |
@@ -34,6 +41,26 @@ fun refusals :: "'\<theta> tevent list \<Rightarrow> '\<theta> set" where
 "refusals (Tock A # t) = A \<union> refusals t" |
 "refusals (Event x # t) = refusals t"
 
+lemma refusals_dist: "refusals(a @ t) = (refusals(a) \<union> refusals(t))"
+  apply (induct a)
+  apply (simp_all)
+  apply (case_tac a1)
+  apply simp_all
+  by auto
+    
+lemma refusals_ord_subset: "(P \<le> Q) \<Longrightarrow> (refusals(P) \<subseteq> refusals(Q))"
+  apply (induct P)
+  apply (simp_all)
+  apply (case_tac a)
+  apply simp_all
+  apply auto
+  apply (metis Prefix_Order.prefixE UnI1 refusals.simps(2) refusals_dist)
+  apply (metis Prefix_Order.prefixE UnCI refusals.simps(2) refusals_dist)
+  by (metis Prefix_Order.prefixE UnI1 refusals.simps(3) refusals_dist)
+ 
+lemma refusals_prefix: "t \<le> u \<and> a \<in> refusals(t) \<Longrightarrow> a \<in> refusals(u)"
+  using refusals_ord_subset by auto
+
 fun idleprefix :: "'\<theta> tevent list \<Rightarrow> '\<theta> tevent list" where
 "idleprefix [] = []" |
 "idleprefix (Tock A # t) = (Tock A # idleprefix t)" |
@@ -57,7 +84,7 @@ translations
   "idleprefix\<^sub>u(t)" == "CONST uop CONST idleprefix t"
   "idlesuffix\<^sub>u(t)" == "CONST uop CONST idlesuffix t"
   "ev\<^sub>u(e)" == "CONST uop CONST Event e"
-  "tock\<^sub>u(t,A)" == "CONST bop CONST Tock t A"
+  "tock\<^sub>u(t,A)" == "CONST bop CONST Tock t A" (* Why does this take two parameters?*)
 
 subsection {* Signature *}
 
@@ -266,4 +293,5 @@ proof -
     finally show ?thesis .
   qed
 qed
+
 end
\ No newline at end of file
diff --git a/theories/utp_timed_rea_designs.thy b/theories/utp_timed_rea_designs.thy
index 4ed614cde..caf82bd21 100644
--- a/theories/utp_timed_rea_designs.thy
+++ b/theories/utp_timed_rea_designs.thy
@@ -15,8 +15,10 @@ class time_trace = trace +
   assumes dur_non_zero [simp]: "dur(t) \<ge> 0"
   and dur_empty [simp]: "dur(0) = 0"
   and dur_concat [simp]: "dur(x + y) = dur(x) + dur(y)"
-  and idle_empty [simp]: "idle(0)"
-  and idle_concat: "idle(x + y) \<longleftrightarrow> (idle(x) \<and> idle(y))"
+  (*and idle_empty [simp]: "idle(0)"*)
+  and idle_concat: "idle(x + y) \<longleftrightarrow> (idle(x) \<and> idle(y))"(* \<longleftrightarrow> "*)
+  and dur_idle_eq: "idle(x) \<equiv> \<forall>y. dur(x) = dur(y) \<longrightarrow> x \<le> y"
+  (*and dur_idle_eq: "x \<le> y \<and> dur(x) = dur(y) \<and> idle(x) \<and> idle(y) \<Longrightarrow> x = y"*)
 begin
 
   lemma dur_mono: "x \<le> y \<Longrightarrow> dur(x) \<le> dur(y)"
@@ -25,6 +27,15 @@ begin
   lemma dur_minus [simp]: "y \<le> x \<Longrightarrow> dur(x - y) = dur(x) - dur(y)"
     by (metis add.commute add_diff_cancel_right' diff_add_cancel_left' dur_concat)
 
+  lemma idle_diff: "x \<le> y \<and> idle(x) \<and> idle(y) \<Longrightarrow> idle(y - x)"
+    using local.diff_add_cancel_left' local.idle_concat by fastforce
+  
+  lemma idle_empty[simp]: "idle(0)"
+    by (simp add: local.dur_idle_eq)
+
+  lemma dur_idle_imp: "x \<le> y \<and> dur(x) = dur(y) \<and> idle(x) \<and> idle(y) \<Longrightarrow> x = y"
+    by (metis local.dur_idle_eq local.le_is_monoid_le local.monoid_le_antisym)
+
 end
 
 class dtime_trace = time_trace +
@@ -64,10 +75,13 @@ translations
   "is-idle" == "CONST uop CONST idle tt"
 
 subsection {* Signature *}
-
+  
+abbreviation Skip :: "('\<sigma>,'t::time_trace,'\<alpha>) hrel_rsp" where
+"Skip \<equiv> II\<^sub>R"
+  
 definition Wait :: "(real, '\<sigma>) uexpr \<Rightarrow> ('\<sigma>,'t::time_trace,'\<alpha>) hrel_rsp" where
-[upred_defs]: "Wait n = \<^bold>R\<^sub>s(true \<turnstile> (\<^bold>l <\<^sub>u \<lceil>n\<rceil>\<^sub>S\<^sub>< \<and> is-idle) \<diamondop> (\<^bold>l =\<^sub>u \<lceil>n\<rceil>\<^sub>S\<^sub>< \<and> is-idle \<and> $st\<acute> =\<^sub>u $st))"
-
+[upred_defs]: "Wait n = \<^bold>R\<^sub>s(true \<turnstile> (\<^bold>l <\<^sub>u \<lceil>n\<rceil>\<^sub>S\<^sub>< \<and> is-idle) \<diamondop> (\<^bold>l =\<^sub>u \<lceil>n\<rceil>\<^sub>S\<^sub>< \<and> is-idle \<and> $st\<acute> =\<^sub>u $st \<and> \<lceil>II\<rceil>\<^sub>R ))"
+  
 definition Interrupt :: "('\<sigma>,'t::time_trace,'\<alpha>) hrel_rsp \<Rightarrow> (real, '\<sigma>) uexpr \<Rightarrow> ('\<sigma>,'t,'\<alpha>) hrel_rsp \<Rightarrow> ('\<sigma>,'t,'\<alpha>) hrel_rsp" (infixl "\<triangle>'(_')" 85) where
 "P \<triangle>(n) Q = \<^bold>R\<^sub>s(((\<^bold>l \<le>\<^sub>u \<lceil>n\<rceil>\<^sub>S\<^sub>< \<Rightarrow> pre\<^sub>R(P)) \<and> (\<^bold>l =\<^sub>u \<lceil>n\<rceil>\<^sub>S\<^sub>< \<Rightarrow> post\<^sub>R(P) wp\<^sub>R pre\<^sub>R(Q)))
                \<turnstile> ((peri\<^sub>R(P) \<and> \<^bold>l \<le>\<^sub>u \<lceil>n\<rceil>\<^sub>S\<^sub><) \<or> ((peri\<^sub>R(P) \<and> \<^bold>l =\<^sub>u \<lceil>n\<rceil>\<^sub>S\<^sub><) ;; peri\<^sub>R(Q)))
@@ -76,4 +90,41 @@ definition Interrupt :: "('\<sigma>,'t::time_trace,'\<alpha>) hrel_rsp \<Rightar
 definition Deadline :: "('\<sigma>,'t::time_trace,'\<alpha>) hrel_rsp \<Rightarrow> (real, '\<sigma>) uexpr \<Rightarrow> ('\<sigma>,'t,'\<alpha>) hrel_rsp" ("_ endsby'(_')" [90,0] 91) where
 "P endsby(n) = P \<triangle>(n) Miracle"
 
+
+lemma Skip_def: "Skip = \<^bold>R\<^sub>s(true \<turnstile> false \<diamondop> ($tr\<acute> =\<^sub>u $tr \<and> $st\<acute> =\<^sub>u $st \<and> \<lceil>II\<rceil>\<^sub>R ))"
+  by (simp add: srdes_skip_def, rel_auto)
+      
+lemma l_zero_is_idle_eq_tr:
+  fixes P :: "('\<sigma>,'t::time_trace,'\<alpha>) hrel_rsp"
+  assumes "P is R1"
+  shows "`(P \<and> \<^bold>l =\<^sub>u \<lceil>0\<rceil>\<^sub>S\<^sub>< \<and> is-idle) \<Rightarrow> ($tr\<acute> =\<^sub>u $tr)`"
+  using assms 
+  apply pred_auto
+  by (metis (no_types, lifting) dur_empty dur_idle_eq dur_idle_imp idle_empty minus_zero_eq)
+
+lemma Wait_0: "Wait 0 = Skip"
+proof -
+  have "Wait 0 = \<^bold>R\<^sub>s(true \<turnstile> (\<^bold>l <\<^sub>u \<lceil>0\<rceil>\<^sub>S\<^sub>< \<and> is-idle) \<diamondop> (\<^bold>l =\<^sub>u \<lceil>0\<rceil>\<^sub>S\<^sub>< \<and> is-idle \<and> $st\<acute> =\<^sub>u $st \<and> \<lceil>II\<rceil>\<^sub>R ))"
+    by pred_auto
+  also have "... = \<^bold>R\<^sub>s(true \<turnstile> false \<diamondop> (\<^bold>l =\<^sub>u \<lceil>0\<rceil>\<^sub>S\<^sub>< \<and> is-idle \<and> $st\<acute> =\<^sub>u $st \<and> \<lceil>II\<rceil>\<^sub>R ))"
+    apply pred_simp
+    using dur_mono by fastforce
+  also have "... = \<^bold>R\<^sub>s(true \<turnstile> false \<diamondop> ($tr\<acute> =\<^sub>u $tr \<and> $st\<acute> =\<^sub>u $st \<and> \<lceil>II\<rceil>\<^sub>R ))"
+    apply pred_auto
+    apply (simp add: dur_idle_eq dur_idle_imp)
+    using minus_zero_eq by blast
+  also have "... = Skip"
+    by (simp add: SRD_srdes_skip Skip_def)
+  finally show ?thesis .
+qed
+  
+lemma Wait_is_R2: "Wait m is R2"
+  by (simp add: Healthy_def' R1_R2c_is_R2 R2_idem RHS_def Wait_def)
+  
+lemma P_seq_R1_false: "P ;; R1 false = false"
+  by (simp add: R1_false)
+    
+lemma R1_false_seq_P: "R1 false ;; P = false"
+  by (simp add: R1_false)
+    
 end
\ No newline at end of file
diff --git a/utils/Library_extra/Terminated_lists.thy b/utils/Library_extra/Terminated_lists.thy
new file mode 100644
index 000000000..dae0c2741
--- /dev/null
+++ b/utils/Library_extra/Terminated_lists.thy
@@ -0,0 +1,695 @@
+section {* Terminated lists *}
+
+theory Terminated_lists
+imports
+  Main
+  Monoid_extra
+begin
+
+text {* Finite terminated lists are lists where the Nil element 
+        can record some information.*}
+
+subsection {* Generic terminated lists datatype *}
+
+datatype ('\<alpha>,'\<theta>) gtlist = Nil "'\<alpha>" ("[;;(_)]") | Cons "'\<theta>" "('\<alpha>,'\<theta>) gtlist" (infixr "#\<^sub>g\<^sub>t" 65) 
+  
+syntax
+  "_gtlist"     :: "args \<Rightarrow> 'a \<Rightarrow> ('\<alpha>,'\<theta>) gtlist"    ("[(_);;(_)]")
+
+translations
+  "[x,xs;;y]" == "(x#\<^sub>g\<^sub>t[xs;;y])"
+  "[x;;y]" == "x#\<^sub>g\<^sub>t[;;y]"
+  
+value "[a,b,c;;e]"
+value "[;;e]"
+  
+text {* If we take '\<alpha> to be the unit type, then we have a traditional
+        list where the Nil element does not record anything else. *}
+
+type_synonym '\<theta> unit_ttlist1 = "(unit,'\<theta>) gtlist"
+  
+primrec ttlist1_list2list :: "'\<theta> unit_ttlist1 \<Rightarrow> '\<theta> list" where
+"ttlist1_list2list (Nil s) = []" |
+"ttlist1_list2list (Cons x xs) = x#(ttlist1_list2list xs)"
+
+primrec list2ttlist1_list :: "'\<theta> list \<Rightarrow> '\<theta> unit_ttlist1" where
+"list2ttlist1_list [] = (Nil ())" |
+"list2ttlist1_list (x#xs) = (Cons x (list2ttlist1_list xs))"
+
+lemma "list2ttlist1_list (ttlist1_list2list sl) = sl"
+  by (induct sl, auto)
+  
+lemma "ttlist1_list2list (list2ttlist1_list sl) = sl"
+  by (induct sl, auto)
+    
+text {* If we wanted to show that given a plus operator between
+        '\<alpha> => '\<theta> yielding '\<theta>, we would need some kind of locale
+        here, and would need a function ('\<alpha> => '\<theta> => '\<theta>) to be
+        able to define plus in a generic way. *}
+
+subsection {* Standard terminated lists *}
+  
+datatype '\<alpha> stlist = Nil "'\<alpha>" ("[;(_)]") | Cons "'\<alpha>" "'\<alpha> stlist" (infixr "#\<^sub>t" 65)  
+  
+syntax
+  "_stlist"     :: "args \<Rightarrow> 'a \<Rightarrow> '\<alpha> stlist"    ("[(_); (_)]")
+
+translations
+  "[x,xs;y]" == "(x#\<^sub>t[xs;y])"
+  "[x;y]" == "x#\<^sub>t[;y]"
+
+value "[a,b,c;e]"
+value "[;e]"
+  
+text {* We can then show that a list is a special
+        case of this structure by defining a pair of functions. *}
+
+primrec stlist2list :: "'\<theta> stlist \<Rightarrow> '\<theta> list" where
+"stlist2list [;s] = []" |
+"stlist2list (x#\<^sub>txs) = x#(stlist2list xs)"  
+
+primrec list2stlist :: "'\<theta> \<Rightarrow> '\<theta> list \<Rightarrow> '\<theta> stlist" where
+"list2stlist a [] = [;a]" |
+"list2stlist a (x#xs) = (Cons x (list2stlist a xs))"
+  
+lemma "stlist2list (list2stlist z sl) = sl"
+  by (induct sl, auto)
+
+text {* And given a stlist with a predefined zero representation,
+        we get the same back. *}
+    
+lemma "list2stlist z (stlist2list (sl#\<^sub>t[;z])) = (sl#\<^sub>t[;z])"
+  by (auto)
+  
+primrec seq2_Nlist2list :: "'\<theta> stlist \<Rightarrow> '\<theta> list" where
+"seq2_Nlist2list [;s] = [s]" |
+"seq2_Nlist2list (x#\<^sub>txs) = x#(seq2_Nlist2list xs)"
+
+primrec Nlist2seq2_list :: "'\<theta> list \<Rightarrow> '\<theta> stlist" where
+"Nlist2seq2_list [] = [;undefined]" |
+"Nlist2seq2_list (x#xs) = (if xs = [] then [;x] else (x#\<^sub>t(Nlist2seq2_list xs)))"
+
+lemma "Nlist2seq2_list (seq2_Nlist2list sl) = sl"
+  apply (induct sl)
+  by (auto)
+  
+lemma 
+  assumes "length sl > 0" 
+  shows "seq2_Nlist2list (Nlist2seq2_list sl) = sl"
+  using assms
+  apply (induct sl)
+  by auto
+    
+subsection {* Auxiliary induction rules *}
+  
+lemma stlist_induct_cons: 
+  "\<lbrakk>
+   \<And>a b.  P [;a] [;b];
+   \<And>a x xs. P (x#\<^sub>txs) [;a] ;
+   \<And>a y ys. P [;a] (y#\<^sub>tys);
+   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#\<^sub>txs) (y#\<^sub>tys) \<rbrakk>
+ \<Longrightarrow> P xs ys"
+  apply (induct xs arbitrary: ys)
+  apply auto
+  apply (case_tac "xa")
+  apply auto
+  apply (case_tac "x")
+  by auto
+
+subsection {* Operators *}
+  
+text {* We define a concatenation operator (plus) based on the plus of the
+        parametrised type being used. *}  
+  
+fun concat_stlist :: "('a::plus) stlist \<Rightarrow> ('a::plus) stlist \<Rightarrow> ('a::plus) stlist" (infixl "@\<^sub>t" 66)
+where
+"[;z] @\<^sub>t [;x] = [;z+x]" |
+"[;z] @\<^sub>t (x#\<^sub>txs) = (z+x)#\<^sub>txs" |
+"(x#\<^sub>txs) @\<^sub>t zs = x#\<^sub>t(xs@\<^sub>tzs)"
+
+text {* We define a last function *}
+  
+primrec last :: "'a stlist \<Rightarrow> 'a" where
+"last [;x] = x" |
+"last (x#\<^sub>txs) = last xs"
+
+subsection {* Classes *}
+
+subsubsection {* Plus *}  
+  
+text {* We now instantiate the plus operator for the stlist type. *}
+  
+instantiation stlist :: (plus) plus
+begin
+
+  definition plus_stlist :: "'a stlist \<Rightarrow> 'a stlist \<Rightarrow> 'a stlist"
+    where "plus_stlist == concat_stlist"
+  
+  instance by (intro_classes)
+end
+  
+lemma stlist_nil_concat_cons:
+  shows "[;a] + (xs#\<^sub>tys) = (a + xs)#\<^sub>tys" 
+  by (simp add:plus_stlist_def)
+
+lemma stlist_not_cons: "d \<noteq> x#\<^sub>td"
+  by (metis add_cancel_left_right lessI less_imp_not_eq2 stlist.size(4))
+    
+lemma stlist_concat_not_eq: "(b#\<^sub>t[;d])+a \<noteq> [;c]+a"
+  unfolding plus_stlist_def
+  apply (induct a rule:stlist.induct)
+  apply simp_all
+  by (metis stlist_not_cons)
+    
+lemma stlist_concat_not_eq2: "(b#\<^sub>t[d;e])+a \<noteq> [;c]+a"
+  unfolding plus_stlist_def
+  apply (induct a rule:stlist.induct)
+  apply simp_all
+  by (metis add_le_same_cancel1 le_add lessI not_less stlist.size(4))
+    
+lemma stlist_concat_noteq: "x1a #\<^sub>t x2 \<noteq> x2"
+  apply (induct x2)
+  by auto
+    
+lemma stlist_concat_noteq2: "(b #\<^sub>t x2) + a \<noteq> (b #\<^sub>t x1a #\<^sub>t x2) + a"
+  by (simp add: plus_stlist_def stlist_not_cons)
+    
+lemma stlist_last_concat:
+  fixes s z :: "'a::plus stlist"
+  shows "last (s + (x#\<^sub>tz)) = last z"
+  unfolding plus_stlist_def
+  apply (induct s)
+  by auto
+    
+lemma stlist_last_concat2:
+  fixes s :: "'a::plus stlist"
+  shows "last (x#\<^sub>t(s + [;z])) = last s + z"
+  unfolding plus_stlist_def
+  apply (induct s)
+  by auto
+    
+lemma stlist_last_concat3:
+  fixes s :: "'a::plus stlist"
+  shows "last ((x#\<^sub>ts) + [;z]) = last s + z"
+  unfolding plus_stlist_def
+  apply (induct s)
+  by auto    
+    
+lemma stlist_eq_nil_pluses_imp0:
+  shows "[;a] = [;c] + e \<Longrightarrow> \<exists>z. e = [;z]"
+  apply (induct e)
+  apply auto
+  by (simp add: stlist_nil_concat_cons)
+    
+lemma stlist_eq_nil:
+  shows "a = b \<longleftrightarrow> [;a] = [;b]"
+  by simp
+    
+lemma stlist_plus_nils:
+  fixes a b :: "'a::plus"
+  shows "a + b = c \<longleftrightarrow> [;a] + [;b] = [;c]"
+  by (simp add: plus_stlist_def)
+     
+lemma stlist_eqnils_plus_zero_cons_imp:
+  fixes a :: "'a::monoid_add"
+  shows "[;a] + (0 #\<^sub>t xs) = [;c] + (0 #\<^sub>t ys) \<Longrightarrow> [;a] + xs = [;c] + ys"
+  by (simp add: stlist_nil_concat_cons)
+    
+lemma stlist_eq_nil_iff_cons_eq1:
+  assumes "xs = ys"
+  shows "[;a] = [;b] \<longleftrightarrow> (a#xs) = (b#ys)"
+  using assms by blast
+    
+lemma stlist_eq_nil_iff_cons_eq2:
+  assumes "xs = ys"
+  shows "a = b \<longleftrightarrow> (a#xs) = (b#ys)"
+  using assms by blast
+    
+subsubsection {* Additive monoid *}
+  
+text {* Given a monoid_add class we also have a monoid_add. On top of
+        plus we define the zero as the parametrised type zero. *}
+  
+instantiation stlist :: (monoid_add) monoid_add
+begin
+  
+  definition zero_stlist :: "'a stlist" where "zero_stlist = [;0]" 
+  
+  lemma stlist_zero_is_zero:
+  shows "[;0] = 0"
+  by (simp add:zero_stlist_def)
+  
+subsubsection {* Lemmas on monoid_add with stlist *}
+    
+lemma stlist_concat_zero_left[simp]: 
+  fixes y::"'a stlist"
+  shows "[;0] + y = y"
+  unfolding plus_stlist_def
+  by (induct y, auto)
+    
+lemma stlist_concat_zero_right[simp]: 
+  fixes y::"'a stlist"
+  shows "y + [;0] = y"
+  unfolding plus_stlist_def
+  by (induct y, auto)
+    
+lemma plus_seq_assoc: 
+  fixes xs ys zs::"'a stlist"
+  shows "(xs + ys) + zs = xs + (ys + zs)"
+  unfolding plus_stlist_def
+  apply (induct xs)
+  apply (induct ys)
+  apply (induct zs)
+  apply auto
+  apply (simp add: add.assoc)
+  by (simp add:add.semigroup_axioms semigroup.assoc)
+    
+instance
+  apply (intro_classes)
+  by (auto simp:plus_seq_assoc zero_stlist_def)
+end
+
+text {* Given an additive monoid type, we can define a front function
+        that yields front(s) + last(s) for a given stlist s *}
+    
+primrec front :: "'a::monoid_add stlist \<Rightarrow> 'a stlist" where
+"front [;x] = 0" |
+"front (x#\<^sub>txs) = (x#\<^sub>tfront xs)"
+
+value "front [a;b]"
+
+lemma stlist_front_concat_last: "s = front(s) + [;last(s)]"
+  unfolding plus_stlist_def
+  apply (induct s)
+  apply auto
+  by (simp add: zero_stlist_def)
+    
+lemma stlist_cons_plus_nil_front_last:
+  shows "(x #\<^sub>t xs) + [;b] = (x #\<^sub>t front(xs)) + [;last(xs) + b]"
+  by (metis (no_types, lifting) concat_stlist.simps(3) plus_seq_assoc plus_stlist_def stlist_front_concat_last stlist_plus_nils)
+  
+lemma stlist_cons_plus_nils:
+  shows "(x #\<^sub>t xs) + [;b] = (y #\<^sub>t ys) + [;d] \<longleftrightarrow> x = y \<and> (xs + [;b] = ys + [;d])"
+  by (simp add: plus_stlist_def)
+    
+lemma stlist_cons_plus_nils_eq_cons:
+  shows "[;e] + (x #\<^sub>t xs) = (y #\<^sub>t ys) \<longleftrightarrow> e + x = y \<and> xs = ys"
+  by (simp add: stlist_nil_concat_cons)
+    
+lemma stlist_plus_cons_eq_front_plus:
+  shows "e + (x #\<^sub>t xs) = front(e) + ((last(e) + x) #\<^sub>t xs)"
+  by (metis plus_seq_assoc stlist_cons_plus_nils_eq_cons stlist_front_concat_last)
+    
+subsubsection {* Orders *}
+  
+text {* We now instantiate the ord class for the stlist type. *}
+  
+instantiation stlist :: (monoid_add) ord
+begin
+  definition less_eq_stlist :: "'a stlist \<Rightarrow> 'a stlist \<Rightarrow> bool" where "less_eq_stlist == monoid_le"
+  definition less_stlist :: "'a stlist \<Rightarrow> 'a stlist \<Rightarrow> bool" where "less_stlist x y == x \<le> y \<and> \<not> (y \<le> x)"
+
+  lemma stlist_plus_follow_concat:
+  fixes a c :: "'a stlist"
+  shows "a + (b #\<^sub>t c) = a + [b;0] + c"
+  by (metis concat_stlist.simps(3) plus_seq_assoc plus_stlist_def stlist_concat_zero_left)  
+    
+  instance by (intro_classes)
+end
+  
+lemma monoid_le_stlist2:
+  "(xs :: 'a::monoid_add stlist) \<le>\<^sub>m ys \<longleftrightarrow> xs \<le> ys"
+  by (simp add: less_eq_stlist_def)
+
+lemma stlist_right_cancel_monoid2:
+  "(b#\<^sub>ta) = (c#\<^sub>ta) \<longleftrightarrow> b = c"  
+  by auto
+    
+subsubsection {* Left Cancelative Monoid *}
+  
+text {* We now instantiate the left_cancel_monoid class for the stlist type. *}
+
+instantiation stlist :: (left_cancel_monoid) left_cancel_monoid
+begin
+  
+lemma stlist_left_zero_cancel:
+  fixes a :: "'a stlist"
+  shows "a + [;b] = a + [;c] \<Longrightarrow> [;b] = [;c]"
+  unfolding plus_stlist_def
+  apply (induct a)
+  apply auto
+  using left_cancel_monoid_class.add_left_imp_eq by blast
+   
+lemma stlist_left_cancel_monoid0:
+  fixes b c :: "'a stlist"
+  shows "[;a] + b = [;a] + c \<Longrightarrow> b = c"
+  unfolding plus_stlist_def
+  apply (induct rule:stlist_induct_cons)
+  apply auto
+  using left_cancel_monoid_class.add_left_imp_eq by blast+
+    
+lemma stlist_left_cancel_monoid:
+  fixes a b c :: "'a stlist"
+  shows "a + b = a + c \<Longrightarrow> b = c"
+  apply (induct a rule:stlist.induct)
+  using Terminated_lists.stlist_left_cancel_monoid0 apply blast
+  by (simp add: plus_stlist_def)
+
+instance apply (intro_classes)
+  using stlist_left_cancel_monoid by blast+
+end
+  
+subsubsection {* Right Cancelative Monoid *}
+  
+text {* We now instantiate the right_cancel_monoid class for the stlist type. *}  
+  
+instantiation stlist :: (right_cancel_monoid) right_cancel_monoid
+begin
+
+lemma stlist_right_cancel_monoid0:
+  fixes b c :: "'a stlist"
+  shows "(b + [;a] = c + [;a]) \<Longrightarrow> b = c"
+  unfolding plus_stlist_def
+  apply (induct b c rule:stlist_induct_cons, auto)
+  using right_cancel_monoid_class.add_right_imp_eq by blast
+    
+lemma stlist_right_cancel_monoid1:
+  fixes b c :: "'a stlist"
+  shows "(b + [a;d] = c + [a;d]) \<Longrightarrow> b = c"
+  unfolding plus_stlist_def
+  apply (induct b c rule:stlist_induct_cons, auto)
+  using right_cancel_monoid_class.add_right_imp_eq apply blast
+  apply (case_tac "xs", simp+)
+  by (case_tac "ys", simp+)
+    
+lemma stlist_right_cancel_monoid:
+  fixes b c :: "'a stlist"
+  shows "b+a = c+a \<Longrightarrow> b = c"
+  apply (induct a arbitrary: b c rule:stlist.induct)
+  using stlist_right_cancel_monoid0 apply blast 
+  by (metis (no_types, lifting) add.assoc concat_stlist.simps(3) plus_stlist_def stlist_concat_zero_left stlist_right_cancel_monoid1 zero_stlist_def)
+
+instance by (intro_classes, simp add:stlist_right_cancel_monoid)
+end
+  
+subsubsection {* Monoid Sum *}    
+  
+instantiation stlist :: (monoid_sum_0) monoid_sum_0
+begin
+    
+lemma stlist_zero_monoid_sum:
+  fixes a :: "'a stlist"
+  shows "a + b = 0 \<Longrightarrow> a = 0"
+  apply (induct a b rule:stlist_induct_cons)
+  by (simp add: plus_stlist_def zero_stlist_def zero_sum_left)+ 
+    
+instance
+  apply (intro_classes)
+  using  stlist_zero_monoid_sum  by blast+
+end
+  
+subsubsection {* Difference *}
+  
+instantiation stlist :: (monoid_add) minus
+begin
+  definition minus_stlist :: "'a stlist \<Rightarrow> 'a stlist \<Rightarrow> 'a stlist" where "minus_stlist == monoid_subtract"
+  
+  instance by intro_classes
+end  
+  
+subsubsection {* Pre trace *}
+
+instantiation stlist :: (pre_trace) pre_trace
+begin
+  
+lemma stlist_eq_sum_conv_nils:
+  fixes a :: "'a::pre_trace"
+  assumes "[;a] + [;b] = [;c] + [;d]"
+  shows "\<exists> e . [;a] = [;c] + e \<and> e + [;b] = [;d] \<or> [;a] + e = [;c] \<and> [;b] = e + [;d]"
+proof -
+ 
+  have a: "([;a] + [;b] = [;c] + [;d]) = (a + b = c + d)"
+    by (metis stlist_plus_nils)
+      
+  have b: "(a + b = c + d) \<Longrightarrow> \<exists> e . a = c + e \<and> e + b = d \<or> a + e = c \<and> b = e + d"
+    by (simp add: sum_eq_sum_conv)
+  
+  then have "(a + b = c + d) \<Longrightarrow> \<exists> e . [;a] = [;c] + e \<and> e + [;b] = [;d] \<or> [;a] + e = [;c] \<and> [;b] = e + [;d]"   
+    by (metis stlist_plus_nils)
+    
+  with a b show ?thesis using assms by simp
+qed
+  
+lemma stlist_eq_sum_conv_nils1:
+  fixes a :: "'a::pre_trace stlist"
+  assumes "a + [;b] = c + [;d]"
+  shows "\<exists> e . a = c + e \<and> e + [;b] = [;d] \<or> a + e = c \<and> [;b] = e + [;d]"
+  using assms
+  apply (induct a c rule:stlist_induct_cons)
+  apply (simp add: stlist_eq_sum_conv_nils)
+  by (simp_all add: plus_stlist_def)
+    
+text {* The next lemma is key to prove the required induction
+        in the following lemma stlist_sum_eq_sum_conv. *}
+    
+lemma stlist_eq_sum_conv_nils2:
+  fixes a :: "'a::pre_trace"
+  assumes "[;a] + b = [;c] + d"
+  shows "\<exists> e . [;a] = [;c] + e \<and> e + b = d \<or> [;a] + e = [;c] \<and> b = e + d"
+  using assms
+  proof (induct b d arbitrary: a c rule:stlist_induct_cons)
+    case (1 a b)
+    then show ?case by (simp add: stlist_eq_sum_conv_nils)
+  next
+    case (2 a x xs)
+    then show ?case by (simp add: plus_stlist_def)
+  next
+    case (3 a y ys)
+    then show ?case by (simp add: plus_stlist_def)
+  next
+    case (4 x xs y ys)
+    have a:"([;a] + (x #\<^sub>t xs) = [;c] + (y #\<^sub>t ys))
+         =
+         (((a + x) #\<^sub>t xs) = ((c + y) #\<^sub>t ys))"
+      by (simp add: stlist_nil_concat_cons)
+    
+    hence eq1:"a + x = c + y"
+      using "4.prems" by blast
+      
+    hence eq2:"xs=ys"
+      using "4.prems" a by blast
+    
+    from eq1 have "\<exists>e. a = c + e \<and> e + x = y \<or> a + e = c \<and> x = e + y"
+      by (simp add: sum_eq_sum_conv)
+        
+    then have "\<exists>e. [;a] = [;c] + e \<and> e + [;x] = [;y] \<or> [;a] + e = [;c] \<and> [;x] = e + [;y]"
+      by (metis stlist_plus_nils)
+        
+    hence "\<exists>e z. [;z] = e \<and> ([;a] = [;c] + e \<and> e + [;x] = [;y] \<or> [;a] + e = [;c] \<and> [;x] = e + [;y])"
+      by (metis stlist_eq_nil_pluses_imp0)
+    
+    hence "\<exists>e z. [;z] = e \<and> ([;a] = [;c] + e \<and> [;z] + (x#\<^sub>txs) = (y#\<^sub>tys) \<or> [;a] + e = [;c] \<and> [;x] = [;z + y])"    
+      using eq2 by (metis (no_types, lifting) "4.prems" concat_stlist.simps(1) plus_seq_assoc plus_stlist_def stlist_left_cancel_monoid0) 
+    
+    hence "\<exists>e z. [;z] = e \<and> ([;a] = [;c] + e \<and> [;z] + (x#\<^sub>txs) = (y#\<^sub>tys) \<or> [;a] + e = [;c] \<and> (x#\<^sub>txs) = [;z] + (y#\<^sub>tys))"
+      using eq2 by (metis (no_types, lifting) "4.prems" concat_stlist.simps(1) plus_seq_assoc plus_stlist_def stlist_left_cancel_monoid0) 
+    
+    hence eq3:"\<exists>e. [;a] = [;c] + e \<and> e + (x#\<^sub>txs) = (y#\<^sub>tys) \<or> [;a] + e = [;c] \<and> (x#\<^sub>txs) = e + (y#\<^sub>tys)"
+      by auto
+        
+    then show ?case by auto   
+qed
+  
+lemma stlist_sum_eq_sum_conv:
+  fixes a :: "'a stlist"
+  shows "(a + b) = (c + d) \<Longrightarrow> \<exists> e . a = c + e \<and> e + b = d \<or> a + e = c \<and> b = e + d"  
+  apply (induct a c rule:stlist_induct_cons)
+  apply (simp add:stlist_eq_sum_conv_nils2)+ 
+  apply (case_tac d)
+  apply (simp add: plus_stlist_def)
+  apply (metis concat_stlist.simps(3) plus_stlist_def stlist_cons_plus_nils_eq_cons)
+  apply (case_tac b)
+  apply (simp add: plus_stlist_def)
+  apply (metis concat_stlist.simps(3) plus_stlist_def stlist_cons_plus_nils_eq_cons)
+  by (simp add: plus_stlist_def)  
+  
+instance by (intro_classes, simp add:stlist_sum_eq_sum_conv)
+end
+
+subsubsection {* Trace *} 
+  
+text {* Given a type of class pre_trace we get a trace. This means that
+        for a given type, as long as we define an appropriate zero, and
+        plus operator, and it obeys the required monoid laws in addition
+        to sum_eq_sum_conv, then the resulting stlist is a trace. *}
+  
+instantiation stlist :: (pre_trace) trace
+begin
+
+instance by (intro_classes, simp_all add:less_eq_stlist_def less_stlist_def minus_stlist_def)
+end
+ 
+lemma monoid_plus_prefix_iff_zero:
+  fixes a b :: "'a::trace"
+  shows "a + x \<le> a \<longleftrightarrow> x = 0"
+  by (metis add.right_neutral antisym le_add left_cancel_monoid_class.add_left_imp_eq)
+    
+lemma stlist_le_nil_imp_le_elements:
+  fixes a b :: "'a::trace"
+  shows "[;a] \<le> [;b] \<Longrightarrow> a \<le> b"
+  apply (simp add: less_eq_stlist_def monoid_le_def)
+  apply auto
+  apply (case_tac c)
+  apply auto
+  apply (simp add: plus_stlist_def)
+  by (simp add: stlist_nil_concat_cons)
+    
+lemma stlist_le_elements_imp_stlist_le_nil:
+  fixes a b :: "'a::trace"
+  shows "a \<le> b \<Longrightarrow> [;a] \<le> [;b]"
+  apply (simp add: less_eq_stlist_def monoid_le_def le_is_monoid_le)
+  by (metis concat_stlist.simps(1) plus_stlist_def)
+    
+lemma stlist_le_nil_iff_le_elements:
+  fixes a b :: "'a::trace"
+  shows "[;a] \<le> [;b] \<longleftrightarrow> a \<le> b"
+  apply auto
+  apply (simp add: stlist_le_nil_imp_le_elements)
+  by (simp add:stlist_le_elements_imp_stlist_le_nil)
+    
+lemma stlist_nil_le_cons_imp_le:
+  fixes xs :: "'a::trace stlist"
+  shows "[;a] \<le> (x#\<^sub>txs) \<Longrightarrow> a \<le> x"
+  apply (simp add:less_eq_stlist_def le_is_monoid_le monoid_le_def)
+  apply auto
+  apply (case_tac c)
+  apply (simp add: plus_stlist_def)
+  by (metis stlist.inject(2) stlist_nil_concat_cons)
+    
+lemma monoid_le_stlist:
+  fixes a :: "'a::monoid_add stlist"
+  shows "a \<le> b \<longleftrightarrow> a \<le>\<^sub>m b"
+  by (simp add:le_is_monoid_le less_eq_stlist_def)
+
+lemma monoid_subtract_stlist: 
+  fixes a :: "'a::monoid_add stlist"
+  shows "(a - b) = (a -\<^sub>m b)"
+  by (simp add:minus_def minus_stlist_def) 
+    
+lemma stlist_minus_nils_imp_minus:
+  fixes a b :: "'a::trace"
+  shows "[;a] - [;b] = [;c] \<Longrightarrow> a - b = c"
+  unfolding minus_stlist_def minus_def
+proof - (* massaged from an smt Isar proof *)
+  assume a1: "[;a] -\<^sub>m [;b] = [;c]"
+  { assume "a -\<^sub>m b \<noteq> c"
+    { assume "[;c] \<noteq> [;a] - [;b]"
+      then have "[;c] \<noteq> [;b] + ([;a] - [;b]) - [;b]"
+        by simp
+      then have "([;b] + [;a] - [;b]) \<noteq> [;a]"
+        by (simp add: a1 minus_stlist_def)
+      then have "[;a] \<noteq> [;b] + [;a] - [;b]"
+        by (auto) }
+    then have "a -\<^sub>m b = c"
+      using a1 by (metis (no_types) Terminated_lists.last.simps(1) add_monoid_diff_cancel_left monoid_le_def monoid_subtract_def stlist_plus_nils zero_stlist_def) }
+  then show "a -\<^sub>m b = c"
+    by meson
+qed
+  
+lemma stlist_minus_imp_minus_nils:
+  fixes a b :: "'a::trace"
+  shows "a - b = c \<Longrightarrow> [;a] - [;b] = [;c]"
+  unfolding minus_stlist_def minus_def
+proof - (* massaged from an smt Isar proof *)
+  assume a1: "a -\<^sub>m b = c"
+  obtain aa :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+      f2: "\<forall>x0 x1. (\<exists>v2. x0 = x1 + v2) = (x0 = x1 + aa x0 x1)"
+    by moura
+  obtain aas :: "'a stlist \<Rightarrow> 'a stlist \<Rightarrow> 'a stlist" where
+    f3: "\<forall>x0 x1. (\<exists>v2. x0 = x1 + v2) = (x0 = x1 + aas x0 x1)"
+    by moura
+  have f4: "[;b] + [;aa a b] = [;b + aa a b]"
+    by (meson stlist_plus_nils)
+  obtain aaa :: "'a stlist \<Rightarrow> 'a" where
+    "\<forall>x0. (\<exists>v3. x0 = [;v3]) = (x0 = [;aaa x0])"
+    by moura
+  then have "[;a] = [;b] + aas [;a] [;b] \<longrightarrow> [;a] -\<^sub>m [;b] = [;c]"
+    using f4 a1 by (metis add_monoid_diff_cancel_left stlist_eq_nil_pluses_imp0 stlist_plus_nils)
+  then show "[;a] -\<^sub>m [;b] = [;c]"
+    using f4 f3 f2 a1 by (metis (no_types) monoid_le_def monoid_subtract_def zero_stlist_def)
+qed
+
+lemma stlist_minus_eq_minus_nils:
+  fixes a b :: "'a::trace"
+  shows "a - b = c \<longleftrightarrow> [;a] - [;b] = [;c]"  
+  by (metis stlist_minus_nils_imp_minus stlist_minus_imp_minus_nils)
+    
+lemma
+  fixes a :: "'a::{trace,right_cancel_monoid}"
+  shows "a = e + a \<longleftrightarrow> e = 0"
+  by (metis add.assoc add.right_neutral left_cancel_monoid_class.add_left_imp_eq right_cancel_monoid_class.add_right_imp_eq)
+    
+lemma stlist_cons_minus_nil_eq:
+  fixes xs :: "'a::trace stlist"
+  assumes "[;a] \<le> (x#\<^sub>txs)"
+  shows "(x#\<^sub>txs) - [;a] = (x-a)#\<^sub>txs" 
+  using assms
+  apply (simp add:minus_stlist_def minus_def le_is_monoid_le less_eq_stlist_def)
+  using stlist_nil_le_cons_imp_le
+  by (metis add_monoid_diff_cancel_left le_is_monoid_le monoid_le_def stlist_nil_concat_cons)
+    
+lemma
+  fixes a :: "'a::trace"
+  shows "[;a] - [;a] = [;a - a]"
+  apply (simp_all only:diff_cancel)
+  by (simp add: zero_stlist_def)
+    
+lemma
+  fixes a :: "'a::trace"
+  shows "[;a] - [;b] = [;a - b]"
+  using stlist_minus_eq_minus_nils by blast
+    
+lemma stlist_le_sum_cases:
+fixes a :: "'a::pre_trace stlist"
+shows "a \<le> b + c \<Longrightarrow> a \<le> b \<or> b \<le> a"
+by (metis less_eq_stlist_def monoid_le_def stlist_sum_eq_sum_conv)
+    
+lemma stlist_nil_minus:
+  fixes a b :: "'a::trace"
+  shows "[;b] - [;a] = [;b-a]"
+  apply (case_tac "a \<le> b")
+  apply auto
+  apply (simp add:minus_stlist_def)
+  apply (metis add_monoid_diff_cancel_left concat_stlist.simps(1) diff_add_cancel_left' plus_stlist_def)
+  apply (simp add:stlist_le_nil_iff_le_elements)
+  by (simp add:zero_stlist_def)
+
+(* assorted lemmas below *)
+  
+lemma stlist_cons_right_prefix:
+  fixes a :: "'a::pre_trace"
+  shows "[;a] \<le> [a;c]"
+proof -
+  have "[;a] \<le> [a;c] = ([;a] \<le> [;a] + [0;c])"
+    unfolding less_eq_stlist_def monoid_le_def plus_stlist_def by simp
+  also have "... = True"
+    by simp
+      
+  finally show ?thesis by simp
+qed
+  
+(* this yields the difA of CTA nicely *)    
+    
+lemma stlist_cons_minus_zero_left:
+  fixes a :: "'a::pre_trace"
+  shows "[a;c] - [;a] = [0;c]"      
+proof -
+  have "[a;c] - [;a] = [;a] + [0;c] - [;a]"
+    unfolding plus_stlist_def minus_stlist_def monoid_subtract_def by simp
+  also have "[;a] + [0;c] - [;a] = [0;c]"
+    by simp
+      
+  finally show ?thesis by simp
+qed
+
+end
\ No newline at end of file
diff --git a/utils/utp_imports.thy b/utils/utp_imports.thy
index c82614a3b..dec5f242b 100644
--- a/utils/utp_imports.thy
+++ b/utils/utp_imports.thy
@@ -24,9 +24,10 @@ imports
   "Library_extra/FSet_extra"
   "Library_extra/List_extra"
   "Library_extra/List_lexord_alt"
+  "Library_extra/Terminated_lists" 
   "Library_extra/Monoid_extra"
   "Library_extra/Pfun"
   "Library_extra/Ffun"
   Profiling
   TotalRecall
-begin end
\ No newline at end of file
+begin end