# HG changeset patch # User wenzelm # Date 1343757304 -7200 # Node ID 3ef76d545aafba4f19773dc7be51cf6661dc6afd # Parent 77c416ef06fa3e48d3661427d2d25360fe4d6da3# Parent ef374008cb7cf66334945328e36855a5bb2dc30f merged diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Codegenerator_Test/RBT_Set_Test.thy --- /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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Codegenerator_Test/ROOT.ML --- 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"]; diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Finite_Set.thy --- 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 \ g) x A" +using assms +proof induction + case (insert a F) + interpret comp_fun_commute "\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 \ bool) \ 'a set \ 'a set" + where "filter P A = fold (\x A'. if P x then Set.insert x A' else A') {} A" + +lemma comp_fun_commute_filter_fold: "comp_fun_commute (\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 \ B = filter (\x. x \ 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 (\k A. Set.insert (f k) A) {} A" +using assms +proof - + interpret comp_fun_commute "\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 (\k s. s \ P k) True A" +using assms +proof - + interpret comp_fun_commute "\k s. s \ 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 (\k s. s \ P k) False A" +using assms +proof - + interpret comp_fun_commute "\k s. s \ P k" by default auto + show ?thesis using assms by (induct A) auto +qed + +lemma comp_fun_commute_Pow_fold: + "comp_fun_commute (\x A. A \ 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 (\x A. A \ Set.insert x ` A) {{}} A" +using assms +proof - + interpret comp_fun_commute "\x A. A \ 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 "(\y\B. {(x, y)}) \ A = fold (\y. Set.insert (x, y)) A B" +proof - + interpret comp_fun_commute "\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 (\x A. fold (\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 \ B = fold (\x A. fold (\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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/IsaMakefile --- 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Library/Library.thy --- 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Library/RBT.thy --- 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\linorder, 'b) RBT_Impl.rbt. is_rbt t}" morphisms impl_of RBT -proof - show "RBT_Impl.Empty \ {t. is_rbt t}" by simp +proof - + have "RBT_Impl.Empty \ ?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\linorder, 'b) rbt \ 'a \ 'b" where - [code]: "lookup t = rbt_lookup (impl_of t)" - -definition empty :: "('a\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\linorder, 'b) rbt \ 'a \ 'b" is "rbt_lookup" +by simp -definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where - "insert k v t = RBT (rbt_insert k v (impl_of t))" +lift_definition empty :: "('a\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\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" where - "delete k t = RBT (rbt_delete k (impl_of t))" +lift_definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('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\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" is "rbt_delete" +by simp -definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" where - [code]: "entries t = RBT_Impl.entries (impl_of t)" +lift_definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" is RBT_Impl.entries +by simp -definition keys :: "('a\linorder, 'b) rbt \ 'a list" where - [code]: "keys t = RBT_Impl.keys (impl_of t)" - -definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" where - "bulkload xs = RBT (rbt_bulkload xs)" +lift_definition keys :: "('a\linorder, 'b) rbt \ '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\linorder \ 'b) list \ ('a, 'b) rbt" is "rbt_bulkload" +by simp -definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" where - "map_entry k f t = RBT (rbt_map_entry k f (impl_of t))" +lift_definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('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 \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is RBT_Impl.map +by simp -definition map :: "('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" where - "map f t = RBT (RBT_Impl.map f (impl_of t))" +lift_definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ '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\linorder, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" is "rbt_union" +by (simp add: rbt_union_is_rbt) -definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" where - [code]: "fold f t = RBT_Impl.fold f (impl_of t)" - +lift_definition foldi :: "('c \ bool) \ ('a \ 'b \ 'c \ 'c) \ ('a :: linorder, 'b) rbt \ 'c \ '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 \ 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 \ 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 \ 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 \ t = RBT_Impl.Empty" @@ -159,15 +147,41 @@ lemma lookup_empty_empty [simp]: "lookup t = Map.empty \ 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) \ set (entries t))" + by transfer (simp add: rbt_lookup_in_tree) + +lemma keys_entries: "(k \ set (keys t)) = (\v. (k, v) \ 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 \ empty \ keys t \ []" + 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 *} diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Library/RBT_Impl.thy --- 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 \ set (keys t) \ (\v. (k, v) \ set (entries t))" by (auto intro: entry_in_tree_keys) (auto simp add: keys_def) +lemma non_empty_rbt_keys: + "t \ rbt.Empty \ keys t \ []" + 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 \ distinct (keys t)" + by (simp add: distinct_entries keys_def) + + subsubsection {* Tree lookup *} primrec (in ord) rbt_lookup :: "('a, 'b) rbt \ 'a \ '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 \ f k v \ fold f lt" by (simp_all add: fold_def fun_eq_iff) +(* fold with continuation predicate *) + +fun foldi :: "('c \ bool) \ ('a \ 'b \ 'c \ 'c) \ ('a :: linorder, 'b) rbt \ 'c \ '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 *} diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Library/RBT_Set.thy --- /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\linorder, unit) rbt \ 'a set" + where "Set t = {x . lookup t x = Some ()}" + +definition Coset :: "('a\linorder, unit) rbt \ '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 \ 'a set) = Inf" .. + +lemma [code, code del]: + "(Sup :: 'a set set \ '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 \ Some () \ 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 "\k. ((k, ()) \ set (entries t)) = (k \ 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 \ 'b \ 'b) \ ('a, _) rbt \ 'b \ 'b" + where [code_unfold]:"fold_keys f t A = fold (\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 \ bool) \ ('a, 'b) rbt \ 'a set" where + "rbt_filter P t = fold (\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 (\k v s. s \ P k) t False = False" +by (induction t) auto + +lemma rbt_foldi_fold_conj: + "RBT_Impl.foldi (\s. s = True) (\k v s. s \ P k) t val = RBT_Impl.fold (\k v s. s \ P k) t val" +proof (induction t arbitrary: val) + case (Branch c t1) then show ?case + by (cases "RBT_Impl.fold (\k v s. s \ P k) t1 True") (simp_all add: Ball_False) +qed simp + +lemma foldi_fold_conj: "foldi (\s. s = True) (\k v s. s \ P k) t val = fold_keys (\k s. s \ 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 (\k v s. s \ P k) t True = True" +by (induction t) auto + +lemma rbt_foldi_fold_disj: + "RBT_Impl.foldi (\s. s = False) (\k v s. s \ P k) t val = RBT_Impl.fold (\k v s. s \ P k) t val" +proof (induction t arbitrary: val) + case (Branch c t1) then show ?case + by (cases "RBT_Impl.fold (\k v s. s \ P k) t1 False") (simp_all add: Bex_True) +qed simp + +lemma foldi_fold_disj: "foldi (\s. s = False) (\k v s. s \ P k) t val = fold_keys (\k s. s \ 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 \ 'a \ 'a) \ ('a::linorder, 'b) RBT_Impl.rbt \ '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 \ 'a" + where "rbt_min t = rbt_fold1_keys min t" + +lemma key_le_right: "rbt_sorted (Branch c lt k v rt) \ (\x. x \set (RBT_Impl.keys rt) \ k \ x)" +by (auto simp: rbt_greater_prop less_imp_le) + +lemma left_le_key: "rbt_sorted (Branch c lt k v rt) \ (\x. x \set (RBT_Impl.keys lt) \ x \ k)" +by (auto simp: rbt_less_prop less_imp_le) + +lemma fold_min_triv: + fixes k :: "_ :: linorder" + shows "(\x\set xs. k \ x) \ 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) \ 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 \ rbt.Empty \ 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 "\color t1 a b t2. P t1 \ P t2 \ t1 = rbt.Empty \ P (Branch color t1 a b t2)" + assumes "\color t1 a b t2. P t1 \ P t2 \ t1 \ rbt.Empty \ 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 \ rbt.Empty" + shows "rbt_min_opt t \ 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 \ rbt.Empty" + shows "\y. y \ set (RBT_Impl.keys t) \ y \ 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 \ y \ set (RBT_Impl.keys t1) \ y \ 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 \ k" by (simp add: left_le_key rbt_min_opt_in_set) + moreover from goal3 have "k \ 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 \ RBT_Impl.Empty" + assumes "is_rbt t" + shows "rbt_min t = rbt_min_opt t" +proof - + interpret ab_semigroup_idem_mult "(min :: 'a \ 'a \ '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 \ 'a" + where "rbt_max t = rbt_fold1_keys max t" + +lemma fold_max_triv: + fixes k :: "_ :: linorder" + shows "(\x\set xs. x \ k) \ 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 \ []" + 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 \ 'a \ '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 \ rbt.Empty \ 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 "\color t1 a b t2. P t1 \ P t2 \ t2 = rbt.Empty \ P (Branch color t1 a b t2)" + assumes "\color t1 a b t2. P t1 \ P t2 \ t2 \ rbt.Empty \ 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 \ rbt.Empty" + shows "rbt_max_opt t \ 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 \ rbt.Empty" + shows "\y. y \ set (RBT_Impl.keys t) \ y \ 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 \ y \ set (RBT_Impl.keys t2) \ y \ 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 \ k" by (simp add: key_le_right rbt_max_opt_in_set) + moreover from goal3 have "y \ 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 \ RBT_Impl.Empty" + assumes "is_rbt t" + shows "rbt_max t = rbt_max_opt t" +proof - + interpret ab_semigroup_idem_mult "(max :: 'a \ 'a \ '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 \ 'a \ 'a) \ ('a::linorder, 'b) rbt \ '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 "\ (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 \ 'a" is rbt_min by simp + +lift_definition r_min_opt :: "('a :: linorder, unit) rbt \ '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 "\ (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 "\ (is_empty t)" + shows "fold_keys min t top = fold1_keys min t" +proof - + have *: "\t. RBT_Impl.keys t \ [] \ 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 \ 'a" is rbt_max by simp + +lift_definition r_max_opt :: "('a :: linorder, unit) rbt \ '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 "\ (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 "\ (is_empty t)" + shows "fold_keys max t bot = fold1_keys max t" +proof - + have *: "\t. RBT_Impl.keys t \ [] \ 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 \ (Set t) = (RBT.lookup t x = Some ())" + "x \ (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 \ 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 \ Set t = rbt_filter (\k. k \ 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 \ A = - rbt_filter (\k. k \ A) t" +proof - + have *: "\A B. (-A \ B) = -(-B \ A)" by blast + show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set) +qed + +lemma union_Set_Set [code]: + "Set t1 \ Set t2 = Set (union t1 t2)" +by (auto simp add: lookup_union map_add_Some_iff Set_def) + +lemma inter_Coset [code]: + "A \ Coset t = fold_keys Set.remove t A" +by (simp add: Diff_eq [symmetric] minus_Set) + +lemma inter_Coset_Coset [code]: + "Coset t1 \ 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 (\k. k \ 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 (\k A. Set.insert (f k) A) t {}" +proof - + have "comp_fun_commute (\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 \ foldi (\s. s = True) (\k v s. s \ P k) t True" +proof - + have "comp_fun_commute (\k s. s \ 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 \ foldi (\s. s = False) (\k v s. s \ P k) t False" +proof - + have "comp_fun_commute (\k s. s \ 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 \ B \ (\x\Set t. x \ B)" + "A \ Coset t \ (\y\Set t. y \ A)" +by auto + +definition non_empty_trees where [code del]: "non_empty_trees t1 t2 \ Coset t1 \ Set t2" + +code_abort non_empty_trees + +lemma subset_Coset_empty_Set_empty [code]: + "Coset t1 \ Set t2 \ (case (impl_of t1, impl_of t2) of + (rbt.Empty, rbt.Empty) => False | + (_, _) => non_empty_trees t1 t2)" +proof - + have *: "\t. impl_of t = rbt.Empty \ 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 \ Set t2 \ foldi (\s. s = True) (\k v s. s \ k \ Set t2) t1 True" +by (simp add: subset_code Ball_Set) + +lemma card_Set [code]: + "card (Set t) = fold_keys (\_ 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 (\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) \ x + | _ \ 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 \ {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 \ 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 (\x A. A \ 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 (\x A. fold_keys (\y. Set.insert (x, y)) t2 A) t1 {}" +proof - + have *:"\x. comp_fun_commute (\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 (\x. Set.insert (x, x)) t {}" +proof - + have "comp_fun_commute (\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 (\(x,y) A. if x \ 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 + (\(x,y) A. fold_keys (\(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 *: "\x y. comp_fun_commute (\(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 \ 'a \ '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 \ 'a \ 'a)" by default (simp add: fun_eq_iff ac_simps) + then have "t \ empty \ 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 \ '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 \ f) t top" +proof - + have "comp_fun_commute ((inf :: 'a \ 'a \ 'a) \ 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 \ 'a \ '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 \ 'a \ 'a)" by default (simp add: fun_eq_iff ac_simps) + then have "t \ empty \ 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 \ '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 \ f) t bot" +proof - + have "comp_fun_commute ((sup :: 'a \ 'a \ 'a) \ 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/List.thy --- 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 \ []" + 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 \ 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) diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- /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\_,/ _\)") + +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 \ H ==> X \ parts H" + | Fst: "{|X,Y|} \ parts H ==> X \ parts H" + | Snd: "{|X,Y|} \ parts H ==> Y \ parts H" + | Body: "Crypt K X \ parts H ==> X \ parts H" + +inductive_set + analz :: "msg set => msg set" + for H :: "msg set" + where + Inj [intro,simp] : "X \ H ==> X \ analz H" + | Fst: "{|X,Y|} \ analz H ==> X \ analz H" + | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" + | Decrypt [dest]: + "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" + +inductive_set + synth :: "msg set => msg set" + for H :: "msg set" + where + Inj [intro]: "X \ H ==> X \ synth H" + | Agent [intro]: "Agent agt \ synth H" + | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" + | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" + +primrec initState +where + initState_Alice: + "initState Alice = {Key (priEK Alice)} \ (Key ` pubEK ` agents)" +| initState_Bob: + "initState Bob = {Key (priEK Bob)} \ (Key ` pubEK ` agents)" +| initState_Spy: + "initState Spy = (Key ` priEK ` bad) \ (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' \ 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} \ used evs + | Gets A X => used evs + | Notes A X => parts {X} \ 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 ((%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 ((%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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy --- /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: "[] \ ns_public" + + | Fake_NS1: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1) \ + \ Says Spy B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + | Fake_NS2: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1); Nonce NB \ analz (spies evs1) \ + \ Says Spy A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs1 \ ns_public" + + (*Alice initiates a protocol run, sending a nonce to Bob*) + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 + "\ns_publicp evs\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs + \ A \ Spy \ B \ Spy \ A \ B + \ Nonce NB \ 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 \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" +proof - + from assms show "A \ Spy" by auto + from assms show "B \ 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|}) \ 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|}) \ 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy --- /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: "[] \ ns_public" + (*Alice initiates a protocol run, sending a nonce to Bob*) + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 + "\ns_publicp evs\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs + \ A \ Spy \ B \ Spy \ A \ B + \ Nonce NB \ analz (spies evs)" +quickcheck[smart_exhaustive, depth = 6, timeout = 30] +quickcheck[narrowing, size = 6, timeout = 30, verbose] +oops + +end diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy --- /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: "[] \ ns_public" + + | Fake: "\evs1 \ ns_public; X \ synth (analz (spies evs1)) \ + \ Says Spy A X # evs1 \ ns_public" + + (*Alice initiates a protocol run, sending a nonce to Bob*) + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 + "\ns_publicp evs\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs + \ A \ Spy \ B \ Spy \ A \ B + \ Nonce NB \ 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 \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" +proof - + from assms show "A \ Spy" by auto + from assms show "B \ 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|}) \ 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|}) \ 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Benchmark/ROOT.ML --- 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" +] diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Examples/Needham_Schroeder_Base.thy --- 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\_,/ _\)") - -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 \ H ==> X \ parts H" - | Fst: "{|X,Y|} \ parts H ==> X \ parts H" - | Snd: "{|X,Y|} \ parts H ==> Y \ parts H" - | Body: "Crypt K X \ parts H ==> X \ parts H" - -inductive_set - analz :: "msg set => msg set" - for H :: "msg set" - where - Inj [intro,simp] : "X \ H ==> X \ analz H" - | Fst: "{|X,Y|} \ analz H ==> X \ analz H" - | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" - | Decrypt [dest]: - "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" - -inductive_set - synth :: "msg set => msg set" - for H :: "msg set" - where - Inj [intro]: "X \ H ==> X \ synth H" - | Agent [intro]: "Agent agt \ synth H" - | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" - | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" - -primrec initState -where - initState_Alice: - "initState Alice = {Key (priEK Alice)} \ (Key ` pubEK ` agents)" -| initState_Bob: - "initState Bob = {Key (priEK Bob)} \ (Key ` pubEK ` agents)" -| initState_Spy: - "initState Spy = (Key ` priEK ` bad) \ (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' \ 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} \ used evs - | Gets A X => used evs - | Notes A X => parts {X} \ 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 ((%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 ((%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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy --- 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: "[] \ ns_public" - - | Fake_NS1: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1) \ - \ Says Spy B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - | Fake_NS2: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1); Nonce NB \ analz (spies evs1) \ - \ Says Spy A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs1 \ ns_public" - - (*Alice initiates a protocol run, sending a nonce to Bob*) - | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ - \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) - | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; - Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) - | NS3: "\evs3 \ ns_public; - Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ - \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 - "\ns_publicp evs\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs - \ A \ Spy \ B \ Spy \ A \ B - \ Nonce NB \ 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 \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" -proof - - from assms show "A \ Spy" by auto - from assms show "B \ 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|}) \ 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|}) \ 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy --- 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: "[] \ ns_public" - (*Alice initiates a protocol run, sending a nonce to Bob*) - | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ - \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) - | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; - Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) - | NS3: "\evs3 \ ns_public; - Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ - \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 - "\ns_publicp evs\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs - \ A \ Spy \ B \ Spy \ A \ B - \ Nonce NB \ 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker_Example.thy --- 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: "[] \ ns_public" - - | Fake: "\evs1 \ ns_public; X \ synth (analz (spies evs1)) \ - \ Says Spy A X # evs1 \ ns_public" - - (*Alice initiates a protocol run, sending a nonce to Bob*) - | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ - \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) - | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; - Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) - | NS3: "\evs3 \ ns_public; - Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ - \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 - "\ns_publicp evs\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs - \ A \ Spy \ B \ Spy \ A \ B - \ Nonce NB \ 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 \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" -proof - - from assms show "A \ Spy" by auto - from assms show "B \ 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|}) \ 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|}) \ 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quickcheck_Examples/ROOT.ML --- 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 () diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quotient_Examples/Lift_RBT.thy --- 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\linorder, 'b) RBT_Impl.rbt. is_rbt t}" - morphisms impl_of RBT -proof - - have "RBT_Impl.Empty \ ?rbt" by simp - then show ?thesis .. -qed - -lemma rbt_eq_iff: - "t1 = t2 \ impl_of t1 = impl_of t2" - by (simp add: impl_of_inject) - -lemma rbt_eqI: - "impl_of t1 = impl_of t2 \ 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\linorder, 'b) rbt \ 'a \ 'b" is "rbt_lookup" -by simp - -lift_definition empty :: "('a\linorder, 'b) rbt" is RBT_Impl.Empty -by (simp add: empty_def) - -lift_definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" is "rbt_insert" -by simp - -lift_definition delete :: "'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" is "rbt_delete" -by simp - -lift_definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" is RBT_Impl.entries -by simp - -lift_definition keys :: "('a\linorder, 'b) rbt \ 'a list" is RBT_Impl.keys -by simp - -lift_definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" is "rbt_bulkload" -by simp - -lift_definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is rbt_map_entry -by simp - -lift_definition map :: "('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is RBT_Impl.map -by simp - -lift_definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ '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\linorder, 'b) rbt \ bool" where - [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \ True | _ \ False)" - - -subsection {* Abstract lookup properties *} - -lemma lookup_RBT: - "is_rbt t \ 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 \ 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 \ 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 \ t = empty" - unfolding is_empty_def by transfer (simp split: rbt.split) - -lemma RBT_lookup_empty [simp]: (*FIXME*) - "rbt_lookup t = Map.empty \ t = RBT_Impl.Empty" - by (cases t) (auto simp add: fun_eq_iff) - -lemma lookup_empty_empty [simp]: - "lookup t = Map.empty \ 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Quotient_Examples/ROOT.ML --- 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"]; diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/ROOT --- 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 diff -r ef374008cb7c -r 3ef76d545aaf src/HOL/Relation.thy --- 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 (\x. Set.insert (Pair x x)) {} A" +proof - + interpret comp_fun_commute "\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 (\(x,y) A. if x \ 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 (\(x,y) A. if x \ S then Set.insert y A else A) {} R" +proof - + interpret comp_fun_commute "(\(x,y) A. if x \ S then Set.insert y A else A)" + by (rule comp_fun_commute_Image_fold) + have *: "\x F. Set.insert x F `` S = (if fst x \ 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 \ X = Finite_Set.fold (\(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S" +proof - + interpret comp_fun_commute "\(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 (\(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 \ (snd x,z) \ 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 (\(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) \ (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 (\(x,y) A. + Finite_Set.fold (\(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)" +proof - + have *: "\a b A. + Finite_Set.fold (\(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \ 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 + (\(x,y) A. Finite_Set.fold (\(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