merged
authorbulwahn
Tue, 28 Sep 2010 13:44:06 +0200
changeset 39768 1c46d4f8afd2
parent 39767 327e463531e4 (current diff)
parent 39759 b4bd83468600 (diff)
child 39769 5bcf4253d579
child 39773 38852e989efa
merged
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/doc-src/Classes/IsaMakefile	Tue Sep 28 11:59:58 2010 +0200
+++ b/doc-src/Classes/IsaMakefile	Tue Sep 28 13:44:06 2010 +0200
@@ -23,10 +23,10 @@
 
 Thy: $(THY)
 
-$(THY): Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML
+$(THY): $(OUT)/HOL Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML
 	@$(USEDIR) HOL Thy
 	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	 Thy/document/pdfsetup.sty Thy/document/session.tex
+	  Thy/document/pdfsetup.sty Thy/document/session.tex
 
 
 ## clean
--- a/src/HOL/IsaMakefile	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 28 13:44:06 2010 +0200
@@ -1053,7 +1053,7 @@
   SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy		\
   SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy	\
   SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy	\
-  SET_Protocol/document/root.tex
+  SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
 
 
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -18,11 +18,11 @@
 
 
 section {*  Executability of @{term check_bounded} *}
-consts
-  list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
-primrec
+
+primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
+where
   "list_all'_rec P n []     = True"
-  "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
+| "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
 
 definition list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   "list_all' P xs \<equiv> list_all'_rec P 0 xs"
--- a/src/HOL/MicroJava/Comp/TranslComp.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/MicroJava/Comp/TranslComp.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -8,71 +8,69 @@
 
 
 (* parameter java_mb only serves to define function index later *)
-consts
- compExpr  :: "java_mb => expr      => instr list"
- compExprs :: "java_mb => expr list => instr list"
- compStmt  :: "java_mb => stmt      => instr list"
-
 
 
 (**********************************************************************)
 (** code generation for expressions **)
 
-primrec
+primrec compExpr :: "java_mb => expr => instr list"
+  and compExprs :: "java_mb => expr list => instr list"
+where
+
 (*class instance creation*)
-"compExpr jmb (NewC c) = [New c]"
+"compExpr jmb (NewC c) = [New c]" |
 
 (*type cast*)
-"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" 
+"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" |
 
 
 (*literals*)
-"compExpr jmb (Lit val) = [LitPush val]" 
+"compExpr jmb (Lit val) = [LitPush val]" |
 
       
 (* binary operation *)                         
 "compExpr jmb (BinOp bo e1 e2) = compExpr jmb e1 @ compExpr jmb e2 @ 
   (case bo of Eq => [Ifcmpeq 3,LitPush(Bool False),Goto 2,LitPush(Bool True)]
-            | Add => [IAdd])" 
+            | Add => [IAdd])" |
 
 (*local variable*)
-"compExpr jmb (LAcc vn) = [Load (index jmb vn)]" 
+"compExpr jmb (LAcc vn) = [Load (index jmb vn)]" |
 
 
 (*assignement*)
-"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" 
+"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" |
 
 
 (*field access*)
-"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]"
+"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]" |
 
 
 (*field assignement - expected syntax:  {_}_.._:=_ *)
 "compExpr jmb (FAss cn e1 fn e2 ) = 
-       compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]"
+       compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]" |
 
 
 (*method call*)
 "compExpr jmb (Call cn e1 mn X ps) = 
-        compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]"
+        compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]" |
 
 
 (** code generation expression lists **)
 
-"compExprs jmb []     = []"
+"compExprs jmb []     = []" |
 
 "compExprs jmb (e#es) = compExpr jmb e @ compExprs jmb es"
 
-  
 
-primrec
+primrec compStmt :: "java_mb => stmt => instr list" where
+
 (** code generation for statements **)
 
-"compStmt jmb Skip = []"                        
+"compStmt jmb Skip = []" |
 
-"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])"
+"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])" |
 
-"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))"
+"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))" |
 
 "compStmt jmb (If(e) c1 Else c2) =
         (let cnstf = LitPush (Bool False);
@@ -82,7 +80,7 @@
              test  = Ifcmpeq (int(length thn +2)); 
              thnex = Goto (int(length els +1))
          in
-         [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)"
+         [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)" |
 
 "compStmt jmb (While(e) c) =
         (let cnstf = LitPush (Bool False);
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -45,16 +45,6 @@
   sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
   where "sttp_of == snd"
 
-consts
-  compTpExpr  :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr
-                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
-  compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list
-                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
-  compTpStmt  :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt
-                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
 definition nochangeST :: "state_type \<Rightarrow> method_type \<times> state_type" where
   "nochangeST sttp == ([Some sttp], sttp)"
 
@@ -80,60 +70,45 @@
 
 (* Expressions *)
 
-primrec
-
+primrec compTpExpr :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr \<Rightarrow>
+    state_type \<Rightarrow> method_type \<times> state_type"
+  and compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list \<Rightarrow>
+    state_type \<Rightarrow> method_type \<times> state_type"
+where
   "compTpExpr jmb G (NewC c) = pushST [Class c]"
-
-  "compTpExpr jmb G (Cast c e) = 
-  (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
-
-  "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
-
-  "compTpExpr jmb G (BinOp bo e1 e2) = 
+| "compTpExpr jmb G (Cast c e) = (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
+| "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
+| "compTpExpr jmb G (BinOp bo e1 e2) =
      (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> 
      (case bo of 
        Eq => popST 2 \<box> pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]
      | Add => replST 2 (PrimT Integer))"
-
-  "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT). 
+| "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT). 
       pushST [ok_val (LT ! (index jmb vn))] (ST, LT))"
-
-  "compTpExpr jmb G (vn::=e) = 
+| "compTpExpr jmb G (vn::=e) = 
       (compTpExpr jmb G e) \<box> dupST \<box> (popST 1)"
-
-
-  "compTpExpr jmb G ( {cn}e..fn ) = 
+| "compTpExpr jmb G ( {cn}e..fn ) = 
       (compTpExpr jmb G e) \<box> replST 1 (snd (the (field (G,cn) fn)))"
-
-  "compTpExpr jmb G (FAss cn e1 fn e2 ) = 
+| "compTpExpr jmb G (FAss cn e1 fn e2 ) = 
       (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> dup_x1ST \<box> (popST 2)"
-
-
-  "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
+| "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
        (compTpExpr jmb G a) \<box> (compTpExprs jmb G ps) \<box> 
        (replST ((length ps) + 1) (method_rT (the (method (G,C) (mn,fpTs)))))"
-
-
-(* Expression lists *)
-
-  "compTpExprs jmb G [] = comb_nil"
-
-  "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
+| "compTpExprs jmb G [] = comb_nil"
+| "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
 
 
 (* Statements *)
-primrec
-   "compTpStmt jmb G Skip = comb_nil"
-
-   "compTpStmt jmb G (Expr e) =  (compTpExpr jmb G e) \<box> popST 1"
-
-   "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
-
-   "compTpStmt jmb G (If(e) c1 Else c2) = 
+primrec compTpStmt :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt \<Rightarrow> 
+    state_type \<Rightarrow> method_type \<times> state_type"
+where
+  "compTpStmt jmb G Skip = comb_nil"
+| "compTpStmt jmb G (Expr e) =  (compTpExpr jmb G e) \<box> popST 1"
+| "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
+| "compTpStmt jmb G (If(e) c1 Else c2) = 
       (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
       (compTpStmt jmb G c1) \<box> nochangeST \<box> (compTpStmt jmb G c2)"
-
-   "compTpStmt jmb G (While(e) c) = 
+| "compTpStmt jmb G (While(e) c) = 
       (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
       (compTpStmt jmb G c) \<box> nochangeST"
 
@@ -141,13 +116,11 @@
                    \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type" where
   "compTpInit jmb == (\<lambda> (vn,ty). (pushST [ty]) \<box>  (storeST (index jmb vn) ty))"
 
-consts
-  compTpInitLvars :: "[java_mb, (vname \<times> ty) list] 
-                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
-primrec 
+primrec compTpInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow>
+    state_type \<Rightarrow> method_type \<times> state_type"
+where
   "compTpInitLvars jmb [] = comb_nil"
-  "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
+| "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
 
 definition start_ST :: "opstack_type" where
   "start_ST == []"
--- a/src/HOL/MicroJava/DFA/Err.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -47,11 +47,9 @@
   where "err_semilat L == semilat(Err.sl L)"
 
 
-consts
-  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
-primrec
+primrec strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)" where
   "strict f Err    = Err"
-  "strict f (OK x) = f x"
+| "strict f (OK x) = f x"
 
 lemma strict_Some [simp]: 
   "(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
--- a/src/HOL/MicroJava/J/Value.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/MicroJava/J/Value.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -22,31 +22,22 @@
                    of clash with HOL/Set.thy" 
   | Addr loc    -- "addresses, i.e. locations of objects "
 
-consts
-  the_Bool :: "val => bool"
-  the_Intg :: "val => int"
-  the_Addr :: "val => loc"
-
-primrec
+primrec the_Bool :: "val => bool" where
   "the_Bool (Bool b) = b"
 
-primrec
+primrec the_Intg :: "val => int" where
   "the_Intg (Intg i) = i"
 
-primrec
+primrec the_Addr :: "val => loc" where
   "the_Addr (Addr a) = a"
 
-consts
-  defpval :: "prim_ty => val"  -- "default value for primitive types"
-  default_val :: "ty => val"   -- "default value for all types"
-
-primrec
+primrec defpval :: "prim_ty => val"  -- "default value for primitive types" where
   "defpval Void    = Unit"
-  "defpval Boolean = Bool False"
-  "defpval Integer = Intg 0"
+| "defpval Boolean = Bool False"
+| "defpval Integer = Intg 0"
 
-primrec
+primrec default_val :: "ty => val"   -- "default value for all types" where
   "default_val (PrimT pt) = defpval pt"
-  "default_val (RefT  r ) = Null"
+| "default_val (RefT  r ) = Null"
 
 end
--- a/src/HOL/MicroJava/J/WellType.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -73,15 +73,13 @@
                          THEN max_spec2appl_meths, THEN appl_methsD]
 
 
-consts
-  typeof :: "(loc => ty option) => val => ty option"
-
-primrec
+primrec typeof :: "(loc => ty option) => val => ty option"
+where
   "typeof dt  Unit    = Some (PrimT Void)"
-  "typeof dt  Null    = Some NT"
-  "typeof dt (Bool b) = Some (PrimT Boolean)"
-  "typeof dt (Intg i) = Some (PrimT Integer)"
-  "typeof dt (Addr a) = dt a"
+| "typeof dt  Null    = Some NT"
+| "typeof dt (Bool b) = Some (PrimT Boolean)"
+| "typeof dt (Intg i) = Some (PrimT Integer)"
+| "typeof dt (Addr a) = dt a"
 
 lemma is_type_typeof [rule_format (no_asm), simp]: 
   "(\<forall>a. v \<noteq> Addr a) --> (\<exists>T. typeof t v = Some T \<and> is_type G T)"
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -13,12 +13,11 @@
                  start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"
 
 
-consts
-  match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
-                          \<Rightarrow> p_count option"
-primrec
+primrec match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
+    \<Rightarrow> p_count option"
+where
   "match_exception_table G cn pc []     = None"
-  "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
+| "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
                                            then Some (fst (snd (snd e))) 
                                            else match_exception_table G cn pc es)"
 
@@ -27,11 +26,11 @@
   where "ex_table_of m == snd (snd (snd m))"
 
 
-consts
-  find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list \<Rightarrow> jvm_state"
-primrec
+primrec find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list
+    \<Rightarrow> jvm_state"
+where
   "find_handler G xcpt hp [] = (xcpt, hp, [])"
-  "find_handler G xcpt hp (fr#frs) = 
+| "find_handler G xcpt hp (fr#frs) = 
       (case xcpt of
          None \<Rightarrow> (None, hp, fr#frs)
        | Some xc \<Rightarrow> 
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/JVM/JVMExecInstr.thy
-    ID:         $Id$
     Author:     Cornelia Pusch, Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
@@ -11,18 +10,16 @@
 theory JVMExecInstr imports JVMInstructions JVMState begin
 
 
-consts
-  exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
-                  cname, sig, p_count, frame list] => jvm_state"
-primrec
+primrec exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
+where
  "exec_instr (Load idx) G hp stk vars Cl sig pc frs = 
-      (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
+      (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr (Store idx) G hp stk vars Cl sig pc frs = 
-      (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)"
+      (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)" |
 
  "exec_instr (LitPush v) G hp stk vars Cl sig pc frs = 
-      (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)"
+      (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr (New C) G hp stk vars Cl sig pc frs = 
   (let (oref,xp') = new_Addr hp;
@@ -30,7 +27,7 @@
        hp'  = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
        pc'  = if xp'=None then pc+1 else pc
    in 
-      (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))"
+      (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Getfield F C) G hp stk vars Cl sig pc frs = 
   (let oref = hd stk;
@@ -38,7 +35,7 @@
        (oc,fs)  = the(hp(the_Addr oref));
        pc'  = if xp'=None then pc+1 else pc
    in
-      (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))"
+      (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Putfield F C) G hp stk vars Cl sig pc frs = 
   (let (fval,oref)= (hd stk, hd(tl stk));
@@ -48,7 +45,7 @@
        hp'  = if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp;
        pc'  = if xp'=None then pc+1 else pc
    in
-      (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))"
+      (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
   (let oref = hd stk;
@@ -56,7 +53,7 @@
        stk' = if xp'=None then stk else tl stk;
        pc'  = if xp'=None then pc+1 else pc
    in
-      (xp', hp, (stk', vars, Cl, sig, pc')#frs))"
+      (xp', hp, (stk', vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
   (let n    = length ps;
@@ -69,7 +66,7 @@
                 [([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)]
               else []
    in 
-      (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" 
+      (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" |
   -- "Because exception handling needs the pc of the Invoke instruction,"
   -- "Invoke doesn't change stk and pc yet (@{text Return} does that)."
 
@@ -82,42 +79,42 @@
    in 
       (None, hp, (val#(drop (n+1) stk),loc,C,sig,pc+1)#tl frs))"
   -- "Return drops arguments from the caller's stack and increases"
-  -- "the program counter in the caller"
+  -- "the program counter in the caller" |
 
  "exec_instr Pop G hp stk vars Cl sig pc frs = 
-      (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)"
+      (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr Dup G hp stk vars Cl sig pc frs = 
-      (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)"
+      (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr Dup_x1 G hp stk vars Cl sig pc frs = 
       (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), 
-                  vars, Cl, sig, pc+1)#frs)"
+                  vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr Dup_x2 G hp stk vars Cl sig pc frs = 
       (None, hp, 
        (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
-       vars, Cl, sig, pc+1)#frs)"
+       vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr Swap G hp stk vars Cl sig pc frs =
   (let (val1,val2) = (hd stk,hd (tl stk))
    in
-      (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
+      (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))" |
 
  "exec_instr IAdd G hp stk vars Cl sig pc frs =
   (let (val1,val2) = (hd stk,hd (tl stk))
    in
       (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), 
-       vars, Cl, sig, pc+1)#frs))"
+       vars, Cl, sig, pc+1)#frs))" |
 
  "exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
   (let (val1,val2) = (hd stk, hd (tl stk));
      pc' = if val1 = val2 then nat(int pc+i) else pc+1
    in
-      (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))"
+      (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Goto i) G hp stk vars Cl sig pc frs =
-      (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)"
+      (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)" |
 
  "exec_instr Throw G hp stk vars Cl sig pc frs =
   (let xcpt  = raise_system_xcpt (hd stk = Null) NullPointer;
--- a/src/HOL/NanoJava/Example.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/NanoJava/Example.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -5,7 +5,9 @@
 
 header "Example"
 
-theory Example imports Equivalence begin
+theory Example
+imports Equivalence
+begin
 
 text {*
 
@@ -89,9 +91,9 @@
 
 subsection "``atleast'' relation for interpretation of Nat ``values''"
 
-consts Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50)
-primrec "s:x\<ge>0     = (x\<noteq>Null)"
-        "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
+primrec Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50) where
+  "s:x\<ge>0     = (x\<noteq>Null)"
+| "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
 
 lemma Nat_atleast_lupd [rule_format, simp]: 
  "\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -21,44 +21,36 @@
 
 subsection{*Predicate Formalizing the Encryption Association between Keys *}
 
-consts
-  KeyCryptKey :: "[key, key, event list] => bool"
-
-primrec
-
-KeyCryptKey_Nil:
-  "KeyCryptKey DK K [] = False"
-
-KeyCryptKey_Cons:
+primrec KeyCryptKey :: "[key, key, event list] => bool"
+where
+  KeyCryptKey_Nil:
+    "KeyCryptKey DK K [] = False"
+| KeyCryptKey_Cons:
       --{*Says is the only important case.
         1st case: CR5, where KC3 encrypts KC2.
         2nd case: any use of priEK C.
         Revision 1.12 has a more complicated version with separate treatment of
           the dependency of KC1, KC2 and KC3 on priEK (CA i.)  Not needed since
           priEK C is never sent (and so can't be lost except at the start). *}
-  "KeyCryptKey DK K (ev # evs) =
-   (KeyCryptKey DK K evs |
-    (case ev of
-      Says A B Z =>
-       ((\<exists>N X Y. A \<noteq> Spy &
+    "KeyCryptKey DK K (ev # evs) =
+     (KeyCryptKey DK K evs |
+      (case ev of
+        Says A B Z =>
+         ((\<exists>N X Y. A \<noteq> Spy &
                  DK \<in> symKeys &
                  Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
-        (\<exists>C. DK = priEK C))
-    | Gets A' X => False
-    | Notes A' X => False))"
+          (\<exists>C. DK = priEK C))
+      | Gets A' X => False
+      | Notes A' X => False))"
 
 
 subsection{*Predicate formalizing the association between keys and nonces *}
 
-consts
-  KeyCryptNonce :: "[key, key, event list] => bool"
-
-primrec
-
-KeyCryptNonce_Nil:
-  "KeyCryptNonce EK K [] = False"
-
-KeyCryptNonce_Cons:
+primrec KeyCryptNonce :: "[key, key, event list] => bool"
+where
+  KeyCryptNonce_Nil:
+    "KeyCryptNonce EK K [] = False"
+| KeyCryptNonce_Cons:
   --{*Says is the only important case.
     1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
     2nd case: CR5, where KC3 encrypts NC3;
--- a/src/HOL/SET_Protocol/Event_SET.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/SET_Protocol/Event_SET.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -35,15 +35,14 @@
 
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: "agent => msg set"
-  knows  :: "[agent, event list] => msg set"
 
 (* Message reception does not extend spy's knowledge because of
    reception invariant enforced by Reception rule in protocol definition*)
-primrec
-
-knows_Nil:
-  "knows A []       = initState A"
-knows_Cons:
+primrec knows :: "[agent, event list] => msg set"
+where
+  knows_Nil:
+    "knows A [] = initState A"
+| knows_Cons:
     "knows A (ev # evs) =
        (if A = Spy then
         (case ev of
@@ -63,15 +62,13 @@
 
 subsection{*Used Messages*}
 
-consts
+primrec used :: "event list => msg set"
+where
   (*Set of items that might be visible to somebody:
-    complement of the set of fresh items*)
-  used :: "event list => msg set"
-
-(* As above, message reception does extend used items *)
-primrec
+    complement of the set of fresh items.
+    As above, message reception does extend used items *)
   used_Nil:  "used []         = (UN B. parts (initState B))"
-  used_Cons: "used (ev # evs) =
+| used_Cons: "used (ev # evs) =
                  (case ev of
                     Says A B X => parts {X} Un (used evs)
                   | Gets A X   => used evs
--- a/src/HOL/SET_Protocol/Public_SET.thy	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Tue Sep 28 13:44:06 2010 +0200
@@ -64,7 +64,11 @@
    RCA and CAs know their own respective keys;
    RCA (has already certified and therefore) knows all CAs public keys; 
    Spy knows all keys of all bad agents.*}
-primrec    
+
+overloading initState \<equiv> "initState"
+begin
+
+primrec initState where
 (*<*)
   initState_CA:
     "initState (CA i)  =
@@ -74,29 +78,31 @@
               Key (pubEK (CA i)), Key (pubSK (CA i)),
               Key (pubEK RCA), Key (pubSK RCA)})"
 
-  initState_Cardholder:
+| initState_Cardholder:
     "initState (Cardholder i)  =    
        {Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
         Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
         Key (pubEK RCA), Key (pubSK RCA)}"
 
-  initState_Merchant:
+| initState_Merchant:
     "initState (Merchant i)  =    
        {Key (priEK (Merchant i)), Key (priSK (Merchant i)),
         Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
         Key (pubEK RCA), Key (pubSK RCA)}"
 
-  initState_PG:
+| initState_PG:
     "initState (PG i)  = 
        {Key (priEK (PG i)), Key (priSK (PG i)),
         Key (pubEK (PG i)), Key (pubSK (PG i)),
         Key (pubEK RCA), Key (pubSK RCA)}"
 (*>*)
-  initState_Spy:
+| initState_Spy:
     "initState Spy = Key ` (invKey ` pubEK ` bad Un
                             invKey ` pubSK ` bad Un
                             range pubEK Un range pubSK)"
 
+end
+
 
 text{*Injective mapping from agents to PANs: an agent can have only one card*}
 
--- a/src/HOL/SET_Protocol/ROOT.ML	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/SET_Protocol/ROOT.ML	Tue Sep 28 13:44:06 2010 +0200
@@ -1,9 +1,3 @@
-(*  Title:      HOL/SET_Protocol/ROOT.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2003  University of Cambridge
-
-Root file for the SET protocol proofs.
-*)
 
 no_document use_thys ["Nat_Bijection"];
-use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];
+use_thys ["SET_Protocol"];
--- a/src/HOL/Tools/Function/function_lib.ML	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Tue Sep 28 13:44:06 2010 +0200
@@ -18,17 +18,6 @@
 fun plural sg pl [x] = sg
   | plural sg pl _ = pl
 
-(* lambda-abstracts over an arbitrarily nested tuple
-  ==> hologic.ML? *)
-fun tupled_lambda vars t =
-  case vars of
-    (Free v) => lambda (Free v) t
-  | (Var v) => lambda (Var v) t
-  | (Const (@{const_name Pair}, Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
-      (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
-  | _ => raise Match
-
-
 fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
   let
     val (n, body) = Term.dest_abs a
--- a/src/HOL/Tools/Function/induction_schema.ML	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Tue Sep 28 13:44:06 2010 +0200
@@ -196,7 +196,7 @@
       |> fold_rev (Logic.all o Free) ws
       |> term_conv thy ind_atomize
       |> Object_Logic.drop_judgment thy
-      |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
+      |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   in
     SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
   end
--- a/src/HOL/Tools/Function/mutual.ML	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Tue Sep 28 13:44:06 2010 +0200
@@ -221,7 +221,7 @@
         val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
         val atup = foldr1 HOLogic.mk_prod avars
       in
-        tupled_lambda atup (list_comb (P, avars))
+        HOLogic.tupled_lambda atup (list_comb (P, avars))
       end
 
     val Ps = map2 mk_P parts newPs
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 13:44:06 2010 +0200
@@ -2021,12 +2021,6 @@
       (fn NONE => "X" | SOME k' => string_of_int k')
         (ks @ [SOME k]))) arities));
 
-fun split_lambda (x as Free _) t = lambda x t
-  | split_lambda (Const (@{const_name Pair}, _) $ t1 $ t2) t =
-    HOLogic.mk_split (split_lambda t1 (split_lambda t2 t))
-  | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
-  | split_lambda t _ = raise (TERM ("split_lambda", [t]))
-
 fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
   | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   | strip_split_abs t = t
@@ -2051,7 +2045,7 @@
       val x = Name.variant names "x"
       val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
       val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
-      val t = fold_rev split_lambda args (PredicateCompFuns.mk_Eval
+      val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
         (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
     in
       (if is_eval then t else Free (x, funT), x :: names)
@@ -2142,8 +2136,8 @@
             val (r, _) = PredicateCompFuns.dest_Eval t'
           in (SOME (fst (strip_comb r)), NONE) end
         val (inargs, outargs) = split_map_mode strip_eval mode args
-        val predterm = fold_rev split_lambda inargs
-          (PredicateCompFuns.mk_Enum (split_lambda (HOLogic.mk_tuple outargs)
+        val predterm = fold_rev HOLogic.tupled_lambda inargs
+          (PredicateCompFuns.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
             (list_comb (Const (name, T), args))))
         val lhs = Const (mode_cname, funT)
         val def = Logic.mk_equals (lhs, predterm)
@@ -3269,7 +3263,7 @@
         val t_pred = compile_expr comp_modifiers ctxt
           (body, deriv) [] additional_arguments;
         val T_pred = dest_predT compfuns (fastype_of t_pred)
-        val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
+        val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output_tuple
       in
         if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred
       end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Sep 28 13:44:06 2010 +0200
@@ -177,15 +177,7 @@
 val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
 val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
 
-fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
-  | mk_split_lambda [x] t = lambda x t
-  | mk_split_lambda xs t =
-  let
-    fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
-      | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
-  in
-    mk_split_lambda' xs t
-  end;
+val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
 
 fun cpu_time description f =
   let
--- a/src/HOL/Tools/hologic.ML	Tue Sep 28 11:59:58 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Tue Sep 28 13:44:06 2010 +0200
@@ -67,6 +67,7 @@
   val split_const: typ * typ * typ -> term
   val mk_split: term -> term
   val flatten_tupleT: typ -> typ list
+  val tupled_lambda: term -> term -> term
   val mk_tupleT: typ list -> typ
   val strip_tupleT: typ -> typ list
   val mk_tuple: term list -> term
@@ -327,6 +328,15 @@
 fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
   | flatten_tupleT T = [T];
 
+(*abstraction over nested tuples*)
+fun tupled_lambda (x as Free _) b = lambda x b
+  | tupled_lambda (x as Var _) b = lambda x b
+  | tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b =
+      mk_split (tupled_lambda u (tupled_lambda v b))
+  | tupled_lambda (Const ("Product_Type.Unity", _)) b =
+      Abs ("x", unitT, b)
+  | tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]);
+
 
 (* tuples with right-fold structure *)