1.1 --- a/doc-src/Classes/IsaMakefile Tue Sep 28 11:59:58 2010 +0200
1.2 +++ b/doc-src/Classes/IsaMakefile Tue Sep 28 13:44:06 2010 +0200
1.3 @@ -23,10 +23,10 @@
1.4
1.5 Thy: $(THY)
1.6
1.7 -$(THY): Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML
1.8 +$(THY): $(OUT)/HOL Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML
1.9 @$(USEDIR) HOL Thy
1.10 @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
1.11 - Thy/document/pdfsetup.sty Thy/document/session.tex
1.12 + Thy/document/pdfsetup.sty Thy/document/session.tex
1.13
1.14
1.15 ## clean
2.1 --- a/src/HOL/IsaMakefile Tue Sep 28 11:59:58 2010 +0200
2.2 +++ b/src/HOL/IsaMakefile Tue Sep 28 13:44:06 2010 +0200
2.3 @@ -1053,7 +1053,7 @@
2.4 SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \
2.5 SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \
2.6 SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \
2.7 - SET_Protocol/document/root.tex
2.8 + SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex
2.9 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
2.10
2.11
3.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Tue Sep 28 11:59:58 2010 +0200
3.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Tue Sep 28 13:44:06 2010 +0200
3.3 @@ -18,11 +18,11 @@
3.4
3.5
3.6 section {* Executability of @{term check_bounded} *}
3.7 -consts
3.8 - list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
3.9 -primrec
3.10 +
3.11 +primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
3.12 +where
3.13 "list_all'_rec P n [] = True"
3.14 - "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
3.15 +| "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
3.16
3.17 definition list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
3.18 "list_all' P xs \<equiv> list_all'_rec P 0 xs"
4.1 --- a/src/HOL/MicroJava/Comp/TranslComp.thy Tue Sep 28 11:59:58 2010 +0200
4.2 +++ b/src/HOL/MicroJava/Comp/TranslComp.thy Tue Sep 28 13:44:06 2010 +0200
4.3 @@ -8,71 +8,69 @@
4.4
4.5
4.6 (* parameter java_mb only serves to define function index later *)
4.7 -consts
4.8 - compExpr :: "java_mb => expr => instr list"
4.9 - compExprs :: "java_mb => expr list => instr list"
4.10 - compStmt :: "java_mb => stmt => instr list"
4.11 -
4.12
4.13
4.14 (**********************************************************************)
4.15 (** code generation for expressions **)
4.16
4.17 -primrec
4.18 +primrec compExpr :: "java_mb => expr => instr list"
4.19 + and compExprs :: "java_mb => expr list => instr list"
4.20 +where
4.21 +
4.22 (*class instance creation*)
4.23 -"compExpr jmb (NewC c) = [New c]"
4.24 +"compExpr jmb (NewC c) = [New c]" |
4.25
4.26 (*type cast*)
4.27 -"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]"
4.28 +"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" |
4.29
4.30
4.31 (*literals*)
4.32 -"compExpr jmb (Lit val) = [LitPush val]"
4.33 +"compExpr jmb (Lit val) = [LitPush val]" |
4.34
4.35
4.36 (* binary operation *)
4.37 "compExpr jmb (BinOp bo e1 e2) = compExpr jmb e1 @ compExpr jmb e2 @
4.38 (case bo of Eq => [Ifcmpeq 3,LitPush(Bool False),Goto 2,LitPush(Bool True)]
4.39 - | Add => [IAdd])"
4.40 + | Add => [IAdd])" |
4.41
4.42 (*local variable*)
4.43 -"compExpr jmb (LAcc vn) = [Load (index jmb vn)]"
4.44 +"compExpr jmb (LAcc vn) = [Load (index jmb vn)]" |
4.45
4.46
4.47 (*assignement*)
4.48 -"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]"
4.49 +"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" |
4.50
4.51
4.52 (*field access*)
4.53 -"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]"
4.54 +"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]" |
4.55
4.56
4.57 (*field assignement - expected syntax: {_}_.._:=_ *)
4.58 "compExpr jmb (FAss cn e1 fn e2 ) =
4.59 - compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]"
4.60 + compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]" |
4.61
4.62
4.63 (*method call*)
4.64 "compExpr jmb (Call cn e1 mn X ps) =
4.65 - compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]"
4.66 + compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]" |
4.67
4.68
4.69 (** code generation expression lists **)
4.70
4.71 -"compExprs jmb [] = []"
4.72 +"compExprs jmb [] = []" |
4.73
4.74 "compExprs jmb (e#es) = compExpr jmb e @ compExprs jmb es"
4.75
4.76 -
4.77
4.78 -primrec
4.79 +primrec compStmt :: "java_mb => stmt => instr list" where
4.80 +
4.81 (** code generation for statements **)
4.82
4.83 -"compStmt jmb Skip = []"
4.84 +"compStmt jmb Skip = []" |
4.85
4.86 -"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])"
4.87 +"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])" |
4.88
4.89 -"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))"
4.90 +"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))" |
4.91
4.92 "compStmt jmb (If(e) c1 Else c2) =
4.93 (let cnstf = LitPush (Bool False);
4.94 @@ -82,7 +80,7 @@
4.95 test = Ifcmpeq (int(length thn +2));
4.96 thnex = Goto (int(length els +1))
4.97 in
4.98 - [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)"
4.99 + [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)" |
4.100
4.101 "compStmt jmb (While(e) c) =
4.102 (let cnstf = LitPush (Bool False);
5.1 --- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Tue Sep 28 11:59:58 2010 +0200
5.2 +++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Tue Sep 28 13:44:06 2010 +0200
5.3 @@ -45,16 +45,6 @@
5.4 sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
5.5 where "sttp_of == snd"
5.6
5.7 -consts
5.8 - compTpExpr :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr
5.9 - \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
5.10 -
5.11 - compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list
5.12 - \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
5.13 -
5.14 - compTpStmt :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt
5.15 - \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
5.16 -
5.17 definition nochangeST :: "state_type \<Rightarrow> method_type \<times> state_type" where
5.18 "nochangeST sttp == ([Some sttp], sttp)"
5.19
5.20 @@ -80,60 +70,45 @@
5.21
5.22 (* Expressions *)
5.23
5.24 -primrec
5.25 -
5.26 +primrec compTpExpr :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr \<Rightarrow>
5.27 + state_type \<Rightarrow> method_type \<times> state_type"
5.28 + and compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list \<Rightarrow>
5.29 + state_type \<Rightarrow> method_type \<times> state_type"
5.30 +where
5.31 "compTpExpr jmb G (NewC c) = pushST [Class c]"
5.32 -
5.33 - "compTpExpr jmb G (Cast c e) =
5.34 - (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
5.35 -
5.36 - "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
5.37 -
5.38 - "compTpExpr jmb G (BinOp bo e1 e2) =
5.39 +| "compTpExpr jmb G (Cast c e) = (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
5.40 +| "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
5.41 +| "compTpExpr jmb G (BinOp bo e1 e2) =
5.42 (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box>
5.43 (case bo of
5.44 Eq => popST 2 \<box> pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]
5.45 | Add => replST 2 (PrimT Integer))"
5.46 -
5.47 - "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT).
5.48 +| "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT).
5.49 pushST [ok_val (LT ! (index jmb vn))] (ST, LT))"
5.50 -
5.51 - "compTpExpr jmb G (vn::=e) =
5.52 +| "compTpExpr jmb G (vn::=e) =
5.53 (compTpExpr jmb G e) \<box> dupST \<box> (popST 1)"
5.54 -
5.55 -
5.56 - "compTpExpr jmb G ( {cn}e..fn ) =
5.57 +| "compTpExpr jmb G ( {cn}e..fn ) =
5.58 (compTpExpr jmb G e) \<box> replST 1 (snd (the (field (G,cn) fn)))"
5.59 -
5.60 - "compTpExpr jmb G (FAss cn e1 fn e2 ) =
5.61 +| "compTpExpr jmb G (FAss cn e1 fn e2 ) =
5.62 (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> dup_x1ST \<box> (popST 2)"
5.63 -
5.64 -
5.65 - "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
5.66 +| "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
5.67 (compTpExpr jmb G a) \<box> (compTpExprs jmb G ps) \<box>
5.68 (replST ((length ps) + 1) (method_rT (the (method (G,C) (mn,fpTs)))))"
5.69 -
5.70 -
5.71 -(* Expression lists *)
5.72 -
5.73 - "compTpExprs jmb G [] = comb_nil"
5.74 -
5.75 - "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
5.76 +| "compTpExprs jmb G [] = comb_nil"
5.77 +| "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
5.78
5.79
5.80 (* Statements *)
5.81 -primrec
5.82 - "compTpStmt jmb G Skip = comb_nil"
5.83 -
5.84 - "compTpStmt jmb G (Expr e) = (compTpExpr jmb G e) \<box> popST 1"
5.85 -
5.86 - "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
5.87 -
5.88 - "compTpStmt jmb G (If(e) c1 Else c2) =
5.89 +primrec compTpStmt :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt \<Rightarrow>
5.90 + state_type \<Rightarrow> method_type \<times> state_type"
5.91 +where
5.92 + "compTpStmt jmb G Skip = comb_nil"
5.93 +| "compTpStmt jmb G (Expr e) = (compTpExpr jmb G e) \<box> popST 1"
5.94 +| "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
5.95 +| "compTpStmt jmb G (If(e) c1 Else c2) =
5.96 (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
5.97 (compTpStmt jmb G c1) \<box> nochangeST \<box> (compTpStmt jmb G c2)"
5.98 -
5.99 - "compTpStmt jmb G (While(e) c) =
5.100 +| "compTpStmt jmb G (While(e) c) =
5.101 (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
5.102 (compTpStmt jmb G c) \<box> nochangeST"
5.103
5.104 @@ -141,13 +116,11 @@
5.105 \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type" where
5.106 "compTpInit jmb == (\<lambda> (vn,ty). (pushST [ty]) \<box> (storeST (index jmb vn) ty))"
5.107
5.108 -consts
5.109 - compTpInitLvars :: "[java_mb, (vname \<times> ty) list]
5.110 - \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
5.111 -
5.112 -primrec
5.113 +primrec compTpInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow>
5.114 + state_type \<Rightarrow> method_type \<times> state_type"
5.115 +where
5.116 "compTpInitLvars jmb [] = comb_nil"
5.117 - "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
5.118 +| "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
5.119
5.120 definition start_ST :: "opstack_type" where
5.121 "start_ST == []"
6.1 --- a/src/HOL/MicroJava/DFA/Err.thy Tue Sep 28 11:59:58 2010 +0200
6.2 +++ b/src/HOL/MicroJava/DFA/Err.thy Tue Sep 28 13:44:06 2010 +0200
6.3 @@ -47,11 +47,9 @@
6.4 where "err_semilat L == semilat(Err.sl L)"
6.5
6.6
6.7 -consts
6.8 - strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
6.9 -primrec
6.10 +primrec strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)" where
6.11 "strict f Err = Err"
6.12 - "strict f (OK x) = f x"
6.13 +| "strict f (OK x) = f x"
6.14
6.15 lemma strict_Some [simp]:
6.16 "(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
7.1 --- a/src/HOL/MicroJava/J/Value.thy Tue Sep 28 11:59:58 2010 +0200
7.2 +++ b/src/HOL/MicroJava/J/Value.thy Tue Sep 28 13:44:06 2010 +0200
7.3 @@ -22,31 +22,22 @@
7.4 of clash with HOL/Set.thy"
7.5 | Addr loc -- "addresses, i.e. locations of objects "
7.6
7.7 -consts
7.8 - the_Bool :: "val => bool"
7.9 - the_Intg :: "val => int"
7.10 - the_Addr :: "val => loc"
7.11 -
7.12 -primrec
7.13 +primrec the_Bool :: "val => bool" where
7.14 "the_Bool (Bool b) = b"
7.15
7.16 -primrec
7.17 +primrec the_Intg :: "val => int" where
7.18 "the_Intg (Intg i) = i"
7.19
7.20 -primrec
7.21 +primrec the_Addr :: "val => loc" where
7.22 "the_Addr (Addr a) = a"
7.23
7.24 -consts
7.25 - defpval :: "prim_ty => val" -- "default value for primitive types"
7.26 - default_val :: "ty => val" -- "default value for all types"
7.27 +primrec defpval :: "prim_ty => val" -- "default value for primitive types" where
7.28 + "defpval Void = Unit"
7.29 +| "defpval Boolean = Bool False"
7.30 +| "defpval Integer = Intg 0"
7.31
7.32 -primrec
7.33 - "defpval Void = Unit"
7.34 - "defpval Boolean = Bool False"
7.35 - "defpval Integer = Intg 0"
7.36 -
7.37 -primrec
7.38 +primrec default_val :: "ty => val" -- "default value for all types" where
7.39 "default_val (PrimT pt) = defpval pt"
7.40 - "default_val (RefT r ) = Null"
7.41 +| "default_val (RefT r ) = Null"
7.42
7.43 end
8.1 --- a/src/HOL/MicroJava/J/WellType.thy Tue Sep 28 11:59:58 2010 +0200
8.2 +++ b/src/HOL/MicroJava/J/WellType.thy Tue Sep 28 13:44:06 2010 +0200
8.3 @@ -73,15 +73,13 @@
8.4 THEN max_spec2appl_meths, THEN appl_methsD]
8.5
8.6
8.7 -consts
8.8 - typeof :: "(loc => ty option) => val => ty option"
8.9 -
8.10 -primrec
8.11 +primrec typeof :: "(loc => ty option) => val => ty option"
8.12 +where
8.13 "typeof dt Unit = Some (PrimT Void)"
8.14 - "typeof dt Null = Some NT"
8.15 - "typeof dt (Bool b) = Some (PrimT Boolean)"
8.16 - "typeof dt (Intg i) = Some (PrimT Integer)"
8.17 - "typeof dt (Addr a) = dt a"
8.18 +| "typeof dt Null = Some NT"
8.19 +| "typeof dt (Bool b) = Some (PrimT Boolean)"
8.20 +| "typeof dt (Intg i) = Some (PrimT Integer)"
8.21 +| "typeof dt (Addr a) = dt a"
8.22
8.23 lemma is_type_typeof [rule_format (no_asm), simp]:
8.24 "(\<forall>a. v \<noteq> Addr a) --> (\<exists>T. typeof t v = Some T \<and> is_type G T)"
9.1 --- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Tue Sep 28 11:59:58 2010 +0200
9.2 +++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Tue Sep 28 13:44:06 2010 +0200
9.3 @@ -13,12 +13,11 @@
9.4 start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"
9.5
9.6
9.7 -consts
9.8 - match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
9.9 - \<Rightarrow> p_count option"
9.10 -primrec
9.11 +primrec match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
9.12 + \<Rightarrow> p_count option"
9.13 +where
9.14 "match_exception_table G cn pc [] = None"
9.15 - "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
9.16 +| "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
9.17 then Some (fst (snd (snd e)))
9.18 else match_exception_table G cn pc es)"
9.19
9.20 @@ -27,11 +26,11 @@
9.21 where "ex_table_of m == snd (snd (snd m))"
9.22
9.23
9.24 -consts
9.25 - find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list \<Rightarrow> jvm_state"
9.26 -primrec
9.27 +primrec find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list
9.28 + \<Rightarrow> jvm_state"
9.29 +where
9.30 "find_handler G xcpt hp [] = (xcpt, hp, [])"
9.31 - "find_handler G xcpt hp (fr#frs) =
9.32 +| "find_handler G xcpt hp (fr#frs) =
9.33 (case xcpt of
9.34 None \<Rightarrow> (None, hp, fr#frs)
9.35 | Some xc \<Rightarrow>
10.1 --- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Tue Sep 28 11:59:58 2010 +0200
10.2 +++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Tue Sep 28 13:44:06 2010 +0200
10.3 @@ -1,5 +1,4 @@
10.4 (* Title: HOL/MicroJava/JVM/JVMExecInstr.thy
10.5 - ID: $Id$
10.6 Author: Cornelia Pusch, Gerwin Klein
10.7 Copyright 1999 Technische Universitaet Muenchen
10.8 *)
10.9 @@ -11,18 +10,16 @@
10.10 theory JVMExecInstr imports JVMInstructions JVMState begin
10.11
10.12
10.13 -consts
10.14 - exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars,
10.15 - cname, sig, p_count, frame list] => jvm_state"
10.16 -primrec
10.17 +primrec exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
10.18 +where
10.19 "exec_instr (Load idx) G hp stk vars Cl sig pc frs =
10.20 - (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
10.21 + (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)" |
10.22
10.23 "exec_instr (Store idx) G hp stk vars Cl sig pc frs =
10.24 - (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)"
10.25 + (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)" |
10.26
10.27 "exec_instr (LitPush v) G hp stk vars Cl sig pc frs =
10.28 - (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)"
10.29 + (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)" |
10.30
10.31 "exec_instr (New C) G hp stk vars Cl sig pc frs =
10.32 (let (oref,xp') = new_Addr hp;
10.33 @@ -30,7 +27,7 @@
10.34 hp' = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
10.35 pc' = if xp'=None then pc+1 else pc
10.36 in
10.37 - (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))"
10.38 + (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))" |
10.39
10.40 "exec_instr (Getfield F C) G hp stk vars Cl sig pc frs =
10.41 (let oref = hd stk;
10.42 @@ -38,7 +35,7 @@
10.43 (oc,fs) = the(hp(the_Addr oref));
10.44 pc' = if xp'=None then pc+1 else pc
10.45 in
10.46 - (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))"
10.47 + (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))" |
10.48
10.49 "exec_instr (Putfield F C) G hp stk vars Cl sig pc frs =
10.50 (let (fval,oref)= (hd stk, hd(tl stk));
10.51 @@ -48,7 +45,7 @@
10.52 hp' = if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp;
10.53 pc' = if xp'=None then pc+1 else pc
10.54 in
10.55 - (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))"
10.56 + (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))" |
10.57
10.58 "exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
10.59 (let oref = hd stk;
10.60 @@ -56,7 +53,7 @@
10.61 stk' = if xp'=None then stk else tl stk;
10.62 pc' = if xp'=None then pc+1 else pc
10.63 in
10.64 - (xp', hp, (stk', vars, Cl, sig, pc')#frs))"
10.65 + (xp', hp, (stk', vars, Cl, sig, pc')#frs))" |
10.66
10.67 "exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
10.68 (let n = length ps;
10.69 @@ -69,7 +66,7 @@
10.70 [([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)]
10.71 else []
10.72 in
10.73 - (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))"
10.74 + (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" |
10.75 -- "Because exception handling needs the pc of the Invoke instruction,"
10.76 -- "Invoke doesn't change stk and pc yet (@{text Return} does that)."
10.77
10.78 @@ -82,42 +79,42 @@
10.79 in
10.80 (None, hp, (val#(drop (n+1) stk),loc,C,sig,pc+1)#tl frs))"
10.81 -- "Return drops arguments from the caller's stack and increases"
10.82 - -- "the program counter in the caller"
10.83 + -- "the program counter in the caller" |
10.84
10.85 "exec_instr Pop G hp stk vars Cl sig pc frs =
10.86 - (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)"
10.87 + (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)" |
10.88
10.89 "exec_instr Dup G hp stk vars Cl sig pc frs =
10.90 - (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)"
10.91 + (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)" |
10.92
10.93 "exec_instr Dup_x1 G hp stk vars Cl sig pc frs =
10.94 (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)),
10.95 - vars, Cl, sig, pc+1)#frs)"
10.96 + vars, Cl, sig, pc+1)#frs)" |
10.97
10.98 "exec_instr Dup_x2 G hp stk vars Cl sig pc frs =
10.99 (None, hp,
10.100 (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
10.101 - vars, Cl, sig, pc+1)#frs)"
10.102 + vars, Cl, sig, pc+1)#frs)" |
10.103
10.104 "exec_instr Swap G hp stk vars Cl sig pc frs =
10.105 (let (val1,val2) = (hd stk,hd (tl stk))
10.106 in
10.107 - (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
10.108 + (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))" |
10.109
10.110 "exec_instr IAdd G hp stk vars Cl sig pc frs =
10.111 (let (val1,val2) = (hd stk,hd (tl stk))
10.112 in
10.113 (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)),
10.114 - vars, Cl, sig, pc+1)#frs))"
10.115 + vars, Cl, sig, pc+1)#frs))" |
10.116
10.117 "exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
10.118 (let (val1,val2) = (hd stk, hd (tl stk));
10.119 pc' = if val1 = val2 then nat(int pc+i) else pc+1
10.120 in
10.121 - (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))"
10.122 + (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))" |
10.123
10.124 "exec_instr (Goto i) G hp stk vars Cl sig pc frs =
10.125 - (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)"
10.126 + (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)" |
10.127
10.128 "exec_instr Throw G hp stk vars Cl sig pc frs =
10.129 (let xcpt = raise_system_xcpt (hd stk = Null) NullPointer;
11.1 --- a/src/HOL/NanoJava/Example.thy Tue Sep 28 11:59:58 2010 +0200
11.2 +++ b/src/HOL/NanoJava/Example.thy Tue Sep 28 13:44:06 2010 +0200
11.3 @@ -5,7 +5,9 @@
11.4
11.5 header "Example"
11.6
11.7 -theory Example imports Equivalence begin
11.8 +theory Example
11.9 +imports Equivalence
11.10 +begin
11.11
11.12 text {*
11.13
11.14 @@ -89,9 +91,9 @@
11.15
11.16 subsection "``atleast'' relation for interpretation of Nat ``values''"
11.17
11.18 -consts Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50)
11.19 -primrec "s:x\<ge>0 = (x\<noteq>Null)"
11.20 - "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)"
11.21 +primrec Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50) where
11.22 + "s:x\<ge>0 = (x\<noteq>Null)"
11.23 +| "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)"
11.24
11.25 lemma Nat_atleast_lupd [rule_format, simp]:
11.26 "\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
12.1 --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Tue Sep 28 11:59:58 2010 +0200
12.2 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Tue Sep 28 13:44:06 2010 +0200
12.3 @@ -21,44 +21,36 @@
12.4
12.5 subsection{*Predicate Formalizing the Encryption Association between Keys *}
12.6
12.7 -consts
12.8 - KeyCryptKey :: "[key, key, event list] => bool"
12.9 -
12.10 -primrec
12.11 -
12.12 -KeyCryptKey_Nil:
12.13 - "KeyCryptKey DK K [] = False"
12.14 -
12.15 -KeyCryptKey_Cons:
12.16 +primrec KeyCryptKey :: "[key, key, event list] => bool"
12.17 +where
12.18 + KeyCryptKey_Nil:
12.19 + "KeyCryptKey DK K [] = False"
12.20 +| KeyCryptKey_Cons:
12.21 --{*Says is the only important case.
12.22 1st case: CR5, where KC3 encrypts KC2.
12.23 2nd case: any use of priEK C.
12.24 Revision 1.12 has a more complicated version with separate treatment of
12.25 the dependency of KC1, KC2 and KC3 on priEK (CA i.) Not needed since
12.26 priEK C is never sent (and so can't be lost except at the start). *}
12.27 - "KeyCryptKey DK K (ev # evs) =
12.28 - (KeyCryptKey DK K evs |
12.29 - (case ev of
12.30 - Says A B Z =>
12.31 - ((\<exists>N X Y. A \<noteq> Spy &
12.32 + "KeyCryptKey DK K (ev # evs) =
12.33 + (KeyCryptKey DK K evs |
12.34 + (case ev of
12.35 + Says A B Z =>
12.36 + ((\<exists>N X Y. A \<noteq> Spy &
12.37 DK \<in> symKeys &
12.38 Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
12.39 - (\<exists>C. DK = priEK C))
12.40 - | Gets A' X => False
12.41 - | Notes A' X => False))"
12.42 + (\<exists>C. DK = priEK C))
12.43 + | Gets A' X => False
12.44 + | Notes A' X => False))"
12.45
12.46
12.47 subsection{*Predicate formalizing the association between keys and nonces *}
12.48
12.49 -consts
12.50 - KeyCryptNonce :: "[key, key, event list] => bool"
12.51 -
12.52 -primrec
12.53 -
12.54 -KeyCryptNonce_Nil:
12.55 - "KeyCryptNonce EK K [] = False"
12.56 -
12.57 -KeyCryptNonce_Cons:
12.58 +primrec KeyCryptNonce :: "[key, key, event list] => bool"
12.59 +where
12.60 + KeyCryptNonce_Nil:
12.61 + "KeyCryptNonce EK K [] = False"
12.62 +| KeyCryptNonce_Cons:
12.63 --{*Says is the only important case.
12.64 1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
12.65 2nd case: CR5, where KC3 encrypts NC3;
13.1 --- a/src/HOL/SET_Protocol/Event_SET.thy Tue Sep 28 11:59:58 2010 +0200
13.2 +++ b/src/HOL/SET_Protocol/Event_SET.thy Tue Sep 28 13:44:06 2010 +0200
13.3 @@ -35,15 +35,14 @@
13.4
13.5 consts (*Initial states of agents -- parameter of the construction*)
13.6 initState :: "agent => msg set"
13.7 - knows :: "[agent, event list] => msg set"
13.8
13.9 (* Message reception does not extend spy's knowledge because of
13.10 reception invariant enforced by Reception rule in protocol definition*)
13.11 -primrec
13.12 -
13.13 -knows_Nil:
13.14 - "knows A [] = initState A"
13.15 -knows_Cons:
13.16 +primrec knows :: "[agent, event list] => msg set"
13.17 +where
13.18 + knows_Nil:
13.19 + "knows A [] = initState A"
13.20 +| knows_Cons:
13.21 "knows A (ev # evs) =
13.22 (if A = Spy then
13.23 (case ev of
13.24 @@ -63,15 +62,13 @@
13.25
13.26 subsection{*Used Messages*}
13.27
13.28 -consts
13.29 +primrec used :: "event list => msg set"
13.30 +where
13.31 (*Set of items that might be visible to somebody:
13.32 - complement of the set of fresh items*)
13.33 - used :: "event list => msg set"
13.34 -
13.35 -(* As above, message reception does extend used items *)
13.36 -primrec
13.37 + complement of the set of fresh items.
13.38 + As above, message reception does extend used items *)
13.39 used_Nil: "used [] = (UN B. parts (initState B))"
13.40 - used_Cons: "used (ev # evs) =
13.41 +| used_Cons: "used (ev # evs) =
13.42 (case ev of
13.43 Says A B X => parts {X} Un (used evs)
13.44 | Gets A X => used evs
14.1 --- a/src/HOL/SET_Protocol/Public_SET.thy Tue Sep 28 11:59:58 2010 +0200
14.2 +++ b/src/HOL/SET_Protocol/Public_SET.thy Tue Sep 28 13:44:06 2010 +0200
14.3 @@ -64,7 +64,11 @@
14.4 RCA and CAs know their own respective keys;
14.5 RCA (has already certified and therefore) knows all CAs public keys;
14.6 Spy knows all keys of all bad agents.*}
14.7 -primrec
14.8 +
14.9 +overloading initState \<equiv> "initState"
14.10 +begin
14.11 +
14.12 +primrec initState where
14.13 (*<*)
14.14 initState_CA:
14.15 "initState (CA i) =
14.16 @@ -74,29 +78,31 @@
14.17 Key (pubEK (CA i)), Key (pubSK (CA i)),
14.18 Key (pubEK RCA), Key (pubSK RCA)})"
14.19
14.20 - initState_Cardholder:
14.21 +| initState_Cardholder:
14.22 "initState (Cardholder i) =
14.23 {Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
14.24 Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
14.25 Key (pubEK RCA), Key (pubSK RCA)}"
14.26
14.27 - initState_Merchant:
14.28 +| initState_Merchant:
14.29 "initState (Merchant i) =
14.30 {Key (priEK (Merchant i)), Key (priSK (Merchant i)),
14.31 Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
14.32 Key (pubEK RCA), Key (pubSK RCA)}"
14.33
14.34 - initState_PG:
14.35 +| initState_PG:
14.36 "initState (PG i) =
14.37 {Key (priEK (PG i)), Key (priSK (PG i)),
14.38 Key (pubEK (PG i)), Key (pubSK (PG i)),
14.39 Key (pubEK RCA), Key (pubSK RCA)}"
14.40 (*>*)
14.41 - initState_Spy:
14.42 +| initState_Spy:
14.43 "initState Spy = Key ` (invKey ` pubEK ` bad Un
14.44 invKey ` pubSK ` bad Un
14.45 range pubEK Un range pubSK)"
14.46
14.47 +end
14.48 +
14.49
14.50 text{*Injective mapping from agents to PANs: an agent can have only one card*}
14.51
15.1 --- a/src/HOL/SET_Protocol/ROOT.ML Tue Sep 28 11:59:58 2010 +0200
15.2 +++ b/src/HOL/SET_Protocol/ROOT.ML Tue Sep 28 13:44:06 2010 +0200
15.3 @@ -1,9 +1,3 @@
15.4 -(* Title: HOL/SET_Protocol/ROOT.ML
15.5 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
15.6 - Copyright 2003 University of Cambridge
15.7 -
15.8 -Root file for the SET protocol proofs.
15.9 -*)
15.10
15.11 no_document use_thys ["Nat_Bijection"];
15.12 -use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];
15.13 +use_thys ["SET_Protocol"];
16.1 --- a/src/HOL/Tools/Function/function_lib.ML Tue Sep 28 11:59:58 2010 +0200
16.2 +++ b/src/HOL/Tools/Function/function_lib.ML Tue Sep 28 13:44:06 2010 +0200
16.3 @@ -18,17 +18,6 @@
16.4 fun plural sg pl [x] = sg
16.5 | plural sg pl _ = pl
16.6
16.7 -(* lambda-abstracts over an arbitrarily nested tuple
16.8 - ==> hologic.ML? *)
16.9 -fun tupled_lambda vars t =
16.10 - case vars of
16.11 - (Free v) => lambda (Free v) t
16.12 - | (Var v) => lambda (Var v) t
16.13 - | (Const (@{const_name Pair}, Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
16.14 - (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
16.15 - | _ => raise Match
16.16 -
16.17 -
16.18 fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
16.19 let
16.20 val (n, body) = Term.dest_abs a
17.1 --- a/src/HOL/Tools/Function/induction_schema.ML Tue Sep 28 11:59:58 2010 +0200
17.2 +++ b/src/HOL/Tools/Function/induction_schema.ML Tue Sep 28 13:44:06 2010 +0200
17.3 @@ -196,7 +196,7 @@
17.4 |> fold_rev (Logic.all o Free) ws
17.5 |> term_conv thy ind_atomize
17.6 |> Object_Logic.drop_judgment thy
17.7 - |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
17.8 + |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
17.9 in
17.10 SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
17.11 end
18.1 --- a/src/HOL/Tools/Function/mutual.ML Tue Sep 28 11:59:58 2010 +0200
18.2 +++ b/src/HOL/Tools/Function/mutual.ML Tue Sep 28 13:44:06 2010 +0200
18.3 @@ -221,7 +221,7 @@
18.4 val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
18.5 val atup = foldr1 HOLogic.mk_prod avars
18.6 in
18.7 - tupled_lambda atup (list_comb (P, avars))
18.8 + HOLogic.tupled_lambda atup (list_comb (P, avars))
18.9 end
18.10
18.11 val Ps = map2 mk_P parts newPs
19.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 28 11:59:58 2010 +0200
19.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 28 13:44:06 2010 +0200
19.3 @@ -2021,12 +2021,6 @@
19.4 (fn NONE => "X" | SOME k' => string_of_int k')
19.5 (ks @ [SOME k]))) arities));
19.6
19.7 -fun split_lambda (x as Free _) t = lambda x t
19.8 - | split_lambda (Const (@{const_name Pair}, _) $ t1 $ t2) t =
19.9 - HOLogic.mk_split (split_lambda t1 (split_lambda t2 t))
19.10 - | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
19.11 - | split_lambda t _ = raise (TERM ("split_lambda", [t]))
19.12 -
19.13 fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
19.14 | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
19.15 | strip_split_abs t = t
19.16 @@ -2051,7 +2045,7 @@
19.17 val x = Name.variant names "x"
19.18 val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
19.19 val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
19.20 - val t = fold_rev split_lambda args (PredicateCompFuns.mk_Eval
19.21 + val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
19.22 (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
19.23 in
19.24 (if is_eval then t else Free (x, funT), x :: names)
19.25 @@ -2142,8 +2136,8 @@
19.26 val (r, _) = PredicateCompFuns.dest_Eval t'
19.27 in (SOME (fst (strip_comb r)), NONE) end
19.28 val (inargs, outargs) = split_map_mode strip_eval mode args
19.29 - val predterm = fold_rev split_lambda inargs
19.30 - (PredicateCompFuns.mk_Enum (split_lambda (HOLogic.mk_tuple outargs)
19.31 + val predterm = fold_rev HOLogic.tupled_lambda inargs
19.32 + (PredicateCompFuns.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
19.33 (list_comb (Const (name, T), args))))
19.34 val lhs = Const (mode_cname, funT)
19.35 val def = Logic.mk_equals (lhs, predterm)
19.36 @@ -3269,7 +3263,7 @@
19.37 val t_pred = compile_expr comp_modifiers ctxt
19.38 (body, deriv) [] additional_arguments;
19.39 val T_pred = dest_predT compfuns (fastype_of t_pred)
19.40 - val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
19.41 + val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output_tuple
19.42 in
19.43 if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred
19.44 end
20.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Sep 28 11:59:58 2010 +0200
20.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Sep 28 13:44:06 2010 +0200
20.3 @@ -177,15 +177,7 @@
20.4 val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
20.5 val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
20.6
20.7 -fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
20.8 - | mk_split_lambda [x] t = lambda x t
20.9 - | mk_split_lambda xs t =
20.10 - let
20.11 - fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
20.12 - | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
20.13 - in
20.14 - mk_split_lambda' xs t
20.15 - end;
20.16 +val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
20.17
20.18 fun cpu_time description f =
20.19 let
21.1 --- a/src/HOL/Tools/hologic.ML Tue Sep 28 11:59:58 2010 +0200
21.2 +++ b/src/HOL/Tools/hologic.ML Tue Sep 28 13:44:06 2010 +0200
21.3 @@ -67,6 +67,7 @@
21.4 val split_const: typ * typ * typ -> term
21.5 val mk_split: term -> term
21.6 val flatten_tupleT: typ -> typ list
21.7 + val tupled_lambda: term -> term -> term
21.8 val mk_tupleT: typ list -> typ
21.9 val strip_tupleT: typ -> typ list
21.10 val mk_tuple: term list -> term
21.11 @@ -327,6 +328,15 @@
21.12 fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
21.13 | flatten_tupleT T = [T];
21.14
21.15 +(*abstraction over nested tuples*)
21.16 +fun tupled_lambda (x as Free _) b = lambda x b
21.17 + | tupled_lambda (x as Var _) b = lambda x b
21.18 + | tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b =
21.19 + mk_split (tupled_lambda u (tupled_lambda v b))
21.20 + | tupled_lambda (Const ("Product_Type.Unity", _)) b =
21.21 + Abs ("x", unitT, b)
21.22 + | tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]);
21.23 +
21.24
21.25 (* tuples with right-fold structure *)
21.26