--- a/Admin/isatest/isatest-stats Mon Sep 21 15:02:23 2009 +0200
+++ b/Admin/isatest/isatest-stats Mon Sep 21 16:16:16 2009 +0200
@@ -24,9 +24,9 @@
HOL-MetisExamples \
HOL-MicroJava \
HOL-NSA \
- HOL-NewNumberTheory \
HOL-Nominal-Examples \
- HOL-NumberTheory \
+ HOL-Number_Theory \
+ HOL-Old_Number_Theory \
HOL-SET-Protocol \
HOL-UNITY \
HOL-Word \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/All_Symmetric.thy Mon Sep 21 16:16:16 2009 +0200
@@ -0,0 +1,12 @@
+theory All_Symmetric
+imports Message
+begin
+
+text {* All keys are symmetric *}
+
+defs all_symmetric_def: "all_symmetric \<equiv> True"
+
+lemma isSym_keys: "K \<in> symKeys"
+ by (simp add: symKeys_def all_symmetric_def invKey_symmetric)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Auth_Public.thy Mon Sep 21 16:16:16 2009 +0200
@@ -0,0 +1,15 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Conventional protocols: rely on conventional Message, Event and Public -- Public-key protocols *}
+
+theory Auth_Public
+imports
+ "NS_Public_Bad"
+ "NS_Public"
+ "TLS"
+ "CertifiedEmail"
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Auth_Shared.thy Mon Sep 21 16:16:16 2009 +0200
@@ -0,0 +1,27 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}
+
+theory Auth_Shared
+imports
+ "NS_Shared"
+ "Kerberos_BAN"
+ "Kerberos_BAN_Gets"
+ "KerberosIV"
+ "KerberosIV_Gets"
+ "KerberosV"
+ "OtwayRees"
+ "OtwayRees_AN"
+ "OtwayRees_Bad"
+ "OtwayReesBella"
+ "WooLam"
+ "Recur"
+ "Yahalom"
+ "Yahalom2"
+ "Yahalom_Bad"
+ "ZhouGollmann"
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Guard/Auth_Guard_Public.thy Mon Sep 21 16:16:16 2009 +0200
@@ -0,0 +1,15 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Blanqui's "guard" concept: protocol-independent secrecy *}
+
+theory Auth_Guard_Public
+imports
+ "P1"
+ "P2"
+ "Guard_NS_Public"
+ "Proto"
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Guard/Auth_Guard_Shared.thy Mon Sep 21 16:16:16 2009 +0200
@@ -0,0 +1,13 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Blanqui's "guard" concept: protocol-independent secrecy *}
+
+theory Auth_Guard_Shared
+imports
+ "Guard_OtwayRees"
+ "Guard_Yahalom"
+begin
+
+end
--- a/src/HOL/Auth/Public.thy Mon Sep 21 15:02:23 2009 +0200
+++ b/src/HOL/Auth/Public.thy Mon Sep 21 16:16:16 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/Public
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -8,7 +7,9 @@
Private and public keys; initial states of agents
*)
-theory Public imports Event begin
+theory Public
+imports Event
+begin
lemma invKey_K: "K \<in> symKeys ==> invKey K = K"
by (simp add: symKeys_def)
--- a/src/HOL/Auth/ROOT.ML Mon Sep 21 15:02:23 2009 +0200
+++ b/src/HOL/Auth/ROOT.ML Mon Sep 21 16:16:16 2009 +0200
@@ -1,51 +1,2 @@
-(* Title: HOL/Auth/ROOT.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-Root file for protocol proofs.
-*)
-
-use_thys [
-
-(* Conventional protocols: rely on
- conventional Message, Event and Public *)
-
-(*Shared-key protocols*)
- "NS_Shared",
- "Kerberos_BAN",
- "Kerberos_BAN_Gets",
- "KerberosIV",
- "KerberosIV_Gets",
- "KerberosV",
- "OtwayRees",
- "OtwayRees_AN",
- "OtwayRees_Bad",
- "OtwayReesBella",
- "WooLam",
- "Recur",
- "Yahalom",
- "Yahalom2",
- "Yahalom_Bad",
- "ZhouGollmann",
-
-(*Public-key protocols*)
- "NS_Public_Bad",
- "NS_Public",
- "TLS",
- "CertifiedEmail",
-
-(*Smartcard protocols: rely on conventional Message and on new
- EventSC and Smartcard *)
-
- "Smartcard/ShoupRubin",
- "Smartcard/ShoupRubinBella",
-
-(*Blanqui's "guard" concept: protocol-independent secrecy*)
- "Guard/P1",
- "Guard/P2",
- "Guard/Guard_NS_Public",
- "Guard/Guard_OtwayRees",
- "Guard/Guard_Yahalom",
- "Guard/Proto"
-];
+use_thys ["Auth_Shared", "Auth_Public", "Smartcard/Auth_Smartcard", "Guard/Auth_Guard_Shared", "Guard/Auth_Guard_Public"];
--- a/src/HOL/Auth/Shared.thy Mon Sep 21 15:02:23 2009 +0200
+++ b/src/HOL/Auth/Shared.thy Mon Sep 21 16:16:16 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/Shared
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -8,7 +7,9 @@
Shared, long-term keys; initial states of agents
*)
-theory Shared imports Event begin
+theory Shared
+imports Event All_Symmetric
+begin
consts
shrK :: "agent => key" (*symmetric keys*);
@@ -20,13 +21,6 @@
apply (simp add: inj_on_def split: agent.split)
done
-text{*All keys are symmetric*}
-
-defs all_symmetric_def: "all_symmetric == True"
-
-lemma isSym_keys: "K \<in> symKeys"
-by (simp add: symKeys_def all_symmetric_def invKey_symmetric)
-
text{*Server knows all long-term keys; other agents know only their own*}
primrec
initState_Server: "initState Server = Key ` range shrK"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Smartcard/Auth_Smartcard.thy Mon Sep 21 16:16:16 2009 +0200
@@ -0,0 +1,13 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard *}
+
+theory Auth_Smartcard
+imports
+ "ShoupRubin"
+ "ShoupRubinBella"
+begin
+
+end
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Mon Sep 21 15:02:23 2009 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Mon Sep 21 16:16:16 2009 +0200
@@ -1,10 +1,11 @@
-(* ID: $Id$
- Author: Giampaolo Bella, Catania University
+(* Author: Giampaolo Bella, Catania University
*)
header{*Theory of smartcards*}
-theory Smartcard imports EventSC begin
+theory Smartcard
+imports EventSC All_Symmetric
+begin
text{*
As smartcards handle long-term (symmetric) keys, this theoy extends and
@@ -42,14 +43,6 @@
shrK_disj_pin [iff]: "shrK P \<noteq> pin Q"
crdK_disj_pin [iff]: "crdK C \<noteq> pin P"
-
-text{*All keys are symmetric*}
-defs all_symmetric_def: "all_symmetric == True"
-
-lemma isSym_keys: "K \<in> symKeys"
-by (simp add: symKeys_def all_symmetric_def invKey_symmetric)
-
-
constdefs
legalUse :: "card => bool" ("legalUse (_)")
"legalUse C == C \<notin> stolen"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Bali/Bali.thy Mon Sep 21 16:16:16 2009 +0200
@@ -0,0 +1,11 @@
+(* Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+header {* The Hoare logic for Bali. *}
+
+theory Bali
+imports AxExample AxSound AxCompl Trans
+begin
+
+end
--- a/src/HOL/Bali/ROOT.ML Mon Sep 21 15:02:23 2009 +0200
+++ b/src/HOL/Bali/ROOT.ML Mon Sep 21 16:16:16 2009 +0200
@@ -1,9 +1,2 @@
-(* Title: HOL/Bali/ROOT.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-The Hoare logic for Bali.
-*)
-
-use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];
+use_thy "Bali"
--- a/src/HOL/IsaMakefile Mon Sep 21 15:02:23 2009 +0200
+++ b/src/HOL/IsaMakefile Mon Sep 21 16:16:16 2009 +0200
@@ -619,6 +619,10 @@
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
$(LOG)/HOL-Auth.gz: $(OUT)/HOL \
+ Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \
+ Auth/Guard/Auth_Guard_Shared.thy \
+ Auth/Guard/Auth_Guard_Public.thy \
+ Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \
Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \
Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \
Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \
@@ -832,7 +836,7 @@
HOL-Bali: HOL $(LOG)/HOL-Bali.gz
-$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy \
+$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy Bali/AxExample.thy \
Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy \
Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy \
Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy \
@@ -1022,6 +1026,7 @@
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
+ Nominal/Examples/Nominal_Examples.thy \
Nominal/Examples/CK_Machine.thy \
Nominal/Examples/CR.thy \
Nominal/Examples/CR_Takahashi.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy Mon Sep 21 16:16:16 2009 +0200
@@ -0,0 +1,25 @@
+(* Author: Christian Urban TU Muenchen *)
+
+header {* Various examples involving nominal datatypes. *}
+
+theory Nominal_Examples
+imports
+ CR
+ CR_Takahashi
+ Class
+ Compile
+ Fsub
+ Height
+ Lambda_mu
+ SN
+ Weakening
+ Crary
+ SOS
+ LocalWeakening
+ Support
+ Contexts
+ Standardization
+ W
+begin
+
+end
--- a/src/HOL/Nominal/Examples/ROOT.ML Mon Sep 21 15:02:23 2009 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML Mon Sep 21 16:16:16 2009 +0200
@@ -1,27 +1,4 @@
-(* Title: HOL/Nominal/Examples/ROOT.ML
- ID: $Id$
- Author: Christian Urban, TU Muenchen
-
-Various examples involving nominal datatypes.
-*)
-use_thys [
- "CR",
- "CR_Takahashi",
- "Class",
- "Compile",
- "Fsub",
- "Height",
- "Lambda_mu",
- "SN",
- "Weakening",
- "Crary",
- "SOS",
- "LocalWeakening",
- "Support",
- "Contexts",
- "Standardization",
- "W"
-];
+use_thy "Nominal_Examples";
-setmp_noncritical quick_and_dirty true use_thy "VC_Condition";
+setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*)
--- a/src/HOL/SMT/Tools/smt_solver.ML Mon Sep 21 15:02:23 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML Mon Sep 21 16:16:16 2009 +0200
@@ -55,8 +55,6 @@
exception SMT_COUNTEREXAMPLE of bool * term list
-val theory_of = Context.cases I ProofContext.theory_of
-
datatype interface = Interface of {
normalize: SMT_Normalize.config list,
@@ -177,12 +175,12 @@
val solver_name_of = snd o SelectedSolver.get
fun select_solver name gen =
- if is_none (lookup_solver (theory_of gen) name)
+ if is_none (lookup_solver (Context.theory_of gen) name)
then error ("SMT solver not registered: " ^ quote name)
else SelectedSolver.map (K (serial (), name)) gen
fun raw_solver_of gen =
- (case lookup_solver (theory_of gen) (solver_name_of gen) of
+ (case lookup_solver (Context.theory_of gen) (solver_name_of gen) of
NONE => error "No SMT solver selected"
| SOME (s, _) => s)
@@ -228,11 +226,11 @@
fun print_setup gen =
let
val t = string_of_int (Config.get_generic gen timeout)
- val names = sort string_ord (all_solver_names_of (theory_of gen))
+ val names = sort string_ord (all_solver_names_of (Context.theory_of gen))
val ns = if null names then [no_solver] else names
val take_info = (fn (_, []) => NONE | info => SOME info)
val infos =
- theory_of gen
+ Context.theory_of gen
|> Symtab.dest o Solvers.get
|> map_filter (fn (n, (_, info)) => take_info (n, info gen))
|> sort (prod_ord string_ord (K EQUAL))
--- a/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 15:02:23 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 16:16:16 2009 +0200
@@ -83,19 +83,24 @@
(*** Progress under weak fairness ***)
-declare atMost_Int_atLeast [simp]
-
lemma leadsTo_common_lemma:
- "[| \<forall>m. F \<in> {m} Co (maxfg m);
- \<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m);
- n \<in> common |]
- ==> F \<in> (atMost n) LeadsTo common"
-apply (rule LeadsTo_weaken_R)
-apply (rule_tac f = id and l = n in GreaterThan_bounded_induct)
-apply (simp_all (no_asm_simp) del: Int_insert_right_if1)
-apply (rule_tac [2] subset_refl)
-apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
-done
+ assumes "\<forall>m. F \<in> {m} Co (maxfg m)"
+ and "\<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m)"
+ and "n \<in> common"
+ shows "F \<in> (atMost n) LeadsTo common"
+proof (rule LeadsTo_weaken_R)
+ show "F \<in> {..n} LeadsTo {..n} \<inter> id -` {n..} \<union> common"
+ proof (induct rule: GreaterThan_bounded_induct [of n _ _ id])
+ case 1
+ from assms have "\<forall>m\<in>{..<n}. F \<in> {..n} \<inter> {m} LeadsTo {..n} \<inter> {m<..} \<union> common"
+ by (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
+ then show ?case by simp
+ qed
+next
+ from `n \<in> common`
+ show "{..n} \<inter> id -` {n..} \<union> common \<subseteq> common"
+ by (simp add: atMost_Int_atLeast)
+qed
(*The "\<forall>m \<in> -common" form echoes CMT6.*)
lemma leadsTo_common: