# HG changeset patch
# User nipkow
# Date 1325177020 -3600
# Node ID 698de142f6f9ff6c99c9cf559d321de1876a133c
# Parent  313be214e40a1e4d7866e5b6c59b6745e63e2bd2
tuned

diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu Dec 29 17:43:40 2011 +0100
@@ -13,12 +13,12 @@
 begin
 
 fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
-"aval' (N n) _ = num' n" |
+"aval' (N n) S = num' n" |
 "aval' (V x) S = lookup S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
 lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
-by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
+by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def lookup_def)
 
 end
 
@@ -46,22 +46,22 @@
 
 text{* Soundness: *}
 
-lemma in_rep_update:
+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)"
-by(simp add: rep_st_def lookup_update)
+by(simp add: \<gamma>_st_def lookup_update)
 
 text{* The soundness proofs are textually identical to the ones for the step
 function operating on states as functions. *}
 
 lemma step_preserves_le2:
-  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
    \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
 proof(induction c arbitrary: cs ca S sa)
   case SKIP thus ?case
     by(auto simp:strip_eq_SKIP)
 next
   case Assign thus ?case
-    by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+    by (fastforce simp: strip_eq_Assign intro: aval'_sound in_gamma_update
       split: option.splits del:subsetD)
 next
   case Semi thus ?case apply (auto simp: strip_eq_Semi)
@@ -70,29 +70,29 @@
   case (If b c1 c2)
   then obtain cs1 cs2 ca1 ca2 P Pa where
       "cs = IF b THEN cs1 ELSE cs2 {P}" "ca = IF b THEN ca1 ELSE ca2 {Pa}"
-      "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+      "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
       "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
     by (fastforce simp: strip_eq_If)
-  moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
-    by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
-  moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
-    by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
+  moreover have "post cs1 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
+  moreover have "post cs2 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
   ultimately show ?case using If.prems(1) by (simp add: If.IH subset_iff)
 next
   case (While b c1)
   then obtain cs1 ca1 I P Ia Pa where
     "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
-    "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+    "I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
     "strip cs1 = c1" "strip ca1 = c1"
     by (fastforce simp: strip_eq_While)
-  moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
-    using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
-    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+  moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (sa \<squnion> post ca1)"
+    using `S \<subseteq> \<gamma>\<^isub>o sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
   ultimately show ?case by (simp add: While.IH subset_iff)
 qed
 
 lemma step_preserves_le:
-  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
    \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
 by (metis le_strip step_preserves_le2 strip_acom)
 
@@ -106,12 +106,12 @@
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
-      show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
-      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
+      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
     qed
   qed
   from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
-    by (blast intro: mono_rep_c order_trans)
+    by (blast intro: mono_gamma_c order_trans)
 qed
 
 end
diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int0_const.thy
--- a/src/HOL/IMP/Abs_Int0_const.thy	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Thu Dec 29 17:43:40 2011 +0100
@@ -8,9 +8,9 @@
 
 datatype cval = Const val | Any
 
-fun rep_cval where
-"rep_cval (Const n) = {n}" |
-"rep_cval (Any) = UNIV"
+fun \<gamma>_cval where
+"\<gamma>_cval (Const n) = {n}" |
+"\<gamma>_cval (Any) = UNIV"
 
 fun plus_cval where
 "plus_cval (Const m) (Const n) = Const(m+n)" |
@@ -52,7 +52,7 @@
 end
 
 
-interpretation Val_abs rep_cval Const plus_cval
+interpretation Val_abs \<gamma>_cval Const plus_cval
 defines aval'_const is aval'
 proof
   case goal1 thus ?case
@@ -66,7 +66,7 @@
     by(auto simp: plus_cval_cases split: cval.split)
 qed
 
-interpretation Abs_Int rep_cval Const plus_cval
+interpretation Abs_Int \<gamma>_cval Const plus_cval
 defines AI_const is AI
 and step_const is step'
 proof qed
@@ -74,7 +74,7 @@
 
 text{* Monotonicity: *}
 
-interpretation Abs_Int_mono rep_cval Const plus_cval
+interpretation Abs_Int_mono \<gamma>_cval Const plus_cval
 proof
   case goal1 thus ?case
     by(auto simp: plus_cval_cases split: cval.split)
diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Thu Dec 29 17:43:40 2011 +0100
@@ -132,7 +132,7 @@
 "None \<squnion> y = y" |
 "x \<squnion> None = x"
 
-lemma [simp]: "x \<squnion> None = x"
+lemma join_None2[simp]: "x \<squnion> None = x"
 by (cases x) simp_all
 
 definition "\<top> = Some \<top>"
@@ -224,23 +224,23 @@
 
 subsection "Abstract Interpretation"
 
-definition rep_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
-"rep_fun rep F = {f. \<forall>x. f x \<in> rep(F x)}"
+definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
+"\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}"
 
-fun rep_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where
-"rep_option rep None = {}" |
-"rep_option rep (Some a) = rep a"
+fun \<gamma>_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where
+"\<gamma>_option \<gamma> None = {}" |
+"\<gamma>_option \<gamma> (Some a) = \<gamma> a"
 
 text{* The interface for abstract values: *}
 
 locale Val_abs =
-fixes rep :: "'a::SL_top \<Rightarrow> val set" ("\<gamma>")
-  assumes mono_rep: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
-  and rep_Top[simp]: "\<gamma> \<top> = UNIV"
+fixes \<gamma> :: "'a::SL_top \<Rightarrow> val set"
+  assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
+  and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
 fixes num' :: "val \<Rightarrow> 'a"
 and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-  assumes rep_num': "n : \<gamma>(num' n)"
-  and rep_plus':
+  assumes gamma_num': "n : \<gamma>(num' n)"
+  and gamma_plus':
  "n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)"
 
 type_synonym 'a st = "(vname \<Rightarrow> 'a)"
@@ -249,7 +249,7 @@
 begin
 
 fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
-"aval' (N n) _ = num' n" |
+"aval' (N n) S = num' n" |
 "aval' (V x) S = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
@@ -272,51 +272,51 @@
 by(induct c arbitrary: S) (simp_all add: Let_def)
 
 
-abbreviation rep_f :: "'a st \<Rightarrow> state set" ("\<gamma>\<^isub>f")
-where "\<gamma>\<^isub>f == rep_fun \<gamma>"
+abbreviation \<gamma>\<^isub>f :: "'a st \<Rightarrow> state set"
+where "\<gamma>\<^isub>f == \<gamma>_fun \<gamma>"
 
-abbreviation rep_u :: "'a st option \<Rightarrow> state set" ("\<gamma>\<^isub>u")
-where "\<gamma>\<^isub>u == rep_option \<gamma>\<^isub>f"
+abbreviation \<gamma>\<^isub>o :: "'a st option \<Rightarrow> state set"
+where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
 
-abbreviation rep_c :: "'a st option acom \<Rightarrow> state set acom" ("\<gamma>\<^isub>c")
-where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>u"
+abbreviation \<gamma>\<^isub>c :: "'a st option acom \<Rightarrow> state set acom"
+where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
 
-lemma rep_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
-by(simp add: Top_fun_def rep_fun_def)
+lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
+by(simp add: Top_fun_def \<gamma>_fun_def)
 
-lemma rep_u_Top[simp]: "\<gamma>\<^isub>u Top = UNIV"
+lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
 by (simp add: Top_option_def)
 
 (* FIXME (maybe also le \<rightarrow> sqle?) *)
 
-lemma mono_rep_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
-by(auto simp: le_fun_def rep_fun_def dest: mono_rep)
+lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
 
-lemma mono_rep_u:
-  "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>u sa \<subseteq> \<gamma>\<^isub>u sa'"
-by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f)
+lemma mono_gamma_o:
+  "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>o sa \<subseteq> \<gamma>\<^isub>o sa'"
+by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f)
 
-lemma mono_rep_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
-by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u)
+lemma mono_gamma_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
+by (induction ca ca' 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)"
-by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def)
+by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def)
 
-lemma in_rep_update:
+lemma in_gamma_update:
   "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(S(x := a))"
-by(simp add: rep_fun_def)
+by(simp add: \<gamma>_fun_def)
 
 lemma step_preserves_le2:
-  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
    \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
 proof(induction c arbitrary: cs ca S sa)
   case SKIP thus ?case
     by(auto simp:strip_eq_SKIP)
 next
   case Assign thus ?case
-    by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+    by (fastforce simp: strip_eq_Assign intro: aval'_sound in_gamma_update
       split: option.splits del:subsetD)
 next
   case Semi thus ?case apply (auto simp: strip_eq_Semi)
@@ -325,29 +325,29 @@
   case (If b c1 c2)
   then obtain cs1 cs2 ca1 ca2 P Pa where
       "cs= IF b THEN cs1 ELSE cs2 {P}" "ca= IF b THEN ca1 ELSE ca2 {Pa}"
-      "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+      "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
       "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
     by (fastforce simp: strip_eq_If)
-  moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
-    by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
-  moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
-    by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
-  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>u sa` by (simp add: If.IH subset_iff)
+  moreover have "post cs1 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
+  moreover have "post cs2 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
+  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o sa` by (simp add: If.IH subset_iff)
 next
   case (While b c1)
   then obtain cs1 ca1 I P Ia Pa where
     "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
-    "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+    "I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
     "strip cs1 = c1" "strip ca1 = c1"
     by (fastforce simp: strip_eq_While)
-  moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
-    using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
-    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+  moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (sa \<squnion> post ca1)"
+    using `S \<subseteq> \<gamma>\<^isub>o sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
   ultimately show ?case by (simp add: While.IH subset_iff)
 qed
 
 lemma step_preserves_le:
-  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
    \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
 by (metis le_strip step_preserves_le2 strip_acom)
 
@@ -361,12 +361,12 @@
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
-      show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
-      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
+      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
     qed
   qed
   from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
-    by (blast intro: mono_rep_c order_trans)
+    by (blast intro: mono_gamma_c order_trans)
 qed
 
 end
diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Thu Dec 29 17:43:40 2011 +0100
@@ -37,24 +37,24 @@
 
 end
 
-locale Val_abs1_rep =
-  Val_abs rep num' plus'
-  for rep :: "'a::L_top_bot \<Rightarrow> val set" ("\<gamma>") and num' plus' +
-assumes inter_rep_subset_rep_meet:
-  "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
-and rep_Bot[simp]: "rep \<bottom> = {}"
+locale Val_abs1_gamma =
+  Val_abs \<gamma> num' plus'
+  for \<gamma> :: "'a::L_top_bot \<Rightarrow> val set" and num' plus' +
+assumes inter_gamma_subset_gamma_meet:
+  "\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
+and gamma_Bot[simp]: "\<gamma> \<bottom> = {}"
 begin
 
-lemma in_rep_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
-by (metis IntI inter_rep_subset_rep_meet set_mp)
+lemma in_gamma_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
+by (metis IntI inter_gamma_subset_gamma_meet set_mp)
 
-lemma rep_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
-by (metis equalityI inter_rep_subset_rep_meet le_inf_iff mono_rep meet_le1 meet_le2)
+lemma gamma_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
+by (metis equalityI inter_gamma_subset_gamma_meet le_inf_iff mono_gamma meet_le1 meet_le2)
 
 end
 
 
-locale Val_abs1 = Val_abs1_rep +
+locale Val_abs1 = Val_abs1_gamma +
 fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
 and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
 assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
@@ -66,14 +66,14 @@
 locale Abs_Int1 = Val_abs1
 begin
 
-lemma in_rep_join_UpI: "s : \<gamma>\<^isub>u S1 | s : \<gamma>\<^isub>u S2 \<Longrightarrow> s : \<gamma>\<^isub>u(S1 \<squnion> S2)"
-by (metis (no_types) join_ge1 join_ge2 mono_rep_u set_rev_mp)
+lemma in_gamma_join_UpI: "s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
+by (metis (no_types) join_ge1 join_ge2 mono_gamma_o set_rev_mp)
 
 fun aval'' :: "aexp \<Rightarrow> 'a st option \<Rightarrow> 'a" where
 "aval'' e None = \<bottom>" |
 "aval'' e (Some sa) = aval' e sa"
 
-lemma aval''_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
+lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
 by(cases S)(simp add: aval'_sound)+
 
 subsubsection "Backward analysis"
@@ -107,31 +107,31 @@
   (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
    in afilter e1 res1 (afilter e2 res2 S))"
 
-lemma afilter_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>u (afilter e a S)"
+lemma afilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
 proof(induction e arbitrary: a S)
   case N thus ?case by simp
 next
   case (V x)
-  obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>u S`
-    by(auto simp: in_rep_up_iff)
-  moreover hence "s x : \<gamma> (lookup S' x)" by(simp add: rep_st_def)
+  obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>o S`
+    by(auto simp: in_gamma_option_iff)
+  moreover hence "s x : \<gamma> (lookup S' x)" by(simp add: \<gamma>_st_def)
   moreover have "s x : \<gamma> a" using V by simp
   ultimately show ?case using V(1)
-    by(simp add: lookup_update Let_def rep_st_def)
-      (metis mono_rep emptyE in_rep_meet rep_Bot subset_empty)
+    by(simp add: lookup_update Let_def \<gamma>_st_def)
+      (metis mono_gamma emptyE in_gamma_meet gamma_Bot subset_empty)
 next
   case (Plus e1 e2) thus ?case
     using filter_plus'[OF _ aval''_sound[OF Plus(3)] aval''_sound[OF Plus(3)]]
     by (auto split: prod.split)
 qed
 
-lemma bfilter_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>u(bfilter b bv S)"
+lemma bfilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>o(bfilter b bv S)"
 proof(induction b arbitrary: S bv)
   case Bc thus ?case by simp
 next
   case (Not b) thus ?case by simp
 next
-  case (And b1 b2) thus ?case by(fastforce simp: in_rep_join_UpI)
+  case (And b1 b2) thus ?case by(fastforce simp: in_gamma_join_UpI)
 next
   case (Less e1 e2) thus ?case
     by (auto split: prod.split)
@@ -162,20 +162,20 @@
 
 subsubsection "Soundness"
 
-lemma in_rep_update:
+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)"
-by(simp add: rep_st_def lookup_update)
+by(simp add: \<gamma>_st_def lookup_update)
 
 
 lemma step_preserves_le2:
-  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
    \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
 proof(induction c arbitrary: cs ca S sa)
   case SKIP thus ?case
     by(auto simp:strip_eq_SKIP)
 next
   case Assign thus ?case
-    by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+    by (fastforce simp: strip_eq_Assign intro: aval'_sound in_gamma_update
       split: option.splits del:subsetD)
 next
   case Semi thus ?case apply (auto simp: strip_eq_Semi)
@@ -184,30 +184,30 @@
   case (If b c1 c2)
   then obtain cs1 cs2 ca1 ca2 P Pa where
       "cs= IF b THEN cs1 ELSE cs2 {P}" "ca= IF b THEN ca1 ELSE ca2 {Pa}"
-      "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+      "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
       "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
     by (fastforce simp: strip_eq_If)
-  moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
-    by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
-  moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
-    by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
-  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>u sa`
+  moreover have "post cs1 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
+  moreover have "post cs2 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
+  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o sa`
     by (simp add: If.IH subset_iff bfilter_sound)
 next
   case (While b c1)
   then obtain cs1 ca1 I P Ia Pa where
     "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
-    "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+    "I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
     "strip cs1 = c1" "strip ca1 = c1"
     by (fastforce simp: strip_eq_While)
-  moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
-    using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
-    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+  moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (sa \<squnion> post ca1)"
+    using `S \<subseteq> \<gamma>\<^isub>o sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
   ultimately show ?case by (simp add: While.IH subset_iff bfilter_sound)
 qed
 
 lemma step_preserves_le:
-  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
    \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
 by (metis le_strip step_preserves_le2 strip_acom)
 
@@ -221,12 +221,12 @@
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
-      show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
-      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
+      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
     qed
   qed
   from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
-    by (blast intro: mono_rep_c order_trans)
+    by (blast intro: mono_gamma_c order_trans)
 qed
 
 end
@@ -255,7 +255,7 @@
 lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'"
 apply(induction e arbitrary: r r' S S')
 apply(auto simp: Let_def split: option.splits prod.splits)
-apply (metis mono_rep subsetD)
+apply (metis mono_gamma subsetD)
 apply(drule_tac x = "list" in mono_lookup)
 apply (metis mono_meet le_trans)
 apply (metis mono_meet mono_lookup mono_update)
diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int1_ivl.thy
--- a/src/HOL/IMP/Abs_Int1_ivl.thy	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Thu Dec 29 17:43:40 2011 +0100
@@ -8,7 +8,7 @@
 
 datatype ivl = I "int option" "int option"
 
-definition "rep_ivl i = (case i of
+definition "\<gamma>_ivl i = (case i of
   I (Some l) (Some h) \<Rightarrow> {l..h} |
   I (Some l) None \<Rightarrow> {l..} |
   I None (Some h) \<Rightarrow> {..h} |
@@ -26,14 +26,14 @@
 definition "num_ivl n = {n\<dots>n}"
 
 definition
-  [code_abbrev]: "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
+  [code_abbrev]: "contained_in i k \<longleftrightarrow> k \<in> \<gamma>_ivl i"
 
 lemma contained_in_simps [code]:
   "contained_in (I (Some l) (Some h)) k \<longleftrightarrow> l \<le> k \<and> k \<le> h"
   "contained_in (I (Some l) None) k \<longleftrightarrow> l \<le> k"
   "contained_in (I None (Some h)) k \<longleftrightarrow> k \<le> h"
   "contained_in (I None None) k \<longleftrightarrow> True"
-  by (simp_all add: contained_in_def rep_ivl_def)
+  by (simp_all add: contained_in_def \<gamma>_ivl_def)
 
 instantiation option :: (plus)plus
 begin
@@ -56,8 +56,8 @@
   (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
 by(auto split:option.split)
 
-lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
-by(auto simp add: rep_ivl_def split: ivl.split option.split)
+lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}"
+by(auto simp add: \<gamma>_ivl_def split: ivl.split option.split)
 
 definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
   case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
@@ -154,9 +154,9 @@
 definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
   case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
 
-lemma rep_minus_ivl:
-  "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
-by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
+lemma gamma_minus_ivl:
+  "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(minus_ivl i1 i2)"
+by(auto simp add: minus_ivl_def \<gamma>_ivl_def split: ivl.splits option.splits)
 
 
 definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
@@ -170,26 +170,26 @@
          I (max_option False (l1 + Some 1) l2) h2)
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
 
-interpretation Val_abs rep_ivl num_ivl plus_ivl
+interpretation Val_abs \<gamma>_ivl num_ivl plus_ivl
 defines aval_ivl is aval'
 proof
   case goal1 thus ?case
-    by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
+    by(auto simp: \<gamma>_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
 next
-  case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def)
+  case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def)
 next
-  case goal3 thus ?case by(simp add: rep_ivl_def num_ivl_def)
+  case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def)
 next
   case goal4 thus ?case
-    by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
+    by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
 qed
 
-interpretation Val_abs1_rep rep_ivl num_ivl plus_ivl
+interpretation Val_abs1_gamma \<gamma>_ivl num_ivl plus_ivl
 proof
   case goal1 thus ?case
-    by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
+    by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
 next
-  case goal2 show ?case by(auto simp add: bot_ivl_def rep_ivl_def empty_def)
+  case goal2 show ?case by(auto simp add: bot_ivl_def \<gamma>_ivl_def empty_def)
 qed
 
 lemma mono_minus_ivl:
@@ -202,19 +202,19 @@
 
 
 interpretation
-  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+  Val_abs1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
 proof
   case goal1 thus ?case
     by(auto simp add: filter_plus_ivl_def)
-      (metis rep_minus_ivl add_diff_cancel add_commute)+
+      (metis gamma_minus_ivl add_diff_cancel add_commute)+
 next
   case goal2 thus ?case
     by(cases a1, cases a2,
-      auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
+      auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
 interpretation
-  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+  Abs_Int1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter
 and step_ivl is step'
@@ -226,7 +226,7 @@
 text{* Monotonicity: *}
 
 interpretation
-  Abs_Int1_mono rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+  Abs_Int1_mono \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
 proof
   case goal1 thus ?case
     by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Thu Dec 29 17:43:40 2011 +0100
@@ -180,7 +180,7 @@
 apply(auto simp add: pfp_WN_def prefp_def split: option.splits)
 by (metis (no_types) strip_lpfpc strip_map2_acom strip_while)
 
-locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
+locale Abs_Int2 = Abs_Int1_mono \<gamma> for \<gamma> :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
 begin
 
 definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where
@@ -196,18 +196,18 @@
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
-      show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
-      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
+      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
     qed
   qed
   from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
-    by (blast intro: mono_rep_c order_trans)
+    by (blast intro: mono_gamma_c order_trans)
 qed
 
 end
 
 interpretation
-  Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl rep_ivl
+  Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl \<gamma>_ivl
 defines AI_ivl' is AI_WN
 proof qed
 
diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Thu Dec 29 17:43:40 2011 +0100
@@ -30,7 +30,7 @@
 lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
 by(rule ext)(auto simp: lookup_def update_def)
 
-definition "rep_st rep F = {f. \<forall>x. f x \<in> rep(lookup F x)}"
+definition "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(lookup F x)}"
 
 instantiation st :: (SL_top) SL_top
 begin
@@ -61,35 +61,36 @@
 context Val_abs
 begin
 
-abbreviation rep_f :: "'a st \<Rightarrow> state set" ("\<gamma>\<^isub>f")
-where "\<gamma>\<^isub>f == rep_st rep"
+abbreviation \<gamma>\<^isub>f :: "'a st \<Rightarrow> state set"
+where "\<gamma>\<^isub>f == \<gamma>_st \<gamma>"
 
-abbreviation rep_u :: "'a st option \<Rightarrow> state set" ("\<gamma>\<^isub>u")
-where "\<gamma>\<^isub>u == rep_option \<gamma>\<^isub>f"
+abbreviation \<gamma>\<^isub>o :: "'a st option \<Rightarrow> state set"
+where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
 
-abbreviation rep_c :: "'a st option acom \<Rightarrow> state set acom" ("\<gamma>\<^isub>c")
-where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>u"
+abbreviation \<gamma>\<^isub>c :: "'a st option acom \<Rightarrow> state set acom"
+where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
 
-lemma rep_f_Top[simp]: "rep_f Top = UNIV"
-by(auto simp: Top_st_def rep_st_def lookup_def)
+lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
+by(auto simp: Top_st_def \<gamma>_st_def lookup_def)
 
-lemma rep_u_Top[simp]: "rep_u Top = UNIV"
+lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
 by (simp add: Top_option_def)
 
 (* FIXME (maybe also le \<rightarrow> sqle?) *)
 
-lemma mono_rep_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
-apply(simp add:rep_st_def subset_iff lookup_def le_st_def split: if_splits)
-by (metis UNIV_I mono_rep rep_Top subsetD)
+lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+apply(simp add:\<gamma>_st_def subset_iff lookup_def le_st_def split: if_splits)
+by (metis UNIV_I mono_gamma gamma_Top subsetD)
 
-lemma mono_rep_u:
-  "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>u sa \<subseteq> \<gamma>\<^isub>u sa'"
-by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f)
+lemma mono_gamma_o:
+  "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>o sa \<subseteq> \<gamma>\<^isub>o sa'"
+by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f)
 
-lemma mono_rep_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
-by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u)
+lemma mono_gamma_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
+by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o)
 
-lemma in_rep_up_iff: "x : rep_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
+lemma in_gamma_option_iff:
+  "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
 by (cases u) auto
 
 end