--- a/src/FOL/FOL.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/FOL.thy Fri Feb 18 17:05:19 2011 +0100
@@ -18,7 +18,7 @@
subsection {* The classical axiom *}
-axioms
+axiomatization where
classical: "(~P ==> P) ==> P"
--- a/src/FOL/IFOL.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/IFOL.thy Fri Feb 18 17:05:19 2011 +0100
@@ -88,42 +88,39 @@
finalconsts
False All Ex eq conj disj imp
-axioms
-
+axiomatization where
(* Equality *)
-
- refl: "a=a"
+ refl: "a=a" and
subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
+
+axiomatization where
(* Propositional logic *)
-
- conjI: "[| P; Q |] ==> P&Q"
- conjunct1: "P&Q ==> P"
- conjunct2: "P&Q ==> Q"
+ conjI: "[| P; Q |] ==> P&Q" and
+ conjunct1: "P&Q ==> P" and
+ conjunct2: "P&Q ==> Q" and
- disjI1: "P ==> P|Q"
- disjI2: "Q ==> P|Q"
- disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R"
+ disjI1: "P ==> P|Q" and
+ disjI2: "Q ==> P|Q" and
+ disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and
- impI: "(P ==> Q) ==> P-->Q"
- mp: "[| P-->Q; P |] ==> Q"
+ impI: "(P ==> Q) ==> P-->Q" and
+ mp: "[| P-->Q; P |] ==> Q" and
FalseE: "False ==> P"
+axiomatization where
(* Quantifiers *)
+ allI: "(!!x. P(x)) ==> (ALL x. P(x))" and
+ spec: "(ALL x. P(x)) ==> P(x)" and
- allI: "(!!x. P(x)) ==> (ALL x. P(x))"
- spec: "(ALL x. P(x)) ==> P(x)"
-
- exI: "P(x) ==> (EX x. P(x))"
+ exI: "P(x) ==> (EX x. P(x))" and
exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R"
-axioms
-
+axiomatization where
(* Reflection, admissible *)
-
- eq_reflection: "(x=y) ==> (x==y)"
+ eq_reflection: "(x=y) ==> (x==y)" and
iff_reflection: "(P<->Q) ==> (P==Q)"
--- a/src/FOL/ex/If.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/If.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/If.ML
+(* Title: FOL/ex/If.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Feb 18 17:05:19 2011 +0100
@@ -13,10 +13,10 @@
zero :: int ("0")
minus :: "int => int" ("- _")
-axioms
- int_assoc: "(x + y::int) + z = x + (y + z)"
- int_zero: "0 + x = x"
- int_minus: "(-x) + x = 0"
+axiomatization where
+ int_assoc: "(x + y::int) + z = x + (y + z)" and
+ int_zero: "0 + x = x" and
+ int_minus: "(-x) + x = 0" and
int_minus2: "-(-x) = x"
section {* Inference of parameter types *}
@@ -527,13 +527,12 @@
end
-consts
- gle :: "'a => 'a => o" gless :: "'a => 'a => o"
- gle' :: "'a => 'a => o" gless' :: "'a => 'a => o"
-
-axioms
- grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
- grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
+axiomatization
+ gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
+ gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
+where
+ grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and
+ grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
text {* Setup *}
--- a/src/FOL/ex/Nat.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/Nat.thy Fri Feb 18 17:05:19 2011 +0100
@@ -12,21 +12,19 @@
typedecl nat
arities nat :: "term"
-consts
- Zero :: nat ("0")
- Suc :: "nat => nat"
+axiomatization
+ Zero :: nat ("0") and
+ Suc :: "nat => nat" and
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
- add :: "[nat, nat] => nat" (infixl "+" 60)
+where
+ induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" and
+ Suc_inject: "Suc(m)=Suc(n) ==> m=n" and
+ Suc_neq_0: "Suc(m)=0 ==> R" and
+ rec_0: "rec(0,a,f) = a" and
+ rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-axioms
- induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
- Suc_inject: "Suc(m)=Suc(n) ==> m=n"
- Suc_neq_0: "Suc(m)=0 ==> R"
- rec_0: "rec(0,a,f) = a"
- rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-
-defs
- add_def: "m+n == rec(m, n, %x y. Suc(y))"
+definition add :: "[nat, nat] => nat" (infixl "+" 60)
+ where "m + n == rec(m, n, %x y. Suc(y))"
subsection {* Proofs about the natural numbers *}
--- a/src/FOL/ex/Prolog.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/Prolog.thy Fri Feb 18 17:05:19 2011 +0100
@@ -11,15 +11,16 @@
typedecl 'a list
arities list :: ("term") "term"
-consts
- Nil :: "'a list"
- Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60)
- app :: "['a list, 'a list, 'a list] => o"
+
+axiomatization
+ Nil :: "'a list" and
+ Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60) and
+ app :: "['a list, 'a list, 'a list] => o" and
rev :: "['a list, 'a list] => o"
-axioms
- appNil: "app(Nil,ys,ys)"
- appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
- revNil: "rev(Nil,Nil)"
+where
+ appNil: "app(Nil,ys,ys)" and
+ appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" and
+ revNil: "rev(Nil,Nil)" and
revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
--- a/src/FOL/ex/Quantifiers_Cla.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/Quantifiers_Cla.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/Quantifiers_Int.thy
+(* Title: FOL/ex/Quantifiers_Cla.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOLP/FOLP.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOLP/FOLP.thy Fri Feb 18 17:05:19 2011 +0100
@@ -11,10 +11,8 @@
("classical.ML") ("simp.ML") ("simpdata.ML")
begin
-consts
- cla :: "[p=>p]=>p"
-axioms
- classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
+axiomatization cla :: "[p=>p]=>p"
+ where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
(*** Classical introduction rules for | and EX ***)
--- a/src/FOLP/ex/Foundation.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOLP/ex/Foundation.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: FOLP/ex/Foundation.ML
+(* Title: FOLP/ex/Foundation.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOLP/ex/Nat.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOLP/ex/Nat.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: FOLP/ex/nat.thy
+(* Title: FOLP/ex/Nat.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/HOL/Auth/Guard/Analz.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Analz.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: december 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Analz.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2001 University of Cambridge
+*)
header{*Decomposition of Analz into two parts*}
--- a/src/HOL/Auth/Guard/Extensions.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: november 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Extensions.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2001 University of Cambridge
+*)
header {*Extensions to Standard Theories*}
--- a/src/HOL/Auth/Guard/Guard.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: january 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Protocol-Independent Confidentiality Theorem on Nonces*}
--- a/src/HOL/Auth/Guard/GuardK.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,18 +1,12 @@
-(******************************************************************************
-very similar to Guard except:
+(* Title: HOL/Auth/Guard/GuardK.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+
+Very similar to Guard except:
- Guard is replaced by GuardK, guard by guardK, Nonce by Key
- some scripts are slightly modified (+ keyset_in, kparts_parts)
- the hypothesis Key n ~:G (keyset G) is added
-
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+*)
header{*protocol-independent confidentiality theorem on keys*}
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,15 +1,9 @@
-(******************************************************************************
-incorporating Lowe's fix (inclusion of B's identity in round 2)
+(* Title: HOL/Auth/Guard/Guard_NS_Public.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+Incorporating Lowe's fix (inclusion of B's identity in round 2).
+*)
header{*Needham-Schroeder-Lowe Public-Key Protocol*}
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard_OtwayRees.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Otway-Rees Protocol*}
--- a/src/HOL/Auth/Guard/Guard_Public.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,15 +1,9 @@
-(******************************************************************************
-lemmas on guarded messages for public protocols
+(* Title: HOL/Auth/Guard/Guard_Public.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+Lemmas on guarded messages for public protocols.
+*)
theory Guard_Public imports Guard Public Extensions begin
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard_Shared.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*lemmas on guarded messages for protocols with symmetric keys*}
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard_Yahalom.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Yahalom Protocol*}
--- a/src/HOL/Auth/Guard/List_Msg.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/List_Msg.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: november 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/List_Msg.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2001 University of Cambridge
+*)
header{*Lists of Messages and Lists of Agents*}
--- a/src/HOL/Auth/Guard/P1.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/P1.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,17 +1,11 @@
-(******************************************************************************
-from G. Karjoth, N. Asokan and C. Gulcu
-"Protecting the computation results of free-roaming agents"
-Mobiles Agents 1998, LNCS 1477
+(* Title: HOL/Auth/Guard/P1.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: february 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+From G. Karjoth, N. Asokan and C. Gulcu
+"Protecting the computation results of free-roaming agents"
+Mobiles Agents 1998, LNCS 1477.
+*)
header{*Protocol P1*}
--- a/src/HOL/Auth/Guard/P2.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/P2.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,17 +1,11 @@
-(******************************************************************************
-from G. Karjoth, N. Asokan and C. Gulcu
-"Protecting the computation results of free-roaming agents"
-Mobiles Agents 1998, LNCS 1477
+(* Title: HOL/Auth/Guard/P2.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+From G. Karjoth, N. Asokan and C. Gulcu
+"Protecting the computation results of free-roaming agents"
+Mobiles Agents 1998, LNCS 1477.
+*)
header{*Protocol P2*}
--- a/src/HOL/Auth/Guard/Proto.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: april 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Proto.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Other Protocol-Independent Results*}
@@ -15,13 +9,13 @@
subsection{*protocols*}
-types rule = "event set * event"
+type_synonym rule = "event set * event"
abbreviation
msg' :: "rule => msg" where
"msg' R == msg (snd R)"
-types proto = "rule set"
+type_synonym proto = "rule set"
definition wdef :: "proto => bool" where
"wdef p == ALL R k. R:p --> Number k:parts {msg' R}
@@ -155,9 +149,9 @@
subsection{*types*}
-types keyfun = "rule => subs => nat => event list => key set"
+type_synonym keyfun = "rule => subs => nat => event list => key set"
-types secfun = "rule => nat => subs => key set => msg"
+type_synonym secfun = "rule => nat => subs => key set => msg"
subsection{*introduction of a fresh guarded nonce*}
--- a/src/HOL/Auth/KerberosIV.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/KerberosIV.thy Fri Feb 18 17:05:19 2011 +0100
@@ -16,7 +16,7 @@
Tgs :: agent where "Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
--- a/src/HOL/Auth/KerberosIV_Gets.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/KerberosIV_Gets.thy Fri Feb 18 17:05:19 2011 +0100
@@ -16,7 +16,7 @@
Tgs :: agent where "Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
--- a/src/HOL/Auth/KerberosV.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/KerberosV.thy Fri Feb 18 17:05:19 2011 +0100
@@ -17,7 +17,7 @@
"Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
--- a/src/HOL/Auth/Message.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Message.thy Fri Feb 18 17:05:19 2011 +0100
@@ -16,7 +16,7 @@
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
by blast
-types
+type_synonym
key = nat
consts
--- a/src/HOL/Auth/Public.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Public.thy Fri Feb 18 17:05:19 2011 +0100
@@ -68,7 +68,7 @@
done
-axioms
+axiomatization where
(*No private key equals any public key (essential to ensure that private
keys are private!) *)
privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
@@ -141,7 +141,7 @@
apply (simp add: inj_on_def split: agent.split)
done
-axioms
+axiomatization where
sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
text{*Injectiveness: Agents' long-term keys are distinct.*}
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri Feb 18 17:05:19 2011 +0100
@@ -5,24 +5,19 @@
theory ShoupRubin imports Smartcard begin
-consts
-
- sesK :: "nat*key => key"
-
-axioms
-
+axiomatization sesK :: "nat*key => key"
+where
(*sesK is injective on each component*)
- inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
-
+ inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')" and
(*all long-term keys differ from sesK*)
- shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
- crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
- pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)"
- pairK_disj_sesK[iff]:"pairK(A,B) \<noteq> sesK(m,pk)"
+ shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)" and
+ crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)" and
+ pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)" and
+ pairK_disj_sesK[iff]:"pairK(A,B) \<noteq> sesK(m,pk)" and
(*needed for base case in analz_image_freshK*)
Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
- Atomic`(KEY`K) \<union> Atomic`(NONCE`N)"
+ Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" and
(*this protocol makes the assumption of secure means
between each agent and his smartcard*)
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri Feb 18 17:05:19 2011 +0100
@@ -11,24 +11,20 @@
Availability. Only the updated version makes the goals of confidentiality,
authentication and key distribution available to both peers.*}
-consts
-
- sesK :: "nat*key => key"
-
-axioms
-
+axiomatization sesK :: "nat*key => key"
+where
(*sesK is injective on each component*)
- inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
+ inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')" and
(*all long-term keys differ from sesK*)
- shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
- crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
- pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)"
- pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)"
+ shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)" and
+ crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)" and
+ pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)" and
+ pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)" and
(*needed for base case in analz_image_freshK*)
Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
- Atomic`(KEY`K) \<union> Atomic`(NONCE`N)"
+ Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" and
(*this protocol makes the assumption of secure means
between each agent and his smartcard*)
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Fri Feb 18 17:05:19 2011 +0100
@@ -16,31 +16,30 @@
smartcard, which independently may be stolen or cloned.
*}
-consts
- shrK :: "agent => key" (*long-term keys saved in smart cards*)
- crdK :: "card => key" (*smart cards' symmetric keys*)
- pin :: "agent => key" (*pin to activate the smart cards*)
+axiomatization
+ shrK :: "agent => key" and (*long-term keys saved in smart cards*)
+ crdK :: "card => key" and (*smart cards' symmetric keys*)
+ pin :: "agent => key" and (*pin to activate the smart cards*)
(*Mostly for Shoup-Rubin*)
- Pairkey :: "agent * agent => nat"
+ Pairkey :: "agent * agent => nat" and
pairK :: "agent * agent => key"
-
-axioms
- inj_shrK: "inj shrK" --{*No two smartcards store the same key*}
- inj_crdK: "inj crdK" --{*Nor do two cards*}
- inj_pin : "inj pin" --{*Nor do two agents have the same pin*}
+where
+ inj_shrK: "inj shrK" and --{*No two smartcards store the same key*}
+ inj_crdK: "inj crdK" and --{*Nor do two cards*}
+ inj_pin : "inj pin" and --{*Nor do two agents have the same pin*}
(*pairK is injective on each component, if we assume encryption to be a PRF
or at least collision free *)
- inj_pairK [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')"
- comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)"
+ inj_pairK [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')" and
+ comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)" and
(*long-term keys differ from each other*)
- pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C"
- pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P"
- pairK_disj_pin [iff]: "pairK(A,B) \<noteq> pin P"
- shrK_disj_crdK [iff]: "shrK P \<noteq> crdK C"
- shrK_disj_pin [iff]: "shrK P \<noteq> pin Q"
+ pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C" and
+ pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P" and
+ pairK_disj_pin [iff]: "pairK(A,B) \<noteq> pin P" and
+ shrK_disj_crdK [iff]: "shrK P \<noteq> crdK C" and
+ shrK_disj_pin [iff]: "shrK P \<noteq> pin Q" and
crdK_disj_pin [iff]: "crdK C \<noteq> pin P"
definition legalUse :: "card => bool" ("legalUse (_)") where
@@ -78,8 +77,8 @@
end
text{*Still relying on axioms*}
-axioms
- Key_supply_ax: "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs"
+axiomatization where
+ Key_supply_ax: "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs" and
(*Needed because of Spy's knowledge of Pairkeys*)
Nonce_supply_ax: "finite NN \<Longrightarrow> \<exists> N. N \<notin> NN & Nonce N \<notin> used evs"
@@ -129,7 +128,7 @@
(*Specialized to shared-key model: no @{term invKey}*)
lemma keysFor_parts_insert:
"\<lbrakk> K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) \<rbrakk>
- \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
+ \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
by (force dest: EventSC.keysFor_parts_insert)
lemma Crypt_imp_keysFor: "Crypt K X \<in> H \<Longrightarrow> K \<in> keysFor H"
--- a/src/HOL/Auth/TLS.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/TLS.thy Fri Feb 18 17:05:19 2011 +0100
@@ -86,9 +86,9 @@
apply (simp add: inj_on_def prod_encode_eq split: role.split)
done
-axioms
+axiomatization where
--{*sessionK makes symmetric keys*}
- isSym_sessionK: "sessionK nonces \<in> symKeys"
+ isSym_sessionK: "sessionK nonces \<in> symKeys" and
--{*sessionK never clashes with a long-term symmetric key
(they don't exist in TLS anyway)*}
--- a/src/HOL/Bali/AxSem.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/AxSem.thy Fri Feb 18 17:05:19 2011 +0100
@@ -36,7 +36,7 @@
\end{itemize}
*}
-types res = vals --{* result entry *}
+type_synonym res = vals --{* result entry *}
abbreviation (input)
Val where "Val x == In1 x"
@@ -58,7 +58,7 @@
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> CONST the_In3"
--{* relation on result values, state and auxiliary variables *}
-types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
+type_synonym 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
translations
(type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
@@ -381,7 +381,7 @@
datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be
something like triple = \<forall>'a. triple ('a assn) term ('a assn) **)
("{(1_)}/ _>/ {(1_)}" [3,65,3]75)
-types 'a triples = "'a triple set"
+type_synonym 'a triples = "'a triple set"
abbreviation
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"
--- a/src/HOL/Bali/Conform.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Conform.thy Fri Feb 18 17:05:19 2011 +0100
@@ -16,7 +16,7 @@
\end{itemize}
*}
-types env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
+type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
section "extension of global store"
--- a/src/HOL/Bali/Decl.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Decl.thy Fri Feb 18 17:05:19 2011 +0100
@@ -136,7 +136,7 @@
subsubsection {* Static Modifier *}
-types stat_modi = bool (* modifier: static *)
+type_synonym stat_modi = bool (* modifier: static *)
subsection {* Declaration (base "class" for member,interface and class
declarations *}
@@ -164,8 +164,7 @@
(type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
(type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
-types
- fdecl (* field declaration, cf. 8.3 *)
+type_synonym fdecl (* field declaration, cf. 8.3 *)
= "vname \<times> field"
@@ -185,7 +184,7 @@
record methd = mhead + (* method in a class *)
mbody::mbody
-types mdecl = "sig \<times> methd" (* method declaration in a class *)
+type_synonym mdecl = "sig \<times> methd" (* method declaration in a class *)
translations
@@ -300,7 +299,7 @@
record iface = ibody + --{* interface *}
isuperIfs:: "qtname list" --{* superinterface list *}
-types
+type_synonym
idecl --{* interface declaration, cf. 9.1 *}
= "qtname \<times> iface"
@@ -332,7 +331,7 @@
record "class" = cbody + --{* class *}
super :: "qtname" --{* superclass *}
superIfs:: "qtname list" --{* implemented interfaces *}
-types
+type_synonym
cdecl --{* class declaration, cf. 8.1 *}
= "qtname \<times> class"
--- a/src/HOL/Bali/DeclConcepts.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1401,7 +1401,7 @@
section "fields and methods"
-types
+type_synonym
fspec = "vname \<times> qtname"
translations
--- a/src/HOL/Bali/DefiniteAssignment.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Fri Feb 18 17:05:19 2011 +0100
@@ -498,7 +498,7 @@
section "The rules of definite assignment"
-types breakass = "(label, lname) tables"
+type_synonym breakass = "(label, lname) tables"
--{* Mapping from a break label, to the set of variables that will be assigned
if the evaluation terminates with this break *}
--- a/src/HOL/Bali/Eval.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Eval.thy Fri Feb 18 17:05:19 2011 +0100
@@ -96,8 +96,8 @@
*}
-types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
- vals = "(val, vvar, val list) sum3"
+type_synonym vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
+type_synonym vals = "(val, vvar, val list) sum3"
translations
(type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
(type) "vals" <= (type) "(val, vvar, val list) sum3"
--- a/src/HOL/Bali/State.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/State.thy Fri Feb 18 17:05:19 2011 +0100
@@ -27,7 +27,7 @@
since its type is given already by the reference to
it (see below) *}
-types vn = "fspec + int" --{* variable name *}
+type_synonym vn = "fspec + int" --{* variable name *}
record obj =
tag :: "obj_tag" --{* generalized object *}
"values" :: "(vn, val) table"
@@ -130,7 +130,7 @@
section "object references"
-types oref = "loc + qtname" --{* generalized object reference *}
+type_synonym oref = "loc + qtname" --{* generalized object reference *}
syntax
Heap :: "loc \<Rightarrow> oref"
Stat :: "qtname \<Rightarrow> oref"
@@ -213,11 +213,11 @@
section "stores"
-types globs --{* global variables: heap and static variables *}
+type_synonym globs --{* global variables: heap and static variables *}
= "(oref , obj) table"
- heap
+type_synonym heap
= "(loc , obj) table"
-(* locals
+(* type_synonym locals
= "(lname, val) table" *) (* defined in Value.thy local variables *)
translations
@@ -579,7 +579,7 @@
section "full program state"
-types
+type_synonym
state = "abopt \<times> st" --{* state including abruption information *}
translations
--- a/src/HOL/Bali/Table.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Table.thy Fri Feb 18 17:05:19 2011 +0100
@@ -29,9 +29,9 @@
\end{itemize}
*}
-types ('a, 'b) table --{* table with key type 'a and contents type 'b *}
+type_synonym ('a, 'b) table --{* table with key type 'a and contents type 'b *}
= "'a \<rightharpoonup> 'b"
- ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *}
+type_synonym ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *}
= "'a \<Rightarrow> 'b set"
--- a/src/HOL/Bali/Term.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Term.thy Fri Feb 18 17:05:19 2011 +0100
@@ -57,7 +57,7 @@
-types locals = "(lname, val) table" --{* local variables *}
+type_synonym locals = "(lname, val) table" --{* local variables *}
datatype jump
@@ -78,7 +78,7 @@
| Jump jump --{* break, continue, return *}
| Error error -- {* runtime errors, we wan't to detect and proof absent
in welltyped programms *}
-types
+type_synonym
abopt = "abrupt option"
text {* Local variable store and exception.
@@ -235,7 +235,7 @@
intermediate steps of class-initialisation.
*}
-types "term" = "(expr+stmt,var,expr list) sum3"
+type_synonym "term" = "(expr+stmt,var,expr list) sum3"
translations
(type) "sig" <= (type) "mname \<times> ty list"
(type) "term" <= (type) "(expr+stmt,var,expr list) sum3"
--- a/src/HOL/Bali/Value.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Value.thy Fri Feb 18 17:05:19 2011 +0100
@@ -26,7 +26,7 @@
primrec the_Addr :: "val \<Rightarrow> loc"
where "the_Addr (Addr a) = a"
-types dyn_ty = "loc \<Rightarrow> ty option"
+type_synonym dyn_ty = "loc \<Rightarrow> ty option"
primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
where
--- a/src/HOL/Bali/WellType.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/WellType.thy Fri Feb 18 17:05:19 2011 +0100
@@ -28,7 +28,7 @@
\end{itemize}
*}
-types lenv
+type_synonym lenv
= "(lname, ty) table" --{* local variables, including This and Result*}
record env =
@@ -49,7 +49,7 @@
section "Static overloading: maximally specific methods "
-types
+type_synonym
emhead = "ref_ty \<times> mhead"
--{* Some mnemotic selectors for emhead *}
@@ -244,7 +244,7 @@
section "Typing for terms"
-types tys = "ty + ty list"
+type_synonym tys = "ty + ty list"
translations
(type) "tys" <= (type) "ty + ty list"
--- a/src/HOL/ZF/Games.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/ZF/Games.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/ZF/MainZF.thy/Games.thy
+(* Title: HOL/ZF/Games.thy
Author: Steven Obua
An application of HOLZF: Partizan Games. See "Partizan Games in
--- a/src/Pure/Concurrent/future.ML Fri Feb 18 16:30:44 2011 +0100
+++ b/src/Pure/Concurrent/future.ML Fri Feb 18 17:05:19 2011 +0100
@@ -203,7 +203,7 @@
Task_Queue.running task (fn () =>
setmp_worker_task task (fn () =>
fold (fn job => fn ok => job valid andalso ok) jobs true) ());
- val _ = Multithreading.tracing 1 (fn () =>
+ val _ = Multithreading.tracing 2 (fn () =>
let
val s = Task_Queue.str_of_task task;
fun micros time = string_of_int (Time.toNanoseconds time div 1000);
--- a/src/Pure/goal.ML Fri Feb 18 16:30:44 2011 +0100
+++ b/src/Pure/goal.ML Fri Feb 18 17:05:19 2011 +0100
@@ -115,7 +115,7 @@
let
val n = m + i;
val _ =
- Multithreading.tracing 1 (fn () =>
+ Multithreading.tracing 2 (fn () =>
("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
in n end);
--- a/src/ZF/AC/AC17_AC1.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/AC/AC17_AC1.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/AC/AC1_AC17.thy
+(* Title: ZF/AC/AC17_AC1.thy
Author: Krzysztof Grabczewski
The equivalence of AC0, AC1 and AC17
--- a/src/ZF/ArithSimp.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ArithSimp.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ArithSimp.ML
+(* Title: ZF/ArithSimp.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
*)
--- a/src/ZF/Bool.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Bool.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/bool.thy
+(* Title: ZF/Bool.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/ZF/Coind/Language.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Coind/Language.thy Fri Feb 18 17:05:19 2011 +0100
@@ -5,14 +5,14 @@
theory Language imports Main begin
-consts
- Const :: i (* Abstract type of constants *)
- c_app :: "[i,i] => i" (* Abstract constructor for fun application*)
-
text{*these really can't be definitions without losing the abstraction*}
-axioms
- constNEE: "c \<in> Const ==> c \<noteq> 0"
+
+axiomatization
+ Const :: i and (* Abstract type of constants *)
+ c_app :: "[i,i] => i" (* Abstract constructor for fun application*)
+where
+ constNEE: "c \<in> Const ==> c \<noteq> 0" and
c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const"
--- a/src/ZF/Coind/Static.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Coind/Static.thy Fri Feb 18 17:05:19 2011 +0100
@@ -9,11 +9,8 @@
parameter of the proof. A concrete version could be defined inductively.
***)
-consts
- isof :: "[i,i] => o"
-
-axioms
- isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
+axiomatization isof :: "[i,i] => o"
+ where isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
(*Its extension to environments*)
--- a/src/ZF/Datatype_ZF.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Datatype_ZF.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/Datatype.thy
+(* Title: ZF/Datatype_ZF.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
*)
--- a/src/ZF/Int_ZF.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Int_ZF.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/Int.thy
+(* Title: ZF/Int_ZF.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
--- a/src/ZF/OrdQuant.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/OrdQuant.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/AC/OrdQuant.thy
+(* Title: ZF/OrdQuant.thy
Authors: Krzysztof Grabczewski and L C Paulson
*)
--- a/src/ZF/Sum.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Sum.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/sum.thy
+(* Title: ZF/Sum.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
--- a/src/ZF/UNITY/AllocBase.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/UNITY/AllocBase.thy Fri Feb 18 17:05:19 2011 +0100
@@ -7,17 +7,16 @@
theory AllocBase imports Follows MultisetSum Guar begin
-consts
- NbT :: i (* Number of tokens in system *)
- Nclients :: i (* Number of clients *)
-
abbreviation (input)
tokbag :: i (* tokbags could be multisets...or any ordered type?*)
where
"tokbag == nat"
-axioms
- NbT_pos: "NbT \<in> nat-{0}"
+axiomatization
+ NbT :: i and (* Number of tokens in system *)
+ Nclients :: i (* Number of clients *)
+where
+ NbT_pos: "NbT \<in> nat-{0}" and
Nclients_pos: "Nclients \<in> nat-{0}"
text{*This function merely sums the elements of a list*}
@@ -27,9 +26,7 @@
"tokens(Nil) = 0"
"tokens (Cons(x,xs)) = x #+ tokens(xs)"
-consts
- bag_of :: "i => i"
-
+consts bag_of :: "i => i"
primrec
"bag_of(Nil) = 0"
"bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
@@ -38,7 +35,7 @@
text{*Definitions needed in Client.thy. We define a recursive predicate
using 0 and 1 to code the truth values.*}
consts all_distinct0 :: "i=>i"
- primrec
+primrec
"all_distinct0(Nil) = 1"
"all_distinct0(Cons(a, l)) =
(if a \<in> set_of_list(l) then 0 else all_distinct0(l))"
--- a/src/ZF/UNITY/AllocImpl.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy Fri Feb 18 17:05:19 2011 +0100
@@ -16,9 +16,9 @@
available_tok :: i (*number of free tokens (T in paper)*) where
"available_tok == Var([succ(succ(2))])"
-axioms
+axiomatization where
alloc_type_assumes [simp]:
- "type_of(NbR) = nat & type_of(available_tok)=nat"
+ "type_of(NbR) = nat & type_of(available_tok)=nat" and
alloc_default_val_assumes [simp]:
"default_val(NbR) = 0 & default_val(available_tok)=0"
--- a/src/ZF/UNITY/ClientImpl.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy Fri Feb 18 17:05:19 2011 +0100
@@ -12,13 +12,13 @@
abbreviation "rel == Var([1])" (* input history: tokens released *)
abbreviation "tok == Var([2])" (* the number of available tokens *)
-axioms
+axiomatization where
type_assumes:
"type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) &
- type_of(rel) = list(tokbag) & type_of(tok) = nat"
+ type_of(rel) = list(tokbag) & type_of(tok) = nat" and
default_val_assumes:
- "default_val(ask) = Nil & default_val(giv) = Nil &
- default_val(rel) = Nil & default_val(tok) = 0"
+ "default_val(ask) = Nil & default_val(giv) = Nil &
+ default_val(rel) = Nil & default_val(tok) = 0"
(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
--- a/src/ZF/UNITY/Mutex.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/UNITY/Mutex.thy Fri Feb 18 17:05:19 2011 +0100
@@ -27,11 +27,11 @@
abbreviation "u == Var([0,1])"
abbreviation "v == Var([1,0])"
-axioms --{** Type declarations **}
- p_type: "type_of(p)=bool & default_val(p)=0"
- m_type: "type_of(m)=int & default_val(m)=#0"
- n_type: "type_of(n)=int & default_val(n)=#0"
- u_type: "type_of(u)=bool & default_val(u)=0"
+axiomatization where --{** Type declarations **}
+ p_type: "type_of(p)=bool & default_val(p)=0" and
+ m_type: "type_of(m)=int & default_val(m)=#0" and
+ n_type: "type_of(n)=int & default_val(n)=#0" and
+ u_type: "type_of(u)=bool & default_val(u)=0" and
v_type: "type_of(v)=bool & default_val(v)=0"
definition
--- a/src/ZF/ZF.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ZF.thy Fri Feb 18 17:05:19 2011 +0100
@@ -207,21 +207,21 @@
subset_def: "A <= B == \<forall>x\<in>A. x\<in>B"
-axioms
+axiomatization where
(* ZF axioms -- see Suppes p.238
Axioms for Union, Pow and Replace state existence only,
uniqueness is derivable using extensionality. *)
- extension: "A = B <-> A <= B & B <= A"
- Union_iff: "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)"
- Pow_iff: "A \<in> Pow(B) <-> A <= B"
+ extension: "A = B <-> A <= B & B <= A" and
+ Union_iff: "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)" and
+ Pow_iff: "A \<in> Pow(B) <-> A <= B" and
(*We may name this set, though it is not uniquely defined.*)
- infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)"
+ infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and
(*This formulation facilitates case analysis on A.*)
- foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)"
+ foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)" and
(*Schema axiom since predicate P is a higher-order variable*)
replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) --> y=z) ==>
--- a/src/ZF/ex/Commutation.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ex/Commutation.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Lambda/Commutation.thy
+(* Title: ZF/ex/Commutation.thy
Author: Tobias Nipkow & Sidi Ould Ehmety
Copyright 1995 TU Muenchen
--- a/src/ZF/ex/LList.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ex/LList.thy Fri Feb 18 17:05:19 2011 +0100
@@ -43,11 +43,9 @@
lconst :: "i => i" where
"lconst(a) == lfp(univ(a), %l. LCons(a,l))"
-consts
- flip :: "i => i"
-axioms
- flip_LNil: "flip(LNil) = LNil"
-
+axiomatization flip :: "i => i"
+where
+ flip_LNil: "flip(LNil) = LNil" and
flip_LCons: "[| x \<in> bool; l \<in> llist(bool) |]
==> flip(LCons(x,l)) = LCons(not(x), flip(l))"
--- a/src/ZF/ex/NatSum.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ex/NatSum.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/Natsum.thy
+(* Title: ZF/ex/NatSum.thy
Author: Tobias Nipkow & Lawrence C Paulson
A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
--- a/src/ZF/pair.thy Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/pair.thy Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/pair
+(* Title: ZF/pair.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge