# HG changeset patch
# User nipkow
# Date 1319096880 -7200
# Node ID e87feee00a4c25e5e916f6667f96d101ce38871a
# Parent  3dd426ae6bead211586ad056807a382434c8d26b
renamed name -> vname

diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -4,11 +4,11 @@
 
 subsection "Arithmetic Expressions"
 
-type_synonym name = string
+type_synonym vname = string
 type_synonym val = int
-type_synonym state = "name \<Rightarrow> val"
+type_synonym state = "vname \<Rightarrow> val"
 
-datatype aexp = N int | V name | Plus aexp aexp
+datatype aexp = N int | V vname | Plus aexp aexp
 
 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
 "aval (N n) _ = n" |
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -11,11 +11,11 @@
 
 datatype 'a acom =
   SKIP   'a                           ("SKIP {_}") |
-  Assign name aexp 'a                 ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
-  Semi   "'a acom" "'a acom"          ("_;//_"  [60, 61] 60) |
-  If     bexp "'a acom" "'a acom" 'a
+  Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
+  Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
+  If     bexp "('a acom)" "('a acom)" 'a
     ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
-  While  'a bexp "'a acom" 'a
+  While  'a bexp "('a acom)" 'a
     ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
 
 fun post :: "'a acom \<Rightarrow>'a" where
@@ -300,7 +300,7 @@
 
 end
 
-type_synonym 'a st = "(name \<Rightarrow> 'a)"
+type_synonym 'a st = "(vname \<Rightarrow> 'a)"
 
 locale Abs_Int_Fun = Val_abs
 begin
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -125,7 +125,7 @@
 text{* Abstract interpretation over abstract values. Abstract states are
 simply functions. The post-fixed point finder is parameterized over. *}
 
-type_synonym 'a st = "name \<Rightarrow> 'a"
+type_synonym 'a st = "vname \<Rightarrow> 'a"
 
 locale Abs_Int_Fun = Val_abs +
 fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
@@ -133,7 +133,7 @@
 assumes above: "x \<sqsubseteq> pfp f x"
 begin
 
-fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
+fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
 "aval' (N n) _ = num' n" |
 "aval' (V x) S = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
@@ -147,7 +147,7 @@
 lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
 by (induct a) (auto simp: rep_num' rep_plus')
 
-fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
+fun AI :: "com \<Rightarrow> 'a st \<Rightarrow> 'a st" where
 "AI SKIP S = S" |
 "AI (x ::= a) S = S(x := aval' a S)" |
 "AI (c1;c2) S = AI c2 (AI c1 S)" |
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -10,7 +10,7 @@
 
 text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
 
-datatype 'a st = FunDom "name \<Rightarrow> 'a" "name list"
+datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
 
 fun "fun" where "fun (FunDom f _) = f"
 fun dom where "dom (FunDom _ A) = A"
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Com.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -4,7 +4,7 @@
 
 datatype
   com = SKIP 
-      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
+      | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
       | Semi   com  com          ("_;/ _"  [60, 61] 60)
       | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
       | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Def_Ass.thy
--- a/src/HOL/IMP/Def_Ass.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Def_Ass.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -3,7 +3,7 @@
 
 subsection "Definite Assignment Analysis"
 
-inductive D :: "name set \<Rightarrow> com \<Rightarrow> name set \<Rightarrow> bool" where
+inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
 Skip: "D A SKIP A" |
 Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
 Semi: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" |
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Def_Ass_Exp.thy
--- a/src/HOL/IMP/Def_Ass_Exp.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Exp.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -5,8 +5,7 @@
 
 subsection "Initialization-Sensitive Expressions Evaluation"
 
-type_synonym val = "int"
-type_synonym state = "name \<Rightarrow> val option"
+type_synonym state = "vname \<Rightarrow> val option"
 
 
 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Fold.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -5,7 +5,7 @@
 subsection "Simple folding of arithmetic expressions"
 
 type_synonym
-  tab = "name \<Rightarrow> val option"
+  tab = "vname \<Rightarrow> val option"
 
 (* maybe better as the composition of substitution and the existing simp_const(0) *)
 fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
@@ -32,7 +32,7 @@
 definition
   "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
 
-primrec lnames :: "com \<Rightarrow> name set" where
+primrec lnames :: "com \<Rightarrow> vname set" where
 "lnames SKIP = {}" |
 "lnames (x ::= a) = {x}" |
 "lnames (c1; c2) = lnames c1 \<union> lnames c2" |
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Hoare.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -8,7 +8,7 @@
 
 type_synonym assn = "state \<Rightarrow> bool"
 
-abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> name \<Rightarrow> state"
+abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
   ("_[_'/_]" [1000,0,0] 999)
 where "s[a/x] == s(x := aval a s)"
 
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Live.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -7,7 +7,7 @@
 
 subsection "Liveness Analysis"
 
-fun L :: "com \<Rightarrow> name set \<Rightarrow> name set" where
+fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
 "L SKIP X = X" |
 "L (x ::= a) X = X-{x} \<union> vars a" |
 "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
@@ -18,14 +18,14 @@
 
 value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
 
-fun "kill" :: "com \<Rightarrow> name set" where
+fun "kill" :: "com \<Rightarrow> vname set" where
 "kill SKIP = {}" |
 "kill (x ::= a) = {x}" |
 "kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
 "kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
 "kill (WHILE b DO c) = {}"
 
-fun gen :: "com \<Rightarrow> name set" where
+fun gen :: "com \<Rightarrow> vname set" where
 "gen SKIP = {}" |
 "gen (x ::= a) = vars a" |
 "gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
@@ -94,7 +94,7 @@
 subsection "Program Optimization"
 
 text{* Burying assignments to dead variables: *}
-fun bury :: "com \<Rightarrow> name set \<Rightarrow> com" where
+fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
 "bury SKIP X = SKIP" |
 "bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
 "bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Poly_Types.thy
--- a/src/HOL/IMP/Poly_Types.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Poly_Types.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -6,7 +6,7 @@
 
 text{* Everything else remains the same. *}
 
-type_synonym tyenv = "name \<Rightarrow> ty"
+type_synonym tyenv = "vname \<Rightarrow> ty"
 
 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
   ("(1_/ \<turnstile>p/ (_ :/ _))" [50,0,50] 50)
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Procs.thy
--- a/src/HOL/IMP/Procs.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Procs.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -4,15 +4,17 @@
 
 subsection "Procedures and Local Variables"
 
+type_synonym pname = string
+
 datatype
   com = SKIP 
-      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
+      | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
       | Semi   com  com          ("_;/ _"  [60, 61] 60)
       | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
       | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
-      | Var    name com         ("(1{VAR _;;/ _})")
-      | Proc   name com com     ("(1{PROC _ = _;;/ _})")
-      | CALL   name
+      | Var    vname com        ("(1{VAR _;;/ _})")
+      | Proc   pname com com    ("(1{PROC _ = _;;/ _})")
+      | CALL   pname
 
 definition "test_com =
 {VAR ''x'';;
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -3,7 +3,7 @@
 
 subsubsection "Dynamic Scoping of Procedures and Variables"
 
-type_synonym penv = "name \<Rightarrow> com"
+type_synonym penv = "pname \<Rightarrow> com"
 
 inductive
   big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -3,7 +3,7 @@
 
 subsubsection "Static Scoping of Procedures, Dynamic of Variables"
 
-type_synonym penv = "(name \<times> com) list"
+type_synonym penv = "(pname \<times> com) list"
 
 inductive
   big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Procs_Stat_Vars_Stat.thy
--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -4,9 +4,9 @@
 subsubsection "Static Scoping of Procedures and Variables"
 
 type_synonym addr = nat
-type_synonym venv = "name \<Rightarrow> addr"
+type_synonym venv = "vname \<Rightarrow> addr"
 type_synonym store = "addr \<Rightarrow> val"
-type_synonym penv = "(name \<times> com \<times> venv) list"
+type_synonym penv = "(pname \<times> com \<times> venv) list"
 
 fun venv :: "penv \<times> venv \<times> nat \<Rightarrow> venv" where
 "venv(_,ve,_) = ve"
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Sec_Type_Expr.thy
--- a/src/HOL/IMP/Sec_Type_Expr.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Sec_Type_Expr.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -11,7 +11,7 @@
 for simplicity. For the sake of examples --- the general theory does not rely
 on it! --- a variable of length @{text n} has security level @{text n}: *}
 
-definition sec :: "name \<Rightarrow> level" where 
+definition sec :: "vname \<Rightarrow> level" where 
   "sec n = size n"
 
 fun sec_aexp :: "aexp \<Rightarrow> level" where
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Types.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -6,10 +6,10 @@
 
 datatype val = Iv int | Rv real
 
-type_synonym name = string
-type_synonym state = "name \<Rightarrow> val"
+type_synonym vname = string
+type_synonym state = "vname \<Rightarrow> val"
 
-datatype aexp =  Ic int | Rc real | V name | Plus aexp aexp
+datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
 
 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
 "taval (Ic i) s (Iv i)" |
@@ -41,7 +41,7 @@
 
 datatype
   com = SKIP 
-      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
+      | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
       | Semi   com  com          ("_; _"  [60, 61] 60)
       | If     bexp com com     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
       | While  bexp com         ("WHILE _ DO _"  [0, 61] 61)
@@ -68,7 +68,7 @@
 
 datatype ty = Ity | Rty
 
-type_synonym tyenv = "name \<Rightarrow> ty"
+type_synonym tyenv = "vname \<Rightarrow> ty"
 
 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
   ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/VC.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -8,7 +8,7 @@
 invariants. *}
 
 datatype acom = Askip
-              | Aassign name aexp
+              | Aassign vname aexp
               | Asemi   acom acom
               | Aif     bexp acom acom
               | Awhile  bexp assn acom
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Vars.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -13,7 +13,7 @@
 via a \emph{type class}, a device that originated with Haskell: *}
  
 class vars =
-fixes vars :: "'a \<Rightarrow> name set"
+fixes vars :: "'a \<Rightarrow> vname set"
 
 text{* This defines a type class ``vars'' with a single
 function of (coincidentally) the same name. Then we define two separated
@@ -22,7 +22,7 @@
 instantiation aexp :: vars
 begin
 
-fun vars_aexp :: "aexp \<Rightarrow> name set" where
+fun vars_aexp :: "aexp \<Rightarrow> vname set" where
 "vars_aexp (N n) = {}" |
 "vars_aexp (V x) = {x}" |
 "vars_aexp (Plus a\<^isub>1 a\<^isub>2) = vars_aexp a\<^isub>1 \<union> vars_aexp a\<^isub>2"
@@ -40,7 +40,7 @@
 instantiation bexp :: vars
 begin
 
-fun vars_bexp :: "bexp \<Rightarrow> name set" where
+fun vars_bexp :: "bexp \<Rightarrow> vname set" where
 "vars_bexp (Bc v) = {}" |
 "vars_bexp (Not b) = vars_bexp b" |
 "vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" |