src/HOL/TLA/Action.thy
changeset 60591 e0b77517f9a9
parent 60588 750c533459b1
child 60592 c9bd1d902f04
     1.1 --- a/src/HOL/TLA/Action.thy	Fri Jun 26 15:03:54 2015 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Fri Jun 26 15:55:44 2015 +0200
     1.3 @@ -53,10 +53,10 @@
     1.4    "_SqAct"           ==   "CONST SqAct"
     1.5    "_AnAct"           ==   "CONST AnAct"
     1.6    "_Enabled"         ==   "CONST enabled"
     1.7 -  "w |= [A]_v"       <=   "_SqAct A v w"
     1.8 -  "w |= <A>_v"       <=   "_AnAct A v w"
     1.9 -  "s |= Enabled A"   <=   "_Enabled A s"
    1.10 -  "w |= unchanged f" <=   "_unchanged f w"
    1.11 +  "w \<Turnstile> [A]_v"       <=   "_SqAct A v w"
    1.12 +  "w \<Turnstile> <A>_v"       <=   "_AnAct A v w"
    1.13 +  "s \<Turnstile> Enabled A"   <=   "_Enabled A s"
    1.14 +  "w \<Turnstile> unchanged f" <=   "_unchanged f w"
    1.15  
    1.16  axiomatization where
    1.17    unl_before:    "(ACT $v) (s,t) \<equiv> v s" and
    1.18 @@ -161,8 +161,8 @@
    1.19    done
    1.20  
    1.21  lemma square_simulation:
    1.22 -   "\<And>f. \<lbrakk> \<turnstile> unchanged f & \<not>B \<longrightarrow> unchanged g;
    1.23 -            \<turnstile> A & \<not>unchanged g \<longrightarrow> B
    1.24 +   "\<And>f. \<lbrakk> \<turnstile> unchanged f \<and> \<not>B \<longrightarrow> unchanged g;
    1.25 +            \<turnstile> A \<and> \<not>unchanged g \<longrightarrow> B
    1.26           \<rbrakk> \<Longrightarrow> \<turnstile> [A]_f \<longrightarrow> [B]_g"
    1.27    apply clarsimp
    1.28    apply (erule squareE)
    1.29 @@ -210,29 +210,29 @@
    1.30    apply (erule maj)
    1.31    done
    1.32  
    1.33 -lemma enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F | G)"
    1.34 +lemma enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F \<or> G)"
    1.35    by (auto elim!: enabled_mono)
    1.36  
    1.37 -lemma enabled_disj2: "\<turnstile> Enabled G \<longrightarrow> Enabled (F | G)"
    1.38 +lemma enabled_disj2: "\<turnstile> Enabled G \<longrightarrow> Enabled (F \<or> G)"
    1.39    by (auto elim!: enabled_mono)
    1.40  
    1.41 -lemma enabled_conj1: "\<turnstile> Enabled (F & G) \<longrightarrow> Enabled F"
    1.42 +lemma enabled_conj1: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled F"
    1.43    by (auto elim!: enabled_mono)
    1.44  
    1.45 -lemma enabled_conj2: "\<turnstile> Enabled (F & G) \<longrightarrow> Enabled G"
    1.46 +lemma enabled_conj2: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled G"
    1.47    by (auto elim!: enabled_mono)
    1.48  
    1.49  lemma enabled_conjE:
    1.50 -    "\<lbrakk> s \<Turnstile> Enabled (F & G); \<lbrakk> s \<Turnstile> Enabled F; s \<Turnstile> Enabled G \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
    1.51 +    "\<lbrakk> s \<Turnstile> Enabled (F \<and> G); \<lbrakk> s \<Turnstile> Enabled F; s \<Turnstile> Enabled G \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
    1.52    apply (frule enabled_conj1 [action_use])
    1.53    apply (drule enabled_conj2 [action_use])
    1.54    apply simp
    1.55    done
    1.56  
    1.57 -lemma enabled_disjD: "\<turnstile> Enabled (F | G) \<longrightarrow> Enabled F | Enabled G"
    1.58 +lemma enabled_disjD: "\<turnstile> Enabled (F \<or> G) \<longrightarrow> Enabled F \<or> Enabled G"
    1.59    by (auto simp add: enabled_def)
    1.60  
    1.61 -lemma enabled_disj: "\<turnstile> Enabled (F | G) = (Enabled F | Enabled G)"
    1.62 +lemma enabled_disj: "\<turnstile> Enabled (F \<or> G) = (Enabled F \<or> Enabled G)"
    1.63    apply clarsimp
    1.64    apply (rule iffI)
    1.65     apply (erule enabled_disjD [action_use])
    1.66 @@ -294,7 +294,7 @@
    1.67  
    1.68  lemma
    1.69    assumes "basevars (x,y,z)"
    1.70 -  shows "\<turnstile> x \<longrightarrow> Enabled ($x & (y$ = #False))"
    1.71 +  shows "\<turnstile> x \<longrightarrow> Enabled ($x \<and> (y$ = #False))"
    1.72    apply (enabled assms)
    1.73    apply auto
    1.74    done