Theory Prefix

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

theory Prefix = Trace:

(*  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]

(*********************************************************)

consts
  prefix         :: "'a trace => 'a trace => bool"
  prefix_closed  :: "('a trace set) => bool"

defs
  prefix_def        : "prefix s t == (EX u. t = s @t u)"
  prefix_closed_def : 
    "prefix_closed T == ALL s t. ((t : T & prefix s t) --> s : T)"

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

lemma prefix_closed_iff:
  "[| t : T ; prefix s t ; prefix_closed T |] ==> s : T"
apply (unfold prefix_closed_def[of T])
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
by (simp)

(*** Prefix itself ***)

lemma prefix_itself[simp]: "prefix s s"
apply (simp add: prefix_def)
apply (rule_tac x="[]t" in exI)
by (simp)

(*** Prefix appt ***)

lemma prefix_appt_simp[simp]: "prefix s (s @t t)"
apply (simp add: prefix_def)
apply (rule_tac x="t" in exI)
by (simp)

lemma prefix_appt: "prefix s t ==> prefix s (t @t u)"
apply (simp add: prefix_def)
apply (erule exE)
apply (simp)
apply (rule_tac x="ua @t u" in exI)
by (simp)

(*** []t is a prefix of any trace ***)

lemma nil_is_prefix[simp]: "prefix []t s"
by (simp add: prefix_def)

(*** the prefix of []t is []t ***)

lemma prefix_of_nil[simp]: "prefix s []t = (s = []t)"
by (simp add: prefix_def)

(*** prefix of [a]t ***)

lemma prefix_of_one[simp]: "prefix s [a]t = (s = []t | s = [a]t)"
by (auto simp add: prefix_def)

(*** not None ***)

lemma prefix_not_None : "[| t ~= None ; prefix s t |] ==> s ~= None"
apply (simp add: prefix_def)
apply (erule exE)
by (simp add: decompo_appt_None)

(*** None ***)

lemma prefix_None1[simp] : "prefix None t = (t = None)"
by (simp add: prefix_def)

lemma prefix_None2[simp] : "prefix s None"
apply (simp add: prefix_def)
by (rule_tac x="None" in exI, simp)

(*** length of prefix ***)

lemma length_of_prefix:
  "[| t ~= None ; prefix s t |] ==> lengtht s <= lengtht t"
apply (case_tac "s ~= None")
apply (simp add: prefix_def)
apply (erule exE)
apply (simp)
by (simp)

(*** prefix closed & prefix ***)

lemma prefix_closed_prop:
  "[| prefix_closed T ; t : T ; prefix s t |] ==> s : T"
apply (unfold prefix_closed_def)
by (blast)

(***********************************************************
                   convenient lemmas
 ***********************************************************)

(*** prefix a#v u ***)

lemma prefix_same_head_only_if:
  "prefix ([a]t @t v) u 
    ==> (EX u'. u = [a]t @t u' & prefix v u')"
apply (simp add: prefix_def)
apply (erule exE)
apply (rule_tac x="v @t ua" in exI, simp)
by (rule_tac x="ua" in exI, simp)

lemma prefix_same_head_if:
  "(EX u'. u = [a]t @t u' & prefix v u')
   ==> prefix ([a]t @t v) u"
apply (simp add: prefix_def)
apply (elim conjE exE)
apply (rule_tac x="ua" in exI)
by (simp)

lemma prefix_same_head[simp]:
  "prefix ([a]t @t v) u 
    = (EX u'. u = [a]t @t u' & prefix v u')"
apply (rule iffI)
apply (simp add: prefix_same_head_only_if)
apply (simp add: prefix_same_head_if)
done

(*** prefix v a#u ***)

lemma prefix_same_head_inv_only_if:
  "prefix v ([Ev a]t @t u)
      ==> u = None | v = []t | (EX v'. v = [Ev a]t @t v' & prefix v' u)"
apply (case_tac "u = None", simp)
apply (simp add: prefix_def)
apply (erule exE)

apply (case_tac "v = None", simp)

apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="v" in spec, simp)
apply (erule disjE, simp)
apply (erule disjE, simp)
apply (elim exE)
apply (simp)
by (rule_tac x="ua" in exI, simp)

lemma prefix_same_head_inv_if:
  "[| u = None | v = []t | (EX v'. v = [Ev a]t @t v' & prefix v' u) |]
      ==> prefix v ([Ev a]t @t u)"
apply (erule disjE)
apply (simp)
apply (erule disjE, simp)
apply (elim conjE exE)
by (auto simp add: prefix_def)

lemma prefix_same_head_inv[simp]:
  "prefix v ([Ev a]t @t u) =
   (u = None | v = []t | (EX v'. v = [Ev a]t @t v' & prefix v' u))"
apply (rule iffI)
apply (simp add: prefix_same_head_inv_only_if)
apply (simp add: prefix_same_head_inv_if)
done

(*** prefix v u#a ***)

(* only if *)

lemma prefix_last_inv_only_if:
  "prefix v (u @t [e]t) ==> (~ notick u | v = u @t [e]t | prefix v u)"
apply (case_tac "~ notick u", simp)

apply (simp add: prefix_def)
apply (erule exE)

apply (case_tac "v @t ua = None")
apply (simp add: decompo_appt_None)

apply (simp add: decompo_appt_not_None)
apply (elim conjE)

apply (insert trace_last_nil_or_unnil)
apply (drule_tac x="ua" in spec, simp)

apply (case_tac "ua ~= []t", simp)
apply (elim conjE exE)
apply (rule disjI2)
apply (simp add: appt_ass_rev del: appt_ass)
apply (rule_tac x="s" in exI, simp)

by (simp)

(* if *)

lemma prefix_last_inv_if:
  "(~ notick u | v = u @t [e]t | prefix v u) ==> prefix v (u @t [e]t)"
apply (erule disjE)
apply (simp add: prefix_def)
apply (rule_tac x="None" in exI, simp)

apply (erule disjE, simp)
by (auto simp add: prefix_def)

lemma prefix_last_inv[simp]:
  "prefix v (u @t [e]t) = (~ notick u | v = u @t [e]t | prefix v u)"
apply (rule iffI)
apply (simp add: prefix_last_inv_only_if)
apply (simp add: prefix_last_inv_if)
done

(*-------------------------*
 |          sett           |
 *-------------------------*)

lemma prefix_subsett: "[| prefix s t ; t ~= None |] ==> sett s <= sett t"
apply (simp add: prefix_def)
apply (erule exE)
by (auto)

lemma prefix_notick: "[| prefix s t ; notick t |] ==> notick s"
apply (case_tac "t = None", simp)
apply (simp add: notick_def)
apply (insert prefix_not_None[of t s], simp)
apply (simp add: prefix_def)
apply (erule exE)
by (simp)

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end