diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -49,33 +49,33 @@
 with a jump, since no breaks, continues or returns are allowed in an 
 expression. *}
 
-consts jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
-primrec
-"jumpNestingOkS jmps (Skip)   = True"
-"jumpNestingOkS jmps (Expr e) = True"
-"jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
-"jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
-                                 jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
-                                           jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
+primrec jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
+where
+  "jumpNestingOkS jmps (Skip)   = True"
+| "jumpNestingOkS jmps (Expr e) = True"
+| "jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
+| "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
+                                   jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
+                                             jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
 --{* The label of the while loop only handles continue jumps. Breaks are only
      handled by @{term Lab} *}
-"jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
-"jumpNestingOkS jmps (Throw e) = True"
-"jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
-                                                jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
-                                        jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (Init C) = True" 
+| "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
+| "jumpNestingOkS jmps (Throw e) = True"
+| "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
+                                                  jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
+                                          jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (Init C) = True" 
  --{* wellformedness of the program must enshure that for all initializers 
       jumpNestingOkS {} holds *} 
 --{* Dummy analysis for intermediate smallstep term @{term  FinA} *}
-"jumpNestingOkS jmps (FinA a c) = False"
+| "jumpNestingOkS jmps (FinA a c) = False"
 
 
 definition jumpNestingOk :: "jump set \<Rightarrow> term \<Rightarrow> bool" where
-"jumpNestingOk jmps t \<equiv> (case t of
+"jumpNestingOk jmps t = (case t of
                       In1 se \<Rightarrow> (case se of
                                    Inl e \<Rightarrow> True
                                  | Inr s \<Rightarrow> jumpNestingOkS jmps s)
@@ -116,48 +116,46 @@
 
 subsection {* Very restricted calculation fallback calculation *}
 
-consts the_LVar_name:: "var \<Rightarrow> lname"
-primrec 
-"the_LVar_name (LVar n) = n"
+primrec the_LVar_name :: "var \<Rightarrow> lname"
+  where "the_LVar_name (LVar n) = n"
 
-consts assignsE :: "expr      \<Rightarrow> lname set" 
-       assignsV :: "var       \<Rightarrow> lname set"
-       assignsEs:: "expr list \<Rightarrow> lname set"
-text {* *}
-primrec
-"assignsE (NewC c)            = {}" 
-"assignsE (NewA t e)          = assignsE e"
-"assignsE (Cast t e)          = assignsE e"
-"assignsE (e InstOf r)        = assignsE e"
-"assignsE (Lit val)           = {}"
-"assignsE (UnOp unop e)       = assignsE e"
-"assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
-                                     then (assignsE e1)
-                                     else (assignsE e1) \<union> (assignsE e2))" 
-"assignsE (Super)             = {}"
-"assignsE (Acc v)             = assignsV v"
-"assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
-                                 (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
-                                                     else {})"
-"assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
-"assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
-                          = (assignsE objRef) \<union> (assignsEs args)"
+primrec assignsE :: "expr \<Rightarrow> lname set" 
+  and assignsV :: "var \<Rightarrow> lname set"
+  and assignsEs:: "expr list \<Rightarrow> lname set"
+where
+  "assignsE (NewC c)            = {}" 
+| "assignsE (NewA t e)          = assignsE e"
+| "assignsE (Cast t e)          = assignsE e"
+| "assignsE (e InstOf r)        = assignsE e"
+| "assignsE (Lit val)           = {}"
+| "assignsE (UnOp unop e)       = assignsE e"
+| "assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
+                                       then (assignsE e1)
+                                       else (assignsE e1) \<union> (assignsE e2))" 
+| "assignsE (Super)             = {}"
+| "assignsE (Acc v)             = assignsV v"
+| "assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
+                                   (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
+                                                       else {})"
+| "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
+| "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
+                            = (assignsE objRef) \<union> (assignsEs args)"
 -- {* Only dummy analysis for intermediate expressions  
       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
-"assignsE (Methd C sig)   = {}" 
-"assignsE (Body  C s)     = {}"   
-"assignsE (InsInitE s e)  = {}"  
-"assignsE (Callee l e)    = {}" 
+| "assignsE (Methd C sig)   = {}" 
+| "assignsE (Body  C s)     = {}"   
+| "assignsE (InsInitE s e)  = {}"  
+| "assignsE (Callee l e)    = {}" 
 
-"assignsV (LVar n)       = {}"
-"assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
-"assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
+| "assignsV (LVar n)       = {}"
+| "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
+| "assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
 
-"assignsEs     [] = {}"
-"assignsEs (e#es) = assignsE e \<union> assignsEs es"
+| "assignsEs     [] = {}"
+| "assignsEs (e#es) = assignsE e \<union> assignsEs es"
 
 definition assigns :: "term \<Rightarrow> lname set" where
-"assigns t \<equiv> (case t of
+"assigns t = (case t of
                 In1 se \<Rightarrow> (case se of
                              Inl e \<Rightarrow> assignsE e
                            | Inr s \<Rightarrow> {})
@@ -190,42 +188,42 @@
 
 subsection "Analysis of constant expressions"
 
-consts constVal :: "expr \<Rightarrow> val option"
-primrec 
-"constVal (NewC c)      = None"
-"constVal (NewA t e)    = None"
-"constVal (Cast t e)    = None"
-"constVal (Inst e r)    = None"
-"constVal (Lit val)     = Some val"
-"constVal (UnOp unop e) = (case (constVal e) of
-                             None   \<Rightarrow> None
-                           | Some v \<Rightarrow> Some (eval_unop unop v))" 
-"constVal (BinOp binop e1 e2) = (case (constVal e1) of
-                                   None    \<Rightarrow> None
-                                 | Some v1 \<Rightarrow> (case (constVal e2) of 
-                                                None    \<Rightarrow> None
-                                              | Some v2 \<Rightarrow> Some (eval_binop 
-                                                                 binop v1 v2)))"
-"constVal (Super)         = None"
-"constVal (Acc v)         = None"
-"constVal (Ass v e)       = None"
-"constVal (Cond b e1 e2)  = (case (constVal b) of
+primrec constVal :: "expr \<Rightarrow> val option"
+where
+  "constVal (NewC c)      = None"
+| "constVal (NewA t e)    = None"
+| "constVal (Cast t e)    = None"
+| "constVal (Inst e r)    = None"
+| "constVal (Lit val)     = Some val"
+| "constVal (UnOp unop e) = (case (constVal e) of
                                None   \<Rightarrow> None
-                             | Some bv\<Rightarrow> (case the_Bool bv of
-                                            True \<Rightarrow> (case (constVal e2) of
-                                                       None   \<Rightarrow> None
-                                                     | Some v \<Rightarrow> constVal e1)
-                                          | False\<Rightarrow> (case (constVal e1) of
-                                                       None   \<Rightarrow> None
-                                                     | Some v \<Rightarrow> constVal e2)))"
+                             | Some v \<Rightarrow> Some (eval_unop unop v))" 
+| "constVal (BinOp binop e1 e2) = (case (constVal e1) of
+                                     None    \<Rightarrow> None
+                                   | Some v1 \<Rightarrow> (case (constVal e2) of 
+                                                  None    \<Rightarrow> None
+                                                | Some v2 \<Rightarrow> Some (eval_binop 
+                                                                   binop v1 v2)))"
+| "constVal (Super)         = None"
+| "constVal (Acc v)         = None"
+| "constVal (Ass v e)       = None"
+| "constVal (Cond b e1 e2)  = (case (constVal b) of
+                                 None   \<Rightarrow> None
+                               | Some bv\<Rightarrow> (case the_Bool bv of
+                                              True \<Rightarrow> (case (constVal e2) of
+                                                         None   \<Rightarrow> None
+                                                       | Some v \<Rightarrow> constVal e1)
+                                            | False\<Rightarrow> (case (constVal e1) of
+                                                         None   \<Rightarrow> None
+                                                       | Some v \<Rightarrow> constVal e2)))"
 --{* Note that @{text "constVal (Cond b e1 e2)"} is stricter as it could be.
      It requires that all tree expressions are constant even if we can decide
      which branch to choose, provided the constant value of @{term b} *}
-"constVal (Call accC statT mode objRef mn pTs args) = None"
-"constVal (Methd C sig)   = None" 
-"constVal (Body  C s)     = None"   
-"constVal (InsInitE s e)  = None"  
-"constVal (Callee l e)    = None" 
+| "constVal (Call accC statT mode objRef mn pTs args) = None"
+| "constVal (Methd C sig)   = None" 
+| "constVal (Body  C s)     = None"   
+| "constVal (InsInitE s e)  = None"  
+| "constVal (Callee l e)    = None" 
 
 lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]: 
   assumes const: "constVal e = Some v" and
@@ -282,55 +280,55 @@
 to a specific boolean value. If the expression cannot evaluate to a 
 @{term Boolean} value UNIV is returned. If we expect true/false the opposite 
 constant false/true will also lead to UNIV. *}
-consts assigns_if:: "bool \<Rightarrow> expr \<Rightarrow> lname set" 
-primrec
-"assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*} 
-"assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
-"assigns_if b (Cast t e)          = assigns_if b e" 
-"assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
-                                                     e is a reference type*}
-"assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
-"assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
-                                         None   \<Rightarrow> (if unop = UNot 
-                                                       then assigns_if (\<not>b) e
-                                                       else UNIV)
-                                       | Some v \<Rightarrow> (if v=Bool b 
-                                                       then {} 
-                                                       else UNIV))"
-"assigns_if b (BinOp binop e1 e2) 
-  = (case constVal (BinOp binop e1 e2) of
-       None \<Rightarrow> (if binop=CondAnd then
-                   (case b of 
-                       True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
-                    |  False \<Rightarrow> assigns_if False e1 \<inter> 
-                                (assigns_if True e1 \<union> assigns_if False e2))
-                else
-               (if binop=CondOr then
-                   (case b of 
-                       True  \<Rightarrow> assigns_if True e1 \<inter> 
-                                (assigns_if False e1 \<union> assigns_if True e2)
-                    |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
-                else assignsE e1 \<union> assignsE e2))
-     | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
+primrec assigns_if :: "bool \<Rightarrow> expr \<Rightarrow> lname set"
+where
+  "assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*} 
+| "assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (Cast t e)          = assigns_if b e" 
+| "assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
+                                                       e is a reference type*}
+| "assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
+| "assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
+                                           None   \<Rightarrow> (if unop = UNot 
+                                                         then assigns_if (\<not>b) e
+                                                         else UNIV)
+                                         | Some v \<Rightarrow> (if v=Bool b 
+                                                         then {} 
+                                                         else UNIV))"
+| "assigns_if b (BinOp binop e1 e2) 
+    = (case constVal (BinOp binop e1 e2) of
+         None \<Rightarrow> (if binop=CondAnd then
+                     (case b of 
+                         True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
+                      |  False \<Rightarrow> assigns_if False e1 \<inter> 
+                                  (assigns_if True e1 \<union> assigns_if False e2))
+                  else
+                 (if binop=CondOr then
+                     (case b of 
+                         True  \<Rightarrow> assigns_if True e1 \<inter> 
+                                  (assigns_if False e1 \<union> assigns_if True e2)
+                      |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
+                  else assignsE e1 \<union> assignsE e2))
+       | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
 
-"assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
-"assigns_if b (Acc v)      = (assignsV v)"
-"assigns_if b (v := e)     = (assignsE (Ass v e))"
-"assigns_if b (c? e1 : e2) = (assignsE c) \<union>
-                               (case (constVal c) of
-                                  None    \<Rightarrow> (assigns_if b e1) \<inter> 
-                                             (assigns_if b e2)
-                                | Some bv \<Rightarrow> (case the_Bool bv of
-                                                True  \<Rightarrow> assigns_if b e1
-                                              | False \<Rightarrow> assigns_if b e2))"
-"assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
-          = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
+| "assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (Acc v)      = (assignsV v)"
+| "assigns_if b (v := e)     = (assignsE (Ass v e))"
+| "assigns_if b (c? e1 : e2) = (assignsE c) \<union>
+                                 (case (constVal c) of
+                                    None    \<Rightarrow> (assigns_if b e1) \<inter> 
+                                               (assigns_if b e2)
+                                  | Some bv \<Rightarrow> (case the_Bool bv of
+                                                  True  \<Rightarrow> assigns_if b e1
+                                                | False \<Rightarrow> assigns_if b e2))"
+| "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
+            = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
 -- {* Only dummy analysis for intermediate expressions  
       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
-"assigns_if b (Methd C sig)   = {}" 
-"assigns_if b (Body  C s)     = {}"   
-"assigns_if b (InsInitE s e)  = {}"  
-"assigns_if b (Callee l e)    = {}" 
+| "assigns_if b (Methd C sig)   = {}" 
+| "assigns_if b (Body  C s)     = {}"   
+| "assigns_if b (InsInitE s e)  = {}"  
+| "assigns_if b (Callee l e)    = {}" 
 
 lemma assigns_if_const_b_simp:
   assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
@@ -429,14 +427,17 @@
 
 subsection {* Lifting set operations to range of tables (map to a set) *}
 
-definition union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65) where
- "A \<Rightarrow>\<union> B \<equiv> \<lambda> k. A k \<union> B k"
+definition
+  union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65)
+  where "A \<Rightarrow>\<union> B = (\<lambda> k. A k \<union> B k)"
 
-definition intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71) where
- "A \<Rightarrow>\<inter>  B \<equiv> \<lambda> k. A k \<inter> B k"
+definition
+  intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71)
+  where "A \<Rightarrow>\<inter>  B = (\<lambda>k. A k \<inter> B k)"
 
-definition all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40) where 
- "A \<Rightarrow>\<union>\<^sub>\<forall> B \<equiv> \<lambda> k. A k \<union> B"
+definition
+  all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40)
+  where "(A \<Rightarrow>\<union>\<^sub>\<forall> B) = (\<lambda> k. A k \<union> B)"
   
 subsubsection {* Binary union of tables *}
 
@@ -507,16 +508,19 @@
          brk :: "breakass" --{* Definetly assigned variables for 
                                 abrupt completion with a break *}
 
-definition rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" where
-"rmlab k A \<equiv> \<lambda> x. if x=k then UNIV else A x"
+definition
+  rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
+  where "rmlab k A = (\<lambda>x. if x=k then UNIV else A x)"
  
 (*
-definition setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
-"setbrk b A \<equiv> {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
+definition
+  setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
+  "setbrk b A = {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
 *)
 
-definition range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80) where 
- "\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}"
+definition
+  range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)
+  where "\<Rightarrow>\<Inter>A = {x |x. \<forall> k. x \<in> A k}"
 
 text {*
 In @{text "E\<turnstile> B \<guillemotright>t\<guillemotright> A"},