Theory Trace_seq

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               November 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Trace_seq = Prefix:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite (notick | t = []t)                 *)
(*                                                                     *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

(*****************************************************************

         1. 
         2. 
         3. 
         4. 

 *****************************************************************)

consts
  rmtick:: "'a trace => 'a trace"

defs
  rmtick_def : 
    "rmtick s == if (notick s | s = None) then s else butlastt s"

(***********************************************************
                        None
 ***********************************************************)

(*------------------*
 |     not None     |
 *------------------*)

lemma rmtick_not_None_only_if: "rmtick s ~= None ==> s ~= None"
apply (simp add: rmtick_def)
apply (erule contrapos_nn)
by (simp)

lemma rmtick_not_None_if: "s ~= None ==> rmtick s ~= None"
apply (simp add: rmtick_def)
by (simp add: batlastt_not_None)

lemma rmtick_not_None[simp]: "(rmtick s ~= None) = (s ~= None)"
apply (rule iffI)
apply (rule rmtick_not_None_only_if, simp)
by (simp add: rmtick_not_None_if)

lemma rmtick_not_None_sym[simp]: "(None ~= rmtick s) = (s ~= None)"
apply (insert rmtick_not_None[of s])
apply (drule sym)
by (auto simp del: rmtick_not_None)

(*------------------*
 |        None      |
 *------------------*)

lemma rmtick_None[simp]: "(rmtick s = None) = (s = None)"
apply (rule iffI)
apply (case_tac "s = None", simp)
apply (simp add: rmtick_not_None_if)
by (simp add: rmtick_def)

lemma rmtick_None_sym[simp]: "(None = rmtick s) = (s = None)"
apply (rule iffI)
apply (case_tac "s = None", simp)
apply (drule sym)
apply (simp add: rmtick_not_None_if)
by (simp add: rmtick_def)

lemma rmtick_None1[simp]: "(rmtick None = None)"
by (simp)

(***********************************************************
                  nil and tick
 ***********************************************************)

(*** notick s --> rmtick s ***)

lemma rmtick_nochange[simp]: "notick s ==> rmtick s = s"
by (simp add: rmtick_def)

(*** rmtick []t ***)

lemma rmtick_nil[simp]: "rmtick []t = []t"
by (simp add: rmtick_def)

(*** rmtick [Tick]t ***)

lemma rmtick_tick[simp]: "rmtick [Tick]t = []t"
by (simp add: rmtick_def)

(*** notick rmtick s ***)

lemma notick_rmtick[simp]: "s ~= None ==> notick (rmtick s)"
apply (case_tac "notick s")
apply (simp_all add: rmtick_def)
apply (simp add: notick_butlast)
done

(***********************************************************
                           appt
 ***********************************************************)

(*-------------------------*
 |       rmtick last       |
 *-------------------------*)

lemma rmtick_last_tick[simp]:
  "notick s ==> rmtick (s @t [Tick]t) = s"
apply (simp add: rmtick_def)
by (simp add: appt_not_None)

(*** notick butlast ***)

lemma rmtick_butlastt: 
  "~ notick s ==> rmtick s = butlastt s"
by (simp add: rmtick_def)

(*-------------------------*
 |   rmtick distribution   |
 *-------------------------*)

lemma rmtick_appt_dist[simp]:
  "notick s ==> rmtick (s @t t) = s @t (rmtick t)"
apply (case_tac "t = None", simp)
apply (insert trace_last_nil_or_unnil)
apply (drule_tac x="t" in spec, simp)
apply (erule disjE, simp)

apply (elim conjE exE, simp)
apply (insert event_tick_or_Ev)
apply (drule_tac x="a" in spec)

apply (erule disjE)   (* Tick *)
apply (simp add: add: appt_ass_rev del: appt_ass)

apply (erule exE)     (* Ev *)
apply (simp add: add: appt_ass_rev del: appt_ass)
done

(***********************************************************
                        prefix
 ***********************************************************)

(*** rmtick prefix ***)

(* only if *)

lemma rmtick_prefix_only_if:
  "prefix s (rmtick t) ==> (t = None) | (EX u. prefix u t & s = rmtick u)"
apply (case_tac "t = None", simp)

apply (insert trace_last_nil_or_unnil)
apply (drule_tac x="t" in spec, simp)
apply (erule disjE, simp)

apply (elim conjE exE, simp)
apply (insert event_tick_or_Ev)
apply (drule_tac x="a" in spec)

 apply (erule disjE)    (* Tick *)
 apply (rule_tac x="s" in exI)
 apply (simp add: prefix_notick)

 apply (erule exE)      (* Ev *)
 apply (simp)

  apply (erule disjE)    (* same length *)
  apply (rule_tac x="sa @t [Ev aa]t" in exI, simp)

  apply (rule_tac x="s" in exI)
  apply (simp add: prefix_notick)
done

(* if *)

lemma rmtick_prefix_if:
  "(t = None) | (EX u. prefix u t & s = rmtick u) ==> prefix s (rmtick t)"
apply (case_tac "t = None", simp, simp)

apply (elim conjE exE)
apply (simp)

apply (insert trace_last_nil_or_unnil)
apply (drule_tac x="t" in spec, simp)
apply (erule disjE, simp)
apply (elim conjE exE)
apply (simp)

 apply (erule disjE, simp)
 apply (case_tac "~ notick u")
 apply (simp add: prefix_notick)

 apply (insert event_tick_or_Ev)
 apply (drule_tac x="a" in spec)

  apply (erule disjE)    (* Tick *)
  apply (simp)

  apply (elim exE)       (* Ev *)
  apply (simp)
done

(* iff *)

lemma rmtick_prefix:
  "prefix s (rmtick t) = ((t = None) | (EX u. prefix u t & s = rmtick u))"
apply (rule iffI)
apply (simp add: rmtick_prefix_only_if)
apply (simp add: rmtick_prefix_if)
done

(*--------------*
 |   reverse    |
 *--------------*)

lemma rmtick_prefix_rev: "prefix s t ==> prefix (rmtick s) t"
apply (simp add: rmtick_def)
apply (intro impI)
apply (simp add: prefix_def)
apply (elim conjE exE)

apply (case_tac "t = None")
apply (rule_tac x="None" in exI, simp)

apply (simp add: decompo_appt_not_None)
apply (rule_tac x="[Tick]t" in exI)
by (simp add: tick_decompo)

lemma rmtick_prefix_rev_simp[simp]: "prefix (rmtick s) s"
by (simp add: rmtick_prefix_rev)

(****************** to add it again ******************)

declare disj_not1 [simp] 
declare not_None_eq [simp] 

end