--- a/src/HOL/IMP/AExp.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/AExp.thy Thu Oct 20 09:59:12 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" |
--- a/src/HOL/IMP/Abs_Int0_fun.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Thu Oct 20 09:59:12 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
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Thu Oct 20 09:59:12 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)" |
--- a/src/HOL/IMP/Abs_State.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Abs_State.thy Thu Oct 20 09:59:12 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"
--- a/src/HOL/IMP/Com.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Com.thy Thu Oct 20 09:59:12 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)
--- a/src/HOL/IMP/Def_Ass.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Def_Ass.thy Thu Oct 20 09:59:12 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" |
--- a/src/HOL/IMP/Def_Ass_Exp.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Exp.thy Thu Oct 20 09:59:12 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
--- a/src/HOL/IMP/Fold.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Fold.thy Thu Oct 20 09:59:12 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" |
--- a/src/HOL/IMP/Hoare.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Hoare.thy Thu Oct 20 09:59:12 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)"
--- a/src/HOL/IMP/Live.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Live.thy Thu Oct 20 09:59:12 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)" |
--- a/src/HOL/IMP/Poly_Types.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Poly_Types.thy Thu Oct 20 09:59:12 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)
--- a/src/HOL/IMP/Procs.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Procs.thy Thu Oct 20 09:59:12 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'';;
--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Thu Oct 20 09:59:12 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)
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Thu Oct 20 09:59:12 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)
--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Thu Oct 20 09:59:12 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"
--- a/src/HOL/IMP/Sec_Type_Expr.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Sec_Type_Expr.thy Thu Oct 20 09:59:12 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
--- a/src/HOL/IMP/Types.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Types.thy Thu Oct 20 09:59:12 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)
--- a/src/HOL/IMP/VC.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/VC.thy Thu Oct 20 09:59:12 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
--- a/src/HOL/IMP/Vars.thy Thu Oct 20 09:11:13 2011 +0200
+++ b/src/HOL/IMP/Vars.thy Thu Oct 20 09:59:12 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" |