# HG changeset patch # User berghofe # Date 1184146093 -7200 # Node ID 1c4672d130b1a069a59dd2551ed3dad2fb1e1cf9 # Parent 75873e94357cceb4ab18e9293413a8e596261068 Adapted to new inductive definition package. diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Coinductive_List.thy --- a/src/HOL/Library/Coinductive_List.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Library/Coinductive_List.thy Wed Jul 11 11:28:13 2007 +0200 @@ -38,17 +38,27 @@ subsection {* Corecursive lists *} -consts +coinductive_set LList :: "'a Datatype.item set \ 'a Datatype.item set" - -coinductive "LList A" - intros + for A :: "'a Datatype.item set" + where NIL [intro]: "NIL \ LList A" - CONS [intro]: "a \ A \ M \ LList A \ CONS a M \ LList A" + | CONS [intro]: "a \ A \ M \ LList A \ CONS a M \ LList A" -lemma LList_mono: "A \ B \ LList A \ LList B" +lemma LList_mono: + assumes subset: "A \ B" + shows "LList A \ LList B" -- {* This justifies using @{text LList} in other recursive type definitions. *} - unfolding LList.defs by (blast intro!: gfp_mono) +proof + fix x + assume "x \ LList A" + then show "x \ LList B" + proof coinduct + case LList + then show ?case using subset + by cases blast+ + qed +qed consts LList_corec_aux :: "nat \ ('a \ ('b Datatype.item \ 'a) option) \ @@ -92,7 +102,7 @@ lemma LList_corec_type: "LList_corec a f \ LList UNIV" proof - - have "LList_corec a f \ {LList_corec a f | a. True}" by blast + have "\x. LList_corec a f = LList_corec x f" by blast then show ?thesis proof coinduct case (LList L) @@ -185,7 +195,7 @@ with Abs_llist have "l = LNil" by (simp add: LNil_def) with LNil show ?thesis . next - case (CONS K a) + case (CONS a K) then have "K \ llist" by (blast intro: llistI) then obtain l' where "K = Rep_llist l'" by cases with CONS and Abs_llist obtain x where "l = LCons x l'" @@ -228,7 +238,7 @@ (is "?corec a \ _") proof (unfold llist_def) let "LList_corec a ?g" = "?corec a" - have "?corec a \ {?corec x | x. True}" by blast + have "\x. ?corec a = ?corec x" by blast then show "?corec a \ LList (range Datatype.Leaf)" proof coinduct case (LList L) @@ -282,14 +292,13 @@ subsection {* Equality as greatest fixed-point -- the bisimulation principle *} -consts +coinductive_set EqLList :: "('a Datatype.item \ 'a Datatype.item) set \ ('a Datatype.item \ 'a Datatype.item) set" - -coinductive "EqLList r" - intros + for r :: "('a Datatype.item \ 'a Datatype.item) set" + where EqNIL: "(NIL, NIL) \ EqLList r" - EqCONS: "(a, b) \ r \ (M, N) \ EqLList r \ + | EqCONS: "(a, b) \ r \ (M, N) \ EqLList r \ (CONS a M, CONS b N) \ EqLList r" lemma EqLList_unfold: @@ -310,10 +319,10 @@ done lemma Domain_EqLList: "Domain (EqLList (diag A)) \ LList A" - apply (simp add: LList.defs NIL_def CONS_def) - apply (rule gfp_upperbound) - apply (subst EqLList_unfold) - apply auto + apply (rule subsetI) + apply (erule LList.coinduct) + apply (subst (asm) EqLList_unfold) + apply (auto simp add: NIL_def CONS_def) done lemma EqLList_diag: "EqLList (diag A) = diag (LList A)" @@ -328,23 +337,23 @@ assumption) apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]]) done - show "?rhs \ ?lhs" - proof - fix p assume "p \ diag (LList A)" - then show "p \ EqLList (diag A)" + { + fix M N assume "(M, N) \ diag (LList A)" + then have "(M, N) \ EqLList (diag A)" proof coinduct - case (EqLList q) - then obtain L where L: "L \ LList A" and q: "q = (L, L)" .. + case (EqLList M N) + then obtain L where L: "L \ LList A" and MN: "M = L" "N = L" by blast from L show ?case proof cases - case NIL with q have ?EqNIL by simp + case NIL with MN have ?EqNIL by simp then show ?thesis .. next - case CONS with q have ?EqCONS by (simp add: diagI) + case CONS with MN have ?EqCONS by (simp add: diagI) then show ?thesis .. qed qed - qed + } + then show "?rhs \ ?lhs" by auto qed lemma EqLList_diag_iff [iff]: "(p \ EqLList (diag A)) = (p \ diag (LList A))" @@ -359,11 +368,11 @@ lemma LList_equalityI [consumes 1, case_names EqLList, case_conclusion EqLList EqNIL EqCONS]: assumes r: "(M, N) \ r" - and step: "\p. p \ r \ - p = (NIL, NIL) \ - (\M N a b. - p = (CONS a M, CONS b N) \ (a, b) \ diag A \ - (M, N) \ r \ EqLList (diag A))" + and step: "\M N. (M, N) \ r \ + M = NIL \ N = NIL \ + (\a b M' N'. + M = CONS a M' \ N = CONS b N' \ (a, b) \ diag A \ + ((M', N') \ r \ (M', N') \ EqLList (diag A)))" shows "M = N" proof - from r have "(M, N) \ EqLList (diag A)" @@ -391,39 +400,39 @@ have "(f M, g M) \ ?bisim" using M by blast then show ?thesis proof (coinduct taking: A rule: LList_equalityI) - case (EqLList q) - then obtain L where q: "q = (f L, g L)" and L: "L \ LList A" by blast + case (EqLList M N) + then obtain L where MN: "M = f L" "N = g L" and L: "L \ LList A" by blast from L show ?case proof (cases L) case NIL - with fun_NIL and q have "q \ diag (LList A)" by auto - then have "q \ EqLList (diag A)" .. + with fun_NIL and MN have "(M, N) \ diag (LList A)" by auto + then have "(M, N) \ EqLList (diag A)" .. then show ?thesis by cases simp_all next - case (CONS K a) + case (CONS a K) from fun_CONS and `a \ A` `K \ LList A` have "?fun_CONS a K" (is "?NIL \ ?CONS") . then show ?thesis proof assume ?NIL - with q CONS have "q \ diag (LList A)" by auto - then have "q \ EqLList (diag A)" .. + with MN CONS have "(M, N) \ diag (LList A)" by auto + then have "(M, N) \ EqLList (diag A)" .. then show ?thesis by cases simp_all next assume ?CONS - with CONS obtain a b M N where - fg: "(f L, g L) = (CONS a M, CONS b N)" + with CONS obtain a b M' N' where + fg: "(f L, g L) = (CONS a M', CONS b N')" and ab: "(a, b) \ diag A" - and MN: "(M, N) \ ?bisim \ diag (LList A)" + and M'N': "(M', N') \ ?bisim \ diag (LList A)" by blast - from MN show ?thesis + from M'N' show ?thesis proof - assume "(M, N) \ ?bisim" - with q fg ab show ?thesis by simp + assume "(M', N') \ ?bisim" + with MN fg ab show ?thesis by simp next - assume "(M, N) \ diag (LList A)" - then have "(M, N) \ EqLList (diag A)" .. - with q fg ab show ?thesis by simp + assume "(M', N') \ diag (LList A)" + then have "(M', N') \ EqLList (diag A)" .. + with MN fg ab show ?thesis by simp qed qed qed @@ -446,18 +455,18 @@ have "(h x, h' x) \ {(h u, h' u) | u. True}" by blast then show "h x = h' x" proof (coinduct rule: LList_equalityI [where A = UNIV]) - case (EqLList q) - then obtain x where q: "q = (h x, h' x)" by blast + case (EqLList M N) + then obtain x where MN: "M = h x" "N = h' x" by blast show ?case proof (cases "f x") case None - with h h' q have ?EqNIL by simp + with h h' MN have ?EqNIL by simp then show ?thesis .. next case (Some p) - with h h' q have "q = - (CONS (fst p) (h (snd p)), CONS (fst p) (h' (snd p)))" - by (simp split: prod.split) + with h h' MN have "M = CONS (fst p) (h (snd p))" + and "N = CONS (fst p) (h' (snd p))" + by (simp_all split: prod.split) then have ?EqCONS by (auto iff: diag_iff) then show ?thesis .. qed @@ -481,18 +490,18 @@ by blast then have "M = N" proof (coinduct rule: LList_equalityI [where A = UNIV]) - case (EqLList q) + case (EqLList M N) then obtain l1 l2 where - q: "q = (Rep_llist l1, Rep_llist l2)" and r: "(l1, l2) \ r" + MN: "M = Rep_llist l1" "N = Rep_llist l2" and r: "(l1, l2) \ r" by auto from step [OF r] show ?case proof assume "?EqLNil (l1, l2)" - with q have ?EqNIL by (simp add: Rep_llist_LNil) + with MN have ?EqNIL by (simp add: Rep_llist_LNil) then show ?thesis .. next assume "?EqLCons (l1, l2)" - with q have ?EqCONS + with MN have ?EqCONS by (force simp add: Rep_llist_LCons EqLList_diag intro: Rep_llist_UNIV) then show ?thesis .. qed @@ -546,7 +555,7 @@ assumes "M \ A" shows "Lconst M \ LList A" proof - - have "Lconst M \ {Lconst M}" by simp + have "Lconst M \ {Lconst (id M)}" by simp then show ?thesis proof coinduct case (LList N) @@ -617,16 +626,16 @@ then show ?thesis proof (coinduct taking: "range (\N :: 'a Datatype.item. N)" rule: LList_equalityI) - case (EqLList q) - then obtain N where q: "q = (?lhs N, ?rhs N)" and N: "N \ LList A" by blast + case (EqLList L M) + then obtain N where LM: "L = ?lhs N" "M = ?rhs N" and N: "N \ LList A" by blast from N show ?case proof cases case NIL - with q have ?EqNIL by simp + with LM have ?EqNIL by simp then show ?thesis .. next case CONS - with q have ?EqCONS by auto + with LM have ?EqCONS by auto then show ?thesis .. qed qed @@ -640,16 +649,16 @@ then show ?thesis proof (coinduct taking: "range (\N :: 'a Datatype.item. N)" rule: LList_equalityI) - case (EqLList q) - then obtain N where q: "q = (?lmap N, N)" and N: "N \ LList A" by blast + case (EqLList L M) + then obtain N where LM: "L = ?lmap N" "M = N" and N: "N \ LList A" by blast from N show ?case proof cases case NIL - with q have ?EqNIL by simp + with LM have ?EqNIL by simp then show ?thesis .. next case CONS - with q have ?EqCONS by auto + with LM have ?EqCONS by auto then show ?thesis .. qed qed diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Graphs.thy --- a/src/HOL/Library/Graphs.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Library/Graphs.thy Wed Jul 11 11:28:13 2007 +0200 @@ -321,7 +321,7 @@ types ('n, 'e) fpath = "('n \ ('e \ 'n) list)" -inductive2 has_fpath :: "('n, 'e) graph \ ('n, 'e) fpath \ bool" +inductive has_fpath :: "('n, 'e) graph \ ('n, 'e) fpath \ bool" for G :: "('n, 'e) graph" where has_fpath_empty: "has_fpath G (n, [])" diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Library/Permutation.thy Wed Jul 11 11:28:13 2007 +0200 @@ -8,19 +8,13 @@ imports Multiset begin -consts - perm :: "('a list * 'a list) set" - -abbreviation - perm_rel :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) where - "x <~~> y == (x, y) \ perm" - -inductive perm - intros +inductive + perm :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) + where Nil [intro!]: "[] <~~> []" - swap [intro!]: "y # x # l <~~> x # y # l" - Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys" - trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs" + | swap [intro!]: "y # x # l <~~> x # y # l" + | Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys" + | trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs" lemma perm_refl [iff]: "l <~~> l" by (induct l) auto diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Library/Zorn.thy Wed Jul 11 11:28:13 2007 +0200 @@ -33,12 +33,12 @@ (if c \ chain S | c \ maxchain S then c else SOME c'. c' \ super S c)" -consts +inductive_set TFin :: "'a set set => 'a set set set" -inductive "TFin S" - intros + for S :: "'a set set" + where succI: "x \ TFin S ==> succ S x \ TFin S" - Pow_UnionI: "Y \ Pow(TFin S) ==> Union(Y) \ TFin S" + | Pow_UnionI: "Y \ Pow(TFin S) ==> Union(Y) \ TFin S" monos Pow_mono diff -r 75873e94357c -r 1c4672d130b1 src/HOL/MetisExamples/Message.thy --- a/src/HOL/MetisExamples/Message.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/MetisExamples/Message.thy Wed Jul 11 11:28:13 2007 +0200 @@ -68,13 +68,14 @@ subsubsection{*Inductive Definition of All Parts" of a Message*} -consts parts :: "msg set => msg set" -inductive "parts H" - intros +inductive_set + parts :: "msg set => msg set" + for H :: "msg set" + where Inj [intro]: "X \ H ==> X \ parts H" - Fst: "{|X,Y|} \ parts H ==> X \ parts H" - Snd: "{|X,Y|} \ parts H ==> Y \ parts H" - Body: "Crypt K X \ parts H ==> X \ parts H" + | Fst: "{|X,Y|} \ parts H ==> X \ parts H" + | Snd: "{|X,Y|} \ parts H ==> Y \ parts H" + | Body: "Crypt K X \ parts H ==> X \ parts H" ML{*ResAtp.problem_name := "Message__parts_mono"*} @@ -329,13 +330,14 @@ messages, including keys. A form of downward closure. Pairs can be taken apart; messages decrypted with known keys. *} -consts analz :: "msg set => msg set" -inductive "analz H" - intros +inductive_set + analz :: "msg set => msg set" + for H :: "msg set" + where Inj [intro,simp] : "X \ H ==> X \ analz H" - Fst: "{|X,Y|} \ analz H ==> X \ analz H" - Snd: "{|X,Y|} \ analz H ==> Y \ analz H" - Decrypt [dest]: + | Fst: "{|X,Y|} \ analz H ==> X \ analz H" + | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" + | Decrypt [dest]: "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" @@ -456,14 +458,14 @@ analz (insert (Crypt K X) H) \ insert (Crypt K X) (analz (insert X H))" apply (rule subsetI) -apply (erule_tac xa = x in analz.induct, auto) +apply (erule_tac x = x in analz.induct, auto) done lemma lemma2: "Key (invKey K) \ analz H ==> insert (Crypt K X) (analz (insert X H)) \ analz (insert (Crypt K X) H)" apply auto -apply (erule_tac xa = x in analz.induct, auto) +apply (erule_tac x = x in analz.induct, auto) apply (blast intro: analz_insertI analz.Decrypt) done @@ -579,15 +581,16 @@ encrypted with known keys. Agent names are public domain. Numbers can be guessed, but Nonces cannot be. *} -consts synth :: "msg set => msg set" -inductive "synth H" - intros +inductive_set + synth :: "msg set => msg set" + for H :: "msg set" + where Inj [intro]: "X \ H ==> X \ synth H" - Agent [intro]: "Agent agt \ synth H" - Number [intro]: "Number n \ synth H" - Hash [intro]: "X \ synth H ==> Hash X \ synth H" - MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" - Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" + | Agent [intro]: "Agent agt \ synth H" + | Number [intro]: "Number n \ synth H" + | Hash [intro]: "X \ synth H ==> Hash X \ synth H" + | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" + | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" text{*Monotonicity*} lemma synth_mono: "G\H ==> synth(G) \ synth(H)" diff -r 75873e94357c -r 1c4672d130b1 src/HOL/NanoJava/AxSem.thy --- a/src/HOL/NanoJava/AxSem.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/NanoJava/AxSem.thy Wed Jul 11 11:28:13 2007 +0200 @@ -18,116 +18,102 @@ "triple" \ (type)"assn \ stmt \ assn" "etriple" \ (type)"assn \ expr \ vassn" -consts hoare :: "(triple set \ triple set) set" -consts ehoare :: "(triple set \ etriple ) set" -syntax (xsymbols) - "@hoare" :: "[triple set, triple set ] => bool" ("_ |\/ _" [61,61] 60) - "@hoare1" :: "[triple set, assn,stmt,assn] => bool" - ("_ \/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60) -"@ehoare" :: "[triple set, etriple ] => bool" ("_ |\\<^sub>e/ _"[61,61]60) -"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool" - ("_ \\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60) -syntax - "@hoare" :: "[triple set, triple set ] => bool" ("_ ||-/ _" [61,61] 60) - "@hoare1" :: "[triple set, assn,stmt,assn] => bool" - ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60) -"@ehoare" :: "[triple set, etriple ] => bool" ("_ ||-e/ _"[61,61] 60) -"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool" - ("_ |-e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60) - -translations "A |\ C" \ "(A,C) \ hoare" - "A \ {P}c{Q}" \ "A |\ {(P,c,Q)}" - "A |\\<^sub>e t" \ "(A,t) \ ehoare" - "A |\\<^sub>e (P,e,Q)" \ "(A,P,e,Q) \ ehoare" (* shouldn't be necessary *) - "A \\<^sub>e {P}e{Q}" \ "A |\\<^sub>e (P,e,Q)" - subsection "Hoare Logic Rules" -inductive hoare ehoare -intros - - Skip: "A |- {P} Skip {P}" - - Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}" +inductive + hoare :: "[triple set, triple set] => bool" ("_ |\/ _" [61, 61] 60) + and ehoare :: "[triple set, etriple] => bool" ("_ |\\<^sub>e/ _" [61, 61] 60) + and hoare1 :: "[triple set, assn,stmt,assn] => bool" + ("_ \/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60) + and ehoare1 :: "[triple set, assn,expr,vassn]=> bool" + ("_ \\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60) +where - Cond: "[| A |-e {P} e {Q}; - \v. A |- {Q v} (if v \ Null then c1 else c2) {R} |] ==> - A |- {P} If(e) c1 Else c2 {R}" + "A \ {P}c{Q} \ A |\ {(P,c,Q)}" +| "A \\<^sub>e {P}e{Q} \ A |\\<^sub>e (P,e,Q)" - Loop: "A |- {\s. P s \ s \ Null} c {P} ==> - A |- {P} While(x) c {\s. P s \ s = Null}" +| Skip: "A \ {P} Skip {P}" + +| Comp: "[| A \ {P} c1 {Q}; A \ {Q} c2 {R} |] ==> A \ {P} c1;;c2 {R}" - LAcc: "A |-e {\s. P (s) s} LAcc x {P}" +| Cond: "[| A \\<^sub>e {P} e {Q}; + \v. A \ {Q v} (if v \ Null then c1 else c2) {R} |] ==> + A \ {P} If(e) c1 Else c2 {R}" - LAss: "A |-e {P} e {\v s. Q (lupd(x\v) s)} ==> - A |- {P} x:==e {Q}" +| Loop: "A \ {\s. P s \ s \ Null} c {P} ==> + A \ {P} While(x) c {\s. P s \ s = Null}" + +| LAcc: "A \\<^sub>e {\s. P (s) s} LAcc x {P}" - FAcc: "A |-e {P} e {\v s. \a. v=Addr a --> Q (get_field s a f) s} ==> - A |-e {P} e..f {Q}" +| LAss: "A \\<^sub>e {P} e {\v s. Q (lupd(x\v) s)} ==> + A \ {P} x:==e {Q}" + +| FAcc: "A \\<^sub>e {P} e {\v s. \a. v=Addr a --> Q (get_field s a f) s} ==> + A \\<^sub>e {P} e..f {Q}" - FAss: "[| A |-e {P} e1 {\v s. \a. v=Addr a --> Q a s}; - \a. A |-e {Q a} e2 {\v s. R (upd_obj a f v s)} |] ==> - A |- {P} e1..f:==e2 {R}" +| FAss: "[| A \\<^sub>e {P} e1 {\v s. \a. v=Addr a --> Q a s}; + \a. A \\<^sub>e {Q a} e2 {\v s. R (upd_obj a f v s)} |] ==> + A \ {P} e1..f:==e2 {R}" - NewC: "A |-e {\s. \a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)} +| NewC: "A \\<^sub>e {\s. \a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)} new C {P}" - Cast: "A |-e {P} e {\v s. (case v of Null => True +| Cast: "A \\<^sub>e {P} e {\v s. (case v of Null => True | Addr a => obj_class s a <=C C) --> Q v s} ==> - A |-e {P} Cast C e {Q}" + A \\<^sub>e {P} Cast C e {Q}" - Call: "[| A |-e {P} e1 {Q}; \a. A |-e {Q a} e2 {R a}; - \a p ls. A |- {\s'. \s. R a p s \ ls = s \ +| Call: "[| A \\<^sub>e {P} e1 {Q}; \a. A \\<^sub>e {Q a} e2 {R a}; + \a p ls. A \ {\s'. \s. R a p s \ ls = s \ s' = lupd(This\a)(lupd(Par\p)(del_locs s))} Meth (C,m) {\s. S (s) (set_locs ls s)} |] ==> - A |-e {P} {C}e1..m(e2) {S}" + A \\<^sub>e {P} {C}e1..m(e2) {S}" - Meth: "\D. A |- {\s'. \s a. s = Addr a \ D = obj_class s a \ D <=C C \ +| Meth: "\D. A \ {\s'. \s a. s = Addr a \ D = obj_class s a \ D <=C C \ P s \ s' = init_locs D m s} Impl (D,m) {Q} ==> - A |- {P} Meth (C,m) {Q}" + A \ {P} Meth (C,m) {Q}" --{* @{text "\Z"} instead of @{text "\Z"} in the conclusion and\\ Z restricted to type state due to limitations of the inductive package *} - Impl: "\Z::state. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- +| Impl: "\Z::state. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\ (\Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> - A ||- (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" + A |\ (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" --{* structural rules *} - Asm: " a \ A ==> A ||- {a}" +| Asm: " a \ A ==> A |\ {a}" - ConjI: " \c \ C. A ||- {c} ==> A ||- C" +| ConjI: " \c \ C. A |\ {c} ==> A |\ C" - ConjE: "[|A ||- C; c \ C |] ==> A ||- {c}" +| ConjE: "[|A |\ C; c \ C |] ==> A |\ {c}" --{* Z restricted to type state due to limitations of the inductive package *} - Conseq:"[| \Z::state. A |- {P' Z} c {Q' Z}; +| Conseq:"[| \Z::state. A \ {P' Z} c {Q' Z}; \s t. (\Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> - A |- {P} c {Q }" + A \ {P} c {Q }" --{* Z restricted to type state due to limitations of the inductive package *} - eConseq:"[| \Z::state. A |-e {P' Z} e {Q' Z}; +| eConseq:"[| \Z::state. A \\<^sub>e {P' Z} e {Q' Z}; \s v t. (\Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> - A |-e {P} e {Q }" + A \\<^sub>e {P} e {Q }" subsection "Fully polymorphic variants, required for Example only" axioms - Conseq:"[| \Z. A |- {P' Z} c {Q' Z}; + Conseq:"[| \Z. A \ {P' Z} c {Q' Z}; \s t. (\Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> - A |- {P} c {Q }" + A \ {P} c {Q }" - eConseq:"[| \Z. A |-e {P' Z} e {Q' Z}; + eConseq:"[| \Z. A \\<^sub>e {P' Z} e {Q' Z}; \s v t. (\Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> - A |-e {P} e {Q }" + A \\<^sub>e {P} e {Q }" - Impl: "\Z. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- + Impl: "\Z. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\ (\Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> - A ||- (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" + A |\ (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" subsection "Derived Rules" diff -r 75873e94357c -r 1c4672d130b1 src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/NanoJava/Equivalence.thy Wed Jul 11 11:28:13 2007 +0200 @@ -12,17 +12,17 @@ constdefs valid :: "[assn,stmt, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) - "|= {P} c {Q} \ \s t. P s --> (\n. s -c -n-> t) --> Q t" + "|= {P} c {Q} \ \s t. P s --> (\n. s -c -n\ t) --> Q t" evalid :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) - "|=e {P} e {Q} \ \s v t. P s --> (\n. s -e>v-n-> t) --> Q v t" + "|=e {P} e {Q} \ \s v t. P s --> (\n. s -e\v-n\ t) --> Q v t" nvalid :: "[nat, triple ] => bool" ("|=_: _" [61,61] 60) - "|=n: t \ let (P,c,Q) = t in \s t. s -c -n-> t --> P s --> Q t" + "|=n: t \ let (P,c,Q) = t in \s t. s -c -n\ t --> P s --> Q t" envalid :: "[nat,etriple ] => bool" ("|=_:e _" [61,61] 60) - "|=n:e t \ let (P,e,Q) = t in \s v t. s -e>v-n-> t --> P s --> Q v t" + "|=n:e t \ let (P,e,Q) = t in \s v t. s -e\v-n\ t --> P s --> Q v t" nvalids :: "[nat, triple set] => bool" ("||=_: _" [61,61] 60) "||=n: T \ \t\T. |=n: t" @@ -108,8 +108,8 @@ apply (rule hoare_ehoare.induct) (*18*) apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *}) -apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : hoare") *}) -apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *}) +apply (tactic {* ALLGOALS (REPEAT o thin_tac "hoare ?x ?y") *}) +apply (tactic {* ALLGOALS (REPEAT o thin_tac "ehoare ?x ?y") *}) apply (simp_all only: cnvalid1_eq cenvalid_def2) apply fast apply fast @@ -161,9 +161,9 @@ subsection "(Relative) Completeness" constdefs MGT :: "stmt => state => triple" - "MGT c Z \ (\s. Z = s, c, \ t. \n. Z -c- n-> t)" + "MGT c Z \ (\s. Z = s, c, \ t. \n. Z -c- n\ t)" MGTe :: "expr => state => etriple" - "MGTe e Z \ (\s. Z = s, e, \v t. \n. Z -e>v-n-> t)" + "MGTe e Z \ (\s. Z = s, e, \v t. \n. Z -e\v-n\ t)" syntax (xsymbols) MGTe :: "expr => state => etriple" ("MGT\<^sub>e") syntax (HTML output) diff -r 75873e94357c -r 1c4672d130b1 src/HOL/NanoJava/OpSem.thy --- a/src/HOL/NanoJava/OpSem.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/NanoJava/OpSem.thy Wed Jul 11 11:28:13 2007 +0200 @@ -8,61 +8,51 @@ theory OpSem imports State begin -consts - exec :: "(state \ stmt \ nat \ state) set" - eval :: "(state \ expr \ val \ nat \ state) set" -syntax (xsymbols) - exec :: "[state,stmt, nat,state] => bool" ("_ -_-_\ _" [98,90, 65,98] 89) - eval :: "[state,expr,val,nat,state] => bool" ("_ -_\_-_\ _"[98,95,99,65,98] 89) -syntax - exec :: "[state,stmt, nat,state] => bool" ("_ -_-_-> _" [98,90, 65,98]89) - eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,65,98]89) -translations - "s -c -n-> s'" == "(s, c, n, s') \ exec" - "s -e>v-n-> s'" == "(s, e, v, n, s') \ eval" +inductive + exec :: "[state,stmt, nat,state] => bool" ("_ -_-_\ _" [98,90, 65,98] 89) + and eval :: "[state,expr,val,nat,state] => bool" ("_ -_\_-_\ _"[98,95,99,65,98] 89) +where + Skip: " s -Skip-n\ s" + +| Comp: "[| s0 -c1-n\ s1; s1 -c2-n\ s2 |] ==> + s0 -c1;; c2-n\ s2" -inductive exec eval intros - Skip: " s -Skip-n-> s" - - Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==> - s0 -c1;; c2-n-> s2" +| Cond: "[| s0 -e\v-n\ s1; s1 -(if v\Null then c1 else c2)-n\ s2 |] ==> + s0 -If(e) c1 Else c2-n\ s2" - Cond: "[| s0 -e>v-n-> s1; s1 -(if v\Null then c1 else c2)-n-> s2 |] ==> - s0 -If(e) c1 Else c2-n-> s2" +| LoopF:" s0 = Null ==> + s0 -While(x) c-n\ s0" +| LoopT:"[| s0 \ Null; s0 -c-n\ s1; s1 -While(x) c-n\ s2 |] ==> + s0 -While(x) c-n\ s2" - LoopF:" s0 = Null ==> - s0 -While(x) c-n-> s0" - LoopT:"[| s0 \ Null; s0 -c-n-> s1; s1 -While(x) c-n-> s2 |] ==> - s0 -While(x) c-n-> s2" +| LAcc: " s -LAcc x\s-n\ s" + +| LAss: " s -e\v-n\ s' ==> + s -x:==e-n\ lupd(x\v) s'" - LAcc: " s -LAcc x>s-n-> s" - - LAss: " s -e>v-n-> s' ==> - s -x:==e-n-> lupd(x\v) s'" +| FAcc: " s -e\Addr a-n\ s' ==> + s -e..f\get_field s' a f-n\ s'" - FAcc: " s -e>Addr a-n-> s' ==> - s -e..f>get_field s' a f-n-> s'" +| FAss: "[| s0 -e1\Addr a-n\ s1; s1 -e2\v-n\ s2 |] ==> + s0 -e1..f:==e2-n\ upd_obj a f v s2" - FAss: "[| s0 -e1>Addr a-n-> s1; s1 -e2>v-n-> s2 |] ==> - s0 -e1..f:==e2-n-> upd_obj a f v s2" - - NewC: " new_Addr s = Addr a ==> - s -new C>Addr a-n-> new_obj a C s" +| NewC: " new_Addr s = Addr a ==> + s -new C\Addr a-n\ new_obj a C s" - Cast: "[| s -e>v-n-> s'; +| Cast: "[| s -e\v-n\ s'; case v of Null => True | Addr a => obj_class s' a \C C |] ==> - s -Cast C e>v-n-> s'" + s -Cast C e\v-n\ s'" - Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; - lupd(This\a)(lupd(Par\p)(del_locs s2)) -Meth (C,m)-n-> s3 - |] ==> s0 -{C}e1..m(e2)>s3-n-> set_locs s2 s3" +| Call: "[| s0 -e1\a-n\ s1; s1 -e2\p-n\ s2; + lupd(This\a)(lupd(Par\p)(del_locs s2)) -Meth (C,m)-n\ s3 + |] ==> s0 -{C}e1..m(e2)\s3-n\ set_locs s2 s3" - Meth: "[| s = Addr a; D = obj_class s a; D\C C; - init_locs D m s -Impl (D,m)-n-> s' |] ==> - s -Meth (C,m)-n-> s'" +| Meth: "[| s = Addr a; D = obj_class s a; D\C C; + init_locs D m s -Impl (D,m)-n\ s' |] ==> + s -Meth (C,m)-n\ s'" - Impl: " s -body Cm- n-> s' ==> - s -Impl Cm-Suc n-> s'" +| Impl: " s -body Cm- n\ s' ==> + s -Impl Cm-Suc n\ s'" inductive_cases exec_elim_cases': diff -r 75873e94357c -r 1c4672d130b1 src/HOL/NanoJava/TypeRel.thy --- a/src/HOL/NanoJava/TypeRel.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/NanoJava/TypeRel.thy Wed Jul 11 11:28:13 2007 +0200 @@ -9,22 +9,18 @@ theory TypeRel imports Decl begin consts - widen :: "(ty \ ty ) set" --{* widening *} subcls1 :: "(cname \ cname) set" --{* subclass *} syntax (xsymbols) - widen :: "[ty , ty ] => bool" ("_ \ _" [71,71] 70) subcls1 :: "[cname, cname] => bool" ("_ \C1 _" [71,71] 70) subcls :: "[cname, cname] => bool" ("_ \C _" [71,71] 70) syntax - widen :: "[ty , ty ] => bool" ("_ <= _" [71,71] 70) subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70) subcls :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70) translations "C \C1 D" == "(C,D) \ subcls1" "C \C D" == "(C,D) \ subcls1^*" - "S \ T" == "(S,T) \ widen" consts method :: "cname => (mname \ methd)" @@ -38,10 +34,12 @@ subcls1_def: "subcls1 \ {(C,D). C\Object \ (\c. class C = Some c \ super c=D)}" text{* Widening, viz. method invocation conversion *} -inductive widen intros - refl [intro!, simp]: "T \ T" - subcls : "C\C D \ Class C \ Class D" - null [intro!]: "NT \ R" +inductive + widen :: "ty => ty => bool" ("_ \ _" [71,71] 70) +where + refl [intro!, simp]: "T \ T" +| subcls: "C\C D \ Class C \ Class D" +| null [intro!]: "NT \ R" lemma subcls1D: "C\C1D \ C \ Object \ (\c. class C = Some c \ super c=D)" diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Nominal/Nominal.thy Wed Jul 11 11:28:13 2007 +0200 @@ -3048,10 +3048,9 @@ section {* abstraction type for the parsing in nominal datatype *} (*==============================================================*) -consts - "ABS_set" :: "('x\('a noption)) set" -inductive ABS_set - intros + +inductive_set ABS_set :: "('x\('a noption)) set" + where ABS_in: "(abs_fun a x)\ABS_set" typedef (ABS) ('x,'a) ABS = "ABS_set::('x\('a noption)) set" diff -r 75873e94357c -r 1c4672d130b1 src/HOL/NumberTheory/BijectionRel.thy --- a/src/HOL/NumberTheory/BijectionRel.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/NumberTheory/BijectionRel.thy Wed Jul 11 11:28:13 2007 +0200 @@ -15,13 +15,12 @@ \bigskip *} -consts +inductive_set bijR :: "('a => 'b => bool) => ('a set * 'b set) set" - -inductive "bijR P" - intros + for P :: "'a => 'b => bool" +where empty [simp]: "({}, {}) \ bijR P" - insert: "P a b ==> a \ A ==> b \ B ==> (A, B) \ bijR P +| insert: "P a b ==> a \ A ==> b \ B ==> (A, B) \ bijR P ==> (insert a A, insert b B) \ bijR P" text {* @@ -41,14 +40,13 @@ symP :: "('a => 'a => bool) => bool" where "symP P = (\a b. P a b = P b a)" -consts +inductive_set bijER :: "('a => 'a => bool) => 'a set set" - -inductive "bijER P" - intros + for P :: "'a => 'a => bool" +where empty [simp]: "{} \ bijER P" - insert1: "P a a ==> a \ A ==> A \ bijER P ==> insert a A \ bijER P" - insert2: "P a b ==> a \ b ==> a \ A ==> b \ A ==> A \ bijER P +| insert1: "P a a ==> a \ A ==> A \ bijER P ==> insert a A \ bijER P" +| insert2: "P a b ==> a \ b ==> a \ A ==> b \ A ==> A \ bijER P ==> insert a (insert b A) \ bijER P" diff -r 75873e94357c -r 1c4672d130b1 src/HOL/NumberTheory/EulerFermat.thy --- a/src/HOL/NumberTheory/EulerFermat.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/NumberTheory/EulerFermat.thy Wed Jul 11 11:28:13 2007 +0200 @@ -17,13 +17,12 @@ subsection {* Definitions and lemmas *} -consts +inductive_set RsetR :: "int => int set set" - -inductive "RsetR m" - intros + for m :: int + where empty [simp]: "{} \ RsetR m" - insert: "A \ RsetR m ==> zgcd (a, m) = 1 ==> + | insert: "A \ RsetR m ==> zgcd (a, m) = 1 ==> \a'. a' \ A --> \ zcong a a' m ==> insert a A \ RsetR m" consts diff -r 75873e94357c -r 1c4672d130b1 src/HOL/SET-Protocol/Cardholder_Registration.thy --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Wed Jul 11 11:28:13 2007 +0200 @@ -92,26 +92,26 @@ subsection{*Formal protocol definition *} -consts set_cr :: "event list set" -inductive set_cr - intros +inductive_set + set_cr :: "event list set" +where Nil: --{*Initial trace is empty*} "[] \ set_cr" - Fake: --{*The spy MAY say anything he CAN say.*} +| Fake: --{*The spy MAY say anything he CAN say.*} "[| evsf \ set_cr; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ set_cr" - Reception: --{*If A sends a message X to B, then B might receive it*} +| Reception: --{*If A sends a message X to B, then B might receive it*} "[| evsr \ set_cr; Says A B X \ set evsr |] ==> Gets B X # evsr \ set_cr" - SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*} +| SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*} "[| evs1 \ set_cr; C = Cardholder k; Nonce NC1 \ used evs1 |] ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \ set_cr" - SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*} +| SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*} "[| evs2 \ set_cr; Gets (CA i) {|Agent C, Nonce NC1|} \ set evs2 |] ==> Says (CA i) C @@ -120,7 +120,7 @@ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} # evs2 \ set_cr" - SET_CR3: +| SET_CR3: --{*RegFormReq: C sends his PAN and a new nonce to CA. C verifies that - nonce received is the same as that sent; @@ -144,7 +144,7 @@ # Notes C {|Key KC1, Agent (CA i)|} # evs3 \ set_cr" - SET_CR4: +| SET_CR4: --{*RegFormRes: CA responds sending NC2 back with a new nonce NCA, after checking that - the digital envelope is correctly encrypted by @{term "pubEK (CA i)"} @@ -160,7 +160,7 @@ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} # evs4 \ set_cr" - SET_CR5: +| SET_CR5: --{*CertReq: C sends his PAN, a new nonce, its proposed public signature key and its half of the secret value to CA. We now assume that C has a fixed key pair, and he submits (pubSK C). @@ -196,7 +196,7 @@ which is just @{term "Crypt K (sign SK X)"}. *} -SET_CR6: +| SET_CR6: "[| evs6 \ set_cr; Nonce NonceCCA \ used evs6; KC2 \ symKeys; KC3 \ symKeys; cardSK \ symKeys; diff -r 75873e94357c -r 1c4672d130b1 src/HOL/SET-Protocol/Merchant_Registration.thy --- a/src/HOL/SET-Protocol/Merchant_Registration.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/SET-Protocol/Merchant_Registration.thy Wed Jul 11 11:28:13 2007 +0200 @@ -13,30 +13,30 @@ encryption keys (@{term "priEK C"}). *} -consts set_mr :: "event list set" -inductive set_mr - intros +inductive_set + set_mr :: "event list set" +where Nil: --{*Initial trace is empty*} "[] \ set_mr" - Fake: --{*The spy MAY say anything he CAN say.*} +| Fake: --{*The spy MAY say anything he CAN say.*} "[| evsf \ set_mr; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ set_mr" - Reception: --{*If A sends a message X to B, then B might receive it*} +| Reception: --{*If A sends a message X to B, then B might receive it*} "[| evsr \ set_mr; Says A B X \ set evsr |] ==> Gets B X # evsr \ set_mr" - SET_MR1: --{*RegFormReq: M requires a registration form to a CA*} +| SET_MR1: --{*RegFormReq: M requires a registration form to a CA*} "[| evs1 \ set_mr; M = Merchant k; Nonce NM1 \ used evs1 |] ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \ set_mr" - SET_MR2: --{*RegFormRes: CA replies with the registration form and the +| SET_MR2: --{*RegFormRes: CA replies with the registration form and the certificates for her keys*} "[| evs2 \ set_mr; Nonce NCA \ used evs2; Gets (CA i) {|Agent M, Nonce NM1|} \ set evs2 |] @@ -45,7 +45,7 @@ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |} # evs2 \ set_mr" - SET_MR3: +| SET_MR3: --{*CertReq: M submits the key pair to be certified. The Notes event allows KM1 to be lost if M is compromised. Piero remarks that the agent mentioned inside the signature is not verified to @@ -66,7 +66,7 @@ # Notes M {|Key KM1, Agent (CA i)|} # evs3 \ set_mr" - SET_MR4: +| SET_MR4: --{*CertRes: CA issues the certificates for merSK and merEK, while checking never to have certified the m even separately. NOTE: In Cardholder Registration the diff -r 75873e94357c -r 1c4672d130b1 src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/SET-Protocol/MessageSET.thy Wed Jul 11 11:28:13 2007 +0200 @@ -100,13 +100,14 @@ subsubsection{*Inductive definition of all "parts" of a message.*} -consts parts :: "msg set => msg set" -inductive "parts H" - intros +inductive_set + parts :: "msg set => msg set" + for H :: "msg set" + where Inj [intro]: "X \ H ==> X \ parts H" - Fst: "{|X,Y|} \ parts H ==> X \ parts H" - Snd: "{|X,Y|} \ parts H ==> Y \ parts H" - Body: "Crypt K X \ parts H ==> X \ parts H" + | Fst: "{|X,Y|} \ parts H ==> X \ parts H" + | Snd: "{|X,Y|} \ parts H ==> Y \ parts H" + | Body: "Crypt K X \ parts H ==> X \ parts H" (*Monotonicity*) @@ -391,13 +392,14 @@ messages, including keys. A form of downward closure. Pairs can be taken apart; messages decrypted with known keys.*} -consts analz :: "msg set => msg set" -inductive "analz H" - intros +inductive_set + analz :: "msg set => msg set" + for H :: "msg set" + where Inj [intro,simp] : "X \ H ==> X \ analz H" - Fst: "{|X,Y|} \ analz H ==> X \ analz H" - Snd: "{|X,Y|} \ analz H ==> Y \ analz H" - Decrypt [dest]: + | Fst: "{|X,Y|} \ analz H ==> X \ analz H" + | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" + | Decrypt [dest]: "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" @@ -521,14 +523,14 @@ analz (insert (Crypt K X) H) \ insert (Crypt K X) (analz (insert X H))" apply (rule subsetI) -apply (erule_tac xa = x in analz.induct, auto) +apply (erule_tac x = x in analz.induct, auto) done lemma lemma2: "Key (invKey K) \ analz H ==> insert (Crypt K X) (analz (insert X H)) \ analz (insert (Crypt K X) H)" apply auto -apply (erule_tac xa = x in analz.induct, auto) +apply (erule_tac x = x in analz.induct, auto) apply (blast intro: analz_insertI analz.Decrypt) done @@ -639,15 +641,16 @@ encrypted with known keys. Agent names are public domain. Numbers can be guessed, but Nonces cannot be.*} -consts synth :: "msg set => msg set" -inductive "synth H" - intros +inductive_set + synth :: "msg set => msg set" + for H :: "msg set" + where Inj [intro]: "X \ H ==> X \ synth H" - Agent [intro]: "Agent agt \ synth H" - Number [intro]: "Number n \ synth H" - Hash [intro]: "X \ synth H ==> Hash X \ synth H" - MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" - Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" + | Agent [intro]: "Agent agt \ synth H" + | Number [intro]: "Number n \ synth H" + | Hash [intro]: "X \ synth H ==> Hash X \ synth H" + | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" + | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" (*Monotonicity*) lemma synth_mono: "G<=H ==> synth(G) <= synth(H)" diff -r 75873e94357c -r 1c4672d130b1 src/HOL/SET-Protocol/Purchase.thy --- a/src/HOL/SET-Protocol/Purchase.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/SET-Protocol/Purchase.thy Wed Jul 11 11:28:13 2007 +0200 @@ -57,24 +57,23 @@ PANSecret :: "nat => nat" --{*Maps Cardholders to PANSecrets.*} - set_pur :: "event list set" - -inductive set_pur - intros +inductive_set + set_pur :: "event list set" +where Nil: --{*Initial trace is empty*} "[] \ set_pur" - Fake: --{*The spy MAY say anything he CAN say.*} +| Fake: --{*The spy MAY say anything he CAN say.*} "[| evsf \ set_pur; X \ synth(analz(knows Spy evsf)) |] ==> Says Spy B X # evsf \ set_pur" - Reception: --{*If A sends a message X to B, then B might receive it*} +| Reception: --{*If A sends a message X to B, then B might receive it*} "[| evsr \ set_pur; Says A B X \ set evsr |] ==> Gets B X # evsr \ set_pur" - Start: +| Start: --{*Added start event which is out-of-band for SET: the Cardholder and the merchant agree on the amounts and uses @{text LID_M} as an identifier. @@ -91,7 +90,7 @@ # Notes M {|Number LID_M, Agent P, Transaction|} # evsStart \ set_pur" - PInitReq: +| PInitReq: --{*Purchase initialization, page 72 of Formal Protocol Desc.*} "[|evsPIReq \ set_pur; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; @@ -100,7 +99,7 @@ Notes C {|Number LID_M, Transaction |} \ set evsPIReq |] ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \ set_pur" - PInitRes: +| PInitRes: --{*Merchant replies with his own label XID and the encryption key certificate of his chosen Payment Gateway. Page 74 of Formal Protocol Desc. We use @{text LID_M} to identify Cardholder*} @@ -118,7 +117,7 @@ cert P (pubEK P) onlyEnc (priSK RCA)|}) # evsPIRes \ set_pur" - PReqUns: +| PReqUns: --{*UNSIGNED Purchase request (CardSecret = 0). Page 79 of Formal Protocol Desc. Merchant never sees the amount in clear. This holds of the real @@ -126,7 +125,8 @@ Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because the CardSecret is 0 and because AuthReq treated the unsigned case very differently from the signed one anyway.*} - "[|evsPReqU \ set_pur; + "!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU. + [|evsPReqU \ set_pur; C = Cardholder k; CardSecret k = 0; Key KC1 \ used evsPReqU; KC1 \ symKeys; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; @@ -146,14 +146,17 @@ # Notes C {|Key KC1, Agent M|} # evsPReqU \ set_pur" - PReqS: +| PReqS: --{*SIGNED Purchase request. Page 77 of Formal Protocol Desc. We could specify the equation @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the Formal Desc. gives PIHead the same format in the unsigned case. However, there's little point, as P treats the signed and unsigned cases differently.*} - "[|evsPReqS \ set_pur; + "!!C Chall_C Chall_M EKj HOD KC2 LID_M M OIData + OIDualSigned OrderDesc P PANData PIData PIDualSigned + PIHead PurchAmt Transaction XID evsPReqS k. + [|evsPReqS \ set_pur; C = Cardholder k; CardSecret k \ 0; Key KC2 \ used evsPReqS; KC2 \ symKeys; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; @@ -179,7 +182,7 @@ --{*Authorization Request. Page 92 of Formal Protocol Desc. Sent in response to Purchase Request.*} - AuthReq: +| AuthReq: "[| evsAReq \ set_pur; Key KM \ used evsAReq; KM \ symKeys; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; @@ -208,7 +211,7 @@ full protocol is [CapToken], [AcqCardMsg], [AuthToken]: optional items for split shipments, recurring payments, etc.*} - AuthResUns: +| AuthResUns: --{*Authorization Response, UNSIGNED*} "[| evsAResU \ set_pur; C = Cardholder k; M = Merchant i; @@ -225,7 +228,7 @@ authCode) # evsAResU \ set_pur" - AuthResS: +| AuthResS: --{*Authorization Response, SIGNED*} "[| evsAResS \ set_pur; C = Cardholder k; @@ -247,7 +250,7 @@ authCode) # evsAResS \ set_pur" - PRes: +| PRes: --{*Purchase response.*} "[| evsPRes \ set_pur; KP \ symKeys; M = Merchant i; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};