--- 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 *)