renamed name -> vname
authornipkow
Thu Oct 20 09:48:00 2011 +0200 (2011-10-20)
changeset 45212e87feee00a4c
parent 45211 3dd426ae6bea
child 45215 1b2132017774
child 45216 a51a70687517
renamed name -> vname
src/HOL/IMP/AExp.thy
src/HOL/IMP/Abs_Int0_fun.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
src/HOL/IMP/Abs_State.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Def_Ass.thy
src/HOL/IMP/Def_Ass_Exp.thy
src/HOL/IMP/Fold.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Live.thy
src/HOL/IMP/Poly_Types.thy
src/HOL/IMP/Procs.thy
src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
src/HOL/IMP/Procs_Stat_Vars_Stat.thy
src/HOL/IMP/Sec_Type_Expr.thy
src/HOL/IMP/Types.thy
src/HOL/IMP/VC.thy
src/HOL/IMP/Vars.thy
     1.1 --- a/src/HOL/IMP/AExp.thy	Wed Oct 19 23:07:48 2011 +0200
     1.2 +++ b/src/HOL/IMP/AExp.thy	Thu Oct 20 09:48:00 2011 +0200
     1.3 @@ -4,11 +4,11 @@
     1.4  
     1.5  subsection "Arithmetic Expressions"
     1.6  
     1.7 -type_synonym name = string
     1.8 +type_synonym vname = string
     1.9  type_synonym val = int
    1.10 -type_synonym state = "name \<Rightarrow> val"
    1.11 +type_synonym state = "vname \<Rightarrow> val"
    1.12  
    1.13 -datatype aexp = N int | V name | Plus aexp aexp
    1.14 +datatype aexp = N int | V vname | Plus aexp aexp
    1.15  
    1.16  fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
    1.17  "aval (N n) _ = n" |
     2.1 --- a/src/HOL/IMP/Abs_Int0_fun.thy	Wed Oct 19 23:07:48 2011 +0200
     2.2 +++ b/src/HOL/IMP/Abs_Int0_fun.thy	Thu Oct 20 09:48:00 2011 +0200
     2.3 @@ -11,11 +11,11 @@
     2.4  
     2.5  datatype 'a acom =
     2.6    SKIP   'a                           ("SKIP {_}") |
     2.7 -  Assign name aexp 'a                 ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
     2.8 -  Semi   "'a acom" "'a acom"          ("_;//_"  [60, 61] 60) |
     2.9 -  If     bexp "'a acom" "'a acom" 'a
    2.10 +  Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
    2.11 +  Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
    2.12 +  If     bexp "('a acom)" "('a acom)" 'a
    2.13      ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
    2.14 -  While  'a bexp "'a acom" 'a
    2.15 +  While  'a bexp "('a acom)" 'a
    2.16      ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
    2.17  
    2.18  fun post :: "'a acom \<Rightarrow>'a" where
    2.19 @@ -300,7 +300,7 @@
    2.20  
    2.21  end
    2.22  
    2.23 -type_synonym 'a st = "(name \<Rightarrow> 'a)"
    2.24 +type_synonym 'a st = "(vname \<Rightarrow> 'a)"
    2.25  
    2.26  locale Abs_Int_Fun = Val_abs
    2.27  begin
     3.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Wed Oct 19 23:07:48 2011 +0200
     3.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Thu Oct 20 09:48:00 2011 +0200
     3.3 @@ -125,7 +125,7 @@
     3.4  text{* Abstract interpretation over abstract values. Abstract states are
     3.5  simply functions. The post-fixed point finder is parameterized over. *}
     3.6  
     3.7 -type_synonym 'a st = "name \<Rightarrow> 'a"
     3.8 +type_synonym 'a st = "vname \<Rightarrow> 'a"
     3.9  
    3.10  locale Abs_Int_Fun = Val_abs +
    3.11  fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
    3.12 @@ -133,7 +133,7 @@
    3.13  assumes above: "x \<sqsubseteq> pfp f x"
    3.14  begin
    3.15  
    3.16 -fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
    3.17 +fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
    3.18  "aval' (N n) _ = num' n" |
    3.19  "aval' (V x) S = S x" |
    3.20  "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
    3.21 @@ -147,7 +147,7 @@
    3.22  lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
    3.23  by (induct a) (auto simp: rep_num' rep_plus')
    3.24  
    3.25 -fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
    3.26 +fun AI :: "com \<Rightarrow> 'a st \<Rightarrow> 'a st" where
    3.27  "AI SKIP S = S" |
    3.28  "AI (x ::= a) S = S(x := aval' a S)" |
    3.29  "AI (c1;c2) S = AI c2 (AI c1 S)" |
     4.1 --- a/src/HOL/IMP/Abs_State.thy	Wed Oct 19 23:07:48 2011 +0200
     4.2 +++ b/src/HOL/IMP/Abs_State.thy	Thu Oct 20 09:48:00 2011 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4  
     4.5  text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
     4.6  
     4.7 -datatype 'a st = FunDom "name \<Rightarrow> 'a" "name list"
     4.8 +datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
     4.9  
    4.10  fun "fun" where "fun (FunDom f _) = f"
    4.11  fun dom where "dom (FunDom _ A) = A"
     5.1 --- a/src/HOL/IMP/Com.thy	Wed Oct 19 23:07:48 2011 +0200
     5.2 +++ b/src/HOL/IMP/Com.thy	Thu Oct 20 09:48:00 2011 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4  
     5.5  datatype
     5.6    com = SKIP 
     5.7 -      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
     5.8 +      | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
     5.9        | Semi   com  com          ("_;/ _"  [60, 61] 60)
    5.10        | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
    5.11        | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
     6.1 --- a/src/HOL/IMP/Def_Ass.thy	Wed Oct 19 23:07:48 2011 +0200
     6.2 +++ b/src/HOL/IMP/Def_Ass.thy	Thu Oct 20 09:48:00 2011 +0200
     6.3 @@ -3,7 +3,7 @@
     6.4  
     6.5  subsection "Definite Assignment Analysis"
     6.6  
     6.7 -inductive D :: "name set \<Rightarrow> com \<Rightarrow> name set \<Rightarrow> bool" where
     6.8 +inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
     6.9  Skip: "D A SKIP A" |
    6.10  Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
    6.11  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" |
     7.1 --- a/src/HOL/IMP/Def_Ass_Exp.thy	Wed Oct 19 23:07:48 2011 +0200
     7.2 +++ b/src/HOL/IMP/Def_Ass_Exp.thy	Thu Oct 20 09:48:00 2011 +0200
     7.3 @@ -5,8 +5,7 @@
     7.4  
     7.5  subsection "Initialization-Sensitive Expressions Evaluation"
     7.6  
     7.7 -type_synonym val = "int"
     7.8 -type_synonym state = "name \<Rightarrow> val option"
     7.9 +type_synonym state = "vname \<Rightarrow> val option"
    7.10  
    7.11  
    7.12  fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where
     8.1 --- a/src/HOL/IMP/Fold.thy	Wed Oct 19 23:07:48 2011 +0200
     8.2 +++ b/src/HOL/IMP/Fold.thy	Thu Oct 20 09:48:00 2011 +0200
     8.3 @@ -5,7 +5,7 @@
     8.4  subsection "Simple folding of arithmetic expressions"
     8.5  
     8.6  type_synonym
     8.7 -  tab = "name \<Rightarrow> val option"
     8.8 +  tab = "vname \<Rightarrow> val option"
     8.9  
    8.10  (* maybe better as the composition of substitution and the existing simp_const(0) *)
    8.11  fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
    8.12 @@ -32,7 +32,7 @@
    8.13  definition
    8.14    "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
    8.15  
    8.16 -primrec lnames :: "com \<Rightarrow> name set" where
    8.17 +primrec lnames :: "com \<Rightarrow> vname set" where
    8.18  "lnames SKIP = {}" |
    8.19  "lnames (x ::= a) = {x}" |
    8.20  "lnames (c1; c2) = lnames c1 \<union> lnames c2" |
     9.1 --- a/src/HOL/IMP/Hoare.thy	Wed Oct 19 23:07:48 2011 +0200
     9.2 +++ b/src/HOL/IMP/Hoare.thy	Thu Oct 20 09:48:00 2011 +0200
     9.3 @@ -8,7 +8,7 @@
     9.4  
     9.5  type_synonym assn = "state \<Rightarrow> bool"
     9.6  
     9.7 -abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> name \<Rightarrow> state"
     9.8 +abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
     9.9    ("_[_'/_]" [1000,0,0] 999)
    9.10  where "s[a/x] == s(x := aval a s)"
    9.11  
    10.1 --- a/src/HOL/IMP/Live.thy	Wed Oct 19 23:07:48 2011 +0200
    10.2 +++ b/src/HOL/IMP/Live.thy	Thu Oct 20 09:48:00 2011 +0200
    10.3 @@ -7,7 +7,7 @@
    10.4  
    10.5  subsection "Liveness Analysis"
    10.6  
    10.7 -fun L :: "com \<Rightarrow> name set \<Rightarrow> name set" where
    10.8 +fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
    10.9  "L SKIP X = X" |
   10.10  "L (x ::= a) X = X-{x} \<union> vars a" |
   10.11  "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
   10.12 @@ -18,14 +18,14 @@
   10.13  
   10.14  value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
   10.15  
   10.16 -fun "kill" :: "com \<Rightarrow> name set" where
   10.17 +fun "kill" :: "com \<Rightarrow> vname set" where
   10.18  "kill SKIP = {}" |
   10.19  "kill (x ::= a) = {x}" |
   10.20  "kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
   10.21  "kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
   10.22  "kill (WHILE b DO c) = {}"
   10.23  
   10.24 -fun gen :: "com \<Rightarrow> name set" where
   10.25 +fun gen :: "com \<Rightarrow> vname set" where
   10.26  "gen SKIP = {}" |
   10.27  "gen (x ::= a) = vars a" |
   10.28  "gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
   10.29 @@ -94,7 +94,7 @@
   10.30  subsection "Program Optimization"
   10.31  
   10.32  text{* Burying assignments to dead variables: *}
   10.33 -fun bury :: "com \<Rightarrow> name set \<Rightarrow> com" where
   10.34 +fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
   10.35  "bury SKIP X = SKIP" |
   10.36  "bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
   10.37  "bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
    11.1 --- a/src/HOL/IMP/Poly_Types.thy	Wed Oct 19 23:07:48 2011 +0200
    11.2 +++ b/src/HOL/IMP/Poly_Types.thy	Thu Oct 20 09:48:00 2011 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  
    11.5  text{* Everything else remains the same. *}
    11.6  
    11.7 -type_synonym tyenv = "name \<Rightarrow> ty"
    11.8 +type_synonym tyenv = "vname \<Rightarrow> ty"
    11.9  
   11.10  inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
   11.11    ("(1_/ \<turnstile>p/ (_ :/ _))" [50,0,50] 50)
    12.1 --- a/src/HOL/IMP/Procs.thy	Wed Oct 19 23:07:48 2011 +0200
    12.2 +++ b/src/HOL/IMP/Procs.thy	Thu Oct 20 09:48:00 2011 +0200
    12.3 @@ -4,15 +4,17 @@
    12.4  
    12.5  subsection "Procedures and Local Variables"
    12.6  
    12.7 +type_synonym pname = string
    12.8 +
    12.9  datatype
   12.10    com = SKIP 
   12.11 -      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
   12.12 +      | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
   12.13        | Semi   com  com          ("_;/ _"  [60, 61] 60)
   12.14        | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
   12.15        | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
   12.16 -      | Var    name com         ("(1{VAR _;;/ _})")
   12.17 -      | Proc   name com com     ("(1{PROC _ = _;;/ _})")
   12.18 -      | CALL   name
   12.19 +      | Var    vname com        ("(1{VAR _;;/ _})")
   12.20 +      | Proc   pname com com    ("(1{PROC _ = _;;/ _})")
   12.21 +      | CALL   pname
   12.22  
   12.23  definition "test_com =
   12.24  {VAR ''x'';;
    13.1 --- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Wed Oct 19 23:07:48 2011 +0200
    13.2 +++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Thu Oct 20 09:48:00 2011 +0200
    13.3 @@ -3,7 +3,7 @@
    13.4  
    13.5  subsubsection "Dynamic Scoping of Procedures and Variables"
    13.6  
    13.7 -type_synonym penv = "name \<Rightarrow> com"
    13.8 +type_synonym penv = "pname \<Rightarrow> com"
    13.9  
   13.10  inductive
   13.11    big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
    14.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Wed Oct 19 23:07:48 2011 +0200
    14.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Thu Oct 20 09:48:00 2011 +0200
    14.3 @@ -3,7 +3,7 @@
    14.4  
    14.5  subsubsection "Static Scoping of Procedures, Dynamic of Variables"
    14.6  
    14.7 -type_synonym penv = "(name \<times> com) list"
    14.8 +type_synonym penv = "(pname \<times> com) list"
    14.9  
   14.10  inductive
   14.11    big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
    15.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Wed Oct 19 23:07:48 2011 +0200
    15.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Thu Oct 20 09:48:00 2011 +0200
    15.3 @@ -4,9 +4,9 @@
    15.4  subsubsection "Static Scoping of Procedures and Variables"
    15.5  
    15.6  type_synonym addr = nat
    15.7 -type_synonym venv = "name \<Rightarrow> addr"
    15.8 +type_synonym venv = "vname \<Rightarrow> addr"
    15.9  type_synonym store = "addr \<Rightarrow> val"
   15.10 -type_synonym penv = "(name \<times> com \<times> venv) list"
   15.11 +type_synonym penv = "(pname \<times> com \<times> venv) list"
   15.12  
   15.13  fun venv :: "penv \<times> venv \<times> nat \<Rightarrow> venv" where
   15.14  "venv(_,ve,_) = ve"
    16.1 --- a/src/HOL/IMP/Sec_Type_Expr.thy	Wed Oct 19 23:07:48 2011 +0200
    16.2 +++ b/src/HOL/IMP/Sec_Type_Expr.thy	Thu Oct 20 09:48:00 2011 +0200
    16.3 @@ -11,7 +11,7 @@
    16.4  for simplicity. For the sake of examples --- the general theory does not rely
    16.5  on it! --- a variable of length @{text n} has security level @{text n}: *}
    16.6  
    16.7 -definition sec :: "name \<Rightarrow> level" where 
    16.8 +definition sec :: "vname \<Rightarrow> level" where 
    16.9    "sec n = size n"
   16.10  
   16.11  fun sec_aexp :: "aexp \<Rightarrow> level" where
    17.1 --- a/src/HOL/IMP/Types.thy	Wed Oct 19 23:07:48 2011 +0200
    17.2 +++ b/src/HOL/IMP/Types.thy	Thu Oct 20 09:48:00 2011 +0200
    17.3 @@ -6,10 +6,10 @@
    17.4  
    17.5  datatype val = Iv int | Rv real
    17.6  
    17.7 -type_synonym name = string
    17.8 -type_synonym state = "name \<Rightarrow> val"
    17.9 +type_synonym vname = string
   17.10 +type_synonym state = "vname \<Rightarrow> val"
   17.11  
   17.12 -datatype aexp =  Ic int | Rc real | V name | Plus aexp aexp
   17.13 +datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
   17.14  
   17.15  inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
   17.16  "taval (Ic i) s (Iv i)" |
   17.17 @@ -41,7 +41,7 @@
   17.18  
   17.19  datatype
   17.20    com = SKIP 
   17.21 -      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
   17.22 +      | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
   17.23        | Semi   com  com          ("_; _"  [60, 61] 60)
   17.24        | If     bexp com com     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
   17.25        | While  bexp com         ("WHILE _ DO _"  [0, 61] 61)
   17.26 @@ -68,7 +68,7 @@
   17.27  
   17.28  datatype ty = Ity | Rty
   17.29  
   17.30 -type_synonym tyenv = "name \<Rightarrow> ty"
   17.31 +type_synonym tyenv = "vname \<Rightarrow> ty"
   17.32  
   17.33  inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
   17.34    ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
    18.1 --- a/src/HOL/IMP/VC.thy	Wed Oct 19 23:07:48 2011 +0200
    18.2 +++ b/src/HOL/IMP/VC.thy	Thu Oct 20 09:48:00 2011 +0200
    18.3 @@ -8,7 +8,7 @@
    18.4  invariants. *}
    18.5  
    18.6  datatype acom = Askip
    18.7 -              | Aassign name aexp
    18.8 +              | Aassign vname aexp
    18.9                | Asemi   acom acom
   18.10                | Aif     bexp acom acom
   18.11                | Awhile  bexp assn acom
    19.1 --- a/src/HOL/IMP/Vars.thy	Wed Oct 19 23:07:48 2011 +0200
    19.2 +++ b/src/HOL/IMP/Vars.thy	Thu Oct 20 09:48:00 2011 +0200
    19.3 @@ -13,7 +13,7 @@
    19.4  via a \emph{type class}, a device that originated with Haskell: *}
    19.5   
    19.6  class vars =
    19.7 -fixes vars :: "'a \<Rightarrow> name set"
    19.8 +fixes vars :: "'a \<Rightarrow> vname set"
    19.9  
   19.10  text{* This defines a type class ``vars'' with a single
   19.11  function of (coincidentally) the same name. Then we define two separated
   19.12 @@ -22,7 +22,7 @@
   19.13  instantiation aexp :: vars
   19.14  begin
   19.15  
   19.16 -fun vars_aexp :: "aexp \<Rightarrow> name set" where
   19.17 +fun vars_aexp :: "aexp \<Rightarrow> vname set" where
   19.18  "vars_aexp (N n) = {}" |
   19.19  "vars_aexp (V x) = {x}" |
   19.20  "vars_aexp (Plus a\<^isub>1 a\<^isub>2) = vars_aexp a\<^isub>1 \<union> vars_aexp a\<^isub>2"
   19.21 @@ -40,7 +40,7 @@
   19.22  instantiation bexp :: vars
   19.23  begin
   19.24  
   19.25 -fun vars_bexp :: "bexp \<Rightarrow> name set" where
   19.26 +fun vars_bexp :: "bexp \<Rightarrow> vname set" where
   19.27  "vars_bexp (Bc v) = {}" |
   19.28  "vars_bexp (Not b) = vars_bexp b" |
   19.29  "vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" |