--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Tue Jul 31 19:55:04 2012 +0200
@@ -0,0 +1,51 @@
+(* Title: HOL/Codegenerator_Test/RBT_Set_Test.thy
+ Author: Ondrej Kuncar
+*)
+
+header {* Test of the code generator using an implementation of sets by RBT trees *}
+
+theory RBT_Set_Test
+imports Library "~~/src/HOL/Library/RBT_Set"
+begin
+
+(*
+ The following code equations have to be deleted because they use
+ lists to implement sets in the code generetor.
+*)
+
+lemma [code, code del]:
+ "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
+
+lemma [code, code del]:
+ "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
+
+lemma [code, code del]:
+ "pred_of_set = pred_of_set" ..
+
+
+lemma [code, code del]:
+ "Cardinality.card' = Cardinality.card'" ..
+
+lemma [code, code del]:
+ "Cardinality.finite' = Cardinality.finite'" ..
+
+lemma [code, code del]:
+ "Cardinality.subset' = Cardinality.subset'" ..
+
+lemma [code, code del]:
+ "Cardinality.eq_set = Cardinality.eq_set" ..
+
+
+lemma [code, code del]:
+ "acc = acc" ..
+
+(*
+ If the code generation ends with an exception with the following message:
+ '"List.set" is not a constructor, on left hand side of equation: ...',
+ the code equation in question has to be either deleted (like many others in this file)
+ or implemented for RBT trees.
+*)
+
+export_code _ checking SML OCaml? Haskell? Scala?
+
+end
--- a/src/HOL/Codegenerator_Test/ROOT.ML Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/Codegenerator_Test/ROOT.ML Tue Jul 31 19:55:04 2012 +0200
@@ -1,1 +1,1 @@
-use_thys ["Generate", "Generate_Pretty"];
+use_thys ["Generate", "Generate_Pretty", "RBT_Set_Test"];
--- a/src/HOL/Finite_Set.thy Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/Finite_Set.thy Tue Jul 31 19:55:04 2012 +0200
@@ -697,6 +697,18 @@
then show ?thesis by simp
qed
+text{* Other properties of @{const fold}: *}
+
+lemma fold_image:
+ assumes "finite A" and "inj_on g A"
+ shows "fold f x (g ` A) = fold (f \<circ> g) x A"
+using assms
+proof induction
+ case (insert a F)
+ interpret comp_fun_commute "\<lambda>x. f (g x)" by default (simp add: comp_fun_commute)
+ from insert show ?case by auto
+qed (simp)
+
end
text{* A simplified version for idempotent functions: *}
@@ -777,6 +789,90 @@
then show ?thesis ..
qed
+definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ where "filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
+
+lemma comp_fun_commute_filter_fold: "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
+proof -
+ interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
+ show ?thesis by default (auto simp: fun_eq_iff)
+qed
+
+lemma inter_filter:
+ assumes "finite B"
+ shows "A \<inter> B = filter (\<lambda>x. x \<in> A) B"
+using assms
+by (induct B) (auto simp: filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
+
+lemma project_filter:
+ assumes "finite A"
+ shows "Set.project P A = filter P A"
+using assms
+by (induct A)
+ (auto simp add: filter_def project_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
+
+lemma image_fold_insert:
+ assumes "finite A"
+ shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A"
+using assms
+proof -
+ interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by default auto
+ show ?thesis using assms by (induct A) auto
+qed
+
+lemma Ball_fold:
+ assumes "finite A"
+ shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A"
+using assms
+proof -
+ interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by default auto
+ show ?thesis using assms by (induct A) auto
+qed
+
+lemma Bex_fold:
+ assumes "finite A"
+ shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A"
+using assms
+proof -
+ interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by default auto
+ show ?thesis using assms by (induct A) auto
+qed
+
+lemma comp_fun_commute_Pow_fold:
+ "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)"
+ by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast
+
+lemma Pow_fold:
+ assumes "finite A"
+ shows "Pow A = fold (\<lambda>x A. A \<union> Set.insert x ` A) {{}} A"
+using assms
+proof -
+ interpret comp_fun_commute "\<lambda>x A. A \<union> Set.insert x ` A" by (rule comp_fun_commute_Pow_fold)
+ show ?thesis using assms by (induct A) (auto simp: Pow_insert)
+qed
+
+lemma fold_union_pair:
+ assumes "finite B"
+ shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B"
+proof -
+ interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by default auto
+ show ?thesis using assms by (induct B arbitrary: A) simp_all
+qed
+
+lemma comp_fun_commute_product_fold:
+ assumes "finite B"
+ shows "comp_fun_commute (\<lambda>x A. fold (\<lambda>y. Set.insert (x, y)) A B)"
+by default (auto simp: fold_union_pair[symmetric] assms)
+
+lemma product_fold:
+ assumes "finite A"
+ assumes "finite B"
+ shows "A \<times> B = fold (\<lambda>x A. fold (\<lambda>y. Set.insert (x, y)) A B) {} A"
+using assms unfolding Sigma_def
+by (induct A)
+ (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair)
+
+
context complete_lattice
begin
@@ -2303,6 +2399,6 @@
by simp
qed
-hide_const (open) Finite_Set.fold
+hide_const (open) Finite_Set.fold Finite_Set.filter
end
--- a/src/HOL/IsaMakefile Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 31 19:55:04 2012 +0200
@@ -1513,10 +1513,6 @@
Quickcheck_Examples/ROOT.ML \
Quickcheck_Examples/Completeness.thy \
Quickcheck_Examples/Hotel_Example.thy \
- Quickcheck_Examples/Needham_Schroeder_Base.thy \
- Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy \
- Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy \
- Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker_Example.thy \
Quickcheck_Examples/Quickcheck_Examples.thy \
Quickcheck_Examples/Quickcheck_Interfaces.thy \
Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \
@@ -1532,7 +1528,7 @@
Quotient_Examples/FSet.thy \
Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
Quotient_Examples/Lift_FSet.thy \
- Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
+ Quotient_Examples/Lift_Set.thy \
Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
@@ -1823,6 +1819,10 @@
$(LOG)/HOL-Quickcheck_Benchmark.gz: $(OUT)/HOL \
Quickcheck_Benchmark/ROOT.ML \
+ Quickcheck_Benchmark/Needham_Schroeder_Base.thy \
+ Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy \
+ Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy \
+ Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy \
Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Benchmark
--- a/src/HOL/Library/Library.thy Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/Library/Library.thy Tue Jul 31 19:55:04 2012 +0200
@@ -55,6 +55,7 @@
Ramsey
Reflection
RBT_Mapping
+ (* RBT_Set *) (* not included because it breaks Codegenerator_Test/Generate*.thy *)
Saturated
Set_Algebras
State_Monad
--- a/src/HOL/Library/RBT.thy Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/Library/RBT.thy Tue Jul 31 19:55:04 2012 +0200
@@ -1,9 +1,10 @@
-(* Author: Florian Haftmann, TU Muenchen *)
+(* Title: HOL/Library/RBT.thy
+ Author: Lukas Bulwahn and Ondrej Kuncar
+*)
-header {* Abstract type of Red-Black Trees *}
+header {* Abstract type of RBT trees *}
-(*<*)
-theory RBT
+theory RBT
imports Main RBT_Impl
begin
@@ -11,8 +12,9 @@
typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
morphisms impl_of RBT
-proof
- show "RBT_Impl.Empty \<in> {t. is_rbt t}" by simp
+proof -
+ have "RBT_Impl.Empty \<in> ?rbt" by simp
+ then show ?thesis ..
qed
lemma rbt_eq_iff:
@@ -31,63 +33,45 @@
"RBT (impl_of t) = t"
by (simp add: impl_of_inverse)
-
subsection {* Primitive operations *}
-definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" where
- [code]: "lookup t = rbt_lookup (impl_of t)"
-
-definition empty :: "('a\<Colon>linorder, 'b) rbt" where
- "empty = RBT RBT_Impl.Empty"
+setup_lifting type_definition_rbt
-lemma impl_of_empty [code abstract]:
- "impl_of empty = RBT_Impl.Empty"
- by (simp add: empty_def RBT_inverse)
+lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup"
+by simp
-definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
- "insert k v t = RBT (rbt_insert k v (impl_of t))"
+lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty
+by (simp add: empty_def)
-lemma impl_of_insert [code abstract]:
- "impl_of (insert k v t) = rbt_insert k v (impl_of t)"
- by (simp add: insert_def RBT_inverse)
-
-definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
- "delete k t = RBT (rbt_delete k (impl_of t))"
+lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_insert"
+by simp
-lemma impl_of_delete [code abstract]:
- "impl_of (delete k t) = rbt_delete k (impl_of t)"
- by (simp add: delete_def RBT_inverse)
+lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete"
+by simp
-definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" where
- [code]: "entries t = RBT_Impl.entries (impl_of t)"
+lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
+by simp
-definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" where
- [code]: "keys t = RBT_Impl.keys (impl_of t)"
-
-definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" where
- "bulkload xs = RBT (rbt_bulkload xs)"
+lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys
+by simp
-lemma impl_of_bulkload [code abstract]:
- "impl_of (bulkload xs) = rbt_bulkload xs"
- by (simp add: bulkload_def RBT_inverse)
+lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload"
+by simp
-definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
- "map_entry k f t = RBT (rbt_map_entry k f (impl_of t))"
+lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
+by simp
-lemma impl_of_map_entry [code abstract]:
- "impl_of (map_entry k f t) = rbt_map_entry k f (impl_of t)"
- by (simp add: map_entry_def RBT_inverse)
+lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map
+by simp
-definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
- "map f t = RBT (RBT_Impl.map f (impl_of t))"
+lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is RBT_Impl.fold
+by simp
-lemma impl_of_map [code abstract]:
- "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
- by (simp add: map_def RBT_inverse)
+lift_definition union :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union"
+by (simp add: rbt_union_is_rbt)
-definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
- [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
-
+lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
+ is RBT_Impl.foldi by simp
subsection {* Derived operations *}
@@ -103,15 +87,15 @@
lemma lookup_impl_of:
"rbt_lookup (impl_of t) = lookup t"
- by (simp add: lookup_def)
+ by transfer (rule refl)
lemma entries_impl_of:
"RBT_Impl.entries (impl_of t) = entries t"
- by (simp add: entries_def)
+ by transfer (rule refl)
lemma keys_impl_of:
"RBT_Impl.keys (impl_of t) = keys t"
- by (simp add: keys_def)
+ by transfer (rule refl)
lemma lookup_empty [simp]:
"lookup empty = Map.empty"
@@ -119,39 +103,43 @@
lemma lookup_insert [simp]:
"lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
- by (simp add: insert_def lookup_RBT rbt_lookup_rbt_insert lookup_impl_of)
+ by transfer (rule rbt_lookup_rbt_insert)
lemma lookup_delete [simp]:
"lookup (delete k t) = (lookup t)(k := None)"
- by (simp add: delete_def lookup_RBT rbt_lookup_rbt_delete lookup_impl_of restrict_complement_singleton_eq)
+ by transfer (simp add: rbt_lookup_rbt_delete restrict_complement_singleton_eq)
lemma map_of_entries [simp]:
"map_of (entries t) = lookup t"
- by (simp add: entries_def map_of_entries lookup_impl_of)
+ by transfer (simp add: map_of_entries)
lemma entries_lookup:
"entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
- by (simp add: entries_def lookup_def entries_rbt_lookup)
+ by transfer (simp add: entries_rbt_lookup)
lemma lookup_bulkload [simp]:
"lookup (bulkload xs) = map_of xs"
- by (simp add: bulkload_def lookup_RBT rbt_lookup_rbt_bulkload)
+ by transfer (rule rbt_lookup_rbt_bulkload)
lemma lookup_map_entry [simp]:
"lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
- by (simp add: map_entry_def lookup_RBT rbt_lookup_rbt_map_entry lookup_impl_of)
+ by transfer (rule rbt_lookup_rbt_map_entry)
lemma lookup_map [simp]:
"lookup (map f t) k = Option.map (f k) (lookup t k)"
- by (simp add: map_def lookup_RBT rbt_lookup_map lookup_impl_of)
+ by transfer (rule rbt_lookup_map)
lemma fold_fold:
"fold f t = List.fold (prod_case f) (entries t)"
- by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
+ by transfer (rule RBT_Impl.fold_def)
+
+lemma impl_of_empty:
+ "impl_of empty = RBT_Impl.Empty"
+ by transfer (rule refl)
lemma is_empty_empty [simp]:
"is_empty t \<longleftrightarrow> t = empty"
- by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
+ unfolding is_empty_def by transfer (simp split: rbt.split)
lemma RBT_lookup_empty [simp]: (*FIXME*)
"rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
@@ -159,15 +147,41 @@
lemma lookup_empty_empty [simp]:
"lookup t = Map.empty \<longleftrightarrow> t = empty"
- by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse)
+ by transfer (rule RBT_lookup_empty)
lemma sorted_keys [iff]:
"sorted (keys t)"
- by (simp add: keys_def RBT_Impl.keys_def rbt_sorted_entries)
+ by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries)
lemma distinct_keys [iff]:
"distinct (keys t)"
- by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
+ by transfer (simp add: RBT_Impl.keys_def distinct_entries)
+
+lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
+ by transfer simp
+
+lemma lookup_union: "lookup (union s t) = lookup s ++ lookup t"
+ by transfer (simp add: rbt_lookup_rbt_union)
+
+lemma lookup_in_tree: "(lookup t k = Some v) = ((k, v) \<in> set (entries t))"
+ by transfer (simp add: rbt_lookup_in_tree)
+
+lemma keys_entries: "(k \<in> set (keys t)) = (\<exists>v. (k, v) \<in> set (entries t))"
+ by transfer (simp add: keys_entries)
+
+lemma fold_def_alt:
+ "fold f t = List.fold (prod_case f) (entries t)"
+ by transfer (auto simp: RBT_Impl.fold_def)
+
+lemma distinct_entries: "distinct (List.map fst (entries t))"
+ by transfer (simp add: distinct_entries)
+
+lemma non_empty_keys: "t \<noteq> empty \<Longrightarrow> keys t \<noteq> []"
+ by transfer (simp add: non_empty_rbt_keys)
+
+lemma keys_def_alt:
+ "keys t = List.map fst (entries t)"
+ by transfer (simp add: RBT_Impl.keys_def)
subsection {* Quickcheck generators *}
--- a/src/HOL/Library/RBT_Impl.thy Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Tue Jul 31 19:55:04 2012 +0200
@@ -62,6 +62,9 @@
"k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))"
by (auto intro: entry_in_tree_keys) (auto simp add: keys_def)
+lemma non_empty_rbt_keys:
+ "t \<noteq> rbt.Empty \<Longrightarrow> keys t \<noteq> []"
+ by (cases t) simp_all
subsubsection {* Search tree properties *}
@@ -121,6 +124,11 @@
(force simp: sorted_append sorted_Cons rbt_ord_props
dest!: entry_in_tree_keys)+
+lemma distinct_keys:
+ "rbt_sorted t \<Longrightarrow> distinct (keys t)"
+ by (simp add: distinct_entries keys_def)
+
+
subsubsection {* Tree lookup *}
primrec (in ord) rbt_lookup :: "('a, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
@@ -1059,7 +1067,7 @@
qed
qed
- from Branch have is_rbt: "is_rbt (RBT_Impl.rbt_union (RBT_Impl.rbt_insert k v s) l)"
+ from Branch have is_rbt: "is_rbt (rbt_union (rbt_insert k v s) l)"
by (auto intro: rbt_union_is_rbt rbt_insert_is_rbt)
with Branch have IHs:
"rbt_lookup (rbt_union (rbt_union (rbt_insert k v s) l) r) = rbt_lookup (rbt_union (rbt_insert k v s) l) ++ rbt_lookup r"
@@ -1148,6 +1156,20 @@
"fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
by (simp_all add: fold_def fun_eq_iff)
+(* fold with continuation predicate *)
+
+fun foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
+ where
+ "foldi c f Empty s = s" |
+ "foldi c f (Branch col l k v r) s = (
+ if (c s) then
+ let s' = foldi c f l s in
+ if (c s') then
+ foldi c f r (f k v s')
+ else s'
+ else
+ s
+ )"
subsection {* Bulkloading a tree *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/RBT_Set.thy Tue Jul 31 19:55:04 2012 +0200
@@ -0,0 +1,824 @@
+(* Title: HOL/Library/RBT_Set.thy
+ Author: Ondrej Kuncar
+*)
+
+header {* Implementation of sets using RBT trees *}
+
+theory RBT_Set
+imports RBT Product_ord
+begin
+
+(*
+ Users should be aware that by including this file all code equations
+ outside of List.thy using 'a list as an implenentation of sets cannot be
+ used for code generation. If such equations are not needed, they can be
+ deleted from the code generator. Otherwise, a user has to provide their
+ own equations using RBT trees.
+*)
+
+section {* Definition of code datatype constructors *}
+
+definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
+ where "Set t = {x . lookup t x = Some ()}"
+
+definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
+ where [simp]: "Coset t = - Set t"
+
+
+section {* Deletion of already existing code equations *}
+
+lemma [code, code del]:
+ "Set.empty = Set.empty" ..
+
+lemma [code, code del]:
+ "Set.is_empty = Set.is_empty" ..
+
+lemma [code, code del]:
+ "uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" ..
+
+lemma [code, code del]:
+ "Set.member = Set.member" ..
+
+lemma [code, code del]:
+ "Set.insert = Set.insert" ..
+
+lemma [code, code del]:
+ "Set.remove = Set.remove" ..
+
+lemma [code, code del]:
+ "UNIV = UNIV" ..
+
+lemma [code, code del]:
+ "Set.project = Set.project" ..
+
+lemma [code, code del]:
+ "image = image" ..
+
+lemma [code, code del]:
+ "Set.subset_eq = Set.subset_eq" ..
+
+lemma [code, code del]:
+ "Ball = Ball" ..
+
+lemma [code, code del]:
+ "Bex = Bex" ..
+
+lemma [code, code del]:
+ "Set.union = Set.union" ..
+
+lemma [code, code del]:
+ "minus_set_inst.minus_set = minus_set_inst.minus_set" ..
+
+lemma [code, code del]:
+ "Set.inter = Set.inter" ..
+
+lemma [code, code del]:
+ "card = card" ..
+
+lemma [code, code del]:
+ "the_elem = the_elem" ..
+
+lemma [code, code del]:
+ "Pow = Pow" ..
+
+lemma [code, code del]:
+ "setsum = setsum" ..
+
+lemma [code, code del]:
+ "Product_Type.product = Product_Type.product" ..
+
+lemma [code, code del]:
+ "Id_on = Id_on" ..
+
+lemma [code, code del]:
+ "Image = Image" ..
+
+lemma [code, code del]:
+ "trancl = trancl" ..
+
+lemma [code, code del]:
+ "relcomp = relcomp" ..
+
+lemma [code, code del]:
+ "wf = wf" ..
+
+lemma [code, code del]:
+ "Min = Min" ..
+
+lemma [code, code del]:
+ "Inf_fin = Inf_fin" ..
+
+lemma [code, code del]:
+ "INFI = INFI" ..
+
+lemma [code, code del]:
+ "Max = Max" ..
+
+lemma [code, code del]:
+ "Sup_fin = Sup_fin" ..
+
+lemma [code, code del]:
+ "SUPR = SUPR" ..
+
+lemma [code, code del]:
+ "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
+
+lemma [code, code del]:
+ "(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" ..
+
+lemma [code, code del]:
+ "sorted_list_of_set = sorted_list_of_set" ..
+
+lemma [code, code del]:
+ "List.map_project = List.map_project" ..
+
+section {* Lemmas *}
+
+
+subsection {* Auxiliary lemmas *}
+
+lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
+by (auto simp: not_Some_eq[THEN iffD1])
+
+lemma finite_Set [simp, intro!]: "finite (Set x)"
+proof -
+ have "Set x = dom (lookup x)" by (auto simp: Set_def)
+ then show ?thesis by simp
+qed
+
+lemma set_keys: "Set t = set(keys t)"
+proof -
+ have "\<And>k. ((k, ()) \<in> set (entries t)) = (k \<in> set (keys t))"
+ by (simp add: keys_entries)
+ then show ?thesis by (auto simp: lookup_in_tree Set_def)
+qed
+
+subsection {* fold and filter *}
+
+lemma finite_fold_rbt_fold_eq:
+ assumes "comp_fun_commute f"
+ shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
+proof -
+ have *: "remdups (entries t) = entries t"
+ using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
+ show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
+qed
+
+definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b"
+ where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"
+
+lemma fold_keys_def_alt:
+ "fold_keys f t s = List.fold f (keys t) s"
+by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)
+
+lemma finite_fold_fold_keys:
+ assumes "comp_fun_commute f"
+ shows "Finite_Set.fold f A (Set t) = fold_keys f t A"
+using assms
+proof -
+ interpret comp_fun_commute f by fact
+ have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries)
+ moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto
+ ultimately show ?thesis
+ by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq
+ comp_comp_fun_commute)
+qed
+
+definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
+ "rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
+
+lemma finite_filter_rbt_filter:
+ "Finite_Set.filter P (Set t) = rbt_filter P t"
+by (simp add: fold_keys_def Finite_Set.filter_def rbt_filter_def
+ finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
+
+
+subsection {* foldi and Ball *}
+
+lemma Ball_False: "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t False = False"
+by (induction t) auto
+
+lemma rbt_foldi_fold_conj:
+ "RBT_Impl.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t val"
+proof (induction t arbitrary: val)
+ case (Branch c t1) then show ?case
+ by (cases "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t1 True") (simp_all add: Ball_False)
+qed simp
+
+lemma foldi_fold_conj: "foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
+unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj)
+
+
+subsection {* foldi and Bex *}
+
+lemma Bex_True: "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True"
+by (induction t) auto
+
+lemma rbt_foldi_fold_disj:
+ "RBT_Impl.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t val"
+proof (induction t arbitrary: val)
+ case (Branch c t1) then show ?case
+ by (cases "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t1 False") (simp_all add: Bex_True)
+qed simp
+
+lemma foldi_fold_disj: "foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
+unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj)
+
+
+subsection {* folding over non empty trees and selecting the minimal and maximal element *}
+
+(** concrete **)
+
+(* The concrete part is here because it's probably not general enough to be moved to RBT_Impl *)
+
+definition rbt_fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a"
+ where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))"
+
+(* minimum *)
+
+definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a"
+ where "rbt_min t = rbt_fold1_keys min t"
+
+lemma key_le_right: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys rt) \<Longrightarrow> k \<le> x)"
+by (auto simp: rbt_greater_prop less_imp_le)
+
+lemma left_le_key: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys lt) \<Longrightarrow> x \<le> k)"
+by (auto simp: rbt_less_prop less_imp_le)
+
+lemma fold_min_triv:
+ fixes k :: "_ :: linorder"
+ shows "(\<forall>x\<in>set xs. k \<le> x) \<Longrightarrow> List.fold min xs k = k"
+by (induct xs) (auto simp add: min_def)
+
+lemma rbt_min_simps:
+ "is_rbt (Branch c RBT_Impl.Empty k v rt) \<Longrightarrow> rbt_min (Branch c RBT_Impl.Empty k v rt) = k"
+by (auto intro: fold_min_triv dest: key_le_right is_rbt_rbt_sorted simp: rbt_fold1_keys_def rbt_min_def)
+
+fun rbt_min_opt where
+ "rbt_min_opt (Branch c RBT_Impl.Empty k v rt) = k" |
+ "rbt_min_opt (Branch c (Branch lc llc lk lv lrt) k v rt) = rbt_min_opt (Branch lc llc lk lv lrt)"
+
+lemma rbt_min_opt_Branch:
+ "t1 \<noteq> rbt.Empty \<Longrightarrow> rbt_min_opt (Branch c t1 k () t2) = rbt_min_opt t1"
+by (cases t1) auto
+
+lemma rbt_min_opt_induct [case_names empty left_empty left_non_empty]:
+ fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
+ assumes "P rbt.Empty"
+ assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
+ assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
+ shows "P t"
+using assms
+ apply (induction t)
+ apply simp
+ apply (case_tac "t1 = rbt.Empty")
+ apply simp_all
+done
+
+lemma rbt_min_opt_in_set:
+ fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
+ assumes "t \<noteq> rbt.Empty"
+ shows "rbt_min_opt t \<in> set (RBT_Impl.keys t)"
+using assms by (induction t rule: rbt_min_opt.induct) (auto)
+
+lemma rbt_min_opt_is_min:
+ fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
+ assumes "rbt_sorted t"
+ assumes "t \<noteq> rbt.Empty"
+ shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<ge> rbt_min_opt t"
+using assms
+proof (induction t rule: rbt_min_opt_induct)
+ case empty
+ then show ?case by simp
+next
+ case left_empty
+ then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
+next
+ case (left_non_empty c t1 k v t2 y)
+ then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
+ with left_non_empty show ?case
+ proof(elim disjE)
+ case goal1 then show ?case
+ by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
+ next
+ case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
+ next
+ case goal3 show ?case
+ proof -
+ from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
+ moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
+ ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
+ qed
+ qed
+qed
+
+lemma rbt_min_eq_rbt_min_opt:
+ assumes "t \<noteq> RBT_Impl.Empty"
+ assumes "is_rbt t"
+ shows "rbt_min t = rbt_min_opt t"
+proof -
+ interpret ab_semigroup_idem_mult "(min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_min
+ unfolding class.ab_semigroup_idem_mult_def by blast
+ show ?thesis
+ by (simp add: Min_eqI rbt_min_opt_is_min rbt_min_opt_in_set assms Min_def[symmetric]
+ non_empty_rbt_keys fold1_set_fold[symmetric] rbt_min_def rbt_fold1_keys_def)
+qed
+
+(* maximum *)
+
+definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a"
+ where "rbt_max t = rbt_fold1_keys max t"
+
+lemma fold_max_triv:
+ fixes k :: "_ :: linorder"
+ shows "(\<forall>x\<in>set xs. x \<le> k) \<Longrightarrow> List.fold max xs k = k"
+by (induct xs) (auto simp add: max_def)
+
+lemma fold_max_rev_eq:
+ fixes xs :: "('a :: linorder) list"
+ assumes "xs \<noteq> []"
+ shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))"
+proof -
+ interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
+ unfolding class.ab_semigroup_idem_mult_def by blast
+ show ?thesis
+ using assms by (auto simp add: fold1_set_fold[symmetric])
+qed
+
+lemma rbt_max_simps:
+ assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)"
+ shows "rbt_max (Branch c lt k v RBT_Impl.Empty) = k"
+proof -
+ have "List.fold max (tl (rev(RBT_Impl.keys lt @ [k]))) (hd (rev(RBT_Impl.keys lt @ [k]))) = k"
+ using assms by (auto intro!: fold_max_triv dest!: left_le_key is_rbt_rbt_sorted)
+ then show ?thesis by (auto simp add: rbt_max_def rbt_fold1_keys_def fold_max_rev_eq)
+qed
+
+fun rbt_max_opt where
+ "rbt_max_opt (Branch c lt k v RBT_Impl.Empty) = k" |
+ "rbt_max_opt (Branch c lt k v (Branch rc rlc rk rv rrt)) = rbt_max_opt (Branch rc rlc rk rv rrt)"
+
+lemma rbt_max_opt_Branch:
+ "t2 \<noteq> rbt.Empty \<Longrightarrow> rbt_max_opt (Branch c t1 k () t2) = rbt_max_opt t2"
+by (cases t2) auto
+
+lemma rbt_max_opt_induct [case_names empty right_empty right_non_empty]:
+ fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
+ assumes "P rbt.Empty"
+ assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
+ assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
+ shows "P t"
+using assms
+ apply (induction t)
+ apply simp
+ apply (case_tac "t2 = rbt.Empty")
+ apply simp_all
+done
+
+lemma rbt_max_opt_in_set:
+ fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
+ assumes "t \<noteq> rbt.Empty"
+ shows "rbt_max_opt t \<in> set (RBT_Impl.keys t)"
+using assms by (induction t rule: rbt_max_opt.induct) (auto)
+
+lemma rbt_max_opt_is_max:
+ fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
+ assumes "rbt_sorted t"
+ assumes "t \<noteq> rbt.Empty"
+ shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<le> rbt_max_opt t"
+using assms
+proof (induction t rule: rbt_max_opt_induct)
+ case empty
+ then show ?case by simp
+next
+ case right_empty
+ then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
+next
+ case (right_non_empty c t1 k v t2 y)
+ then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
+ with right_non_empty show ?case
+ proof(elim disjE)
+ case goal1 then show ?case
+ by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
+ next
+ case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
+ next
+ case goal3 show ?case
+ proof -
+ from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
+ moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
+ ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
+ qed
+ qed
+qed
+
+lemma rbt_max_eq_rbt_max_opt:
+ assumes "t \<noteq> RBT_Impl.Empty"
+ assumes "is_rbt t"
+ shows "rbt_max t = rbt_max_opt t"
+proof -
+ interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
+ unfolding class.ab_semigroup_idem_mult_def by blast
+ show ?thesis
+ by (simp add: Max_eqI rbt_max_opt_is_max rbt_max_opt_in_set assms Max_def[symmetric]
+ non_empty_rbt_keys fold1_set_fold[symmetric] rbt_max_def rbt_fold1_keys_def)
+qed
+
+
+(** abstract **)
+
+lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
+ is rbt_fold1_keys by simp
+
+lemma fold1_keys_def_alt:
+ "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
+ by transfer (simp add: rbt_fold1_keys_def)
+
+lemma finite_fold1_fold1_keys:
+ assumes "class.ab_semigroup_mult f"
+ assumes "\<not> (is_empty t)"
+ shows "Finite_Set.fold1 f (Set t) = fold1_keys f t"
+proof -
+ interpret ab_semigroup_mult f by fact
+ show ?thesis using assms
+ by (auto simp: fold1_keys_def_alt set_keys fold_def_alt fold1_distinct_set_fold non_empty_keys)
+qed
+
+(* minimum *)
+
+lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
+
+lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
+
+lemma r_min_alt_def: "r_min t = fold1_keys min t"
+by transfer (simp add: rbt_min_def)
+
+lemma r_min_eq_r_min_opt:
+ assumes "\<not> (is_empty t)"
+ shows "r_min t = r_min_opt t"
+using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
+
+lemma fold_keys_min_top_eq:
+ fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
+ assumes "\<not> (is_empty t)"
+ shows "fold_keys min t top = fold1_keys min t"
+proof -
+ have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top =
+ List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
+ by (simp add: hd_Cons_tl[symmetric])
+ { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
+ have "List.fold min (x#xs) top = List.fold min xs x"
+ by (simp add: inf_min[symmetric])
+ } note ** = this
+ show ?thesis using assms
+ unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
+ apply transfer
+ apply (case_tac t)
+ apply simp
+ apply (subst *)
+ apply simp
+ apply (subst **)
+ apply simp
+ done
+qed
+
+(* maximum *)
+
+lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
+
+lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
+
+lemma r_max_alt_def: "r_max t = fold1_keys max t"
+by transfer (simp add: rbt_max_def)
+
+lemma r_max_eq_r_max_opt:
+ assumes "\<not> (is_empty t)"
+ shows "r_max t = r_max_opt t"
+using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
+
+lemma fold_keys_max_bot_eq:
+ fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
+ assumes "\<not> (is_empty t)"
+ shows "fold_keys max t bot = fold1_keys max t"
+proof -
+ have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot =
+ List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
+ by (simp add: hd_Cons_tl[symmetric])
+ { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
+ have "List.fold max (x#xs) bot = List.fold max xs x"
+ by (simp add: sup_max[symmetric])
+ } note ** = this
+ show ?thesis using assms
+ unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
+ apply transfer
+ apply (case_tac t)
+ apply simp
+ apply (subst *)
+ apply simp
+ apply (subst **)
+ apply simp
+ done
+qed
+
+
+section {* Code equations *}
+
+code_datatype Set Coset
+
+lemma empty_Set [code]:
+ "Set.empty = Set RBT.empty"
+by (auto simp: Set_def)
+
+lemma UNIV_Coset [code]:
+ "UNIV = Coset RBT.empty"
+by (auto simp: Set_def)
+
+lemma is_empty_Set [code]:
+ "Set.is_empty (Set t) = RBT.is_empty t"
+ unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1])
+
+lemma compl_code [code]:
+ "- Set xs = Coset xs"
+ "- Coset xs = Set xs"
+by (simp_all add: Set_def)
+
+lemma member_code [code]:
+ "x \<in> (Set t) = (RBT.lookup t x = Some ())"
+ "x \<in> (Coset t) = (RBT.lookup t x = None)"
+by (simp_all add: Set_def)
+
+lemma insert_code [code]:
+ "Set.insert x (Set t) = Set (RBT.insert x () t)"
+ "Set.insert x (Coset t) = Coset (RBT.delete x t)"
+by (auto simp: Set_def)
+
+lemma remove_code [code]:
+ "Set.remove x (Set t) = Set (RBT.delete x t)"
+ "Set.remove x (Coset t) = Coset (RBT.insert x () t)"
+by (auto simp: Set_def)
+
+lemma union_Set [code]:
+ "Set t \<union> A = fold_keys Set.insert t A"
+proof -
+ interpret comp_fun_idem Set.insert
+ by (fact comp_fun_idem_insert)
+ from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`]
+ show ?thesis by (auto simp add: union_fold_insert)
+qed
+
+lemma inter_Set [code]:
+ "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
+by (simp add: inter_filter finite_filter_rbt_filter)
+
+lemma minus_Set [code]:
+ "A - Set t = fold_keys Set.remove t A"
+proof -
+ interpret comp_fun_idem Set.remove
+ by (fact comp_fun_idem_remove)
+ from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`]
+ show ?thesis by (auto simp add: minus_fold_remove)
+qed
+
+lemma union_Coset [code]:
+ "Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
+proof -
+ have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
+ show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
+qed
+
+lemma union_Set_Set [code]:
+ "Set t1 \<union> Set t2 = Set (union t1 t2)"
+by (auto simp add: lookup_union map_add_Some_iff Set_def)
+
+lemma inter_Coset [code]:
+ "A \<inter> Coset t = fold_keys Set.remove t A"
+by (simp add: Diff_eq [symmetric] minus_Set)
+
+lemma inter_Coset_Coset [code]:
+ "Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
+by (auto simp add: lookup_union map_add_Some_iff Set_def)
+
+lemma minus_Coset [code]:
+ "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
+by (simp add: inter_Set[simplified Int_commute])
+
+lemma project_Set [code]:
+ "Set.project P (Set t) = (rbt_filter P t)"
+by (auto simp add: project_filter finite_filter_rbt_filter)
+
+lemma image_Set [code]:
+ "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
+proof -
+ have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
+ then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
+qed
+
+lemma Ball_Set [code]:
+ "Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
+proof -
+ have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
+ then show ?thesis
+ by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
+qed
+
+lemma Bex_Set [code]:
+ "Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
+proof -
+ have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
+ then show ?thesis
+ by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
+qed
+
+lemma subset_code [code]:
+ "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)"
+ "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
+by auto
+
+definition non_empty_trees where [code del]: "non_empty_trees t1 t2 \<longleftrightarrow> Coset t1 \<le> Set t2"
+
+code_abort non_empty_trees
+
+lemma subset_Coset_empty_Set_empty [code]:
+ "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of
+ (rbt.Empty, rbt.Empty) => False |
+ (_, _) => non_empty_trees t1 t2)"
+proof -
+ have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
+ by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
+ have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
+ show ?thesis
+ by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split simp: non_empty_trees_def)
+qed
+
+text {* A frequent case – avoid intermediate sets *}
+lemma [code_unfold]:
+ "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
+by (simp add: subset_code Ball_Set)
+
+lemma card_Set [code]:
+ "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
+by (auto simp add: card_def fold_image_def intro!: finite_fold_fold_keys) (default, simp)
+
+lemma setsum_Set [code]:
+ "setsum f (Set xs) = fold_keys (plus o f) xs 0"
+proof -
+ have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
+ then show ?thesis
+ by (auto simp add: setsum_def fold_image_def finite_fold_fold_keys o_def)
+qed
+
+definition not_a_singleton_tree where [code del]: "not_a_singleton_tree x y = x y"
+
+code_abort not_a_singleton_tree
+
+lemma the_elem_set [code]:
+ fixes t :: "('a :: linorder, unit) rbt"
+ shows "the_elem (Set t) = (case impl_of t of
+ (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
+ | _ \<Rightarrow> not_a_singleton_tree the_elem (Set t))"
+proof -
+ {
+ fix x :: "'a :: linorder"
+ let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty"
+ have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
+ then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
+
+ have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x"
+ by (subst(asm) RBT_inverse[symmetric, OF *])
+ (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
+ }
+ then show ?thesis unfolding not_a_singleton_tree_def
+ by(auto split: rbt.split unit.split color.split)
+qed
+
+lemma Pow_Set [code]:
+ "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
+by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
+
+lemma product_Set [code]:
+ "Product_Type.product (Set t1) (Set t2) =
+ fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
+proof -
+ have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
+ show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]
+ by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
+qed
+
+lemma Id_on_Set [code]:
+ "Id_on (Set t) = fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
+proof -
+ have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
+ then show ?thesis
+ by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
+qed
+
+lemma Image_Set [code]:
+ "(Set t) `` S = fold_keys (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) t {}"
+by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold])
+
+lemma trancl_set_ntrancl [code]:
+ "trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)"
+by (simp add: finite_trancl_ntranl)
+
+lemma relcomp_Set[code]:
+ "(Set t1) O (Set t2) = fold_keys
+ (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
+proof -
+ interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
+ have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
+ by default (auto simp add: fun_eq_iff)
+ show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
+ by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
+qed
+
+lemma wf_set [code]:
+ "wf (Set t) = acyclic (Set t)"
+by (simp add: wf_iff_acyclic_if_finite)
+
+definition not_non_empty_tree where [code del]: "not_non_empty_tree x y = x y"
+
+code_abort not_non_empty_tree
+
+lemma Min_fin_set_fold [code]:
+ "Min (Set t) = (if is_empty t then not_non_empty_tree Min (Set t) else r_min_opt t)"
+proof -
+ have *:"(class.ab_semigroup_mult (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_min
+ unfolding class.ab_semigroup_idem_mult_def by blast
+ show ?thesis
+ by (auto simp add: Min_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_min_alt_def
+ r_min_eq_r_min_opt[symmetric])
+qed
+
+lemma Inf_fin_set_fold [code]:
+ "Inf_fin (Set t) = Min (Set t)"
+by (simp add: inf_min Inf_fin_def Min_def)
+
+lemma Inf_Set_fold:
+ fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
+ shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
+proof -
+ have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
+ then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
+ by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
+ then show ?thesis
+ by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
+qed
+
+definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
+declare Inf'_def[symmetric, code_unfold]
+declare Inf_Set_fold[folded Inf'_def, code]
+
+lemma INFI_Set_fold [code]:
+ "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
+proof -
+ have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
+ by default (auto simp add: fun_eq_iff ac_simps)
+ then show ?thesis
+ by (auto simp: INF_fold_inf finite_fold_fold_keys)
+qed
+
+lemma Max_fin_set_fold [code]:
+ "Max (Set t) = (if is_empty t then not_non_empty_tree Max (Set t) else r_max_opt t)"
+proof -
+ have *:"(class.ab_semigroup_mult (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_max
+ unfolding class.ab_semigroup_idem_mult_def by blast
+ show ?thesis
+ by (auto simp add: Max_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_max_alt_def
+ r_max_eq_r_max_opt[symmetric])
+qed
+
+lemma Sup_fin_set_fold [code]:
+ "Sup_fin (Set t) = Max (Set t)"
+by (simp add: sup_max Sup_fin_def Max_def)
+
+lemma Sup_Set_fold:
+ fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
+ shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
+proof -
+ have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
+ then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
+ by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
+ then show ?thesis
+ by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
+qed
+
+definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
+declare Sup'_def[symmetric, code_unfold]
+declare Sup_Set_fold[folded Sup'_def, code]
+
+lemma SUPR_Set_fold [code]:
+ "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
+proof -
+ have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
+ by default (auto simp add: fun_eq_iff ac_simps)
+ then show ?thesis
+ by (auto simp: SUP_fold_sup finite_fold_fold_keys)
+qed
+
+lemma sorted_list_set[code]:
+ "sorted_list_of_set (Set t) = keys t"
+by (auto simp add: set_keys intro: sorted_distinct_set_unique)
+
+hide_const (open) RBT_Set.Set RBT_Set.Coset
+
+end
--- a/src/HOL/List.thy Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/List.thy Tue Jul 31 19:55:04 2012 +0200
@@ -2458,6 +2458,28 @@
"Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
+lemma (in ab_semigroup_mult) fold1_distinct_set_fold:
+ assumes "xs \<noteq> []"
+ assumes d: "distinct xs"
+ shows "Finite_Set.fold1 times (set xs) = List.fold times (tl xs) (hd xs)"
+proof -
+ interpret comp_fun_commute times by (fact comp_fun_commute)
+ from assms obtain y ys where xs: "xs = y # ys"
+ by (cases xs) auto
+ then have *: "y \<notin> set ys" using assms by simp
+ from xs d have **: "remdups ys = ys" by safe (induct ys, auto)
+ show ?thesis
+ proof (cases "set ys = {}")
+ case True with xs show ?thesis by simp
+ next
+ case False
+ then have "fold1 times (Set.insert y (set ys)) = Finite_Set.fold times y (set ys)"
+ by (simp_all add: fold1_eq_fold *)
+ with xs show ?thesis
+ by (simp add: fold_set_fold_remdups **)
+ qed
+qed
+
lemma (in comp_fun_idem) fold_set_fold:
"Finite_Set.fold f y (set xs) = fold f xs y"
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Tue Jul 31 19:55:04 2012 +0200
@@ -0,0 +1,200 @@
+theory Needham_Schroeder_Base
+imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
+begin
+
+datatype agent = Alice | Bob | Spy
+
+definition agents :: "agent set"
+where
+ "agents = {Spy, Alice, Bob}"
+
+definition bad :: "agent set"
+where
+ "bad = {Spy}"
+
+datatype key = pubEK agent | priEK agent
+
+fun invKey
+where
+ "invKey (pubEK A) = priEK A"
+| "invKey (priEK A) = pubEK A"
+
+datatype
+ msg = Agent agent
+ | Key key
+ | Nonce nat
+ | MPair msg msg
+ | Crypt key msg
+
+syntax
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
+
+syntax (xsymbols)
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+
+translations
+ "{|x, y, z|}" == "{|x, {|y, z|}|}"
+ "{|x, y|}" == "CONST MPair x y"
+
+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"
+
+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]:
+ "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
+
+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"
+ | 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"
+
+primrec initState
+where
+ initState_Alice:
+ "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
+| initState_Bob:
+ "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
+| initState_Spy:
+ "initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
+
+datatype
+ event = Says agent agent msg
+ | Gets agent msg
+ | Notes agent msg
+
+
+primrec knows :: "agent => event list => msg set"
+where
+ knows_Nil: "knows A [] = initState A"
+| knows_Cons:
+ "knows A (ev # evs) =
+ (if A = Spy then
+ (case ev of
+ Says A' B X => insert X (knows Spy evs)
+ | Gets A' X => knows Spy evs
+ | Notes A' X =>
+ if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
+ else
+ (case ev of
+ Says A' B X =>
+ if A'=A then insert X (knows A evs) else knows A evs
+ | Gets A' X =>
+ if A'=A then insert X (knows A evs) else knows A evs
+ | Notes A' X =>
+ if A'=A then insert X (knows A evs) else knows A evs))"
+
+abbreviation (input)
+ spies :: "event list => msg set" where
+ "spies == knows Spy"
+
+primrec used :: "event list => msg set"
+where
+ used_Nil: "used [] = Union (parts ` initState ` agents)"
+| used_Cons: "used (ev # evs) =
+ (case ev of
+ Says A B X => parts {X} \<union> used evs
+ | Gets A X => used evs
+ | Notes A X => parts {X} \<union> used evs)"
+
+subsection {* Preparations for sets *}
+
+fun find_first :: "('a => 'b option) => 'a list => 'b option"
+where
+ "find_first f [] = None"
+| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
+
+consts cps_of_set :: "'a set => ('a => term list option) => term list option"
+
+lemma
+ [code]: "cps_of_set (set xs) f = find_first f xs"
+sorry
+
+consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option"
+consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued"
+
+lemma
+ [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
+sorry
+
+consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
+ => 'b list => 'a Quickcheck_Exhaustive.three_valued"
+
+lemma [code]:
+ "find_first' f [] = Quickcheck_Exhaustive.No_value"
+ "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
+sorry
+
+lemma
+ [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
+sorry
+
+setup {*
+let
+ val Fun = Predicate_Compile_Aux.Fun
+ val Input = Predicate_Compile_Aux.Input
+ val Output = Predicate_Compile_Aux.Output
+ val Bool = Predicate_Compile_Aux.Bool
+ val oi = Fun (Output, Fun (Input, Bool))
+ val ii = Fun (Input, Fun (Input, Bool))
+ fun of_set compfuns (Type ("fun", [T, _])) =
+ case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
+ Type ("Quickcheck_Exhaustive.three_valued", _) =>
+ Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
+ | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T)
+ | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
+ fun member compfuns (U as Type ("fun", [T, _])) =
+ (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
+ (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
+
+in
+ Core_Data.force_modes_and_compilations @{const_name Set.member}
+ [(oi, (of_set, false)), (ii, (member, false))]
+end
+*}
+
+subsection {* Derived equations for analz, parts and synth *}
+
+lemma [code]:
+ "analz H = (let
+ H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
+ in if H' = H then H else analz H')"
+sorry
+
+lemma [code]:
+ "parts H = (let
+ H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
+ in if H' = H then H else parts H')"
+sorry
+
+definition synth' :: "msg set => msg => bool"
+where
+ "synth' H m = (m : synth H)"
+
+lemmas [code_pred_intro] = synth.intros[folded synth'_def]
+
+code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
+declare ListMem_iff[symmetric, code_pred_inline]
+declare [[quickcheck_timing]]
+
+setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
+declare [[quickcheck_full_support = false]]
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy Tue Jul 31 19:55:04 2012 +0200
@@ -0,0 +1,100 @@
+theory Needham_Schroeder_Guided_Attacker_Example
+imports Needham_Schroeder_Base
+begin
+
+inductive_set ns_public :: "event list set"
+ where
+ (*Initial trace is empty*)
+ Nil: "[] \<in> ns_public"
+
+ | Fake_NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1) \<rbrakk>
+ \<Longrightarrow> Says Spy B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
+ | Fake_NS2: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk>
+ \<Longrightarrow> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ # evs1 \<in> ns_public"
+
+ (*Alice initiates a protocol run, sending a nonce to Bob*)
+ | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
+ (*Bob responds to Alice's message with a further nonce*)
+ | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
+ Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ # evs2 \<in> ns_public"
+
+ (*Alice proves her existence by sending NB back to Bob.*)
+ | NS3: "\<lbrakk>evs3 \<in> ns_public;
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
+
+declare ListMem_iff[symmetric, code_pred_inline]
+
+lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
+
+code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
+thm ns_publicp.equation
+
+code_pred [generator_cps] ns_publicp .
+thm ns_publicp.generator_cps_equation
+
+
+lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
+quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample]
+(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
+oops
+
+lemma
+ "\<lbrakk>ns_publicp evs\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
+ \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
+ \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
+(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample]
+quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
+oops
+
+section {* Proving the counterexample trace for validation *}
+
+lemma
+ assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
+ assumes "evs =
+ [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
+ Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
+ Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
+ Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
+ shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
+proof -
+ from assms show "A \<noteq> Spy" by auto
+ from assms show "B \<noteq> Spy" by auto
+ have "[] : ns_public" by (rule Nil)
+ then have first_step: "[?e0] : ns_public"
+ proof (rule NS1)
+ show "Nonce 0 ~: used []" by eval
+ qed
+ then have "[?e1, ?e0] : ns_public"
+ proof (rule Fake_NS1)
+ show "Nonce 0 : analz (knows Spy [?e0])" by eval
+ qed
+ then have "[?e2, ?e1, ?e0] : ns_public"
+ proof (rule NS2)
+ show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
+ show " Nonce 1 ~: used [?e1, ?e0]" by eval
+ qed
+ then show "evs : ns_public"
+ unfolding assms
+ proof (rule NS3)
+ show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
+ show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|})
+ : set [?e2, ?e1, ?e0]" by simp
+ qed
+ from assms show "Nonce NB : analz (knows Spy evs)"
+ apply simp
+ apply (rule analz.intros(4))
+ apply (rule analz.intros(1))
+ apply (auto simp add: bad_def)
+ done
+qed
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy Tue Jul 31 19:55:04 2012 +0200
@@ -0,0 +1,47 @@
+theory Needham_Schroeder_No_Attacker_Example
+imports Needham_Schroeder_Base
+begin
+
+inductive_set ns_public :: "event list set"
+ where
+ (*Initial trace is empty*)
+ Nil: "[] \<in> ns_public"
+ (*Alice initiates a protocol run, sending a nonce to Bob*)
+ | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
+ (*Bob responds to Alice's message with a further nonce*)
+ | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
+ Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ # evs2 \<in> ns_public"
+
+ (*Alice proves her existence by sending NB back to Bob.*)
+ | NS3: "\<lbrakk>evs3 \<in> ns_public;
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
+
+code_pred [skip_proof] ns_publicp .
+thm ns_publicp.equation
+
+code_pred [generator_cps] ns_publicp .
+thm ns_publicp.generator_cps_equation
+
+lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
+(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose]
+quickcheck[exhaustive, size = 8, timeout = 3600, verbose]
+quickcheck[narrowing, size = 7, timeout = 3600, verbose]*)
+quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample]
+oops
+
+lemma
+ "\<lbrakk>ns_publicp evs\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
+ \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
+ \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
+quickcheck[smart_exhaustive, depth = 6, timeout = 30]
+quickcheck[narrowing, size = 6, timeout = 30, verbose]
+oops
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy Tue Jul 31 19:55:04 2012 +0200
@@ -0,0 +1,96 @@
+theory Needham_Schroeder_Unguided_Attacker_Example
+imports Needham_Schroeder_Base
+begin
+
+inductive_set ns_public :: "event list set"
+ where
+ (*Initial trace is empty*)
+ Nil: "[] \<in> ns_public"
+
+ | Fake: "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk>
+ \<Longrightarrow> Says Spy A X # evs1 \<in> ns_public"
+
+ (*Alice initiates a protocol run, sending a nonce to Bob*)
+ | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
+ (*Bob responds to Alice's message with a further nonce*)
+ | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
+ Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ # evs2 \<in> ns_public"
+
+ (*Alice proves her existence by sending NB back to Bob.*)
+ | NS3: "\<lbrakk>evs3 \<in> ns_public;
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
+
+declare ListMem_iff[symmetric, code_pred_inline]
+
+lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
+
+code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
+thm ns_publicp.equation
+
+code_pred [generator_cps] ns_publicp .
+thm ns_publicp.generator_cps_equation
+
+
+lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
+quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample]
+(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
+oops
+
+lemma
+ "\<lbrakk>ns_publicp evs\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
+ \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
+ \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
+quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample]
+(*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
+oops
+
+section {* Proving the counterexample trace for validation *}
+
+lemma
+ assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
+ assumes "evs =
+ [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
+ Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
+ Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
+ Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
+ shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
+proof -
+ from assms show "A \<noteq> Spy" by auto
+ from assms show "B \<noteq> Spy" by auto
+ have "[] : ns_public" by (rule Nil)
+ then have first_step: "[?e0] : ns_public"
+ proof (rule NS1)
+ show "Nonce 0 ~: used []" by eval
+ qed
+ then have "[?e1, ?e0] : ns_public"
+ proof (rule Fake)
+ show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))"
+ by (intro synth.intros(2,3,4,1)) eval+
+ qed
+ then have "[?e2, ?e1, ?e0] : ns_public"
+ proof (rule NS2)
+ show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
+ show " Nonce 1 ~: used [?e1, ?e0]" by eval
+ qed
+ then show "evs : ns_public"
+ unfolding assms
+ proof (rule NS3)
+ show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
+ show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp
+ qed
+ from assms show "Nonce NB : analz (knows Spy evs)"
+ apply simp
+ apply (rule analz.intros(4))
+ apply (rule analz.intros(1))
+ apply (auto simp add: bad_def)
+ done
+qed
+
+end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Benchmark/ROOT.ML Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/Quickcheck_Benchmark/ROOT.ML Tue Jul 31 19:55:04 2012 +0200
@@ -1,1 +1,6 @@
-use_thys ["Find_Unused_Assms_Examples"]
+Unsynchronized.setmp quick_and_dirty true use_thys [
+ "Find_Unused_Assms_Examples",
+ "Needham_Schroeder_No_Attacker_Example",
+ "Needham_Schroeder_Guided_Attacker_Example",
+ "Needham_Schroeder_Unguided_Attacker_Example"
+]
--- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_Base.thy Tue Jul 31 17:40:33 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,200 +0,0 @@
-theory Needham_Schroeder_Base
-imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
-begin
-
-datatype agent = Alice | Bob | Spy
-
-definition agents :: "agent set"
-where
- "agents = {Spy, Alice, Bob}"
-
-definition bad :: "agent set"
-where
- "bad = {Spy}"
-
-datatype key = pubEK agent | priEK agent
-
-fun invKey
-where
- "invKey (pubEK A) = priEK A"
-| "invKey (priEK A) = pubEK A"
-
-datatype
- msg = Agent agent
- | Key key
- | Nonce nat
- | MPair msg msg
- | Crypt key msg
-
-syntax
- "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
-
-syntax (xsymbols)
- "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
-
-translations
- "{|x, y, z|}" == "{|x, {|y, z|}|}"
- "{|x, y|}" == "CONST MPair x y"
-
-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"
-
-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]:
- "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
-
-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"
- | 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"
-
-primrec initState
-where
- initState_Alice:
- "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
-| initState_Bob:
- "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
-| initState_Spy:
- "initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
-
-datatype
- event = Says agent agent msg
- | Gets agent msg
- | Notes agent msg
-
-
-primrec knows :: "agent => event list => msg set"
-where
- knows_Nil: "knows A [] = initState A"
-| knows_Cons:
- "knows A (ev # evs) =
- (if A = Spy then
- (case ev of
- Says A' B X => insert X (knows Spy evs)
- | Gets A' X => knows Spy evs
- | Notes A' X =>
- if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
- else
- (case ev of
- Says A' B X =>
- if A'=A then insert X (knows A evs) else knows A evs
- | Gets A' X =>
- if A'=A then insert X (knows A evs) else knows A evs
- | Notes A' X =>
- if A'=A then insert X (knows A evs) else knows A evs))"
-
-abbreviation (input)
- spies :: "event list => msg set" where
- "spies == knows Spy"
-
-primrec used :: "event list => msg set"
-where
- used_Nil: "used [] = Union (parts ` initState ` agents)"
-| used_Cons: "used (ev # evs) =
- (case ev of
- Says A B X => parts {X} \<union> used evs
- | Gets A X => used evs
- | Notes A X => parts {X} \<union> used evs)"
-
-subsection {* Preparations for sets *}
-
-fun find_first :: "('a => 'b option) => 'a list => 'b option"
-where
- "find_first f [] = None"
-| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
-
-consts cps_of_set :: "'a set => ('a => term list option) => term list option"
-
-lemma
- [code]: "cps_of_set (set xs) f = find_first f xs"
-sorry
-
-consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option"
-consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued"
-
-lemma
- [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
-sorry
-
-consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
- => 'b list => 'a Quickcheck_Exhaustive.three_valued"
-
-lemma [code]:
- "find_first' f [] = Quickcheck_Exhaustive.No_value"
- "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
-sorry
-
-lemma
- [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
-sorry
-
-setup {*
-let
- val Fun = Predicate_Compile_Aux.Fun
- val Input = Predicate_Compile_Aux.Input
- val Output = Predicate_Compile_Aux.Output
- val Bool = Predicate_Compile_Aux.Bool
- val oi = Fun (Output, Fun (Input, Bool))
- val ii = Fun (Input, Fun (Input, Bool))
- fun of_set compfuns (Type ("fun", [T, _])) =
- case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
- Type ("Quickcheck_Exhaustive.three_valued", _) =>
- Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
- | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T)
- | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
- fun member compfuns (U as Type ("fun", [T, _])) =
- (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
- (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
-
-in
- Core_Data.force_modes_and_compilations @{const_name Set.member}
- [(oi, (of_set, false)), (ii, (member, false))]
-end
-*}
-
-subsection {* Derived equations for analz, parts and synth *}
-
-lemma [code]:
- "analz H = (let
- H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
- in if H' = H then H else analz H')"
-sorry
-
-lemma [code]:
- "parts H = (let
- H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
- in if H' = H then H else parts H')"
-sorry
-
-definition synth' :: "msg set => msg => bool"
-where
- "synth' H m = (m : synth H)"
-
-lemmas [code_pred_intro] = synth.intros[folded synth'_def]
-
-code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
-
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
-declare ListMem_iff[symmetric, code_pred_inline]
-declare [[quickcheck_timing]]
-
-setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
-declare [[quickcheck_full_support = false]]
-
-end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy Tue Jul 31 17:40:33 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-theory Needham_Schroeder_Guided_Attacker_Example
-imports Needham_Schroeder_Base
-begin
-
-inductive_set ns_public :: "event list set"
- where
- (*Initial trace is empty*)
- Nil: "[] \<in> ns_public"
-
- | Fake_NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1) \<rbrakk>
- \<Longrightarrow> Says Spy B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
- # evs1 \<in> ns_public"
- | Fake_NS2: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk>
- \<Longrightarrow> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
- # evs1 \<in> ns_public"
-
- (*Alice initiates a protocol run, sending a nonce to Bob*)
- | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
- # evs1 \<in> ns_public"
- (*Bob responds to Alice's message with a further nonce*)
- | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
- Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
- # evs2 \<in> ns_public"
-
- (*Alice proves her existence by sending NB back to Bob.*)
- | NS3: "\<lbrakk>evs3 \<in> ns_public;
- Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
- Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
-
-declare ListMem_iff[symmetric, code_pred_inline]
-
-lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
-
-code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
-thm ns_publicp.equation
-
-code_pred [generator_cps] ns_publicp .
-thm ns_publicp.generator_cps_equation
-
-
-lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
-quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample]
-(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
-oops
-
-lemma
- "\<lbrakk>ns_publicp evs\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
- \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
- \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
-(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample]
-quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
-oops
-
-section {* Proving the counterexample trace for validation *}
-
-lemma
- assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
- assumes "evs =
- [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
- Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
- Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
- Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
- shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
-proof -
- from assms show "A \<noteq> Spy" by auto
- from assms show "B \<noteq> Spy" by auto
- have "[] : ns_public" by (rule Nil)
- then have first_step: "[?e0] : ns_public"
- proof (rule NS1)
- show "Nonce 0 ~: used []" by eval
- qed
- then have "[?e1, ?e0] : ns_public"
- proof (rule Fake_NS1)
- show "Nonce 0 : analz (knows Spy [?e0])" by eval
- qed
- then have "[?e2, ?e1, ?e0] : ns_public"
- proof (rule NS2)
- show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
- show " Nonce 1 ~: used [?e1, ?e0]" by eval
- qed
- then show "evs : ns_public"
- unfolding assms
- proof (rule NS3)
- show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
- show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|})
- : set [?e2, ?e1, ?e0]" by simp
- qed
- from assms show "Nonce NB : analz (knows Spy evs)"
- apply simp
- apply (rule analz.intros(4))
- apply (rule analz.intros(1))
- apply (auto simp add: bad_def)
- done
-qed
-
-end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy Tue Jul 31 17:40:33 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-theory Needham_Schroeder_No_Attacker_Example
-imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
-begin
-
-inductive_set ns_public :: "event list set"
- where
- (*Initial trace is empty*)
- Nil: "[] \<in> ns_public"
- (*Alice initiates a protocol run, sending a nonce to Bob*)
- | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
- # evs1 \<in> ns_public"
- (*Bob responds to Alice's message with a further nonce*)
- | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
- Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
- # evs2 \<in> ns_public"
-
- (*Alice proves her existence by sending NB back to Bob.*)
- | NS3: "\<lbrakk>evs3 \<in> ns_public;
- Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
- Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
-
-code_pred [skip_proof] ns_publicp .
-thm ns_publicp.equation
-
-code_pred [generator_cps] ns_publicp .
-thm ns_publicp.generator_cps_equation
-
-lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
-(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose]
-quickcheck[exhaustive, size = 8, timeout = 3600, verbose]
-quickcheck[narrowing, size = 7, timeout = 3600, verbose]*)
-quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample]
-oops
-
-lemma
- "\<lbrakk>ns_publicp evs\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
- \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
- \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
-quickcheck[smart_exhaustive, depth = 6, timeout = 30]
-quickcheck[narrowing, size = 6, timeout = 30, verbose]
-oops
-
-end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker_Example.thy Tue Jul 31 17:40:33 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-theory Needham_Schroeder_Unguided_Attacker_Example
-imports Needham_Schroeder_Base
-begin
-
-inductive_set ns_public :: "event list set"
- where
- (*Initial trace is empty*)
- Nil: "[] \<in> ns_public"
-
- | Fake: "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk>
- \<Longrightarrow> Says Spy A X # evs1 \<in> ns_public"
-
- (*Alice initiates a protocol run, sending a nonce to Bob*)
- | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
- # evs1 \<in> ns_public"
- (*Bob responds to Alice's message with a further nonce*)
- | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
- Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
- # evs2 \<in> ns_public"
-
- (*Alice proves her existence by sending NB back to Bob.*)
- | NS3: "\<lbrakk>evs3 \<in> ns_public;
- Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
- Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
-
-declare ListMem_iff[symmetric, code_pred_inline]
-
-lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
-
-code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
-thm ns_publicp.equation
-
-code_pred [generator_cps] ns_publicp .
-thm ns_publicp.generator_cps_equation
-
-
-lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
-quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample]
-(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
-oops
-
-lemma
- "\<lbrakk>ns_publicp evs\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
- \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
- \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
-quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample]
-(*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
-oops
-
-section {* Proving the counterexample trace for validation *}
-
-lemma
- assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
- assumes "evs =
- [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
- Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
- Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
- Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
- shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
-proof -
- from assms show "A \<noteq> Spy" by auto
- from assms show "B \<noteq> Spy" by auto
- have "[] : ns_public" by (rule Nil)
- then have first_step: "[?e0] : ns_public"
- proof (rule NS1)
- show "Nonce 0 ~: used []" by eval
- qed
- then have "[?e1, ?e0] : ns_public"
- proof (rule Fake)
- show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))"
- by (intro synth.intros(2,3,4,1)) eval+
- qed
- then have "[?e2, ?e1, ?e0] : ns_public"
- proof (rule NS2)
- show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
- show " Nonce 1 ~: used [?e1, ?e0]" by eval
- qed
- then show "evs : ns_public"
- unfolding assms
- proof (rule NS3)
- show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
- show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp
- qed
- from assms show "Nonce NB : analz (knows Spy evs)"
- apply simp
- apply (rule analz.intros(4))
- apply (rule analz.intros(1))
- apply (auto simp add: bad_def)
- done
-qed
-
-end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Examples/ROOT.ML Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML Tue Jul 31 19:55:04 2012 +0200
@@ -1,14 +1,10 @@
use_thys [
-(* "Find_Unused_Assms_Examples", *)
"Quickcheck_Examples"
(*,
"Quickcheck_Lattice_Examples",
"Completeness",
"Quickcheck_Interfaces",
- "Hotel_Example",
- "Needham_Schroeder_No_Attacker_Example",
- "Needham_Schroeder_Guided_Attacker_Example",
- "Needham_Schroeder_Unguided_Attacker_Example"*)
+ "Hotel_Example",*)
];
if getenv "ISABELLE_GHC" = "" then ()
--- a/src/HOL/Quotient_Examples/Lift_RBT.thy Tue Jul 31 17:40:33 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,159 +0,0 @@
-(* Title: HOL/Quotient_Examples/Lift_RBT.thy
- Author: Lukas Bulwahn and Ondrej Kuncar
-*)
-
-header {* Lifting operations of RBT trees *}
-
-theory Lift_RBT
-imports Main "~~/src/HOL/Library/RBT_Impl"
-begin
-
-(* TODO: Replace the ancient Library/RBT theory by this example of the lifting and transfer mechanism. *)
-
-subsection {* Type definition *}
-
-typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
- morphisms impl_of RBT
-proof -
- have "RBT_Impl.Empty \<in> ?rbt" by simp
- then show ?thesis ..
-qed
-
-lemma rbt_eq_iff:
- "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
- by (simp add: impl_of_inject)
-
-lemma rbt_eqI:
- "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
- by (simp add: rbt_eq_iff)
-
-lemma is_rbt_impl_of [simp, intro]:
- "is_rbt (impl_of t)"
- using impl_of [of t] by simp
-
-lemma RBT_impl_of [simp, code abstype]:
- "RBT (impl_of t) = t"
- by (simp add: impl_of_inverse)
-
-subsection {* Primitive operations *}
-
-setup_lifting type_definition_rbt
-
-lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup"
-by simp
-
-lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty
-by (simp add: empty_def)
-
-lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_insert"
-by simp
-
-lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete"
-by simp
-
-lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
-by simp
-
-lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys
-by simp
-
-lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload"
-by simp
-
-lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
-by simp
-
-lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map
-by simp
-
-lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is RBT_Impl.fold
-by simp
-
-export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
-
-subsection {* Derived operations *}
-
-definition is_empty :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
- [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
-
-
-subsection {* Abstract lookup properties *}
-
-lemma lookup_RBT:
- "is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t"
- by (simp add: lookup_def RBT_inverse)
-
-lemma lookup_impl_of:
- "rbt_lookup (impl_of t) = lookup t"
- by transfer (rule refl)
-
-lemma entries_impl_of:
- "RBT_Impl.entries (impl_of t) = entries t"
- by transfer (rule refl)
-
-lemma keys_impl_of:
- "RBT_Impl.keys (impl_of t) = keys t"
- by transfer (rule refl)
-
-lemma lookup_empty [simp]:
- "lookup empty = Map.empty"
- by (simp add: empty_def lookup_RBT fun_eq_iff)
-
-lemma lookup_insert [simp]:
- "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
- by transfer (rule rbt_lookup_rbt_insert)
-
-lemma lookup_delete [simp]:
- "lookup (delete k t) = (lookup t)(k := None)"
- by transfer (simp add: rbt_lookup_rbt_delete restrict_complement_singleton_eq)
-
-lemma map_of_entries [simp]:
- "map_of (entries t) = lookup t"
- by transfer (simp add: map_of_entries)
-
-lemma entries_lookup:
- "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
- by transfer (simp add: entries_rbt_lookup)
-
-lemma lookup_bulkload [simp]:
- "lookup (bulkload xs) = map_of xs"
- by transfer (rule rbt_lookup_rbt_bulkload)
-
-lemma lookup_map_entry [simp]:
- "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
- by transfer (rule rbt_lookup_rbt_map_entry)
-
-lemma lookup_map [simp]:
- "lookup (map f t) k = Option.map (f k) (lookup t k)"
- by transfer (rule rbt_lookup_map)
-
-lemma fold_fold:
- "fold f t = List.fold (prod_case f) (entries t)"
- by transfer (rule RBT_Impl.fold_def)
-
-lemma impl_of_empty:
- "impl_of empty = RBT_Impl.Empty"
- by transfer (rule refl)
-
-lemma is_empty_empty [simp]:
- "is_empty t \<longleftrightarrow> t = empty"
- unfolding is_empty_def by transfer (simp split: rbt.split)
-
-lemma RBT_lookup_empty [simp]: (*FIXME*)
- "rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
- by (cases t) (auto simp add: fun_eq_iff)
-
-lemma lookup_empty_empty [simp]:
- "lookup t = Map.empty \<longleftrightarrow> t = empty"
- by transfer (rule RBT_lookup_empty)
-
-lemma sorted_keys [iff]:
- "sorted (keys t)"
- by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries)
-
-lemma distinct_keys [iff]:
- "distinct (keys t)"
- by transfer (simp add: RBT_Impl.keys_def distinct_entries)
-
-
-end
\ No newline at end of file
--- a/src/HOL/Quotient_Examples/ROOT.ML Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML Tue Jul 31 19:55:04 2012 +0200
@@ -5,5 +5,5 @@
*)
use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Lift_FSet",
- "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"];
+ "Lift_Set", "Lift_Fun", "Quotient_Rat", "Lift_DList"];
--- a/src/HOL/ROOT Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/ROOT Tue Jul 31 19:55:04 2012 +0200
@@ -153,7 +153,7 @@
session Codegenerator_Test = "HOL-Library" +
options [document = false, document_graph = false, browser_info = false]
- theories Generate Generate_Pretty
+ theories Generate Generate_Pretty RBT_Set_Test
session Metis_Examples = HOL +
description {*
@@ -740,8 +740,11 @@
Quickcheck_Narrowing_Examples
session Quickcheck_Benchmark = HOL +
- theories [condition = ISABELLE_BENCHMARK]
- Find_Unused_Assms_Examples (* FIXME more *)
+ theories [condition = ISABELLE_BENCHMARK, quick_and_dirty]
+ Find_Unused_Assms_Examples
+ Needham_Schroeder_No_Attacker_Example
+ Needham_Schroeder_Guided_Attacker_Example
+ Needham_Schroeder_Unguided_Attacker_Example (* FIXME more *)
session Quotient_Examples = HOL +
description {*
@@ -755,7 +758,6 @@
Quotient_Message
Lift_FSet
Lift_Set
- Lift_RBT
Lift_Fun
Quotient_Rat
Lift_DList
--- a/src/HOL/Relation.thy Tue Jul 31 17:40:33 2012 +0200
+++ b/src/HOL/Relation.thy Tue Jul 31 19:55:04 2012 +0200
@@ -1041,5 +1041,83 @@
lemmas Powp_mono [mono] = Pow_mono [to_pred]
+subsubsection {* Expressing relation operations via @{const Finite_Set.fold} *}
+
+lemma Id_on_fold:
+ assumes "finite A"
+ shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A"
+proof -
+ interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" by default auto
+ show ?thesis using assms unfolding Id_on_def by (induct A) simp_all
+qed
+
+lemma comp_fun_commute_Image_fold:
+ "comp_fun_commute (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)"
+proof -
+ interpret comp_fun_idem Set.insert
+ by (fact comp_fun_idem_insert)
+ show ?thesis
+ by default (auto simp add: fun_eq_iff comp_fun_commute split:prod.split)
+qed
+
+lemma Image_fold:
+ assumes "finite R"
+ shows "R `` S = Finite_Set.fold (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) {} R"
+proof -
+ interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)"
+ by (rule comp_fun_commute_Image_fold)
+ have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))"
+ by (auto intro: rev_ImageI)
+ show ?thesis using assms by (induct R) (auto simp: *)
+qed
+
+lemma insert_relcomp_union_fold:
+ assumes "finite S"
+ shows "{x} O S \<union> X = Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S"
+proof -
+ interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'"
+ proof -
+ interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
+ show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')"
+ by default (auto simp add: fun_eq_iff split:prod.split)
+ qed
+ have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x,z) \<in> S}" by (auto simp: relcomp_unfold intro!: exI)
+ show ?thesis unfolding *
+ using `finite S` by (induct S) (auto split: prod.split)
+qed
+
+lemma insert_relcomp_fold:
+ assumes "finite S"
+ shows "Set.insert x R O S =
+ Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S"
+proof -
+ have "Set.insert x R O S = ({x} O S) \<union> (R O S)" by auto
+ then show ?thesis by (auto simp: insert_relcomp_union_fold[OF assms])
+qed
+
+lemma comp_fun_commute_relcomp_fold:
+ assumes "finite S"
+ shows "comp_fun_commute (\<lambda>(x,y) A.
+ Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)"
+proof -
+ have *: "\<And>a b A.
+ Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A"
+ by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong)
+ show ?thesis by default (auto simp: *)
+qed
+
+lemma relcomp_fold:
+ assumes "finite R"
+ assumes "finite S"
+ shows "R O S = Finite_Set.fold
+ (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
+proof -
+ show ?thesis using assms by (induct R)
+ (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
+ cong: if_cong)
+qed
+
+
+
end