header {* Representing a state in TLA*  *}

theory State
imports Liveness
begin

typedecl state

instance state :: world ..

types
  'a statefun = "(state,'a) stfun"
  statepred  = "bool statefun"
  'a tempfun = "(state,'a) formfun"
  temporal = "state formula"

consts
  (* Formalizing type "state" would require formulas to be tagged with
     their underlying state space and would result in a system that is
     much harder to use. (Unlike Hoare logic or Unity, TLA has quantification
     over state variables, and therefore one usually works with different
     state spaces within a single specification.) Instead, "state" is just
     an anonymous type whose only purpose is to provide "Skolem" constants.
     Moreover, we do not define a type of state variables separate from that
     of arbitrary state functions, again in order to simplify the definition
     of flexible quantification later on. Nevertheless, we need to distinguish
     state variables, mainly to define the enabledness of actions. The user
     identifies (tuples of) "base" state variables in a specification via the
     "meta predicate" basevars, which is defined here.
  *)
  stvars    :: "'a statefun => bool"

syntax
  "PRED"    :: "lift => 'a"                          ("PRED _")
  "_stvars" :: "lift => bool"                        ("basevars _")

translations
  "PRED P"   =>  "(P::state => _)"
  "_stvars"  ==  "stvars"

defs
  (* Base variables may be assigned arbitrary (type-correct) values.
     Note that vs may be a tuple of variables. The correct identification
     of base variables is up to the user who must take care not to
     introduce an inconsistency. For example, "basevars (x,x)" would
     definitely be inconsistent.
  *)
  basevars_def:  "stvars vs \<equiv> range vs = UNIV"


lemma basevars: "\<And> vs. basevars vs \<Longrightarrow> \<exists> u. vs u = c" 
proof -
  fix vs :: "state \<Rightarrow> 'a"
  assume H1: "basevars vs"
  from H1 have "range vs = UNIV" by (unfold basevars_def)
  from this show "\<exists> u. vs u = c"
  proof (rule_tac b=c and f=vs in rangeE)
    assume "range vs = UNIV"
    from this show "c \<in> range vs" by simp
  next
    fix x
    assume a1:"range vs = UNIV" and
           a2: "c = vs x"
    from a2 have "vs x = c" by blast
    thus "\<exists>u. vs u = c" by (auto simp add: exI)
   qed
qed

ML "set show_types"

lemma basevars_range: "\<And> vs. range vs = UNIV \<Longrightarrow> \<exists> u. vs u = c" 
proof -
  fix vs :: "'a \<Rightarrow> 'b"
  assume H1: "range vs = UNIV"
  from H1 show "\<exists> u. vs u = c"
  proof (rule_tac b=c and f=vs in rangeE)
    assume "range vs = UNIV"
    from this show "c \<in> range vs" by simp
  next
    fix x
    assume a1:"range vs = UNIV" and
           a2: "c = vs x"
    from a2 have "vs x = c" by blast
    thus "\<exists>u. vs u = c" by (auto simp add: exI)
   qed
qed

(* lemma used in base_pair1 :: FIX ME: should encorporate it *)
lemma bpair1: "\<And>(x \<Colon> state  \<Rightarrow> 'b) y \<Colon> state \<Rightarrow> 'c. range (LIFT(x, y)) = UNIV \<Longrightarrow> UNIV \<subseteq> range x"
proof (rule subsetI)
 fix x :: "state \<Rightarrow> 'b"
 fix y :: "state \<Rightarrow> 'c"
 fix xa :: "'b"
 assume a2: "range (LIFT(x,y))=UNIV"
 from a2 have g1: "\<exists> u. (LIFT(x, y)) u = (xa, arbitrary)"
                      by (drule_tac c="(xa,arbitrary)" in basevars_range)
 from g1 show "xa \<in> range x" by auto
qed

lemma base_pair1: "basevars (x,y) \<Longrightarrow> basevars x "
proof -
   fix x :: "state \<Rightarrow> 'a"
   fix y :: "state \<Rightarrow> 'b"
   assume H1: "basevars (x,y)"
   from H1  have H2: "range (LIFT(x, y)) = UNIV" by (unfold basevars_def)
   have S1: "range x \<subseteq> UNIV"  by  (rule subset_UNIV)
   moreover
   from H2 have S2: "UNIV \<subseteq> range x" by (rule bpair1) (* FIXME: replace with proof (bpair1) - doesn't work *)
   ultimately have "range x = UNIV" by (rule equalityI)
   thus "basevars x" by (unfold basevars_def)   
qed

lemma bpair2: "\<And>(x \<Colon> state \<Rightarrow> 'a) y \<Colon> state \<Rightarrow> 'b. range (LIFT(x, y)) = UNIV \<Longrightarrow> UNIV \<subseteq> range y"
proof (rule subsetI)
 fix x :: "state \<Rightarrow> 'a"
 fix y :: "state \<Rightarrow> 'b"
 fix xa :: "'b"
 assume a2: "range (LIFT(x,y))=UNIV"
 from a2 have g1: "\<exists> u. (LIFT(x, y)) u = (arbitrary,xa)"
                      by (drule_tac c="(arbitrary,xa)" in basevars_range)
 from this obtain u where "(LIFT(x, y)) u = (arbitrary,xa)" ..
 thus "xa \<in> range y" by auto
qed

lemma base_pair2: "basevars (x,y) \<Longrightarrow> basevars y"
proof -
 fix x :: "state \<Rightarrow> 'a"
 fix y :: "state \<Rightarrow> 'b"
 assume H1: "basevars (x,y)"
 from H1  have H2: "range (LIFT(x, y)) = UNIV" by (unfold basevars_def)
   have S1: "range y \<subseteq> UNIV"  by  (rule subset_UNIV)
 moreover
   from H2 have S2: "UNIV \<subseteq> range y" by (rule bpair2) (* FIXME: replace with proof - doesn't work *)
 ultimately have "range y = UNIV" by (rule equalityI)
 thus "basevars y" by (unfold basevars_def)   
qed

lemma base_pair: "basevars (x,y) \<Longrightarrow> basevars x \<and> basevars y"
proof -
 fix x :: "state \<Rightarrow> 'a"
 fix y :: "state \<Rightarrow> 'b"
 assume H1: "basevars (x,y)" show "basevars x \<and> basevars y"
 proof (rule conjI)
   from H1 show "basevars x" by (rule base_pair1)
 next
   from H1 show "basevars y" by (rule base_pair2)
 qed
qed

lemma base_pair: "\<And> x y. basevars (x,y) \<Longrightarrow> basevars x \<and> basevars y"
proof -
 fix x :: "state \<Rightarrow> 'a"
 fix y :: "state \<Rightarrow> 'b"
 assume H1: "basevars (x,y)" show "basevars x \<and> basevars y"
 proof (rule conjI)
   from H1 show "basevars x" by (rule base_pair1)
 next
   from H1 show "basevars y" by (rule base_pair2)
 qed
qed

text{* 
Since the @{typ unit} type has just one value, any state function can be
regarded as @{term base}. The following axiom can sometimes be useful
because it gives a trivial solution for @{text basevars} premises.
*}

lemma unit_base: "basevars (v::state \<Rightarrow> unit)"
proof -
  have "range v = UNIV \<longrightarrow> basevars (v::state \<Rightarrow> unit)"
    by (auto simp add: basevars_def)
  thus ?thesis by auto
qed

lemma baseE: assumes H1: "basevars v" and H2:"\<And> x. v x = c \<Longrightarrow> Q"
              shows  "Q"
proof -
  from H1 have "\<exists> u. v u = c" by (rule basevars)
  from this obtain u where "v u = c" ..
  with H2 show "Q" by auto
qed

lemma  fixes x :: "state \<Rightarrow> bool"
      assumes h1: "basevars (x,x)"
       shows      "False"
proof -
  thm "basevars"
  from h1 have "\<exists> u. (LIFT (x,x)) u = (False,True)"
    by (rule basevars)
  thus False by auto
qed

(* Cannot prove for type variable !! *)

lemma  fixes x :: "state \<Rightarrow> nat"
      assumes h1: "basevars (x,x)"
       shows      "False"
proof -
  thm "basevars"
  from h1 have "\<exists> u. (LIFT (x,x)) u = (0,1)"
    by (rule basevars)
  thus False by auto
qed

lemma first_baseE: assumes H1: "basevars v" and H2: "\<And> x. v (first x) = c \<Longrightarrow> Q"
              shows  "Q"
proof -
  from H2 have H2': "\<And> x. v (x (0::nat)) = c \<Longrightarrow> Q" 
    by (simp add: first_def)
  from H1 have "\<exists> u. v u = c" by (rule basevars)
  from this obtain u where "v u = c" ..
  with H2' show "Q" by auto
qed

lemma base_enabled:
  assumes h1: "basevars vs"
  and h2: "\<exists> c. \<forall> u. vs (first u) = c \<longrightarrow> (((first s) ## u) \<Turnstile> F )"
  shows "s \<Turnstile> Enabled F"
proof (unfold enabled_def)
  from h2 obtain c where g1: "\<forall> u. vs (first u) = c \<longrightarrow> (((first s) ## u) \<Turnstile> F)" ..
  from h1 have "\<exists> u. vs u = c" by (rule basevars)
  from this obtain u where "vs u = c" ..
  hence "\<exists> k. vs (k (0::nat)) = c" by auto
  then obtain k where "vs (k (0::nat)) = c" ..
  hence g2: "vs (first k) = c" by (simp add: first_def)
  from g1 have "vs (first k) = c \<longrightarrow> (((first s) ## k) \<Turnstile> F)" ..
  with g2 have "(((first s) ## k) \<Turnstile> F)" by auto
  thus "\<exists> k. ((first s) ## k) \<Turnstile> F" by blast
qed

section "Temporal Quantifiers"

consts
  EEx        :: "('a statefun \<Rightarrow> temporal) \<Rightarrow> temporal"       (binder "Eex " 10)
  AAll       :: "('a statefun \<Rightarrow> temporal) \<Rightarrow> temporal"       (binder "Aall " 10)

syntax
 "_EEx"     :: "[idts, lift] \<Rightarrow> lift"                ("(3EEX _./ _)" [0,10] 10)
  "_AAll"    :: "[idts, lift] \<Rightarrow> lift"                ("(3AALL _./ _)" [0,10] 10)

translations
  "_EEx v A"  ==   "Eex v. A"
  "_AAll v A" ==   "Aall v. A"

syntax (xsymbols)
  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)

axioms 
  eexI: "\<turnstile> F x \<longrightarrow> (\<exists>\<exists> x. F x)"
  eexE: "\<lbrakk>s \<Turnstile> (\<exists>\<exists> x. F x) ; basevars vs; (!! x. \<lbrakk> basevars (x,vs); s \<Turnstile> F x \<rbrakk> \<Longrightarrow> s \<Turnstile> G)\<rbrakk> \<Longrightarrow> (s \<Turnstile> G)" 
  eexSTUT: "STUTINV F x \<Longrightarrow> STUTINV (\<exists>\<exists> x. F x)"
  history: "\<turnstile> (I \<and> \<box>[A]_v) = (\<exists>\<exists> h. ($h = ha) \<and> I \<and> \<box>[A \<and> h$=hb]_(h,v))"


end