# HG changeset patch
# User nipkow
# Date 1348228617 -7200
# Node ID 860b7c6bd913ded93d8606ae6b8e3787a7b54154
# Parent  2694d1615eefe43d314f9fb690a46bc354f51527
tuned names

diff -r 2694d1615eef -r 860b7c6bd913 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Fri Sep 21 13:39:30 2012 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Fri Sep 21 13:56:57 2012 +0200
@@ -275,16 +275,16 @@
 by(induct C arbitrary: S) (simp_all add: Let_def)
 
 
-abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"
-where "\<gamma>\<^isub>f == \<gamma>_fun \<gamma>"
+abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"
+where "\<gamma>\<^isub>s == \<gamma>_fun \<gamma>"
 
 abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
-where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
+where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>s"
 
 abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
 where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
 
-lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
+lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s Top = UNIV"
 by(simp add: Top_fun_def \<gamma>_fun_def)
 
 lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
@@ -292,23 +292,23 @@
 
 (* FIXME (maybe also le \<rightarrow> sqle?) *)
 
-lemma mono_gamma_f: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>f f1 \<subseteq> \<gamma>\<^isub>f f2"
+lemma mono_gamma_s: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
 by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
 
 lemma mono_gamma_o:
   "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
-by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_f)
+by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
 
 lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
 by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
 
 text{* Soundness: *}
 
-lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
+lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
 by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def)
 
 lemma in_gamma_update:
-  "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(S(x := a))"
+  "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))"
 by(simp add: \<gamma>_fun_def)
 
 lemma step_preserves_le:
diff -r 2694d1615eef -r 860b7c6bd913 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Fri Sep 21 13:39:30 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Fri Sep 21 13:56:57 2012 +0200
@@ -48,7 +48,7 @@
 "aval' (V x) S = fun S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
-lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> vars a \<subseteq> dom S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
+lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> vars a \<subseteq> dom S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
 by (induction a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def)
 
 end
@@ -81,7 +81,7 @@
 text{* Soundness: *}
 
 lemma in_gamma_update:
-  "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(update S x a)"
+  "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
 by(simp add: \<gamma>_st_def)
 
 theorem step_preserves_le:
diff -r 2694d1615eef -r 860b7c6bd913 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Fri Sep 21 13:39:30 2012 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Fri Sep 21 13:56:57 2012 +0200
@@ -119,7 +119,7 @@
   case N thus ?case by simp (metis test_num')
 next
   case (V x)
-  obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>o S`
+  obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>s S'" using `s : \<gamma>\<^isub>o S`
     by(auto simp: in_gamma_option_iff)
   moreover hence "s x : \<gamma> (fun S' x)"
     using V(1,2) by(simp add: \<gamma>_st_def L_st_def)
@@ -176,7 +176,7 @@
 subsubsection "Soundness"
 
 lemma in_gamma_update:
-  "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(update S x a)"
+  "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
 by(simp add: \<gamma>_st_def)
 
 theorem step_preserves_le:
diff -r 2694d1615eef -r 860b7c6bd913 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Fri Sep 21 13:39:30 2012 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Fri Sep 21 13:56:57 2012 +0200
@@ -184,16 +184,16 @@
 locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
 begin
 
-abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"
-where "\<gamma>\<^isub>f == \<gamma>_st \<gamma>"
+abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"
+where "\<gamma>\<^isub>s == \<gamma>_st \<gamma>"
 
 abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
-where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
+where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>s"
 
 abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
 where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
 
-lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f (top c) = UNIV"
+lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (top c) = UNIV"
 by(auto simp: top_st_def \<gamma>_st_def)
 
 lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
@@ -201,13 +201,13 @@
 
 (* FIXME (maybe also le \<rightarrow> sqle?) *)
 
-lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
 apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
 by (metis mono_gamma subsetD)
 
 lemma mono_gamma_o:
   "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
-by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_f)
+by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
 
 lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
 by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)