Adapted to new inductive definition package.
--- 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 \<Rightarrow> 'a Datatype.item set"
-
-coinductive "LList A"
- intros
+ for A :: "'a Datatype.item set"
+ where
NIL [intro]: "NIL \<in> LList A"
- CONS [intro]: "a \<in> A \<Longrightarrow> M \<in> LList A \<Longrightarrow> CONS a M \<in> LList A"
+ | CONS [intro]: "a \<in> A \<Longrightarrow> M \<in> LList A \<Longrightarrow> CONS a M \<in> LList A"
-lemma LList_mono: "A \<subseteq> B \<Longrightarrow> LList A \<subseteq> LList B"
+lemma LList_mono:
+ assumes subset: "A \<subseteq> B"
+ shows "LList A \<subseteq> 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 \<in> LList A"
+ then show "x \<in> LList B"
+ proof coinduct
+ case LList
+ then show ?case using subset
+ by cases blast+
+ qed
+qed
consts
LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
@@ -92,7 +102,7 @@
lemma LList_corec_type: "LList_corec a f \<in> LList UNIV"
proof -
- have "LList_corec a f \<in> {LList_corec a f | a. True}" by blast
+ have "\<exists>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 \<in> 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 \<in> _")
proof (unfold llist_def)
let "LList_corec a ?g" = "?corec a"
- have "?corec a \<in> {?corec x | x. True}" by blast
+ have "\<exists>x. ?corec a = ?corec x" by blast
then show "?corec a \<in> 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 \<times> 'a Datatype.item) set \<Rightarrow>
('a Datatype.item \<times> 'a Datatype.item) set"
-
-coinductive "EqLList r"
- intros
+ for r :: "('a Datatype.item \<times> 'a Datatype.item) set"
+ where
EqNIL: "(NIL, NIL) \<in> EqLList r"
- EqCONS: "(a, b) \<in> r \<Longrightarrow> (M, N) \<in> EqLList r \<Longrightarrow>
+ | EqCONS: "(a, b) \<in> r \<Longrightarrow> (M, N) \<in> EqLList r \<Longrightarrow>
(CONS a M, CONS b N) \<in> EqLList r"
lemma EqLList_unfold:
@@ -310,10 +319,10 @@
done
lemma Domain_EqLList: "Domain (EqLList (diag A)) \<subseteq> 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 \<subseteq> ?lhs"
- proof
- fix p assume "p \<in> diag (LList A)"
- then show "p \<in> EqLList (diag A)"
+ {
+ fix M N assume "(M, N) \<in> diag (LList A)"
+ then have "(M, N) \<in> EqLList (diag A)"
proof coinduct
- case (EqLList q)
- then obtain L where L: "L \<in> LList A" and q: "q = (L, L)" ..
+ case (EqLList M N)
+ then obtain L where L: "L \<in> 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 \<subseteq> ?lhs" by auto
qed
lemma EqLList_diag_iff [iff]: "(p \<in> EqLList (diag A)) = (p \<in> diag (LList A))"
@@ -359,11 +368,11 @@
lemma LList_equalityI
[consumes 1, case_names EqLList, case_conclusion EqLList EqNIL EqCONS]:
assumes r: "(M, N) \<in> r"
- and step: "\<And>p. p \<in> r \<Longrightarrow>
- p = (NIL, NIL) \<or>
- (\<exists>M N a b.
- p = (CONS a M, CONS b N) \<and> (a, b) \<in> diag A \<and>
- (M, N) \<in> r \<union> EqLList (diag A))"
+ and step: "\<And>M N. (M, N) \<in> r \<Longrightarrow>
+ M = NIL \<and> N = NIL \<or>
+ (\<exists>a b M' N'.
+ M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> diag A \<and>
+ ((M', N') \<in> r \<or> (M', N') \<in> EqLList (diag A)))"
shows "M = N"
proof -
from r have "(M, N) \<in> EqLList (diag A)"
@@ -391,39 +400,39 @@
have "(f M, g M) \<in> ?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 \<in> LList A" by blast
+ case (EqLList M N)
+ then obtain L where MN: "M = f L" "N = g L" and L: "L \<in> LList A" by blast
from L show ?case
proof (cases L)
case NIL
- with fun_NIL and q have "q \<in> diag (LList A)" by auto
- then have "q \<in> EqLList (diag A)" ..
+ with fun_NIL and MN have "(M, N) \<in> diag (LList A)" by auto
+ then have "(M, N) \<in> EqLList (diag A)" ..
then show ?thesis by cases simp_all
next
- case (CONS K a)
+ case (CONS a K)
from fun_CONS and `a \<in> A` `K \<in> LList A`
have "?fun_CONS a K" (is "?NIL \<or> ?CONS") .
then show ?thesis
proof
assume ?NIL
- with q CONS have "q \<in> diag (LList A)" by auto
- then have "q \<in> EqLList (diag A)" ..
+ with MN CONS have "(M, N) \<in> diag (LList A)" by auto
+ then have "(M, N) \<in> 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) \<in> diag A"
- and MN: "(M, N) \<in> ?bisim \<union> diag (LList A)"
+ and M'N': "(M', N') \<in> ?bisim \<union> diag (LList A)"
by blast
- from MN show ?thesis
+ from M'N' show ?thesis
proof
- assume "(M, N) \<in> ?bisim"
- with q fg ab show ?thesis by simp
+ assume "(M', N') \<in> ?bisim"
+ with MN fg ab show ?thesis by simp
next
- assume "(M, N) \<in> diag (LList A)"
- then have "(M, N) \<in> EqLList (diag A)" ..
- with q fg ab show ?thesis by simp
+ assume "(M', N') \<in> diag (LList A)"
+ then have "(M', N') \<in> EqLList (diag A)" ..
+ with MN fg ab show ?thesis by simp
qed
qed
qed
@@ -446,18 +455,18 @@
have "(h x, h' x) \<in> {(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) \<in> r"
+ MN: "M = Rep_llist l1" "N = Rep_llist l2" and r: "(l1, l2) \<in> 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 \<in> A"
shows "Lconst M \<in> LList A"
proof -
- have "Lconst M \<in> {Lconst M}" by simp
+ have "Lconst M \<in> {Lconst (id M)}" by simp
then show ?thesis
proof coinduct
case (LList N)
@@ -617,16 +626,16 @@
then show ?thesis
proof (coinduct taking: "range (\<lambda>N :: 'a Datatype.item. N)"
rule: LList_equalityI)
- case (EqLList q)
- then obtain N where q: "q = (?lhs N, ?rhs N)" and N: "N \<in> LList A" by blast
+ case (EqLList L M)
+ then obtain N where LM: "L = ?lhs N" "M = ?rhs N" and N: "N \<in> 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 (\<lambda>N :: 'a Datatype.item. N)"
rule: LList_equalityI)
- case (EqLList q)
- then obtain N where q: "q = (?lmap N, N)" and N: "N \<in> LList A" by blast
+ case (EqLList L M)
+ then obtain N where LM: "L = ?lmap N" "M = N" and N: "N \<in> 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
--- 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 \<times> ('e \<times> 'n) list)"
-inductive2 has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool"
+inductive has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool"
for G :: "('n, 'e) graph"
where
has_fpath_empty: "has_fpath G (n, [])"
--- 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) \<in> 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
--- 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 \<notin> chain S | c \<in> maxchain S
then c else SOME c'. c' \<in> 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 \<in> TFin S ==> succ S x \<in> TFin S"
- Pow_UnionI: "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
+ | Pow_UnionI: "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
monos Pow_mono
--- 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 \<in> H ==> X \<in> parts H"
- Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
- Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
- Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
+ | Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
+ | Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
+ | Body: "Crypt K X \<in> parts H ==> X \<in> 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 \<in> H ==> X \<in> analz H"
- Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
- Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
- Decrypt [dest]:
+ | Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
+ | Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+ | Decrypt [dest]:
"[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
@@ -456,14 +458,14 @@
analz (insert (Crypt K X) H) \<subseteq>
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) \<in> analz H ==>
insert (Crypt K X) (analz (insert X H)) \<subseteq>
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 \<in> H ==> X \<in> synth H"
- Agent [intro]: "Agent agt \<in> synth H"
- Number [intro]: "Number n \<in> synth H"
- Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"
- MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
- Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+ | Agent [intro]: "Agent agt \<in> synth H"
+ | Number [intro]: "Number n \<in> synth H"
+ | Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"
+ | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+ | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
text{*Monotonicity*}
lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
--- 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" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
"etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
-consts hoare :: "(triple set \<times> triple set) set"
-consts ehoare :: "(triple set \<times> etriple ) set"
-syntax (xsymbols)
- "@hoare" :: "[triple set, triple set ] => bool" ("_ |\<turnstile>/ _" [61,61] 60)
- "@hoare1" :: "[triple set, assn,stmt,assn] => bool"
- ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
-"@ehoare" :: "[triple set, etriple ] => bool" ("_ |\<turnstile>\<^sub>e/ _"[61,61]60)
-"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool"
- ("_ \<turnstile>\<^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 |\<turnstile> C" \<rightleftharpoons> "(A,C) \<in> hoare"
- "A \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
- "A |\<turnstile>\<^sub>e t" \<rightleftharpoons> "(A,t) \<in> ehoare"
- "A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (* shouldn't be necessary *)
- "A \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^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" ("_ |\<turnstile>/ _" [61, 61] 60)
+ and ehoare :: "[triple set, etriple] => bool" ("_ |\<turnstile>\<^sub>e/ _" [61, 61] 60)
+ and hoare1 :: "[triple set, assn,stmt,assn] => bool"
+ ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
+ and ehoare1 :: "[triple set, assn,expr,vassn]=> bool"
+ ("_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
+where
- Cond: "[| A |-e {P} e {Q};
- \<forall>v. A |- {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
- A |- {P} If(e) c1 Else c2 {R}"
+ "A \<turnstile> {P}c{Q} \<equiv> A |\<turnstile> {(P,c,Q)}"
+| "A \<turnstile>\<^sub>e {P}e{Q} \<equiv> A |\<turnstile>\<^sub>e (P,e,Q)"
- Loop: "A |- {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
- A |- {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
+| Skip: "A \<turnstile> {P} Skip {P}"
+
+| Comp: "[| A \<turnstile> {P} c1 {Q}; A \<turnstile> {Q} c2 {R} |] ==> A \<turnstile> {P} c1;;c2 {R}"
- LAcc: "A |-e {\<lambda>s. P (s<x>) s} LAcc x {P}"
+| Cond: "[| A \<turnstile>\<^sub>e {P} e {Q};
+ \<forall>v. A \<turnstile> {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
+ A \<turnstile> {P} If(e) c1 Else c2 {R}"
- LAss: "A |-e {P} e {\<lambda>v s. Q (lupd(x\<mapsto>v) s)} ==>
- A |- {P} x:==e {Q}"
+| Loop: "A \<turnstile> {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
+ A \<turnstile> {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
+
+| LAcc: "A \<turnstile>\<^sub>e {\<lambda>s. P (s<x>) s} LAcc x {P}"
- FAcc: "A |-e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
- A |-e {P} e..f {Q}"
+| LAss: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. Q (lupd(x\<mapsto>v) s)} ==>
+ A \<turnstile> {P} x:==e {Q}"
+
+| FAcc: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
+ A \<turnstile>\<^sub>e {P} e..f {Q}"
- FAss: "[| A |-e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
- \<forall>a. A |-e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
- A |- {P} e1..f:==e2 {R}"
+| FAss: "[| A \<turnstile>\<^sub>e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
+ \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
+ A \<turnstile> {P} e1..f:==e2 {R}"
- NewC: "A |-e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
+| NewC: "A \<turnstile>\<^sub>e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
new C {P}"
- Cast: "A |-e {P} e {\<lambda>v s. (case v of Null => True
+| Cast: "A \<turnstile>\<^sub>e {P} e {\<lambda>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 \<turnstile>\<^sub>e {P} Cast C e {Q}"
- Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
- \<forall>a p ls. A |- {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and>
+| Call: "[| A \<turnstile>\<^sub>e {P} e1 {Q}; \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {R a};
+ \<forall>a p ls. A \<turnstile> {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and>
s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s))}
Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
- A |-e {P} {C}e1..m(e2) {S}"
+ A \<turnstile>\<^sub>e {P} {C}e1..m(e2) {S}"
- Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and>
+| Meth: "\<forall>D. A \<turnstile> {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and>
P s \<and> s' = init_locs D m s}
Impl (D,m) {Q} ==>
- A |- {P} Meth (C,m) {Q}"
+ A \<turnstile> {P} Meth (C,m) {Q}"
--{* @{text "\<Union>Z"} instead of @{text "\<forall>Z"} in the conclusion and\\
Z restricted to type state due to limitations of the inductive package *}
- Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||-
+| Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile>
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
- A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
+ A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
--{* structural rules *}
- Asm: " a \<in> A ==> A ||- {a}"
+| Asm: " a \<in> A ==> A |\<turnstile> {a}"
- ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
+| ConjI: " \<forall>c \<in> C. A |\<turnstile> {c} ==> A |\<turnstile> C"
- ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
+| ConjE: "[|A |\<turnstile> C; c \<in> C |] ==> A |\<turnstile> {c}"
--{* Z restricted to type state due to limitations of the inductive package *}
- Conseq:"[| \<forall>Z::state. A |- {P' Z} c {Q' Z};
+| Conseq:"[| \<forall>Z::state. A \<turnstile> {P' Z} c {Q' Z};
\<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
- A |- {P} c {Q }"
+ A \<turnstile> {P} c {Q }"
--{* Z restricted to type state due to limitations of the inductive package *}
- eConseq:"[| \<forall>Z::state. A |-e {P' Z} e {Q' Z};
+| eConseq:"[| \<forall>Z::state. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
\<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
- A |-e {P} e {Q }"
+ A \<turnstile>\<^sub>e {P} e {Q }"
subsection "Fully polymorphic variants, required for Example only"
axioms
- Conseq:"[| \<forall>Z. A |- {P' Z} c {Q' Z};
+ Conseq:"[| \<forall>Z. A \<turnstile> {P' Z} c {Q' Z};
\<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
- A |- {P} c {Q }"
+ A \<turnstile> {P} c {Q }"
- eConseq:"[| \<forall>Z. A |-e {P' Z} e {Q' Z};
+ eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
\<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
- A |-e {P} e {Q }"
+ A \<turnstile>\<^sub>e {P} e {Q }"
- Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||-
+ Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile>
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
- A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
+ A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
subsection "Derived Rules"
--- 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} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c -n-> t) --> Q t"
+ "|= {P} c {Q} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c -n\<rightarrow> t) --> Q t"
evalid :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
- "|=e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e>v-n-> t) --> Q v t"
+ "|=e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e\<succ>v-n\<rightarrow> t) --> Q v t"
nvalid :: "[nat, triple ] => bool" ("|=_: _" [61,61] 60)
- "|=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c -n-> t --> P s --> Q t"
+ "|=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c -n\<rightarrow> t --> P s --> Q t"
envalid :: "[nat,etriple ] => bool" ("|=_:e _" [61,61] 60)
- "|=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e>v-n-> t --> P s --> Q v t"
+ "|=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e\<succ>v-n\<rightarrow> t --> P s --> Q v t"
nvalids :: "[nat, triple set] => bool" ("||=_: _" [61,61] 60)
"||=n: T \<equiv> \<forall>t\<in>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 \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n-> t)"
+ "MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n\<rightarrow> t)"
MGTe :: "expr => state => etriple"
- "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
+ "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> t)"
syntax (xsymbols)
MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
syntax (HTML output)
--- 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 \<times> stmt \<times> nat \<times> state) set"
- eval :: "(state \<times> expr \<times> val \<times> nat \<times> state) set"
-syntax (xsymbols)
- exec :: "[state,stmt, nat,state] => bool" ("_ -_-_\<rightarrow> _" [98,90, 65,98] 89)
- eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[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') \<in> exec"
- "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval"
+inductive
+ exec :: "[state,stmt, nat,state] => bool" ("_ -_-_\<rightarrow> _" [98,90, 65,98] 89)
+ and eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89)
+where
+ Skip: " s -Skip-n\<rightarrow> s"
+
+| Comp: "[| s0 -c1-n\<rightarrow> s1; s1 -c2-n\<rightarrow> s2 |] ==>
+ s0 -c1;; c2-n\<rightarrow> 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\<succ>v-n\<rightarrow> s1; s1 -(if v\<noteq>Null then c1 else c2)-n\<rightarrow> s2 |] ==>
+ s0 -If(e) c1 Else c2-n\<rightarrow> s2"
- Cond: "[| s0 -e>v-n-> s1; s1 -(if v\<noteq>Null then c1 else c2)-n-> s2 |] ==>
- s0 -If(e) c1 Else c2-n-> s2"
+| LoopF:" s0<x> = Null ==>
+ s0 -While(x) c-n\<rightarrow> s0"
+| LoopT:"[| s0<x> \<noteq> Null; s0 -c-n\<rightarrow> s1; s1 -While(x) c-n\<rightarrow> s2 |] ==>
+ s0 -While(x) c-n\<rightarrow> s2"
- LoopF:" s0<x> = Null ==>
- s0 -While(x) c-n-> s0"
- LoopT:"[| s0<x> \<noteq> Null; s0 -c-n-> s1; s1 -While(x) c-n-> s2 |] ==>
- s0 -While(x) c-n-> s2"
+| LAcc: " s -LAcc x\<succ>s<x>-n\<rightarrow> s"
+
+| LAss: " s -e\<succ>v-n\<rightarrow> s' ==>
+ s -x:==e-n\<rightarrow> lupd(x\<mapsto>v) s'"
- LAcc: " s -LAcc x>s<x>-n-> s"
-
- LAss: " s -e>v-n-> s' ==>
- s -x:==e-n-> lupd(x\<mapsto>v) s'"
+| FAcc: " s -e\<succ>Addr a-n\<rightarrow> s' ==>
+ s -e..f\<succ>get_field s' a f-n\<rightarrow> s'"
- FAcc: " s -e>Addr a-n-> s' ==>
- s -e..f>get_field s' a f-n-> s'"
+| FAss: "[| s0 -e1\<succ>Addr a-n\<rightarrow> s1; s1 -e2\<succ>v-n\<rightarrow> s2 |] ==>
+ s0 -e1..f:==e2-n\<rightarrow> 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\<succ>Addr a-n\<rightarrow> new_obj a C s"
- Cast: "[| s -e>v-n-> s';
+| Cast: "[| s -e\<succ>v-n\<rightarrow> s';
case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==>
- s -Cast C e>v-n-> s'"
+ s -Cast C e\<succ>v-n\<rightarrow> s'"
- Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2;
- lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n-> s3
- |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
+| Call: "[| s0 -e1\<succ>a-n\<rightarrow> s1; s1 -e2\<succ>p-n\<rightarrow> s2;
+ lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n\<rightarrow> s3
+ |] ==> s0 -{C}e1..m(e2)\<succ>s3<Res>-n\<rightarrow> set_locs s2 s3"
- Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
- init_locs D m s -Impl (D,m)-n-> s' |] ==>
- s -Meth (C,m)-n-> s'"
+| Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
+ init_locs D m s -Impl (D,m)-n\<rightarrow> s' |] ==>
+ s -Meth (C,m)-n\<rightarrow> s'"
- Impl: " s -body Cm- n-> s' ==>
- s -Impl Cm-Suc n-> s'"
+| Impl: " s -body Cm- n\<rightarrow> s' ==>
+ s -Impl Cm-Suc n\<rightarrow> s'"
inductive_cases exec_elim_cases':
--- 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 \<times> ty ) set" --{* widening *}
subcls1 :: "(cname \<times> cname) set" --{* subclass *}
syntax (xsymbols)
- widen :: "[ty , ty ] => bool" ("_ \<preceq> _" [71,71] 70)
subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70)
subcls :: "[cname, cname] => bool" ("_ \<preceq>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 \<prec>C1 D" == "(C,D) \<in> subcls1"
"C \<preceq>C D" == "(C,D) \<in> subcls1^*"
- "S \<preceq> T" == "(S,T) \<in> widen"
consts
method :: "cname => (mname \<rightharpoonup> methd)"
@@ -38,10 +34,12 @@
subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
text{* Widening, viz. method invocation conversion *}
-inductive widen intros
- refl [intro!, simp]: "T \<preceq> T"
- subcls : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
- null [intro!]: "NT \<preceq> R"
+inductive
+ widen :: "ty => ty => bool" ("_ \<preceq> _" [71,71] 70)
+where
+ refl [intro!, simp]: "T \<preceq> T"
+| subcls: "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
+| null [intro!]: "NT \<preceq> R"
lemma subcls1D:
"C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)"
--- 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\<Rightarrow>('a noption)) set"
-inductive ABS_set
- intros
+
+inductive_set ABS_set :: "('x\<Rightarrow>('a noption)) set"
+ where
ABS_in: "(abs_fun a x)\<in>ABS_set"
typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a noption)) set"
--- 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]: "({}, {}) \<in> bijR P"
- insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
+| insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
==> (insert a A, insert b B) \<in> bijR P"
text {*
@@ -41,14 +40,13 @@
symP :: "('a => 'a => bool) => bool" where
"symP P = (\<forall>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]: "{} \<in> bijER P"
- insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P"
- insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P
+| insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P"
+| insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P
==> insert a (insert b A) \<in> bijER P"
--- 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]: "{} \<in> RsetR m"
- insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
+ | insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
\<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
consts
--- 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*}
"[] \<in> set_cr"
- Fake: --{*The spy MAY say anything he CAN say.*}
+| Fake: --{*The spy MAY say anything he CAN say.*}
"[| evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)) |]
==> Says Spy B X # evsf \<in> 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 \<in> set_cr; Says A B X \<in> set evsr |]
==> Gets B X # evsr \<in> 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 \<in> set_cr; C = Cardholder k; Nonce NC1 \<notin> used evs1 |]
==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \<in> set_cr"
- SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
+| SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
"[| evs2 \<in> set_cr;
Gets (CA i) {|Agent C, Nonce NC1|} \<in> set evs2 |]
==> Says (CA i) C
@@ -120,7 +120,7 @@
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
# evs2 \<in> 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 \<in> 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 \<in> 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 \<in> set_cr;
Nonce NonceCCA \<notin> used evs6;
KC2 \<in> symKeys; KC3 \<in> symKeys; cardSK \<notin> symKeys;
--- 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*}
"[] \<in> set_mr"
- Fake: --{*The spy MAY say anything he CAN say.*}
+| Fake: --{*The spy MAY say anything he CAN say.*}
"[| evsf \<in> set_mr; X \<in> synth (analz (knows Spy evsf)) |]
==> Says Spy B X # evsf \<in> 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 \<in> set_mr; Says A B X \<in> set evsr |]
==> Gets B X # evsr \<in> 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 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |]
==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \<in> 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 \<in> set_mr; Nonce NCA \<notin> used evs2;
Gets (CA i) {|Agent M, Nonce NM1|} \<in> set evs2 |]
@@ -45,7 +45,7 @@
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |}
# evs2 \<in> 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 \<in> 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
--- 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 \<in> H ==> X \<in> parts H"
- Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
- Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
- Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
+ | Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
+ | Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
+ | Body: "Crypt K X \<in> parts H ==> X \<in> 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 \<in> H ==> X \<in> analz H"
- Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
- Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
- Decrypt [dest]:
+ | Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
+ | Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+ | Decrypt [dest]:
"[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
@@ -521,14 +523,14 @@
analz (insert (Crypt K X) H) \<subseteq>
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) \<in> analz H ==>
insert (Crypt K X) (analz (insert X H)) \<subseteq>
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 \<in> H ==> X \<in> synth H"
- Agent [intro]: "Agent agt \<in> synth H"
- Number [intro]: "Number n \<in> synth H"
- Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"
- MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
- Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+ | Agent [intro]: "Agent agt \<in> synth H"
+ | Number [intro]: "Number n \<in> synth H"
+ | Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"
+ | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+ | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
(*Monotonicity*)
lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
--- 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*}
"[] \<in> set_pur"
- Fake: --{*The spy MAY say anything he CAN say.*}
+| Fake: --{*The spy MAY say anything he CAN say.*}
"[| evsf \<in> set_pur; X \<in> synth(analz(knows Spy evsf)) |]
==> Says Spy B X # evsf \<in> 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 \<in> set_pur; Says A B X \<in> set evsr |]
==> Gets B X # evsr \<in> 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 \<in> set_pur"
- PInitReq:
+| PInitReq:
--{*Purchase initialization, page 72 of Formal Protocol Desc.*}
"[|evsPIReq \<in> set_pur;
Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
@@ -100,7 +99,7 @@
Notes C {|Number LID_M, Transaction |} \<in> set evsPIReq |]
==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \<in> 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 \<in> 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 \<in> set_pur;
+ "!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU.
+ [|evsPReqU \<in> set_pur;
C = Cardholder k; CardSecret k = 0;
Key KC1 \<notin> used evsPReqU; KC1 \<in> symKeys;
Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
@@ -146,14 +146,17 @@
# Notes C {|Key KC1, Agent M|}
# evsPReqU \<in> 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 \<in> 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 \<in> set_pur;
C = Cardholder k;
CardSecret k \<noteq> 0; Key KC2 \<notin> used evsPReqS; KC2 \<in> 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 \<in> set_pur;
Key KM \<notin> used evsAReq; KM \<in> 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 \<in> set_pur;
C = Cardholder k; M = Merchant i;
@@ -225,7 +228,7 @@
authCode)
# evsAResU \<in> set_pur"
- AuthResS:
+| AuthResS:
--{*Authorization Response, SIGNED*}
"[| evsAResS \<in> set_pur;
C = Cardholder k;
@@ -247,7 +250,7 @@
authCode)
# evsAResS \<in> set_pur"
- PRes:
+| PRes:
--{*Purchase response.*}
"[| evsPRes \<in> set_pur; KP \<in> symKeys; M = Merchant i;
Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};