diff --git a/thys/Affine_Arithmetic/Executable_Euclidean_Space.thy b/thys/Affine_Arithmetic/Executable_Euclidean_Space.thy --- a/thys/Affine_Arithmetic/Executable_Euclidean_Space.thy +++ b/thys/Affine_Arithmetic/Executable_Euclidean_Space.thy @@ -1,1077 +1,1078 @@ section \Euclidean Space: Executability\ theory Executable_Euclidean_Space imports "HOL-Analysis.Multivariate_Analysis" "List-Index.List_Index" "HOL-Library.Float" + "HOL-Library.Code_Cardinality" Affine_Arithmetic_Auxiliarities begin subsection \Ordered representation of Basis and Rounding of Components\ class executable_euclidean_space = ordered_euclidean_space + fixes Basis_list eucl_down eucl_truncate_down eucl_truncate_up assumes eucl_down_def: "eucl_down p b = (\i \ Basis. round_down p (b \ i) *\<^sub>R i)" assumes eucl_truncate_down_def: "eucl_truncate_down q b = (\i \ Basis. truncate_down q (b \ i) *\<^sub>R i)" assumes eucl_truncate_up_def: "eucl_truncate_up q b = (\i \ Basis. truncate_up q (b \ i) *\<^sub>R i)" assumes Basis_list[simp]: "set Basis_list = Basis" assumes distinct_Basis_list[simp]: "distinct Basis_list" begin lemma length_Basis_list: "length Basis_list = card Basis" by (metis Basis_list distinct_Basis_list distinct_card) end lemma eucl_truncate_down_zero[simp]: "eucl_truncate_down p 0 = 0" by (auto simp: eucl_truncate_down_def truncate_down_zero) lemma eucl_truncate_up_zero[simp]: "eucl_truncate_up p 0 = 0" by (auto simp: eucl_truncate_up_def) subsection \Instantiations\ instantiation real::executable_euclidean_space begin definition Basis_list_real :: "real list" where "Basis_list_real = [1]" definition "eucl_down prec b = round_down prec b" definition "eucl_truncate_down prec b = truncate_down prec b" definition "eucl_truncate_up prec b = truncate_up prec b" instance proof qed (auto simp: Basis_list_real_def eucl_down_real_def eucl_truncate_down_real_def eucl_truncate_up_real_def) end instantiation prod::(executable_euclidean_space, executable_euclidean_space) executable_euclidean_space begin definition Basis_list_prod :: "('a \ 'b) list" where "Basis_list_prod = zip Basis_list (replicate (length (Basis_list::'a list)) 0) @ zip (replicate (length (Basis_list::'b list)) 0) Basis_list" definition "eucl_down p a = (eucl_down p (fst a), eucl_down p (snd a))" definition "eucl_truncate_down p a = (eucl_truncate_down p (fst a), eucl_truncate_down p (snd a))" definition "eucl_truncate_up p a = (eucl_truncate_up p (fst a), eucl_truncate_up p (snd a))" instance proof show "set Basis_list = (Basis::('a*'b) set)" by (auto simp: Basis_list_prod_def Basis_prod_def elim!: in_set_zipE) (auto simp: Basis_list[symmetric] in_set_zip in_set_conv_nth simp del: Basis_list) show "distinct (Basis_list::('a*'b)list)" using distinct_Basis_list[where 'a='a] distinct_Basis_list[where 'a='b] by (auto simp: Basis_list_prod_def Basis_list intro: distinct_zipI1 distinct_zipI2 elim!: in_set_zipE) qed (auto simp: eucl_down_prod_def eucl_truncate_down_prod_def eucl_truncate_up_prod_def sum_Basis_prod_eq inner_add_left inner_sum_left inner_Basis eucl_down_def eucl_truncate_down_def eucl_truncate_up_def intro!: euclidean_eqI[where 'a="'a*'b"]) end lemma eucl_truncate_down_Basis[simp]: "i \ Basis \ eucl_truncate_down e x \ i = truncate_down e (x \ i)" by (simp add: eucl_truncate_down_def) lemma eucl_truncate_down_correct: "dist (x::'a::executable_euclidean_space) (eucl_down e x) \ {0..sqrt (DIM('a)) * 2 powr of_int (- e)}" proof - have "dist x (eucl_down e x) = sqrt (\i\Basis. (dist (x \ i) (eucl_down e x \ i))\<^sup>2)" unfolding euclidean_dist_l2[where 'a='a] L2_set_def .. also have "\ \ sqrt (\i\(Basis::'a set). ((2 powr of_int (- e))\<^sup>2))" by (intro real_sqrt_le_mono sum_mono power_mono) (auto simp: dist_real_def eucl_down_def abs_round_down_le) finally show ?thesis by (simp add: real_sqrt_mult) qed lemma eucl_down: "eucl_down e (x::'a::executable_euclidean_space) \ x" by (auto simp add: eucl_le[where 'a='a] round_down eucl_down_def) lemma eucl_truncate_down: "eucl_truncate_down e (x::'a::executable_euclidean_space) \ x" by (auto simp add: eucl_le[where 'a='a] truncate_down) lemma eucl_truncate_down_le: "x \ y \ eucl_truncate_down w x \ (y::'a::executable_euclidean_space)" using eucl_truncate_down by (rule order.trans) lemma eucl_truncate_up_Basis[simp]: "i \ Basis \ eucl_truncate_up e x \ i = truncate_up e (x \ i)" by (simp add: eucl_truncate_up_def truncate_up_def) lemma eucl_truncate_up: "x \ eucl_truncate_up e (x::'a::executable_euclidean_space)" by (auto simp add: eucl_le[where 'a='a] round_up truncate_up_def) lemma eucl_truncate_up_le: "x \ y \ x \ eucl_truncate_up e (y::'a::executable_euclidean_space)" using _ eucl_truncate_up by (rule order.trans) lemma eucl_truncate_down_mono: fixes x::"'a::executable_euclidean_space" shows "x \ y \ eucl_truncate_down p x \ eucl_truncate_down p y" by (auto simp: eucl_le[where 'a='a] intro!: truncate_down_mono) lemma eucl_truncate_up_mono: fixes x::"'a::executable_euclidean_space" shows "x \ y \ eucl_truncate_up p x \ eucl_truncate_up p y" by (auto simp: eucl_le[where 'a='a] intro!: truncate_up_mono) lemma infnorm[code]: fixes x::"'a::executable_euclidean_space" shows "infnorm x = fold max (map (\i. abs (x \ i)) Basis_list) 0" by (auto simp: Max.set_eq_fold[symmetric] infnorm_Max[symmetric] infnorm_pos_le intro!: max.absorb2[symmetric]) declare Inf_real_def[code del] declare Sup_real_def[code del] declare Inf_prod_def[code del] declare Sup_prod_def[code del] declare [[code abort: "Inf::real set \ real"]] declare [[code abort: "Sup::real set \ real"]] declare [[code abort: "Inf::('a::Inf * 'b::Inf) set \ 'a * 'b"]] declare [[code abort: "Sup::('a::Sup * 'b::Sup) set \ 'a * 'b"]] lemma nth_Basis_list_in_Basis[simp]: "n < length (Basis_list::'a::executable_euclidean_space list) \ Basis_list ! n \ (Basis::'a set)" by (metis Basis_list nth_mem) subsection \Representation as list\ lemma nth_eq_iff_index: "distinct xs \ n < length xs \ xs ! n = i \ n = index xs i" using index_nth_id by fastforce lemma in_Basis_index_Basis_list: "i \ Basis \ i = Basis_list ! index Basis_list i" by simp lemmas [simp] = length_Basis_list lemma sum_Basis_sum_nth_Basis_list: "(\i\Basis. f i) = (\i(x, i)\zip xs Basis_list. x *\<^sub>R i)" lemma eucl_of_list_nth: assumes "length xs = DIM('a)" shows "eucl_of_list xs = (\iR ((Basis_list::'a list) ! i))" by (auto simp: eucl_of_list_def sum_list_sum_nth length_Basis_list assms atLeast0LessThan) lemma eucl_of_list_inner: fixes i::"'a::executable_euclidean_space" assumes i: "i \ Basis" assumes l: "length xs = DIM('a)" shows "eucl_of_list xs \ i = xs ! (index Basis_list i)" by (simp add: eucl_of_list_nth[OF l] inner_sum_left assms inner_Basis nth_eq_iff_index sum.delta if_distrib cong: if_cong) lemma inner_eucl_of_list: fixes i::"'a::executable_euclidean_space" assumes i: "i \ Basis" assumes l: "length xs = DIM('a)" shows "i \ eucl_of_list xs = xs ! (index Basis_list i)" using eucl_of_list_inner[OF assms] by (auto simp: inner_commute) definition "list_of_eucl x = map ((\) x) Basis_list" lemma index_Basis_list_nth[simp]: "i < DIM('a::executable_euclidean_space) \ index Basis_list ((Basis_list::'a list) ! i) = i" by (simp add: index_nth_id) lemma list_of_eucl_eucl_of_list[simp]: "length xs = DIM('a::executable_euclidean_space) \ list_of_eucl (eucl_of_list xs::'a) = xs" by (auto simp: list_of_eucl_def eucl_of_list_inner intro!: nth_equalityI) lemma eucl_of_list_list_of_eucl[simp]: "eucl_of_list (list_of_eucl x) = x" by (auto simp: list_of_eucl_def eucl_of_list_inner intro!: euclidean_eqI[where 'a='a]) lemma length_list_of_eucl[simp]: "length (list_of_eucl (x::'a::executable_euclidean_space)) = DIM('a)" by (auto simp: list_of_eucl_def) lemma list_of_eucl_nth[simp]: "n < DIM('a::executable_euclidean_space) \ list_of_eucl x ! n = x \ (Basis_list ! n::'a)" by (auto simp: list_of_eucl_def) lemma nth_ge_len: "n \ length xs \ xs ! n = [] ! (n - length xs)" by (induction xs arbitrary: n) auto lemma list_of_eucl_nth_if: "list_of_eucl x ! n = (if n < DIM('a::executable_euclidean_space) then x \ (Basis_list ! n::'a) else [] ! (n - DIM('a)))" apply (auto simp: list_of_eucl_def ) apply (subst nth_ge_len) apply auto done lemma list_of_eucl_eq_iff: "list_of_eucl (x::'a::executable_euclidean_space) = list_of_eucl (y::'b::executable_euclidean_space) \ (DIM('a) = DIM('b) \ (\i < DIM('b). x \ Basis_list ! i = y \ Basis_list ! i))" by (auto simp: list_eq_iff_nth_eq) lemma eucl_le_Basis_list_iff: "(x::'a::executable_euclidean_space) \ y \ (\i Basis_list ! i \ y \ Basis_list ! i)" apply (auto simp: eucl_le[where 'a='a]) subgoal for i subgoal by (auto dest!: spec[where x="index Basis_list i"]) done done lemma eucl_of_list_inj: "length xs = DIM('a::executable_euclidean_space) \ length ys = DIM('a) \ (eucl_of_list xs::'a) = eucl_of_list (ys) \ xs = ys" apply (auto intro!: nth_equalityI simp: euclidean_eq_iff[where 'a="'a"] eucl_of_list_inner) using nth_Basis_list_in_Basis[where 'a="'a"] by fastforce lemma eucl_of_list_map_plus[simp]: assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" shows "(eucl_of_list (map (\x. f x + g x) xs)::'a) = eucl_of_list (map f xs) + eucl_of_list (map g xs)" by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner) lemma eucl_of_list_map_uminus[simp]: assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" shows "(eucl_of_list (map (\x. - f x) xs)::'a) = - eucl_of_list (map f xs)" by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner) lemma eucl_of_list_map_mult_left[simp]: assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" shows "(eucl_of_list (map (\x. r * f x) xs)::'a) = r *\<^sub>R eucl_of_list (map f xs)" by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner) lemma eucl_of_list_map_mult_right[simp]: assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" shows "(eucl_of_list (map (\x. f x * r) xs)::'a) = r *\<^sub>R eucl_of_list (map f xs)" by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner) lemma eucl_of_list_map_divide_right[simp]: assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" shows "(eucl_of_list (map (\x. f x / r) xs)::'a) = eucl_of_list (map f xs) /\<^sub>R r" by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner divide_simps) lemma eucl_of_list_map_const[simp]: assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" shows "(eucl_of_list (map (\x. c) xs)::'a) = c *\<^sub>R One" by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner) lemma replicate_eq_list_of_eucl_zero: "replicate DIM('a::executable_euclidean_space) 0 = list_of_eucl (0::'a)" by (auto intro!: nth_equalityI) lemma eucl_of_list_append_zeroes[simp]: "eucl_of_list (xs @ replicate n 0) = eucl_of_list xs" unfolding eucl_of_list_def apply (auto simp: sum_list_sum_nth) apply (rule sum.mono_neutral_cong_right) by (auto simp: nth_append) lemma Basis_prodD: assumes "(i, j) \ Basis" shows "i \ Basis \ j = 0 \ i = 0 \ j \ Basis" using assms by (auto simp: Basis_prod_def) lemma eucl_of_list_take_DIM[simp]: assumes "d = DIM('b::executable_euclidean_space)" shows "(eucl_of_list (take d xs)::'b) = (eucl_of_list xs)" by (auto simp: eucl_of_list_inner eucl_of_list_def fst_sum_list sum_list_sum_nth assms dest!: Basis_prodD) lemma eucl_of_list_eqI: assumes "take DIM('a) (xs @ replicate (DIM('a) - length xs) 0) = take DIM('a) (ys @ replicate (DIM('a) - length ys) 0)" shows "eucl_of_list xs = (eucl_of_list ys::'a::executable_euclidean_space)" proof - have "(eucl_of_list xs::'a) = eucl_of_list (take DIM('a) (xs @ replicate (DIM('a) - length xs) 0))" by (simp add: ) also note assms also have "eucl_of_list (take DIM('a) (ys @ replicate (DIM('a) - length ys) 0)) = (eucl_of_list ys::'a)" by simp finally show ?thesis . qed lemma eucl_of_list_replicate_zero[simp]: "eucl_of_list (replicate E 0) = 0" proof - have "eucl_of_list (replicate E 0) = (eucl_of_list (replicate E 0 @ replicate (DIM('a) - E) 0)::'a)" by simp also have "\ = eucl_of_list (replicate DIM('a) 0)" apply (rule eucl_of_list_eqI) by (auto simp: min_def nth_append intro!: nth_equalityI) also have "\ = 0" by (simp add: replicate_eq_list_of_eucl_zero) finally show ?thesis by simp qed lemma eucl_of_list_Nil[simp]: "eucl_of_list [] = 0" using eucl_of_list_replicate_zero[of 0] by simp lemma fst_eucl_of_list_prod: shows "fst (eucl_of_list xs::'b::executable_euclidean_space \ _) = (eucl_of_list (take DIM('b) xs)::'b)" apply (auto simp: eucl_of_list_inner eucl_of_list_def fst_sum_list dest!: Basis_prodD) apply (simp add: sum_list_sum_nth) apply (rule sum.mono_neutral_cong_right) subgoal by simp subgoal by auto subgoal by (auto simp: Basis_list_prod_def nth_append) subgoal by (auto simp: Basis_list_prod_def nth_append) done lemma index_zip_replicate1[simp]: "index (zip (replicate d a) bs) (a, b) = index bs b" if "d = length bs" using that by (induction bs arbitrary: d) auto lemma index_zip_replicate2[simp]: "index (zip as (replicate d b)) (a, b) = index as a" if "d = length as" using that by (induction as arbitrary: d) auto lemma index_Basis_list_prod[simp]: fixes a::"'a::executable_euclidean_space" and b::"'b::executable_euclidean_space" shows "a \ Basis \ index Basis_list (a, 0::'b) = index Basis_list a" "b \ Basis \ index Basis_list (0::'a, b) = DIM('a) + index Basis_list b" by (auto simp: Basis_list_prod_def index_append in_set_zip zip_replicate index_map_inj dest: spec[where x="index Basis_list a"]) lemma eucl_of_list_eq_takeI: assumes "(eucl_of_list (take DIM('a::executable_euclidean_space) xs)::'a) = x" shows "eucl_of_list xs = x" using eucl_of_list_take_DIM[OF refl, of xs, where 'b='a] assms by auto lemma eucl_of_list_inner_le: fixes i::"'a::executable_euclidean_space" assumes i: "i \ Basis" assumes l: "length xs \ DIM('a)" shows "eucl_of_list xs \ i = xs ! (index Basis_list i)" proof - have "(eucl_of_list xs::'a) = eucl_of_list (take DIM('a) (xs @ (replicate (DIM('a) - length xs) 0)))" by (rule eucl_of_list_eq_takeI) simp also have "\ \ i = xs ! (index Basis_list i)" using assms by (subst eucl_of_list_inner) auto finally show ?thesis . qed lemma eucl_of_list_prod_if: assumes "length xs = DIM('a::executable_euclidean_space) + DIM('b::executable_euclidean_space)" shows "eucl_of_list xs = (eucl_of_list (take DIM('a) xs)::'a, eucl_of_list (drop DIM('a) xs)::'b)" apply (rule euclidean_eqI) using assms apply (auto simp: eucl_of_list_inner dest!: Basis_prodD) apply (subst eucl_of_list_inner_le) apply (auto simp: Basis_list_prod_def index_append in_set_zip) done lemma snd_eucl_of_list_prod: shows "snd (eucl_of_list xs::'b::executable_euclidean_space \ 'c::executable_euclidean_space) = (eucl_of_list (drop DIM('b) xs)::'c)" proof (cases "length xs \ DIM('b)") case True then show ?thesis by (auto simp: eucl_of_list_inner eucl_of_list_def snd_sum_list dest!: Basis_prodD) (simp add: sum_list_sum_nth Basis_list_prod_def nth_append) next case False have "xs = take DIM('b) xs @ drop DIM('b) xs" by simp also have "eucl_of_list \ = (eucl_of_list (\ @ replicate (length xs - DIM('c)) 0)::'b \ 'c)" by simp finally have "eucl_of_list xs = (eucl_of_list (xs @ replicate (DIM('b) + DIM('c) - length xs) 0)::'b \ 'c)" by simp also have "\ = eucl_of_list (take (DIM ('b \ 'c)) (xs @ replicate (DIM('b) + DIM('c) - length xs) 0))" by (simp add: ) finally have *: "(eucl_of_list xs::'b\'c) = eucl_of_list (take DIM('b \ 'c) (xs @ replicate (DIM('b) + DIM('c) - length xs) 0))" by simp show ?thesis apply (subst *) apply (subst eucl_of_list_prod_if) subgoal by simp subgoal apply simp apply (subst (2) eucl_of_list_take_DIM[OF refl, symmetric]) apply (subst (2) eucl_of_list_take_DIM[OF refl, symmetric]) apply (rule arg_cong[where f=eucl_of_list]) by (auto intro!: nth_equalityI simp: nth_append min_def split: if_splits) done qed lemma eucl_of_list_prod: shows "eucl_of_list xs = (eucl_of_list (take DIM('b) xs)::'b::executable_euclidean_space, eucl_of_list (drop DIM('b) xs)::'c::executable_euclidean_space)" using snd_eucl_of_list_prod[of xs, where 'b='b and 'c='c] using fst_eucl_of_list_prod[of xs, where 'b='b and 'a='c] by (auto simp del: snd_eucl_of_list_prod fst_eucl_of_list_prod simp add: prod_eq_iff) lemma eucl_of_list_real[simp]: "eucl_of_list [x] = (x::real)" by (auto simp: eucl_of_list_def Basis_list_real_def) lemma eucl_of_list_append[simp]: assumes "length xs = DIM('i::executable_euclidean_space)" assumes "length ys = DIM('j::executable_euclidean_space)" shows "eucl_of_list (xs @ ys) = (eucl_of_list xs::'i, eucl_of_list ys::'j)" using assms by (auto simp: eucl_of_list_prod) lemma list_allI: "(\x. x \ set xs \ P x) \ list_all P xs" by (auto simp: list_all_iff) lemma concat_map_nthI: assumes "\x y. x \ set xs \ y \ set (f x) \ P y" assumes "j < length (concat (map f xs))" shows "P (concat (map f xs) ! j)" proof - have "list_all P (concat (map f xs))" by (rule list_allI) (auto simp: assms) then show ?thesis by (auto simp: list_all_length assms) qed lemma map_nth_append1: assumes "length xs = d" shows "map ((!) (xs @ ys)) [0.. y = z" by (metis eucl_of_list_list_of_eucl) lemma length_Basis_list_pos[simp]: "length Basis_list > 0" by (metis length_pos_if_in_set Basis_list SOME_Basis) lemma Basis_list_nth_nonzero: "i < length (Basis_list::'a::executable_euclidean_space list) \ (Basis_list::'a list) ! i \ 0" by (auto dest!: nth_mem simp: nonzero_Basis) lemma nth_Basis_list_prod: "i < DIM('a) + DIM('b) \ (Basis_list::('a::executable_euclidean_space \ 'b::executable_euclidean_space) list) ! i = (if i < DIM('a) then (Basis_list ! i, 0) else (0, Basis_list ! (i - DIM('a))))" by (auto simp: Basis_list_nth_nonzero prod_eq_iff Basis_list_prod_def nth_append not_less) lemma eucl_of_list_if: assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" "distinct xs" shows "eucl_of_list (map (\xa. if xa = x then 1 else 0) (xs::nat list)) = (if x \ set xs then Basis_list ! index xs x else 0::'a)" by (rule euclidean_eqI) (auto simp: eucl_of_list_inner inner_Basis index_nth_id) lemma take_append_take_minus_idem: "take n XS @ map ((!) XS) [n..b\Basis. f b)" by (subst sum_list_distinct_conv_sum_set) (auto simp: Basis_list distinct_Basis_list) lemma hd_Basis_list[simp]: "hd Basis_list \ Basis" unfolding Basis_list[symmetric] by (rule hd_in_set) (auto simp: set_empty[symmetric]) definition "inner_lv_rel a b = sum_list (map2 (*) a b)" lemma eucl_of_list_inner_eq: "(eucl_of_list xs::'a) \ eucl_of_list ys = inner_lv_rel xs ys" if "length xs = DIM('a::executable_euclidean_space)" "length ys = DIM('a)" using that by (subst euclidean_inner[abs_def], subst sum_list_Basis_list[symmetric]) (auto simp: eucl_of_list_inner sum_list_sum_nth index_nth_id inner_lv_rel_def) lemma euclidean_vec_componentwise: "(\(xa::'a::euclidean_space^'b::finite)\Basis. f xa) = (\a\Basis. (\b::'b\UNIV. f (axis b a)))" apply (auto simp: Basis_vec_def) apply (subst sum.swap) apply (subst sum.Union_disjoint) apply auto apply (simp add: axis_eq_axis nonzero_Basis) apply (simp add: axis_eq_axis nonzero_Basis) apply (subst sum.reindex) apply (auto intro!: injI) subgoal apply (auto simp: set_eq_iff) by (metis (full_types) all_not_in_conv inner_axis_axis inner_eq_zero_iff nonempty_Basis nonzero_Basis) apply (rule sum.cong[OF refl]) apply (auto ) apply (rule sum.reindex_cong[OF _ _ refl]) apply (auto intro!: inj_onI) using axis_eq_axis by blast lemma vec_nth_inner_scaleR_craziness: "f (x $ i \ j) *\<^sub>R j = (\xa\UNIV. f (x $ xa \ j) *\<^sub>R axis xa j) $ i" by vector (auto simp: axis_def if_distrib scaleR_vec_def sum.delta' cong: if_cong) instantiation vec :: ("{executable_euclidean_space}", enum) executable_euclidean_space begin definition Basis_list_vec :: "('a, 'b) vec list" where "Basis_list_vec = concat (map (\n. map (axis n) Basis_list) enum_class.enum)" definition eucl_down_vec :: "int \ ('a, 'b) vec \ ('a, 'b) vec" where "eucl_down_vec p x = (\ i. eucl_down p (x $ i))" definition eucl_truncate_down_vec :: "nat \ ('a, 'b) vec \ ('a, 'b) vec" where "eucl_truncate_down_vec p x = (\ i. eucl_truncate_down p (x $ i))" definition eucl_truncate_up_vec :: "nat \ ('a, 'b) vec \ ('a, 'b) vec" where "eucl_truncate_up_vec p x = (\ i. eucl_truncate_up p (x $ i))" instance proof show *: "set (Basis_list::('a, 'b) vec list) = Basis" unfolding Basis_list_vec_def Basis_vec_def apply (auto simp: Basis_list_vec_def vec_eq_iff distinct_map Basis_vec_def intro!: distinct_concat inj_onI split: if_splits) apply (auto simp: Basis_list_vec_def vec_eq_iff distinct_map enum_distinct UNIV_enum[symmetric] intro!: distinct_concat inj_onI split: if_splits) done have "length (Basis_list::('a, 'b) vec list) = CARD('b) * DIM('a)" by (auto simp: Basis_list_vec_def length_concat o_def enum_distinct sum_list_distinct_conv_sum_set UNIV_enum[symmetric]) then show "distinct (Basis_list::('a, 'b) vec list)" using * by (auto intro!: card_distinct) qed (simp_all only: vector_cart[symmetric] vec_eq_iff eucl_down_vec_def eucl_down_def eucl_truncate_down_vec_def eucl_truncate_down_def eucl_truncate_up_vec_def eucl_truncate_up_def, auto simp: euclidean_vec_componentwise inner_axis Basis_list_vec_def vec_nth_inner_scaleR_craziness intro!: sum.cong[OF refl]) end lemma concat_same_lengths_nth: assumes "\xs. xs \ set XS \ length xs = N" assumes "i < length XS * N" "N > 0" shows "concat XS ! i = XS ! (i div N) ! (i mod N)" using assms apply (induction XS arbitrary: i) apply (auto simp: nth_append nth_Cons split: nat.splits) apply (simp add: div_eq_0_iff) by (metis Suc_inject div_geq mod_geq) lemma concat_map_map_index: shows "concat (map (\n. map (f n) xs) ys) = map (\i. f (ys ! (i div length xs)) (xs ! (i mod length xs))) [0..(x, y)\zip xs (map g xs). f x y) = (\x\set xs. f x (g x))" by (force simp add: sum_list_distinct_conv_sum_set assms distinct_zipI1 split_beta' in_set_zip in_set_conv_nth inj_on_convol_ident intro!: sum.reindex_cong[where l="\x. (x, g x)"]) lemma sum_list_zip_map_of: assumes "distinct bs" assumes "length xs = length bs" shows "(\(x, y)\zip xs bs. f x y) = (\x\set bs. f (the (map_of (zip bs xs) x)) x)" proof - have "(\(x, y)\zip xs bs. f x y) = (\(y, x)\zip bs xs. f x y)" by (subst zip_commute) (auto simp: o_def split_beta') also have "\ = (\(x, y)\zip bs (map (the o map_of (zip bs xs)) bs). f y x)" proof (rule arg_cong, rule map_cong) have "xs = (map (the \ map_of (zip bs xs)) bs)" using assms by (auto intro!: nth_equalityI simp: map_nth map_of_zip_nth) then show "zip bs xs = zip bs (map (the \ map_of (zip bs xs)) bs)" by simp qed auto also have "\ = (\x\set bs. f (the (map_of (zip bs xs) x)) x)" using assms(1) by (subst sum_list_zip_map) (auto simp: o_def) finally show ?thesis . qed lemma vec_nth_matrix: "vec_nth (vec_nth (matrix y) i) j = vec_nth (y (axis j 1)) i" unfolding matrix_def by simp lemma matrix_eqI: assumes "\x. x \ Basis \ A *v x = B *v x" shows "(A::real^'n^'n) = B" apply vector using assms apply (auto simp: Basis_vec_def) by (metis cart_eq_inner_axis matrix_vector_mul_component) lemma matrix_columnI: assumes "\i. column i A = column i B" shows "(A::real^'n^'n) = B" using assms apply vector apply (auto simp: column_def) apply vector by (metis iso_tuple_UNIV_I vec_lambda_inject) lemma vec_nth_Basis: fixes x::"real^'n" shows "x \ Basis \ vec_nth x i = (if x = axis i 1 then 1 else 0)" apply (auto simp: Basis_vec_def) by (metis cart_eq_inner_axis inner_axis_axis) lemma vec_nth_eucl_of_list_eq: "length M = CARD('n) \ vec_nth (eucl_of_list M::real^'n::enum) i = M ! index Basis_list (axis i (1::real))" apply (auto simp: eucl_of_list_def) apply (subst sum_list_zip_map_of) apply (auto intro!: distinct_zipI2 simp: split_beta') apply (subst sum.cong[OF refl]) apply (subst vec_nth_Basis) apply (force simp: set_zip) apply (rule refl) apply (auto simp: if_distrib sum.delta cong: if_cong) subgoal apply (cases "map_of (zip Basis_list M) (axis i 1::real^'n::enum)") subgoal premises prems proof - have "fst ` set (zip Basis_list M) = (Basis::(real^'n::enum) set)" using prems by (auto simp: in_set_zip) then show ?thesis using prems by (subst (asm) map_of_eq_None_iff) simp qed subgoal for a apply (auto simp: in_set_zip) subgoal premises prems for n by (metis DIM_cart DIM_real index_Basis_list_nth mult.right_neutral prems(2) prems(3)) done done done lemma index_Basis_list_axis1: "index Basis_list (axis i (1::real)) = index enum_class.enum i" apply (auto simp: Basis_list_vec_def Basis_list_real_def ) apply (subst index_map_inj) by (auto intro!: injI simp: axis_eq_axis) lemma vec_nth_eq_list_of_eucl1: "(vec_nth (M::real^'n::enum) i) = list_of_eucl M ! (index enum_class.enum i)" apply (subst eucl_of_list_list_of_eucl[of M, symmetric]) apply (subst vec_nth_eucl_of_list_eq) unfolding index_Basis_list_axis1 by auto lemma enum_3[simp]: "(enum_class.enum::3 list) = [0, 1, 2]" by code_simp+ lemma three_eq_zero: "(3::3) = 0" by simp lemma forall_3': "(\i::3. P i) \ P 0 \ P 1 \ P 2" using forall_3 three_eq_zero by auto lemma euclidean_eq_list_of_euclI: "x = y" if "list_of_eucl x = list_of_eucl y" using that by (metis eucl_of_list_list_of_eucl) lemma axis_one_neq_zero[simp]: "axis xa (1::'a::zero_neq_one) \ 0" by (auto simp: axis_def vec_eq_iff) lemma eucl_of_list_vec_nth3[simp]: "(eucl_of_list [g, h, i]::real^3) $ 0 = g" "(eucl_of_list [g, h, i]::real^3) $ 1 = h" "(eucl_of_list [g, h, i]::real^3) $ 2 = i" "(eucl_of_list [g, h, i]::real^3) $ 3 = g" by (auto simp: cart_eq_inner_axis eucl_of_list_inner vec_nth_eq_list_of_eucl1 index_Basis_list_axis1) type_synonym R3 = "real*real*real" lemma Basis_list_R3: "Basis_list = [(1,0,0), (0, 1, 0), (0, 0, 1)::R3]" by (auto simp: Basis_list_prod_def Basis_list_real_def zero_prod_def) lemma Basis_list_vec3: "Basis_list = [axis 0 1::real^3, axis 1 1, axis 2 1]" by (auto simp: Basis_list_vec_def Basis_list_real_def) lemma eucl_of_list3[simp]: "eucl_of_list [a, b, c] = (a, b, c)" by (auto simp: eucl_of_list_inner Basis_list_vec_def zero_prod_def Basis_prod_def Basis_list_vec3 Basis_list_R3 intro!: euclidean_eqI[where 'a=R3]) subsection \Bounded Linear Functions\ subsection \bounded linear functions\ locale blinfun_syntax begin no_notation vec_nth (infixl "$" 90) notation blinfun_apply (infixl "$" 999) end lemma bounded_linear_via_derivative: fixes f::"'a::real_normed_vector \ 'b::euclidean_space \\<^sub>L 'c::real_normed_vector" \ \TODO: generalize?\ assumes "\i. ((\x. blinfun_apply (f x) i) has_derivative (\x. f' y x i)) (at y)" shows "bounded_linear (f' y x)" proof - interpret linear "f' y x" proof (unfold_locales, goal_cases) case (1 v w) from has_derivative_unique[OF assms[of "v + w", unfolded blinfun.bilinear_simps] has_derivative_add[OF assms[of v] assms[of w]], THEN fun_cong, of x] show ?case . next case (2 r v) from has_derivative_unique[OF assms[of "r *\<^sub>R v", unfolded blinfun.bilinear_simps] has_derivative_scaleR_right[OF assms[of v], of r], THEN fun_cong, of x] show ?case . qed let ?bnd = "\i\Basis. norm (f' y x i)" { fix v have "f' y x v = (\i\Basis. (v \ i) *\<^sub>R f' y x i)" by (subst euclidean_representation[symmetric]) (simp add: sum scaleR) also have "norm \ \ norm v * ?bnd" by (auto intro!: order.trans[OF norm_sum] sum_mono mult_right_mono simp: sum_distrib_left Basis_le_norm) finally have "norm (f' y x v) \ norm v * ?bnd" . } then show ?thesis by unfold_locales auto qed definition blinfun_scaleR::"('a::real_normed_vector \\<^sub>L real) \ 'b::real_normed_vector \ ('a \\<^sub>L 'b)" where "blinfun_scaleR a b = blinfun_scaleR_left b o\<^sub>L a" lemma blinfun_scaleR_transfer[transfer_rule]: "rel_fun (pcr_blinfun (=) (=)) (rel_fun (=) (pcr_blinfun (=) (=))) (\a b c. a c *\<^sub>R b) blinfun_scaleR" by (auto simp: blinfun_scaleR_def rel_fun_def pcr_blinfun_def cr_blinfun_def OO_def) lemma blinfun_scaleR_rep_eq[simp]: "blinfun_scaleR a b c = a c *\<^sub>R b" by (simp add: blinfun_scaleR_def) lemma bounded_linear_blinfun_scaleR: "bounded_linear (blinfun_scaleR a)" unfolding blinfun_scaleR_def[abs_def] by (auto intro!: bounded_linear_intros) lemma blinfun_scaleR_has_derivative[derivative_intros]: assumes "(f has_derivative f') (at x within s)" shows "((\x. blinfun_scaleR a (f x)) has_derivative (\x. blinfun_scaleR a (f' x))) (at x within s)" using bounded_linear_blinfun_scaleR assms by (rule bounded_linear.has_derivative) lemma blinfun_componentwise: fixes f::"'a::real_normed_vector \ 'b::euclidean_space \\<^sub>L 'c::real_normed_vector" shows "f = (\x. \i\Basis. blinfun_scaleR (blinfun_inner_left i) (f x i))" by (auto intro!: blinfun_eqI simp: blinfun.sum_left euclidean_representation blinfun.scaleR_right[symmetric] blinfun.sum_right[symmetric]) lemma blinfun_has_derivative_componentwiseI: fixes f::"'a::real_normed_vector \ 'b::euclidean_space \\<^sub>L 'c::real_normed_vector" assumes "\i. i \ Basis \ ((\x. f x i) has_derivative blinfun_apply (f' i)) (at x)" shows "(f has_derivative (\x. \i\Basis. blinfun_scaleR (blinfun_inner_left i) (f' i x))) (at x)" by (subst blinfun_componentwise) (force intro: derivative_eq_intros assms simp: blinfun.bilinear_simps) lemma has_derivative_BlinfunI: fixes f::"'a::real_normed_vector \ 'b::euclidean_space \\<^sub>L 'c::real_normed_vector" assumes "\i. ((\x. f x i) has_derivative (\x. f' y x i)) (at y)" shows "(f has_derivative (\x. Blinfun (f' y x))) (at y)" proof - have 1: "f = (\x. \i\Basis. blinfun_scaleR (blinfun_inner_left i) (f x i))" by (rule blinfun_componentwise) moreover have 2: "(\ has_derivative (\x. \i\Basis. blinfun_scaleR (blinfun_inner_left i) (f' y x i))) (at y)" by (force intro: assms derivative_eq_intros) moreover interpret f': bounded_linear "f' y x" for x by (rule bounded_linear_via_derivative) (rule assms) have 3: "(\i\Basis. blinfun_scaleR (blinfun_inner_left i) (f' y x i)) i = f' y x i" for x i by (auto simp: if_distrib if_distribR blinfun.bilinear_simps f'.scaleR[symmetric] f'.sum[symmetric] euclidean_representation intro!: blinfun_euclidean_eqI) have 4: "blinfun_apply (Blinfun (f' y x)) = f' y x" for x apply (subst bounded_linear_Blinfun_apply) subgoal by unfold_locales subgoal by simp done show ?thesis apply (subst 1) apply (rule 2[THEN has_derivative_eq_rhs]) apply (rule ext) apply (rule blinfun_eqI) apply (subst 3) apply (subst 4) apply (rule refl) done qed lemma has_derivative_Blinfun: assumes "(f has_derivative f') F" shows "(f has_derivative Blinfun f') F" using assms by (subst bounded_linear_Blinfun_apply) auto lift_definition flip_blinfun:: "('a::real_normed_vector \\<^sub>L 'b::real_normed_vector \\<^sub>L 'c::real_normed_vector) \ 'b \\<^sub>L 'a \\<^sub>L 'c" is "\f x y. f y x" using bounded_bilinear.bounded_linear_left bounded_bilinear.bounded_linear_right bounded_bilinear.flip by auto lemma flip_blinfun_apply[simp]: "flip_blinfun f a b = f b a" by transfer simp lemma le_norm_blinfun: shows "norm (blinfun_apply f x) / norm x \ norm f" by transfer (rule le_onorm) lemma norm_flip_blinfun[simp]: "norm (flip_blinfun x) = norm x" (is "?l = ?r") proof (rule antisym) from order_trans[OF norm_blinfun, OF mult_right_mono, OF norm_blinfun, OF norm_ge_zero, of x] show "?l \ ?r" by (auto intro!: norm_blinfun_bound simp: ac_simps) have "norm (x a b) \ norm (flip_blinfun x) * norm a * norm b" for a b proof - have "norm (x a b) / norm a \ norm (flip_blinfun x b)" by (rule order_trans[OF _ le_norm_blinfun]) auto also have "\ \ norm (flip_blinfun x) * norm b" by (rule norm_blinfun) finally show ?thesis by (auto simp add: divide_simps blinfun.bilinear_simps algebra_simps split: if_split_asm) qed then show "?r \ ?l" by (auto intro!: norm_blinfun_bound) qed lemma bounded_linear_flip_blinfun[bounded_linear]: "bounded_linear flip_blinfun" by unfold_locales (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI exI[where x=1]) lemma dist_swap2_swap2[simp]: "dist (flip_blinfun f) (flip_blinfun g) = dist f g" by (metis (no_types) bounded_linear_flip_blinfun dist_blinfun_def linear_simps(2) norm_flip_blinfun) context includes blinfun.lifting begin lift_definition blinfun_of_vmatrix::"(real^'m^'n) \ ((real^('m::finite)) \\<^sub>L (real^('n::finite)))" is "matrix_vector_mult:: ((real, 'm) vec, 'n) vec \ ((real, 'm) vec \ (real, 'n) vec)" unfolding linear_linear by (rule matrix_vector_mul_linear) lemma matrix_blinfun_of_vmatrix[simp]: "matrix (blinfun_of_vmatrix M) = M" apply vector apply (auto simp: matrix_def) apply transfer by (metis cart_eq_inner_axis matrix_vector_mul_component) end lemma blinfun_apply_componentwise: "B = (\i\Basis. blinfun_scaleR (blinfun_inner_left i) (blinfun_apply B i))" using blinfun_componentwise[of "\x. B", unfolded fun_eq_iff] by blast lemma blinfun_apply_eq_sum: assumes [simp]: "length v = CARD('n)" shows "blinfun_apply (B::(real^'n::enum)\\<^sub>L(real^'m::enum)) (eucl_of_list v) = (\ij Basis_list ! i) * v ! j) *\<^sub>R (Basis_list ! i))" apply (subst blinfun_apply_componentwise[of B]) apply (auto intro!: euclidean_eqI[where 'a="(real,'m) vec"] simp: blinfun.bilinear_simps eucl_of_list_inner inner_sum_left inner_Basis if_distrib sum_Basis_sum_nth_Basis_list nth_eq_iff_index if_distribR cong: if_cong) apply (subst sum.swap) by (auto simp: sum.delta algebra_simps) lemma in_square_lemma[intro, simp]: "x * C + y < D * C" if "x < D" "y < C" for x::nat proof - have "x * C + y < (D - 1) * C + C" apply (rule add_le_less_mono) apply (rule mult_right_mono) using that by auto also have "\ \ D * C" using that by (auto simp: algebra_simps) finally show ?thesis . qed lemma less_square_imp_div_less[intro, simp]: "i < E * D \ i div E < D" for i::nat by (metis div_eq_0_iff div_mult2_eq gr_implies_not0 mult_not_zero) lemma in_square_lemma'[intro, simp]: "i < L \ n < N \ i * N + n < N * L" for i n::nat by (metis in_square_lemma mult.commute) lemma distinct_nth_eq_iff: "distinct xs \ x < length xs \ y < length xs \ xs ! x = xs ! y \ x = y" by (drule inj_on_nth[where I="{..i. axis (enum_class.enum ! (i div CARD('i))) (axis (enum_class.enum ! (i mod CARD('i))) 1)) ((index enum_class.enum j) * CARD('i) + index enum_class.enum i)" by (auto simp: index_less_cardi enum_UNIV) note less=in_square_lemma[OF index_less_cardj index_less_cardi, of j i] show ?thesis apply (subst *) apply (subst index_map_inj_on[where S="{.. Basis \ vec_nth (vec_nth x i) j = ((if x = axis i (axis j 1) then 1 else 0))" by (auto simp: Basis_vec_def axis_def) lemma vec_nth_eucl_of_list_eq2: "length M = CARD('n) * CARD('m) \ vec_nth (vec_nth (eucl_of_list M::real^'n::enum^'m::enum) i) j = M ! index Basis_list (axis i (axis j (1::real)))" apply (auto simp: eucl_of_list_def) apply (subst sum_list_zip_map_of) apply (auto intro!: distinct_zipI2 simp: split_beta') apply (subst sum.cong[OF refl]) apply (subst vec_nth_Basis2) apply (force simp: set_zip) apply (rule refl) apply (auto simp: if_distrib sum.delta cong: if_cong) subgoal apply (cases "map_of (zip Basis_list M) (axis i (axis j 1)::real^'n::enum^'m::enum)") subgoal premises prems proof - have "fst ` set (zip Basis_list M) = (Basis::(real^'n::enum^'m::enum) set)" using prems by (auto simp: in_set_zip) then show ?thesis using prems by (subst (asm) map_of_eq_None_iff) auto qed subgoal for a apply (auto simp: in_set_zip) subgoal premises prems for n proof - have "n < card (Basis::(real^'n::_^'m::_) set)" by (simp add: prems(4)) then show ?thesis by (metis index_Basis_list_nth prems(2)) qed done done done lemma vec_nth_eq_list_of_eucl2: "vec_nth (vec_nth (M::real^'n::enum^'m::enum) i) j = list_of_eucl M ! (index enum_class.enum i * CARD('n) + index enum_class.enum j)" apply (subst eucl_of_list_list_of_eucl[of M, symmetric]) apply (subst vec_nth_eucl_of_list_eq2) unfolding index_Basis_list_axis2 by auto theorem eucl_of_list_matrix_vector_mult_eq_sum_nth_Basis_list: assumes "length M = CARD('n) * CARD('m)" assumes "length v = CARD('n)" shows "(eucl_of_list M::real^'n::enum^'m::enum) *v eucl_of_list v = (\ijR Basis_list ! i)" apply (vector matrix_vector_mult_def) apply (auto simp: ) apply (subst vec_nth_eucl_of_list_eq2) apply (auto simp: assms) apply (subst vec_nth_eucl_of_list_eq) apply (auto simp: assms index_Basis_list_axis2 index_Basis_list_axis1 vec_nth_Basis sum.delta nth_eq_iff_index if_distrib cong: if_cong) subgoal for i apply (rule sum.reindex_cong[where l="nth enum_class.enum"]) apply (auto simp: enum_distinct card_UNIV_length_enum distinct_nth_eq_iff intro!: inj_onI) apply (rule image_eqI[OF ]) apply (rule nth_index[symmetric]) apply (auto simp: enum_UNIV) by (auto simp: algebra_simps enum_UNIV enum_distinct index_nth_id) subgoal for i using index_less[of i "enum_class.enum" "CARD('n)"] by (auto simp: enum_UNIV card_UNIV_length_enum) done lemma index_enum_less[intro, simp]: "index enum_class.enum (i::'n::enum) < CARD('n)" by (auto intro!: index_less simp: enum_UNIV card_UNIV_length_enum) lemmas [intro, simp] = enum_distinct lemmas [simp] = card_UNIV_length_enum[symmetric] enum_UNIV lemma sum_index_enum_eq: "(\(k::'n::enum)\UNIV. f (index enum_class.enum k)) = (\i*) chapter \User guide\ text_raw \\label{chapter:Userguide}\ text \ This user guide shows how to use and extend the lightweight containers framework (LC). For a more theoretical discussion, see \cite{Lochbihler2013ITP}. This user guide assumes that you are familiar with refinement in the code generator \cite{HaftmannBulwahn2013codetut,HaftmannKrausKuncarNipkow2013ITP}. The theory \Containers_Userguide\ generates it; so if you want to experiment with the examples, you can find their source code there. Further examples can be found in the @{dir \Examples\} folder. \ section \Characteristics\ text_raw \ \isastyletext \begin{itemize} \ text_raw \ \isastyletext \item \textbf{Separate type classes for code generation} \\ LC follows the ideal that type classes for code generation should be separate from the standard type classes in Isabelle. LC's type classes are designed such that every type can become an instance, so well-sortedness errors during code generation can always be remedied. \ text_raw \ \isastyletext \item \textbf{Multiple implementations} \\ LC supports multiple simultaneous implementations of the same container type. For example, the following implements at the same time (i)~the set of @{typ bool} as a distinct list of the elements, (ii)~@{typ "int set"} as a RBT of the elements or as the RBT of the complement, and (iii)~sets of functions as monad-style lists: \par \ value "({True}, {1 :: int}, - {2 :: int, 3}, {\x :: int. x * x, \y. y + 1})" text_raw \ \isastyletext \par The LC type classes are the key to simultaneously supporting different implementations. \item \textbf{Extensibility} \\ The LC framework is designed for being extensible. You can add new containers, implementations and element types any time. \end{itemize} \ section \Getting started\ text_raw \\label{section:getting:started}\ text \ Add the entry theory @{theory Containers.Containers} for LC to the end of your imports. This will reconfigure the code generator such that it implements the types @{typ "'a set"} for sets and @{typ "('a, 'b) mapping"} for maps with one of the data structures supported. As with all the theories that adapt the code generator setup, it is important that @{theory Containers.Containers} comes at the end of the imports. + \textbf{Note:} LC should not be used together with the theory @{text "HOL-Library.Code_Cardinality"}. + Run the following command, e.g., to check that LC works correctly and implements sets of @{typ int}s as red-black trees (RBT): \ value [code] "{1 :: int}" text \ This should produce @{value [names_short] "{1 :: int}"}. Without LC, sets are represented as (complements of) a list of elements, i.e., @{term "set [1 :: int]"} in the example. \ text \ If your exported code does not use your own types as elements of sets or maps and you have not declared any code equation for these containers, then your \isacommand{export{\isacharunderscore}code} command will use LC to implement @{typ "'a set"} and @{typ "('a, 'b) mapping"}. Our running example will be arithmetic expressions. The function @{term "vars e"} computes the variables that occur in the expression @{term e} \ type_synonym vname = string datatype expr = Var vname | Lit int | Add expr expr fun vars :: "expr \ vname set" where "vars (Var v) = {v}" | "vars (Lit i) = {}" | "vars (Add e\<^sub>1 e\<^sub>2) = vars e\<^sub>1 \ vars e\<^sub>2" value "vars (Var ''x'')" text \ To illustrate how to deal with type variables, we will use the following variant where variable names are polymorphic: \ datatype 'a expr' = Var' 'a | Lit' int | Add' "'a expr'" "'a expr'" fun vars' :: "'a expr' \ 'a set" where "vars' (Var' v) = {v}" | "vars' (Lit' i) = {}" | "vars' (Add' e\<^sub>1 e\<^sub>2) = vars' e\<^sub>1 \ vars' e\<^sub>2" value "vars' (Var' (1 :: int))" section \New types as elements\ text \ This section explains LC's type classes and shows how to instantiate them. If you want to use your own types as the elements of sets or the keys of maps, you must instantiate up to eight type classes: @{class ceq} (\S\ref{subsection:ceq}), @{class ccompare} (\S\ref{subsection:ccompare}), @{class set_impl} (\S\ref{subsection:set_impl}), @{class mapping_impl} (\S\ref{subsection:mapping_impl}), @{class cenum} (\S\ref{subsection:cenum}), @{class finite_UNIV} (\S\ref{subsection:finite_UNIV}), @{class card_UNIV} (\S\ref{subsection:card_UNIV}), and @{class cproper_interval} (\S\ref{subsection:cproper_interval}). Otherwise, well-sortedness errors like the following will occur: \begin{verbatim} *** Wellsortedness error: *** Type expr not of sort {ceq,ccompare} *** No type arity expr :: ceq *** At command "value" \end{verbatim} In detail, the sort requirements on the element type @{typ "'a"} are: \begin{itemize} \item @{class ceq} (\S\ref{subsection:ceq}), @{class ccompare} (\S\ref{subsection:ccompare}), and @{class set_impl} (\S\ref{subsection:set_impl}) for @{typ "'a set"} in general \item @{class cenum} (\S\ref{subsection:cenum}) for set comprehensions @{term "{x. P x}"}, \item @{class card_UNIV}, @{class cproper_interval} for @{typ "'a set set"} and any deeper nesting of sets (\S\ref{subsection:card_UNIV}),% \footnote{% These type classes are only required for set complements (see \S\ref{subsection:well:sortedness}). } and \item @{class equal},% \footnote{% We deviate here from the strict separation of type classes, because it does not make sense to store types in a map on which we do not have equality, because the most basic operation @{term "Mapping.lookup"} inherently requires equality. } @{class ccompare} (\S\ref{subsection:ccompare}) and @{class mapping_impl} (\S\ref{subsection:mapping_impl}) for @{typ "('a, 'b) mapping"}. \end{itemize} \ subsection \Equality testing\ text_raw \\label{subsection:ceq}\ (*<*)context fixes dummy :: "'a :: {cenum, ceq, ccompare, set_impl, mapping_impl}" begin(*>*) text \ The type class @{class ceq} defines the operation @{term [source] "CEQ('a) :: ('a \ 'a \ bool) option" } for testing whether two elements are equal.% \footnote{% Technically, the type class @{class ceq} defines the operation @{term [source] ceq}. As usage often does not fully determine @{term [source] ceq}'s type, we use the notation @{term "CEQ('a)"} that explicitly mentions the type. In detail, @{term "CEQ('a)"} is translated to @{term [source] "CEQ('a) :: ('a \ 'a \ bool) option" } including the type constraint. We do the same for the other type class operators: @{term "CCOMPARE('a)"} constrains the operation @{term [source] ccompare} (\S\ref{subsection:ccompare}), @{term [source] "SET_IMPL('a)"} constrains the operation @{term [source] set_impl}, (\S\ref{subsection:set_impl}), @{term [source] "MAPPING_IMPL('a)"} (constrains the operation @{term [source] mapping_impl}, (\S\ref{subsection:mapping_impl}), and @{term "CENUM('a)"} constrains the operation @{term [source] cenum}, \S\ref{subsection:cenum}. } The test is embedded in an \option\ value to allow for types that do not support executable equality test such as @{typ "'a \ 'b"}. Whenever possible, @{term "CEQ('a)"} should provide an executable equality operator. Otherwise, membership tests on such sets will raise an exception at run-time. For data types, the \derive\ command can automatically instantiates of @{class ceq}, we only have to tell it whether an equality operation should be provided or not (parameter \no\). \ (*<*)end(*>*) derive (eq) ceq expr datatype example = Example derive (no) ceq example text \ In the remainder of this subsection, we look at how to manually instantiate a type for @{class ceq}. First, the simple case of a type constructor \simple_tycon\ without parameters that already is an instance of @{class equal}: \ typedecl simple_tycon axiomatization where simple_tycon_equal: "OFCLASS(simple_tycon, equal_class)" instance simple_tycon :: equal by (rule simple_tycon_equal) instantiation simple_tycon :: ceq begin definition "CEQ(simple_tycon) = Some (=)" instance by(intro_classes)(simp add: ceq_simple_tycon_def) end text \ For polymorphic types, this is a bit more involved, as the next example with @{typ "'a expr'"} illustrates (note that we could have delegated all this to \derive\). First, we need an operation that implements equality tests with respect to a given equality operation on the polymorphic type. For data types, we can use the relator which the transfer package (method \transfer\) requires and the BNF package generates automatically. As we have used the old datatype package for @{typ "'a expr'"}, we must define it manually: \ context fixes R :: "'a \ 'b \ bool" begin fun expr'_rel :: "'a expr' \ 'b expr' \ bool" where "expr'_rel (Var' v) (Var' v') \ R v v'" | "expr'_rel (Lit' i) (Lit' i') \ i = i'" | "expr'_rel (Add' e\<^sub>1 e\<^sub>2) (Add' e\<^sub>1' e\<^sub>2') \ expr'_rel e\<^sub>1 e\<^sub>1' \ expr'_rel e\<^sub>2 e\<^sub>2'" | "expr'_rel _ _ \ False" end text \If we give HOL equality as parameter, the relator is equality:\ lemma expr'_rel_eq: "expr'_rel (=) e\<^sub>1 e\<^sub>2 \ e\<^sub>1 = e\<^sub>2" by(induct e\<^sub>1 e\<^sub>2 rule: expr'_rel.induct) simp_all text \ Then, the instantiation is again canonical: \ instantiation expr' :: (ceq) ceq begin definition "CEQ('a expr') = (case ID CEQ('a) of None \ None | Some eq \ Some (expr'_rel eq))" instance by(intro_classes) (auto simp add: ceq_expr'_def expr'_rel_eq[abs_def] dest: Collection_Eq.ID_ceq split: option.split_asm) end (*<*)context fixes dummy :: "'a :: ceq" begin(*>*) text \ Note the following two points: First, the instantiation should avoid to use @{term "(=)"} on terms of the polymorphic type. This keeps the LC framework separate from the type class @{class equal}, i.e., every choice of @{typ "'a"} in @{typ "'a expr'"} can be of sort @{class "ceq"}. The easiest way to achieve this is to obtain the equality test from @{term "CEQ('a)"}. Second, we use @{term "ID CEQ('a)"} instead of @{term "CEQ('a)"}. In proofs, we want that the simplifier uses assumptions like \CEQ('a) = Some \\ for rewriting. However, @{term "CEQ('a)"} is a nullary constant, so the simplifier reverses such an equation, i.e., it only rewrites \Some \\ to @{term "CEQ('a :: ceq)"}. Applying the identity function @{term "ID"} to @{term "CEQ('a :: ceq)"} avoids this, and the code generator eliminates all occurrences of @{term "ID"}. Although @{thm ID_def} by definition, do not use the conventional @{term "id"} instead of @{term ID}, because @{term "id CEQ('a :: ceq)"} immediately simplifies to @{term "CEQ('a :: ceq)"}. \ (*<*)end(*>*) subsection \Ordering\ text_raw \\label{subsection:ccompare}\ (*<*)context fixes dummy :: "'a :: {ccompare, ceq}" begin(*>*) text \ LC takes the order for storing elements in search trees from the type class @{class ccompare} rather than @{class compare}, because we cannot instantiate @{class compare} for some types (e.g., @{typ "'a set"} as @{term "(\)"} is not linear). Similar to @{term "CEQ('a)"} in class @{term ceq}, the class @{class ccompare} specifies an optional comparator @{term [source] "CCOMPARE('a) :: (('a \ 'a \ order)) option" }. If you cannot or do not want to implement a comparator on your type, you can default to @{term "None"}. In that case, you will not be able to use your type as elements of sets or as keys in maps implemented by search trees. If the type is a data type or instantiates @{class compare} and we wish to use that comparator also for the search tree, instantiation is again canonical: For our data type @{typ expr}, derive does everything! \ (*<*)end(*>*) (*<*)(*>*) derive ccompare expr (*<*)(*>*) text \ In general, the pattern for type constructors without parameters looks as follows: \ axiomatization where simple_tycon_compare: "OFCLASS(simple_tycon, compare_class)" instance simple_tycon :: compare by (rule simple_tycon_compare) derive (compare) ccompare simple_tycon text \ For polymorphic types like @{typ "'a expr'"}, we should not do everything manually: First, we must define a comparator that takes the comparator on the type variable @{typ "'a"} as a parameter. This is necessary to maintain the separation between Isabelle/HOL's type classes (like @{class compare}) and LC's. Such a comparator is again easily defined by derive. \ derive ccompare expr' thm ccompare_expr'_def comparator_expr'_simps subsection \Heuristics for picking an implementation\ text_raw \\label{subsection:set_impl} \label{subsection:mapping_impl}\ (*<*)context fixes dummy :: "'a :: {ceq, ccompare, set_impl, mapping_impl}" begin(*>*) text \ Now, we have defined the necessary operations on @{typ expr} and @{typ "'a expr'"} to store them in a set or use them as the keys in a map. But before we can actually do so, we also have to say which data structure to use. The type classes @{class set_impl} and @{class mapping_impl} are used for this. They define the overloaded operations @{term [source] "SET_IMPL('a) :: ('a, set_impl) phantom" } and @{term [source] "MAPPING_IMPL('a) :: ('a, mapping_impl) phantom"}, respectively. The phantom type @{typ "('a, 'b) phantom"} from theory @{theory "HOL-Library.Phantom_Type"} is isomorphic to @{typ "'b"}, but formally depends on @{typ "'a"}. This way, the type class operations meet the requirement that their type contains exactly one type variable. The Haskell and ML compiler will get rid of the extra type constructor again. For sets, you can choose between @{term set_Collect} (characteristic function @{term P} like in @{term "{x. P x}"}), @{term set_DList} (distinct list), @{term set_RBT} (red-black tree), and @{term set_Monad} (list with duplicates). Additionally, you can define @{term "set_impl"} as @{term "set_Choose"} which picks the implementation based on the available operations (RBT if @{term "CCOMPARE('a)"} provides a linear order, else distinct lists if @{term "CEQ('a)"} provides equality testing, and lists with duplicates otherwise). @{term "set_Choose"} is the safest choice because it picks only a data structure when the required operations are actually available. If @{term set_impl} picks a specific implementation, Isabelle does not ensure that all required operations are indeed available. For maps, the choices are @{term "mapping_Assoc_List"} (associative list without duplicates), @{term "mapping_RBT"} (red-black tree), and @{term "mapping_Mapping"} (closures with function update). Again, there is also the @{term "mapping_Choose"} heuristics. For simple cases, \derive\ can be used again (even if the type is not a data type). Consider, e.g., the following instantiations: @{typ "expr set"} uses RBTs, @{typ "(expr, _) mapping"} and @{typ "'a expr' set"} use the heuristics, and @{typ "('a expr', _) mapping"} uses the same implementation as @{typ "('a, _) mapping"}. \ (*<*)end(*>*) derive (rbt) set_impl expr derive (choose) mapping_impl expr derive (choose) set_impl expr' text \ More complex cases such as taking the implementation preference of a type parameter must be done manually. \ instantiation expr' :: (mapping_impl) mapping_impl begin definition "MAPPING_IMPL('a expr') = Phantom('a expr') (of_phantom MAPPING_IMPL('a))" instance .. end (*<*) locale mynamespace begin definition empty where "empty = Mapping.empty" declare (in -) mynamespace.empty_def [code] (*>*) text \ To see the effect of the different configurations, consider the following examples where @{term [names_short] "empty"} refers to @{term "Mapping.empty"}. For that, we must disable pretty printing for sets as follows: \ declare (*<*)(in -) (*>*)pretty_sets[code_post del] text \ \begin{center} \small \begin{tabular}{ll} \toprule \isamarkuptrue\isacommand{value}\isamarkupfalse\ {\isacharbrackleft}code{\isacharbrackright} & \textbf{result} \\ \midrule @{term [source] "{} :: expr set"} & @{value [names_short] "{} :: expr set"} \\ @{term [source] "empty :: (expr, unit) mapping"} & @{value [names_short] "empty :: (expr, unit) mapping"} \\ \midrule @{term [source] "{} :: string expr' set"} & @{value [names_short] "{} :: string expr' set"} \\ @{term [source] "{} :: (nat \ nat) expr' set"} & @{value [names_short] "{} :: (nat \ nat) expr' set"} \\ @{term [source] "{} :: bool expr' set"} & @{value [names_short] "{} :: bool expr' set"} \\ @{term [source] "empty :: (bool expr', unit) mapping"} & @{value [names_short] "empty :: (bool expr', unit) mapping"} \\ \bottomrule \end{tabular} \end{center} For @{typ expr}, @{term mapping_Choose} picks RBTs, because @{term "CCOMPARE(expr)"} provides a comparison operation for @{typ "expr"}. For @{typ "'a expr'"}, the effect of @{term set_Choose} is more pronounced: @{term "CCOMPARE(string)"} is not @{term "None"}, so neither is @{term "CCOMPARE(string expr')"}, and @{term set_Choose} picks RBTs. As @{typ "nat \ nat"} neither provides equality tests (@{class ceq}) nor comparisons (@{class ccompare}), neither does @{typ "(nat \ nat) expr'"}, so we use lists with duplicates. The last two examples show the difference between inheriting a choice and choosing freshly: By default, @{typ bool} prefers distinct (associative) lists over RBTs, because there are just two elements. As @{typ "bool expr'"} enherits the choice for maps from @{typ bool}, an associative list implements @{term [source] "empty :: (bool expr', unit) mapping"}. For sets, in contrast, @{term "SET_IMPL('a expr')"} discards @{typ 'a}'s preferences and picks RBTs, because there is a comparison operation. Finally, let's enable pretty-printing for sets again: \ declare (*<*)(in -) (*>*)pretty_sets [code_post] (*<*) (* The following value commands ensure that the code generator executes @{value ...} above, I could not find a way to specify [code] to @{value}. *) value [code] "{} :: expr set" value [code] "empty :: (expr, unit) mapping" value [code] "{} :: string expr' set" value [code] "{} :: (nat \ nat) expr' set" value [code] "{} :: bool expr' set" value [code] "empty :: (bool expr', unit) mapping" (*>*) (*<*)end(*>*) subsection \Set comprehensions\ text_raw \\label{subsection:cenum}\ (*<*)context fixes dummy :: "'a :: cenum" begin(*>*) text \ If you use the default code generator setup that comes with Isabelle, set comprehensions @{term [source] "{x. P x} :: 'a set"} are only executable if the type @{typ 'a} has sort @{class enum}. Internally, Isabelle's code generator transforms set comprehensions into an explicit list of elements which it obtains from the list @{term enum} of all of @{typ "'a"}'s elements. Thus, the type must be an instance of @{class enum}, i.e., finite in particular. For example, @{term "{c. CHR ''A'' \ c \ c \ CHR ''D''}"} evaluates to @{term "set ''ABCD''"}, the set of the characters A, B, C, and D. For compatibility, LC also implements such an enumeration strategy, but avoids the finiteness restriction. The type class @{class cenum} mimicks @{class enum}, but its single parameter @{term [source] "cEnum :: ('a list \ (('a \ bool) \ bool) \ (('a \ bool) \ bool)) option"} combines all of @{class enum}'s parameters, namely a list of all elements, a universal and an existential quantifier. \option\ ensures that every type can be an instance as @{term "CENUM('a)"} can always default to @{term None}. For types that define @{term "CENUM('a)"}, set comprehensions evaluate to a list of their elements. Otherwise, set comprehensions are represented as a closure. This means that if the generated code contains at least one set comprehension, all element types of a set must instantiate @{class cenum}. Infinite types default to @{term None}, and enumerations for finite types are canoncial, see @{theory Containers.Collection_Enum} for examples. \ (*<*)end(*>*) instantiation expr :: cenum begin definition "CENUM(expr) = None" instance by(intro_classes)(simp_all add: cEnum_expr_def) end derive (no) cenum expr' derive compare_order expr text_raw \\par\medskip \isastyletext For example,\ value "({b. b = True}, {x. compare x (Lit 0) = Lt})" text_raw \ \isastyletext{} yields @{value "({b. b = True}, {x. compare x (Lit 0) = Lt})"} \ text \ LC keeps complements of such enumerated set comprehensions, i.e., @{term "- {b. b = True}"} evaluates to @{value "- {b. b = True}"}. If you want that the complement operation actually computes the elements of the complements, you have to replace the code equations for @{term uminus} as follows: \ declare Set_uminus_code[code del] Set_uminus_cenum[code] (*<*)value "- {b. b = True}"(*>*) text \ Then, @{term "- {b. b = True}"} becomes @{value "- {b. b = True}"}, but this applies to all complement invocations. For example, @{term [source] "UNIV :: bool set"} becomes @{value "UNIV :: bool set"}. \ (*<*)declare Set_uminus_cenum[code del] Set_uminus_code[code](*>*) subsection \Nested sets\ text_raw \\label{subsection:finite_UNIV} \label{subsection:card_UNIV} \label{subsection:cproper_interval}\ (*<*)context fixes dummy :: "'a :: {card_UNIV, cproper_interval}" begin(*>*) text \ To deal with nested sets such as @{typ "expr set set"}, the element type must provide three operations from three type classes: \begin{itemize} \item @{class finite_UNIV} from theory @{theory "HOL-Library.Cardinality"} defines the constant @{term [source] "finite_UNIV :: ('a, bool) phantom"} which designates whether the type is finite. \item @{class card_UNIV} from theory @{theory "HOL-Library.Cardinality"} defines the constant @{term [source] "card_UNIV :: ('a, nat) phantom"} which returns @{term "CARD('a)"}, i.e., the number of values in @{typ 'a}. If @{typ "'a"} is infinite, @{term "CARD('a) = 0"}. \item @{class cproper_interval} from theory @{theory Containers.Collection_Order} defines the function @{term [source] "cproper_interval :: 'a option \ 'a option \ bool"}. If the type @{typ "'a"} is finite and @{term "CCOMPARE('a)"} yields a linear order on @{typ "'a"}, then @{term "cproper_interval x y"} returns whether the open interval between @{term "x"} and @{term "y"} is non-empty. The bound @{term "None"} denotes unboundedness. \end{itemize} Note that the type class @{class finite_UNIV} must not be confused with the type class @{class finite}. @{class finite_UNIV} allows the generated code to examine whether a type is finite whereas @{class finite} requires that the type in fact is finite. \ (*<*)end(*>*) text \ For datatypes, the theory @{theory Containers.Card_Datatype} defines some machinery to assist in proving that the type is (in)finite and has a given number of elements -- see @{file \Examples/Card_Datatype_Ex.thy\} for examples. With this, it is easy to instantiate @{class card_UNIV} for our running examples: \ lemma inj_expr [simp]: "inj Lit" "inj Var" "inj Add" "inj (Add e)" by(simp_all add: fun_eq_iff inj_on_def) lemma infinite_UNIV_expr: "\ finite (UNIV :: expr set)" including card_datatype proof - have "rangeIt (Lit 0) (Add (Lit 0)) \ UNIV" by simp from finite_subset[OF this] show ?thesis by auto qed instantiation expr :: card_UNIV begin definition "finite_UNIV = Phantom(expr) False" definition "card_UNIV = Phantom(expr) 0" instance by intro_classes (simp_all add: finite_UNIV_expr_def card_UNIV_expr_def infinite_UNIV_expr) end lemma inj_expr' [simp]: "inj Lit'" "inj Var'" "inj Add'" "inj (Add' e)" by(simp_all add: fun_eq_iff inj_on_def) lemma infinite_UNIV_expr': "\ finite (UNIV :: 'a expr' set)" including card_datatype proof - have "rangeIt (Lit' 0) (Add' (Lit' 0)) \ UNIV" by simp from finite_subset[OF this] show ?thesis by auto qed instantiation expr' :: (type) card_UNIV begin definition "finite_UNIV = Phantom('a expr') False" definition "card_UNIV = Phantom('a expr') 0" instance by intro_classes (simp_all add: finite_UNIV_expr'_def card_UNIV_expr'_def infinite_UNIV_expr') end text \ As @{typ expr} and @{typ "'a expr'"} are infinite, instantiating @{class cproper_interval} is trivial, because @{class cproper_interval} only makes assumptions about its parameters for finite types. Nevertheless, it is important to actually define @{term cproper_interval}, because the code generator requires a code equation. \ instantiation expr :: cproper_interval begin definition cproper_interval_expr :: "expr proper_interval" where "cproper_interval_expr _ _ = undefined" instance by(intro_classes)(simp add: infinite_UNIV_expr) end instantiation expr' :: (ccompare) cproper_interval begin definition cproper_interval_expr' :: "'a expr' proper_interval" where "cproper_interval_expr' _ _ = undefined" instance by(intro_classes)(simp add: infinite_UNIV_expr') end subsubsection \Instantiation of @{class proper_interval}\ text \ To illustrate what to do with finite types, we instantiate @{class proper_interval} for @{typ expr}. Like @{class ccompare} relates to @{class compare}, the class @{class cproper_interval} has a counterpart @{class proper_interval} without the finiteness assumption. Here, we first have to gather the simplification rules of the comparator from the derive invocation, especially, how the strict order of the comparator, @{term lt_of_comp}, can be defined. Since the order on lists is not yet shown to be consistent with the comparators that are used for lists, this part of the userguide is currently not available. \ (* instantiation expr :: proper_interval begin lemma less_expr_conv: "(<) = lt_of_comp comparator_expr" "(\) = le_of_comp comparator_expr" using less_expr_def less_eq_expr_def unfolding compare_expr_def by auto lemma lt_of_comp_expr: "lt_of_comp comparator_expr e1 e2 = ( case e1 of Var x1 \ (case e2 of Var x2 \ lt_of_comp (comparator_list comparator_of) x1 x2 | Lit _ \ True | Add _ _ \ True) | Lit i1 \ (case e2 of Var _ \ False | Lit i2 \ lt_of_comp comparator_of i1 i2 | Add _ _ \ True) | Add a1 b1 \ (case e2 of Var _ \ False | Lit _ \ False | Add a2 b2 \ lt_of_comp comparator_expr a1 a2 \ le_of_comp comparator_expr a1 a2 \ lt_of_comp comparator_expr b1 b2) )" by (simp add: lt_of_comp_def le_of_comp_def comp_lex_code split: expr.split order.split) fun proper_interval_expr :: "expr option \ expr option \ bool" where "proper_interval_expr None (Some (Var x)) \ proper_interval None (Some x)" | "proper_interval_expr (Some (Var x)) (Some (Var y)) \ proper_interval (Some x) (Some y)" | "proper_interval_expr (Some (Lit i)) (Some (Lit j)) \ proper_interval (Some i) (Some j)" | "proper_interval_expr (Some (Lit i)) (Some (Var x)) \ False" | "proper_interval_expr (Some (Add e1 e2)) (Some (Lit i)) \ False" | "proper_interval_expr (Some (Add e1 e2)) (Some (Var x)) \ False" | "proper_interval_expr (Some (Add e1 e2)) (Some (Add e1' e2')) \ (case compare e1 e1' of Lt \ True | Eq \ proper_interval_expr (Some e2) (Some e2') | Gt \ False)" | "proper_interval_expr _ _ \ True" instance proof(intro_classes) fix x y :: expr show "proper_interval None (Some y) = (\z. z < y)" unfolding less_expr_conv by (cases y)(auto simp add: lt_of_comp_expr intro: exI[where x="''''"]) { fix x y have "x < Add x y" unfolding less_expr_conv by(induct x arbitrary: y)(simp_all add: lt_of_comp_expr) } note le_Add = this thus "proper_interval (Some x) None = (\z. x < z)" by(simp add: less_expr_def exI[where x="Add x y"]) note [simp] = less_expr_conv lt_of_comp_expr show "proper_interval (Some x) (Some y) = (\z. x < z \ z < y)" proof(induct "Some x" "Some y" arbitrary: x y rule: proper_interval_expr.induct) case 2 show ?case by(auto simp add: proper_interval_list_aux_correct) next case (3 i j) show ?case by(auto intro: exI[where x="Lit (i + 1)"]) next case (7 e1 e2 e1' e2') thus ?case by(auto intro: le_Add simp add: le_less) next case ("8_2" i e1 e2) show ?case by(auto intro: exI[where x="Lit (i + 1)"]) next case ("8_5" x i) show ?case by(auto intro: exI[where x="Var (x @ [undefined])"] simp add: less_append_same_iff) next case ("8_6" x e1 e2) show ?case by(auto intro: exI[where x="Lit 0"]) next case ("8_7" i e1 e2) show ?case by(auto intro: exI[where x="Lit (i + 1)"]) next case ("8_10" x i) show ?case by(auto intro: exI[where x="Lit (i - 1)"]) next case ("8_12" x e1 e2) show ?case by(auto intro: exI[where x="Lit 0"]) next case ("8_13" i e1 e2) show ?case by(auto intro: exI[where x="Lit (i + 1)"]) qed auto qed simp end *) (*<*) value "{{Lit 1}}" value "{{{Lit 1}}}" value "{{{{Lit 1}}}}" (*>*) section \New implementations for containers\ text_raw \\label{section:new:implementation}\ (*<*) typedecl 'v trie_raw (*>*) text \ This section explains how to add a new implementation for a container type. If you do so, please consider to add your implementation to this AFP entry. \ subsection \Model and verify the data structure\ text_raw \\label{subsection:implement:data:structure}\ text \ First, you of course have to define the data structure and verify that it has the required properties. As our running example, we use a trie to implement @{typ "('a, 'b) mapping"}. A trie is a binary tree whose the nodes store the values, the keys are the paths from the root to the given node. We use lists of @{typ bool}ans for the keys where the @{typ bool}ean indicates whether we should go to the left or right child. For brevity, we skip this step and rather assume that the type @{typ "'v trie_raw"} of tries has following operations and properties: \ type_synonym trie_key = "bool list" axiomatization trie_empty :: "'v trie_raw" and trie_update :: "trie_key \ 'v \ 'v trie_raw \ 'v trie_raw" and trie_lookup :: "'v trie_raw \ trie_key \ 'v option" and trie_keys :: "'v trie_raw \ trie_key set" where trie_lookup_empty: "trie_lookup trie_empty = Map.empty" and trie_lookup_update: "trie_lookup (trie_update k v t) = (trie_lookup t)(k \ v)" and trie_keys_dom_lookup: "trie_keys t = dom (trie_lookup t)" text \ This is only a minimal example. A full-fledged implementation has to provide more operations and -- for efficiency -- should use more than just @{typ bool}eans for the keys. \ (*<*) (* Implement trie by free term algebra *) code_datatype trie_empty trie_update lemmas [code] = trie_lookup_empty trie_lookup_update lemma trie_keys_empty [code]: "trie_keys trie_empty = {}" by(simp add: trie_keys_dom_lookup trie_lookup_empty) lemma trie_keys_update [code]: "trie_keys (trie_update k v t) = insert k (trie_keys t)" by(simp add: trie_keys_dom_lookup trie_lookup_update) (*>*) subsection \Generalise the data structure\ text_raw \\label{subsection:introduce:type:class}\ text \ As @{typ "('k, 'v) mapping"} store keys of arbitrary type @{typ "'k"}, not just @{typ "trie_key"}, we cannot use @{typ "'v trie_raw"} directly. Instead, we must first convert arbitrary types @{typ "'k"} into @{typ "trie_key"}. Of course, this is not always possbile, but we only have to make sure that we pick tries as implementation only if the types do. This is similar to red-black trees which require an order. Hence, we introduce a type class to convert arbitrary keys into trie keys. We make the conversions optional such that every type can instantiate the type class, just as LC does for @{class ceq} and @{class ccompare}. \ type_synonym 'a cbl = "(('a \ bool list) \ (bool list \ 'a)) option" class cbl = fixes cbl :: "'a cbl" assumes inj_to_bl: "ID cbl = Some (to_bl, from_bl) \ inj to_bl" and to_bl_inverse: "ID cbl = Some (to_bl, from_bl) \ from_bl (to_bl a) = a" begin abbreviation from_bl where "from_bl \ snd (the (ID cbl))" abbreviation to_bl where "to_bl \ fst (the (ID cbl))" end text \ It is best to immediately provide the instances for as many types as possible. Here, we only present two examples: @{typ unit} provides conversion functions, @{typ "'a \ 'b"} does not. \ instantiation unit :: cbl begin definition "cbl = Some (\_. [], \_. ())" instance by(intro_classes)(auto simp add: cbl_unit_def ID_Some intro: injI) end instantiation "fun" :: (type, type) cbl begin definition "cbl = (None :: ('a \ 'b) cbl)" instance by intro_classes(simp_all add: cbl_fun_def ID_None) end subsection \Hide the invariants of the data structure\ text_raw \\label{subsection:hide:invariants}\ text \ Many data structures have invariants on which the operations rely. You must hide such invariants in a \isamarkuptrue\isacommand{typedef}\isamarkupfalse{} before connecting to the container, because the code generator cannot handle explicit invariants. The type must be inhabited even if the types of the elements do not provide the required operations. The easiest way is often to ignore all invariants in that case. In our example, we require that all keys in the trie represent encoded values. \ typedef (overloaded) ('k :: cbl, 'v) trie = "{t :: 'v trie_raw. trie_keys t \ range (to_bl :: 'k \ trie_key) \ ID (cbl :: 'k cbl) = None}" proof show "trie_empty \ ?trie" by(simp add: trie_keys_dom_lookup trie_lookup_empty) qed text \ Next, transfer the operations to the new type. The transfer package does a good job here. \ setup_lifting type_definition_trie \ \also sets up code generation\ lift_definition empty :: "('k :: cbl, 'v) trie" is trie_empty by(simp add: trie_keys_empty) lift_definition lookup :: "('k :: cbl, 'v) trie \ 'k \ 'v option" is "\t. trie_lookup t \ to_bl" . lift_definition update :: "'k \ 'v \ ('k :: cbl, 'v) trie \ ('k, 'v) trie" is "trie_update \ to_bl" by(auto simp add: trie_keys_dom_lookup trie_lookup_update) lift_definition keys :: "('k :: cbl, 'v) trie \ 'k set" is "\t. from_bl ` trie_keys t" . text \ And now we go for the properties. Note that some properties hold only if the type class operations are actually provided, i.e., @{term "cbl \ None"} in our example. \ lemma lookup_empty: "lookup empty = Map.empty" by transfer(simp add: trie_lookup_empty fun_eq_iff) context fixes t :: "('k :: cbl, 'v) trie" assumes ID_cbl: "ID (cbl :: 'k cbl) \ None" begin lemma lookup_update: "lookup (update k v t) = (lookup t)(k \ v)" using ID_cbl by transfer(auto simp add: trie_lookup_update fun_eq_iff dest: inj_to_bl[THEN injD]) lemma keys_conv_dom_lookup: "keys t = dom (lookup t)" using ID_cbl by transfer(force simp add: trie_keys_dom_lookup to_bl_inverse intro: rev_image_eqI) end subsection \Connecting to the container\ text_raw \\label{subsection:connect:container}\ text \ Connecting to the container (@{typ "('a, 'b) mapping"} in our example) takes three steps: \begin{enumerate} \item Define a new pseudo-constructor \item Implement the container operations for the new type \item Configure the heuristics to automatically pick an implementation \item Test thoroughly \end{enumerate} Thorough testing is particularly important, because Isabelle does not check whether you have implemented all your operations, whether you have configured your heuristics sensibly, nor whether your implementation always terminates. \ subsubsection \Define a new pseudo-constructor\ text \ Define a function that returns the abstract container view for a data structure value, and declare it as a datatype constructor for code generation with \isamarkuptrue\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse. Unfortunately, you have to repeat all existing pseudo-constructors, because there is no way to extract the current set of pseudo-constructors from the code generator. We call them pseudo-constructors, because they do not behave like datatype constructors in the logic. For example, ours are neither injective nor disjoint. \ definition Trie_Mapping :: "('k :: cbl, 'v) trie \ ('k, 'v) mapping" where [simp, code del]: "Trie_Mapping t = Mapping.Mapping (lookup t)" code_datatype Assoc_List_Mapping RBT_Mapping Mapping Trie_Mapping subsubsection \Implement the operations\ text \ Next, you have to prove and declare code equations that implement the container operations for the new implementation. Typically, these just dispatch to the operations on the type from \S\ref{subsection:hide:invariants}. Some operations depend on the type class operations from \S\ref{subsection:introduce:type:class} being defined; then, the code equation must check that the operations are indeed defined. If not, there is usually no way to implement the operation, so the code should raise an exception. Logically, we use the function @{term "Code.abort"} of type @{typ "String.literal \ (unit \ 'a) \ 'a"} with definition @{term "\_ f. f ()"}, but the generated code raises an exception \texttt{Fail} with the given message (the unit closure avoids non-termination in strict languages). This function gets the exception message and the unit-closure of the equation's left-hand side as argument, because it is then trivial to prove equality. Again, we only show a small set of operations; a realistic implementation should cover as many as possible. \ context fixes t :: "('k :: cbl, 'v) trie" begin lemma lookup_Trie_Mapping [code]: "Mapping.lookup (Trie_Mapping t) = lookup t" \ \Lookup does not need the check on @{term cbl}, because we have defined the pseudo-constructor @{term Trie_Mapping} in terms of @{term "lookup"}\ by simp(transfer, simp) lemma update_Trie_Mapping [code]: "Mapping.update k v (Trie_Mapping t) = (case ID cbl :: 'k cbl of None \ Code.abort (STR ''update Trie_Mapping: cbl = None'') (\_. Mapping.update k v (Trie_Mapping t)) | Some _ \ Trie_Mapping (update k v t))" by(simp split: option.split add: lookup_update Mapping.update.abs_eq) lemma keys_Trie_Mapping [code]: "Mapping.keys (Trie_Mapping t) = (case ID cbl :: 'k cbl of None \ Code.abort (STR ''keys Trie_Mapping: cbl = None'') (\_. Mapping.keys (Trie_Mapping t)) | Some _ \ keys t)" by(simp add: Mapping.keys.abs_eq keys_conv_dom_lookup split: option.split) end text \ These equations do not replace the existing equations for the other constructors, but they do take precedence over them. If there is already a generic implementation for an operation @{term "foo"}, say @{term "foo A = gen_foo A"}, and you prove a specialised equation @{term "foo (Trie_Mapping t) = trie_foo t"}, then when you call @{term "foo"} on some @{term "Trie_Mapping t"}, your equation will kick in. LC exploits this sequentiality especially for binary operators on sets like @{term "(\)"}, where there are generic implementations and faster specialised ones. \ subsubsection \Configure the heuristics\ text \ Finally, you should setup the heuristics that automatically picks a container implementation based on the types of the elements (\S\ref{subsection:set_impl}). The heuristics uses a type with a single value, e.g., @{typ mapping_impl} with value @{term Mapping_IMPL}, but there is one pseudo-constructor for each container implementation in the generated code. All these pseudo-constructors are the same in the logic, but they are different in the generated code. Hence, the generated code can distinguish them, but we do not have to commit to anything in the logic. This allows to reconfigure and extend the heuristic at any time. First, define and declare a new pseudo-constructor for the heuristics. Again, be sure to redeclare all previous pseudo-constructors. \ definition mapping_Trie :: mapping_impl where [simp]: "mapping_Trie = Mapping_IMPL" code_datatype mapping_Choose mapping_Assoc_List mapping_RBT mapping_Mapping mapping_Trie text \ Then, adjust the implementation of the automatic choice. For every initial value of the container (such as the empty map or the empty set), there is one new constant (e.g., @{term mapping_empty_choose} and @{term set_empty_choose}) equivalent to it. Its code equation, however, checks the available operations from the type classes and picks an appropriate implementation. For example, the following prefers red-black trees over tries, but tries over associative lists: \ lemma mapping_empty_choose_code [code]: "(mapping_empty_choose :: ('a :: {ccompare, cbl}, 'b) mapping) = (case ID CCOMPARE('a) of Some _ \ RBT_Mapping RBT_Mapping2.empty | None \ case ID (cbl :: 'a cbl) of Some _ \ Trie_Mapping empty | None \ Assoc_List_Mapping DAList.empty)" by(auto split: option.split simp add: DAList.lookup_empty[abs_def] Mapping.empty_def lookup_empty) text \ There is also a second function for every such initial value that dispatches on the pseudo-constructors for @{typ mapping_impl}. This function is used to pick the right implementation for types that specify a preference. \ lemma mapping_empty_code [code]: "mapping_empty mapping_Trie = Trie_Mapping empty" by(simp add: lookup_empty Mapping.empty_def) text \ For @{typ "('k, 'v) mapping"}, LC also has a function @{term "mapping_impl_choose2"} which is given two preferences and returns one (for @{typ "'a set"}, it is called @{term "set_impl_choose2"}). Polymorphic type constructors like @{typ "'a + 'b"} use it to pick an implementation based on the preferences of @{typ "'a"} and @{typ "'b"}. By default, it returns @{term mapping_Choose}, i.e., ignore the preferences. You should add a code equation like the following that overrides this choice if both preferences are your new data structure: \ lemma mapping_impl_choose2_Trie [code]: "mapping_impl_choose2 mapping_Trie mapping_Trie = mapping_Trie" by(simp add: mapping_Trie_def) text \ If your new data structure is better than the existing ones for some element type, you should reconfigure the type's preferene. As all preferences are logically equal, you can prove (and declare) the appropriate code equation. For example, the following prefers tries for keys of type @{typ "unit"}: \ lemma mapping_impl_unit_Trie [code]: "MAPPING_IMPL(unit) = Phantom(unit) mapping_Trie" by(simp add: mapping_impl_unit_def) value "Mapping.empty :: (unit, int) mapping" text \ You can also use your new pseudo-constructor with \derive\ in instantiations, just give its name as option: \ derive (mapping_Trie) mapping_impl simple_tycon section \Changing the configuration\ text \ As containers are connected to data structures only by refinement in the code generator, this can always be adapted later on. You can add new data structures as explained in \S\ref{section:new:implementation}. If you want to drop one, you redeclare the remaining pseudo-constructors with \isamarkuptrue\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse{} and delete all code equations that pattern-match on the obsolete pseudo-constructors. The command \isamarkuptrue\isacommand{code{\isacharunderscore}thms}\isamarkupfalse{} will tell you which constants have such code equations. You can also freely adapt the heuristics for picking implementations as described in \S\ref{subsection:connect:container}. One thing, however, you cannot change afterwards, namely the decision whether an element type supports an operation and if so how it does, because this decision is visible in the logic. \ section \New containers types\ text \ We hope that the above explanations and the examples with sets and maps suffice to show what you need to do if you add a new container type, e.g., priority queues. There are three steps: \begin{enumerate} \item \textbf{Introduce a type constructor for the container.} \\ Your new container type must not be a composite type, like @{typ "'a \ 'b option"} for maps, because refinement for code generation only works with a single type constructor. Neither should you reuse a type constructor that is used already in other contexts, e.g., do not use @{typ "'a list"} to model queues. Introduce a new type constructor if necessary (e.g., @{typ "('a, 'b) mapping"} for maps) -- if your container type already has its own type constructor, everything is fine. \item \textbf{Implement the data structures} \\ and connect them to the container type as described in \S\ref{section:new:implementation}. \item \textbf{Define a heuristics for picking an implementation.} \\ See \cite{Lochbihler2013ITP} for an explanation. \end{enumerate} \ section \Troubleshooting\ text \ This section describes some difficulties in using LC that we have come across, provides some background for them, and discusses how to overcome them. If you experience other difficulties, please contact the author. \ subsection \Nesting of mappings\ text \ Mappings can be arbitrarily nested on the value side, e.g., @{typ "('a, ('b, 'c) mapping) mapping"}. However, @{typ "('a, 'b) mapping"} cannot currently be the key of a mapping, i.e., code generation fails for @{typ "(('a, 'b) mapping, 'c) mapping"}. Simiarly, you cannot have a set of mappings like @{typ "('a, 'b) mapping set"} at the moment. There are no issues to make this work, we have just not seen the need for it. If you need to generate code for such types, please get in touch with the author. \ subsection \Wellsortedness errors\ text_raw \\label{subsection:well:sortedness}\ text \ LC uses its own hierarchy of type classes which is distinct from Isabelle/HOL's. This ensures that every type can be made an instance of LC's type classes. Consequently, you must instantiate these classes for your own types. The following lists where you can find information about the classes and examples how to instantiate them: \begin{center} \begin{tabular}{lll} \textbf{type class} & \textbf{user guide} & \textbf{theory} \\ @{class card_UNIV} & \S\ref{subsection:card_UNIV} & @{theory "HOL-Library.Cardinality"} %@{term "Cardinality.card_UNIV_class"} \\ @{class cenum} & \S\ref{subsection:cenum} & @{theory Containers.Collection_Enum} %@{term "Collection_Enum.cenum_class"} \\ @{class ceq} & \S\ref{subsection:ceq} & @{theory Containers.Collection_Eq} %@{term "Collection_Eq.ceq_class"} \\ @{class ccompare} & \S\ref{subsection:ccompare} & @{theory Containers.Collection_Order} %@{term "Collection_Order.ccompare_class"} \\ @{class cproper_interval} & \S\ref{subsection:cproper_interval} & @{theory Containers.Collection_Order} %@{term "Collection_Order.cproper_interval_class"} \\ @{class finite_UNIV} & \S\ref{subsection:finite_UNIV} & @{theory "HOL-Library.Cardinality"} %@{term "Cardinality.finite_UNIV_class"} \\ @{class mapping_impl} & \S\ref{subsection:mapping_impl} & @{theory Containers.Mapping_Impl} %@{term "Mapping_Impl.mapping_impl_class"} \\ @{class set_impl} & \S\ref{subsection:set_impl} & @{theory Containers.Set_Impl} %@{term "Set_Impl.set_impl_class"} \\ \end{tabular} \end{center} The type classes @{class card_UNIV} and @{class cproper_interval} are only required to implement the operations on set complements. If your code does not need complements, you can manually delete the code equations involving @{const "Complement"}, the theorem list @{thm [source] set_complement_code} collects them. It is also recommended that you remove the pseudo-constructor @{const Complement} from the code generator. Note that some set operations like @{term "A - B"} and @{const UNIV} have no code equations any more. \ declare set_complement_code[code del] code_datatype Collect_set DList_set RBT_set Set_Monad (*<*) datatype minimal_sorts = Minimal_Sorts bool derive (eq) ceq minimal_sorts derive (no) ccompare minimal_sorts derive (monad) set_impl minimal_sorts derive (no) cenum minimal_sorts value "{Minimal_Sorts True} \ {} \ Minimal_Sorts ` {True, False}" (*>*) subsection \Exception raised at run-time\ text_raw \\label{subsection:set_impl_unsupported_operation}\ text \ Not all combinations of data and container implementation are possible. For example, you cannot implement a set of functions with a RBT, because there is no order on @{typ "'a \ 'b"}. If you try, the code will raise an exception \texttt{Fail} (with an exception message) or \texttt{Match}. They can occur in three cases: \begin{enumerate} \item You have misconfigured the heuristics that picks implementations (\S\ref{subsection:set_impl}), or you have manually picked an implementation that requires an operation that the element type does not provide. Printing a stack trace for the exception may help you in locating the error. \item You are trying to invoke an operation on a set complement which cannot be implemented on a complement representation, e.g., @{term "(`)"}. If the element type is enumerable, provide an instance of @{class cenum} and choose to represent complements of sets of enumerable types by the elements rather than the elements of the complement (see \S\ref{subsection:cenum} for how to do this). \item You use set comprehensions on types which do not provide an enumeration (i.e., they are represented as closures) or you chose to represent a map as a closure. A lot of operations are not implementable for closures, in particular those that return some element of the container Inspect the code equations with \isacommand{code{\isacharunderscore}thms} and look for calls to @{term "Collect_set"} and @{term "Mapping"} which are LC's constructor for sets and maps as closures. Note that the code generator preprocesses set comprehensions like @{term "{i < 4|i :: int. i > 2}"} to @{term "(\i :: int. i < 4) ` {i. i > 2}"}, so this is a set comprehension over @{typ int} rather than @{typ bool}. \end{enumerate} \ (*<*) definition test_set_impl_unsupported_operation1 :: "unit \ (int \ int) set" where "test_set_impl_unsupported_operation1 _ = RBT_set RBT_Set2.empty \ {}" definition test_set_impl_unsupported_operation2 :: "unit \ bool set" where "test_set_impl_unsupported_operation2 _ = {i < 4 | i :: int. i > 2}" definition test_mapping_impl_unsupported_operation :: "unit \ bool" where "test_mapping_impl_unsupported_operation _ = Mapping.is_empty (RBT_Mapping (RBT_Mapping2.empty) :: (Enum.finite_4, unit) mapping)" ML_val \ fun test_fail s f = let fun error s' = Fail ("exception Fail \"" ^ s ^ "\" expected, but got " ^ s') in (f (); raise (error "no exception") ) handle Fail s' => if s = s' then () else raise (error s') end; test_fail "union RBT_set Set_Monad: ccompare = None" @{code test_set_impl_unsupported_operation1}; test_fail "image Collect_set" @{code test_set_impl_unsupported_operation2}; test_fail "is_empty RBT_Mapping: ccompare = None" @{code test_mapping_impl_unsupported_operation}; \ (*>*) subsection \LC slows down my code\ text \ Normally, this will not happen, because LC's data structures are more efficient than Isabelle's list-based implementations. However, in some rare cases, you can experience a slowdown: \ (*<*) definition tiny_set :: "nat set" where tiny_set_code: "tiny_set = {1, 2}" (*>*) text_raw \ \isastyletext \begin{enumerate} \item \textbf{Your containers contain just a few elements.} \\ In that case, the overhead of the heuristics to pick an implementation outweighs the benefits of efficient implementations. You should identify the tiny containers and disable the heuristics locally. You do so by replacing the initial value like @{term "{}"} and @{term "Mapping.empty"} with low-overhead constructors like @{term "Set_Monad"} and @{term "Mapping"}. For example, if @{thm [source] tiny_set_code}: @{thm tiny_set_code} is your code equation with a tiny set, the following changes the code equation to directly use the list-based representation, i.e., disables the heuristics: \par \ lemma empty_Set_Monad: "{} = Set_Monad []" by simp declare tiny_set_code[code del, unfolded empty_Set_Monad, code] text_raw \ \isastyletext \par If you want to globally disable the heuristics, you can also declare an equation like @{thm [source] empty_Set_Monad} as [code]. \item \textbf{The element type contains many type constructors and some type variables.} \\ LC heavily relies on type classes, and type classes are implemented as dictionaries if the compiler cannot statically resolve them, i.e., if there are type variables. For type constructors with type variables (like @{typ "'a * 'b"}), LC's definitions of the type class parameters recursively calls itself on the type variables, i.e., @{typ "'a"} and @{typ "'b"}. If the element type is polymorphic, the compiler cannot precompute these recursive calls and therefore they have to be constructed repeatedly at run time. If you wrap your complicated type in a new type constructor, you can define optimised equations for the type class parameters. \end{enumerate} \ (*<*) end (*>*) diff --git a/thys/Containers/ITP-2013/Benchmark_Set_Default.thy b/thys/Containers/ITP-2013/Benchmark_Set_Default.thy --- a/thys/Containers/ITP-2013/Benchmark_Set_Default.thy +++ b/thys/Containers/ITP-2013/Benchmark_Set_Default.thy @@ -1,22 +1,23 @@ theory Benchmark_Set_Default imports Benchmark_Set + "HOL-Library.Code_Cardinality" "HOL-Library.Code_Target_Nat" begin text \Implement set equality for all combinations of @{term "List.set"} and @{term "List.coset"}\ -lemma [code]: "equal_class.equal A B \ Cardinality.eq_set A B" +lemma [code]: "equal_class.equal A B \ Code_Cardinality.eq_set A B" by(simp add: equal_eq) ML_val \ val seed = (Code_Numeral.natural_of_integer 12345, Code_Numeral.natural_of_integer 67889); val n = @{code nat_of_integer} 30; val m = @{code nat_of_integer} 40; val c = @{code Benchmark_Set.complete} n m seed; \ notepad begin have "Benchmark_Set.complete 30 40 (12345, 67889) = (30, 4294967296)" by eval end end diff --git a/thys/Containers/ITP-2013/Benchmark_Set_LC.thy b/thys/Containers/ITP-2013/Benchmark_Set_LC.thy --- a/thys/Containers/ITP-2013/Benchmark_Set_LC.thy +++ b/thys/Containers/ITP-2013/Benchmark_Set_LC.thy @@ -1,88 +1,86 @@ theory Benchmark_Set_LC imports Benchmark_Set Containers.Set_Impl "HOL-Library.Code_Target_Nat" begin -lemma [code_unfold del]: "card \ Cardinality.card'" by(simp) - instantiation word :: (len) ceq begin definition "CEQ('a word) = Some (=)" instance by(intro_classes)(simp add: ceq_word_def) end instantiation word :: (len) compare begin definition "compare_word = (comparator_of :: 'a word comparator)" instance by(intro_classes)(simp add: compare_word_def comparator_of) end instantiation word :: (len) ccompare begin definition "CCOMPARE('a word) = Some compare" instance by(intro_classes)(simp add: ccompare_word_def comparator_compare) end instantiation word :: (len) set_impl begin definition "SET_IMPL('a word) = Phantom('a word) set_RBT" instance .. end instantiation word :: (len) proper_interval begin fun proper_interval_word :: "'a word option \ 'a word option \ bool" where "proper_interval_word None None = True" | "proper_interval_word None (Some y) = (y \ 0)" | "proper_interval_word (Some x) None = (x \ - 1)" | "proper_interval_word (Some x) (Some y) = (x < y \ x \ y - 1)" instance proof let ?pi = "proper_interval :: 'a word proper_interval" show "?pi None None = True" by simp fix y show "?pi None (Some y) = (\z. z < y)" using word_neq_0_conv [of y] by auto fix x show "?pi (Some x) None = (\z. x < z)" using word_order.not_eq_extremum [of x] by auto have "(x < y \ x \ y - 1) = (\z>x. z < y)" (is "?lhs \ ?rhs") proof assume ?lhs then obtain "x < y" "x \ y - 1" .. have "0 \ uint x" by simp also have "\ < uint y" using \x < y\ by(simp add: word_less_def) finally have "0 < uint y" . then have "y - 1 < y" by(simp add: word_less_def uint_sub_if' not_le) moreover from \0 < uint y\ \x < y\ \x \ y - 1\ have "x < y - 1" by(simp add: word_less_def uint_sub_if' uint_arith_simps(3)) ultimately show ?rhs by blast next assume ?rhs then obtain z where z: "x < z" "z < y" by blast have "0 \ uint z" by simp also have "\ < uint y" using \z < y\ by(simp add: word_less_def) finally show ?lhs using z by(auto simp add: word_less_def uint_sub_if') qed thus "?pi (Some x) (Some y) = (\z>x. z < y)" by simp qed end instantiation word :: (len) cproper_interval begin definition "cproper_interval = (proper_interval :: 'a word proper_interval)" instance by( intro_classes, simp add: cproper_interval_word_def ccompare_word_def compare_word_def le_lt_comparator_of ID_Some proper_interval_class.axioms) end instantiation word :: (len) cenum begin definition "CENUM('a word) = None" instance by(intro_classes)(simp_all add: cEnum_word_def) end notepad begin have "Benchmark_Set.complete 30 40 (12345, 67899) = (32, 4294967296)" by eval end end diff --git a/thys/Containers/Set_Impl.thy b/thys/Containers/Set_Impl.thy --- a/thys/Containers/Set_Impl.thy +++ b/thys/Containers/Set_Impl.thy @@ -1,2071 +1,2035 @@ (* Title: Containers/Set_Impl.thy Author: Andreas Lochbihler, KIT René Thiemann, UIBK *) theory Set_Impl imports Collection_Enum DList_Set RBT_Set2 Closure_Set Containers_Generator Complex_Main begin section \Different implementations of sets\ subsection \Auxiliary functions\ text \A simple quicksort implementation\ context ord begin function (sequential) quicksort_acc :: "'a list \ 'a list \ 'a list" and quicksort_part :: "'a list \ 'a \ 'a list \ 'a list \ 'a list \ 'a list \ 'a list" where "quicksort_acc ac [] = ac" | "quicksort_acc ac [x] = x # ac" | "quicksort_acc ac (x # xs) = quicksort_part ac x [] [] [] xs" | "quicksort_part ac x lts eqs gts [] = quicksort_acc (eqs @ x # quicksort_acc ac gts) lts" | "quicksort_part ac x lts eqs gts (z # zs) = (if z > x then quicksort_part ac x lts eqs (z # gts) zs else if z < x then quicksort_part ac x (z # lts) eqs gts zs else quicksort_part ac x lts (z # eqs) gts zs)" by pat_completeness simp_all lemma length_quicksort_accp: "quicksort_acc_quicksort_part_dom (Inl (ac, xs)) \ length (quicksort_acc ac xs) = length ac + length xs" and length_quicksort_partp: "quicksort_acc_quicksort_part_dom (Inr (ac, x, lts, eqs, gts, zs)) \ length (quicksort_part ac x lts eqs gts zs) = length ac + 1 + length lts + length eqs + length gts + length zs" apply(induct rule: quicksort_acc_quicksort_part.pinduct) apply(simp_all add: quicksort_acc.psimps quicksort_part.psimps) done termination apply(relation "measure (case_sum (\(_, xs). 2 * length xs ^ 2) (\(_, _, lts, eqs, gts, zs). 2 * (length lts + length eqs + length gts + length zs) ^ 2 + length zs + 1))") apply(simp_all add: power2_eq_square add_mult_distrib add_mult_distrib2 length_quicksort_accp) done definition quicksort :: "'a list \ 'a list" where "quicksort = quicksort_acc []" lemma set_quicksort_acc [simp]: "set (quicksort_acc ac xs) = set ac \ set xs" and set_quicksort_part [simp]: "set (quicksort_part ac x lts eqs gts zs) = set ac \ {x} \ set lts \ set eqs \ set gts \ set zs" by(induct ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct)(auto split: if_split_asm) lemma set_quicksort [simp]: "set (quicksort xs) = set xs" by(simp add: quicksort_def) lemma distinct_quicksort_acc: "distinct (quicksort_acc ac xs) = distinct (ac @ xs)" and distinct_quicksort_part: "distinct (quicksort_part ac x lts eqs gts zs) = distinct (ac @ [x] @ lts @ eqs @ gts @ zs)" by(induct ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct) auto lemma distinct_quicksort [simp]: "distinct (quicksort xs) = distinct xs" by(simp add: quicksort_def distinct_quicksort_acc) end lemmas [code] = ord.quicksort_acc.simps quicksort_acc.simps ord.quicksort_part.simps quicksort_part.simps ord.quicksort_def quicksort_def context linorder begin lemma sorted_quicksort_acc: "\ sorted ac; \x \ set xs. \a \ set ac. x < a \ \ sorted (quicksort_acc ac xs)" and sorted_quicksort_part: "\ sorted ac; \y \ set lts \ {x} \ set eqs \ set gts \ set zs. \a \ set ac. y < a; \y \ set lts. y < x; \y \ set eqs. y = x; \y \ set gts. y > x \ \ sorted (quicksort_part ac x lts eqs gts zs)" proof(induction ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct) case 1 thus ?case by simp next case 2 thus ?case by(auto) next case 3 thus ?case by simp next case (4 ac x lts eqs gts) note ac_greater = \\y\set lts \ {x} \ set eqs \ set gts \ set []. \a\set ac. y < a\ have "sorted eqs" "set eqs \ {x}" using \\y\set eqs. y = x\ by(induct eqs)(simp_all) moreover have "\y \ set ac \ set gts. x \ y" using \\a\set gts. x < a\ ac_greater by auto moreover have "sorted (quicksort_acc ac gts)" using \sorted ac\ ac_greater by(auto intro: "4.IH") ultimately have "sorted (eqs @ x # quicksort_acc ac gts)" by(auto simp add: sorted_append) moreover have "\y\set lts. \a\set (eqs @ x # quicksort_acc ac gts). y < a" using \\y\set lts. y < x\ ac_greater \\a\set gts. x < a\ \\y\set eqs. y = x\ by fastforce ultimately show ?case by(simp add: "4.IH") next case 5 thus ?case by(simp add: not_less order_eq_iff) qed lemma sorted_quicksort [simp]: "sorted (quicksort xs)" by(simp add: quicksort_def sorted_quicksort_acc) lemma insort_key_append1: "\y \ set ys. f x < f y \ insort_key f x (xs @ ys) = insort_key f x xs @ ys" proof(induct xs) case Nil thus ?case by(cases ys) auto qed simp lemma insort_key_append2: "\y \ set xs. f x > f y \ insort_key f x (xs @ ys) = xs @ insort_key f x ys" by(induct xs) auto lemma sort_key_append: "\x\set xs. \y\set ys. f x < f y \ sort_key f (xs @ ys) = sort_key f xs @ sort_key f ys" by(induct xs)(simp_all add: insort_key_append1) definition single_list :: "'a \ 'a list" where "single_list a = [a]" lemma to_single_list: "x # xs = single_list x @ xs" by(simp add: single_list_def) lemma sort_snoc: "sort (xs @ [x]) = insort x (sort xs)" by(induct xs)(simp_all add: insort_left_comm) lemma sort_append_swap: "sort (xs @ ys) = sort (ys @ xs)" by(induct xs arbitrary: ys rule: rev_induct)(simp_all add: sort_snoc[symmetric]) lemma sort_append_swap2: "sort (xs @ ys @ zs) = sort (ys @ xs @ zs)" by(induct xs)(simp_all, subst (1 2) sort_append_swap, simp) lemma sort_Cons_append_swap: "sort (x # xs) = sort (xs @ [x])" by(subst sort_append_swap) simp lemma sort_append_Cons_swap: "sort (ys @ x # xs) = sort (ys @ xs @ [x])" apply(induct ys) apply(simp only: append.simps sort_Cons_append_swap) apply simp done lemma quicksort_acc_conv_sort: "quicksort_acc ac xs = sort xs @ ac" and quicksort_part_conv_sort: "\ \y \ set lts. y < x; \y \ set eqs. y = x; \y \ set gts. y > x \ \ quicksort_part ac x lts eqs gts zs = sort (lts @ eqs @ gts @ x # zs) @ ac" proof(induct ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct) case 1 thus ?case by simp next case 2 thus ?case by simp next case 3 thus ?case by simp next case (4 ac x lts eqs gts) note eqs = \\y\set eqs. y = x\ { fix eqs assume "\y\set eqs. y = x" hence "insort x eqs = x # eqs" by(induct eqs) simp_all } note [simp] = this from eqs have [simp]: "sort eqs = eqs" by(induct eqs) simp_all from eqs have [simp]: "eqs @ [x] = x # eqs" by(induct eqs) simp_all show ?case using 4 apply(subst sort_key_append) apply(auto 4 3 dest: bspec)[1] apply(simp add: append_assoc[symmetric] sort_snoc del: append_assoc) apply(subst sort_key_append) apply(auto 4 3 simp add: insort_key_append1 dest: bspec) done next case (5 ac x lts eqs gts z zs) have "\ \ z < x; \ x < z \ \ z = x" by simp thus ?case using 5 apply(simp del: sort_key_simps) apply(safe, simp_all del: sort_key_simps add: to_single_list) apply(subst sort_append_swap) apply(fold append_assoc) apply(subst (2) sort_append_swap) apply(subst sort_append_swap2) apply(unfold append_assoc) apply(rule refl) apply(subst (1 5) append_assoc[symmetric]) apply(subst (1 2) sort_append_swap) apply(unfold append_assoc) apply(subst sort_append_swap2) apply(subst (1 2) sort_append_swap) apply(unfold append_assoc) apply(subst sort_append_swap2) apply(rule refl) apply(subst (2 6) append_assoc[symmetric]) apply(subst (2 5) append_assoc[symmetric]) apply(subst (1 2) sort_append_swap2) apply(subst (4) append_assoc) apply(subst (2) sort_append_swap2) apply simp done qed lemma quicksort_conv_sort: "quicksort xs = sort xs" by(simp add: quicksort_def quicksort_acc_conv_sort) lemma sort_remdups: "sort (remdups xs) = remdups (sort xs)" by(rule sorted_distinct_set_unique) simp_all end text \Removing duplicates from a sorted list\ context ord begin fun remdups_sorted :: "'a list \ 'a list" where "remdups_sorted [] = []" | "remdups_sorted [x] = [x]" | "remdups_sorted (x#y#xs) = (if x < y then x # remdups_sorted (y#xs) else remdups_sorted (y#xs))" end lemmas [code] = ord.remdups_sorted.simps context linorder begin lemma [simp]: assumes "sorted xs" shows sorted_remdups_sorted: "sorted (remdups_sorted xs)" and set_remdups_sorted: "set (remdups_sorted xs) = set xs" using assms by(induct xs rule: remdups_sorted.induct)(auto) lemma distinct_remdups_sorted [simp]: "sorted xs \ distinct (remdups_sorted xs)" by(induct xs rule: remdups_sorted.induct)(auto) lemma remdups_sorted_conv_remdups: "sorted xs \ remdups_sorted xs = remdups xs" by(induct xs rule: remdups_sorted.induct)(auto) end text \An specialised operation to convert a finite set into a sorted list\ definition csorted_list_of_set :: "'a :: ccompare set \ 'a list" where [code del]: "csorted_list_of_set A = (if ID CCOMPARE('a) = None \ \ finite A then undefined else linorder.sorted_list_of_set cless_eq A)" lemma csorted_list_of_set_set [simp]: "\ ID CCOMPARE('a :: ccompare) = Some c; linorder.sorted (le_of_comp c) xs; distinct xs \ \ linorder.sorted_list_of_set (le_of_comp c) (set xs) = xs" by(simp add: distinct_remdups_id linorder.sorted_list_of_set_sort_remdups[OF ID_ccompare] linorder.sorted_sort_id[OF ID_ccompare]) lemma csorted_list_of_set_split: fixes A :: "'a :: ccompare set" shows "P (csorted_list_of_set A) \ (\xs. ID CCOMPARE('a) \ None \ finite A \ A = set xs \ distinct xs \ linorder.sorted cless_eq xs \ P xs) \ (ID CCOMPARE('a) = None \ \ finite A \ P undefined)" by(auto simp add: csorted_list_of_set_def linorder.sorted_list_of_set[OF ID_ccompare]) code_identifier code_module Set \ (SML) Set_Impl | code_module Set_Impl \ (SML) Set_Impl subsection \Delete code equation with set as constructor\ lemma is_empty_unfold [code_unfold]: "set_eq A {} = Set.is_empty A" "set_eq {} A = Set.is_empty A" by(auto simp add: Set.is_empty_def set_eq_def) definition is_UNIV :: "'a set \ bool" where [code del]: "is_UNIV A \ A = UNIV" lemma is_UNIV_unfold [code_unfold]: "A = UNIV \ is_UNIV A" "UNIV = A \ is_UNIV A" "set_eq A UNIV \ is_UNIV A" "set_eq UNIV A \ is_UNIV A" by(auto simp add: is_UNIV_def set_eq_def) -lemma [code_unfold del, symmetric, code_post del]: - "x \ set xs \ List.member xs x" -by(simp add: List.member_def) - -lemma [code_unfold del, symmetric, code_post del]: - "finite \ Cardinality.finite'" by(simp) - -lemma [code_unfold del, symmetric, code_post del]: - "card \ Cardinality.card'" by simp - declare [[code drop: Set.empty Set.is_empty uminus_set_inst.uminus_set Set.member Set.insert Set.remove UNIV Set.filter image Set.subset_eq Ball Bex Set.union minus_set_inst.minus_set Set.inter card Set.bind the_elem Pow sum Gcd Lcm Product_Type.product Id_on Image trancl relcomp wf Min Inf_fin Max Sup_fin "Inf :: 'a set set \ 'a set" "Sup :: 'a set set \ 'a set" sorted_list_of_set List.map_project Sup_pred_inst.Sup_pred finite - Cardinality.finite' card - Cardinality.card' Inf_pred_inst.Inf_pred pred_of_set - Cardinality.subset' - Cardinality.eq_set Wellfounded.acc Bleast can_select - "set_eq :: 'a set \ 'a set \ bool" + (* "set_eq :: 'a set \ 'a set \ bool" *) irrefl bacc set_of_pred set_of_seq ]] -declare - Cardinality.finite'_def[code] - Cardinality.card'_def[code] - subsection \Set implementations\ definition Collect_set :: "('a \ bool) \ 'a set" where [simp]: "Collect_set = Collect" definition DList_set :: "'a :: ceq set_dlist \ 'a set" where "DList_set = Collect o DList_Set.member" definition RBT_set :: "'a :: ccompare set_rbt \ 'a set" where "RBT_set = Collect o RBT_Set2.member" definition Complement :: "'a set \ 'a set" where [simp]: "Complement A = - A" definition Set_Monad :: "'a list \ 'a set" where [simp]: "Set_Monad = set" code_datatype Collect_set DList_set RBT_set Set_Monad Complement lemma DList_set_empty [simp]: "DList_set DList_Set.empty = {}" by(simp add: DList_set_def) lemma RBT_set_empty [simp]: "RBT_set RBT_Set2.empty = {}" by(simp add: RBT_set_def) lemma RBT_set_conv_keys: "ID CCOMPARE('a :: ccompare) \ None \ RBT_set (t :: 'a set_rbt) = set (RBT_Set2.keys t)" by(clarsimp simp add: RBT_set_def member_conv_keys) subsection \Set operations\ text \ A collection of all the theorems about @{const Complement}. \ ML \ structure Set_Complement_Eqs = Named_Thms ( val name = @{binding set_complement_code} val description = "Code equations involving set complement" ) \ setup \Set_Complement_Eqs.setup\ text \Various fold operations over sets\ typedef ('a, 'b) comp_fun_commute = "{f :: 'a \ 'b \ 'b. comp_fun_commute f}" morphisms comp_fun_commute_apply Abs_comp_fun_commute by(rule exI[where x="\_. id"])(simp, unfold_locales, auto) setup_lifting type_definition_comp_fun_commute lemma comp_fun_commute_apply' [simp]: "comp_fun_commute_on UNIV (comp_fun_commute_apply f)" using comp_fun_commute_apply[of f] by (simp add: comp_fun_commute_def') lift_definition set_fold_cfc :: "('a, 'b) comp_fun_commute \ 'b \ 'a set \ 'b" is "Finite_Set.fold" . declare [[code drop: set_fold_cfc]] lemma set_fold_cfc_code [code]: fixes xs :: "'a :: ceq list" and dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows set_fold_cfc_Complement[set_complement_code]: "set_fold_cfc f''' b (Complement A) = Code.abort (STR ''set_fold_cfc not supported on Complement'') (\_. set_fold_cfc f''' b (Complement A))" and "set_fold_cfc f''' b (Collect_set P) = Code.abort (STR ''set_fold_cfc not supported on Collect_set'') (\_. set_fold_cfc f''' b (Collect_set P))" "set_fold_cfc f b (Set_Monad xs) = (case ID CEQ('a) of None \ Code.abort (STR ''set_fold_cfc Set_Monad: ceq = None'') (\_. set_fold_cfc f b (Set_Monad xs)) | Some eq \ List.fold (comp_fun_commute_apply f) (equal_base.list_remdups eq xs) b)" (is ?Set_Monad) "set_fold_cfc f' b (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''set_fold_cfc DList_set: ceq = None'') (\_. set_fold_cfc f' b (DList_set dxs)) | Some _ \ DList_Set.fold (comp_fun_commute_apply f') dxs b)" (is ?DList_set) "set_fold_cfc f'' b (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''set_fold_cfc RBT_set: ccompare = None'') (\_. set_fold_cfc f'' b (RBT_set rbt)) | Some _ \ RBT_Set2.fold (comp_fun_commute_apply f'') rbt b)" (is ?RBT_set) proof - note fold_set_fold_remdups = comp_fun_commute_def' comp_fun_commute_on.fold_set_fold_remdups[OF _ subset_UNIV] show ?Set_Monad by(auto split: option.split dest!: Collection_Eq.ID_ceq simp add: set_fold_cfc_def fold_set_fold_remdups) show ?DList_set apply(auto split: option.splits simp add: DList_set_def) apply transfer apply(auto dest: Collection_Eq.ID_ceq simp add: List.member_def[abs_def] fold_set_fold_remdups distinct_remdups_id) done show ?RBT_set apply(auto split: option.split simp add: RBT_set_conv_keys fold_conv_fold_keys) apply transfer apply(simp add: fold_set_fold_remdups distinct_remdups_id linorder.distinct_keys[OF ID_ccompare] ord.is_rbt_rbt_sorted) done qed simp_all typedef ('a, 'b) comp_fun_idem = "{f :: 'a \ 'b \ 'b. comp_fun_idem f}" morphisms comp_fun_idem_apply Abs_comp_fun_idem by(rule exI[where x="\_. id"])(simp, unfold_locales, auto) setup_lifting type_definition_comp_fun_idem lemma comp_fun_idem_apply' [simp]: "comp_fun_idem_on UNIV (comp_fun_idem_apply f)" using comp_fun_idem_apply[of f] by (simp add: comp_fun_idem_def') lift_definition set_fold_cfi :: "('a, 'b) comp_fun_idem \ 'b \ 'a set \ 'b" is "Finite_Set.fold" . declare [[code drop: set_fold_cfi]] lemma set_fold_cfi_code [code]: fixes xs :: "'a list" and dxs :: "'b :: ceq set_dlist" and rbt :: "'c :: ccompare set_rbt" shows "set_fold_cfi f b (Complement A) = Code.abort (STR ''set_fold_cfi not supported on Complement'') (\_. set_fold_cfi f b (Complement A))" "set_fold_cfi f b (Collect_set P) = Code.abort (STR ''set_fold_cfi not supported on Collect_set'') (\_. set_fold_cfi f b (Collect_set P))" "set_fold_cfi f b (Set_Monad xs) = List.fold (comp_fun_idem_apply f) xs b" (is ?Set_Monad) "set_fold_cfi f' b (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''set_fold_cfi DList_set: ceq = None'') (\_. set_fold_cfi f' b (DList_set dxs)) | Some _ \ DList_Set.fold (comp_fun_idem_apply f') dxs b)" (is ?DList_set) "set_fold_cfi f'' b (RBT_set rbt) = (case ID CCOMPARE('c) of None \ Code.abort (STR ''set_fold_cfi RBT_set: ccompare = None'') (\_. set_fold_cfi f'' b (RBT_set rbt)) | Some _ \ RBT_Set2.fold (comp_fun_idem_apply f'') rbt b)" (is ?RBT_set) proof - show ?Set_Monad by(auto split: option.split dest!: Collection_Eq.ID_ceq simp add: set_fold_cfi_def comp_fun_idem_def' comp_fun_idem_on.fold_set_fold[OF _ subset_UNIV]) show ?DList_set apply(auto split: option.split simp add: DList_set_def) apply transfer apply(auto dest: Collection_Eq.ID_ceq simp add: List.member_def[abs_def] comp_fun_idem_def' comp_fun_idem_on.fold_set_fold[OF _ subset_UNIV]) done show ?RBT_set apply(auto split: option.split simp add: RBT_set_conv_keys fold_conv_fold_keys) apply transfer apply(simp add: comp_fun_idem_def' comp_fun_idem_on.fold_set_fold[OF _ subset_UNIV]) done qed simp_all typedef 'a semilattice_set = "{f :: 'a \ 'a \ 'a. semilattice_set f}" morphisms semilattice_set_apply Abs_semilattice_set proof show "(\x y. if x = y then x else undefined) \ ?semilattice_set" unfolding mem_Collect_eq by(unfold_locales) simp_all qed setup_lifting type_definition_semilattice_set lemma semilattice_set_apply' [simp]: "semilattice_set (semilattice_set_apply f)" using semilattice_set_apply[of f] by simp lemma comp_fun_idem_semilattice_set_apply [simp]: "comp_fun_idem_on UNIV (semilattice_set_apply f)" proof - interpret semilattice_set "semilattice_set_apply f" by simp show ?thesis by(unfold_locales)(simp_all add: fun_eq_iff left_commute) qed lift_definition set_fold1 :: "'a semilattice_set \ 'a set \ 'a" is "semilattice_set.F" . lemma (in semilattice_set) F_set_conv_fold: "xs \ [] \ F (set xs) = Finite_Set.fold f (hd xs) (set (tl xs))" by(clarsimp simp add: neq_Nil_conv eq_fold) lemma set_fold1_code [code]: fixes rbt :: "'a :: {ccompare, lattice} set_rbt" and dxs :: "'b :: {ceq, lattice} set_dlist" shows set_fold1_Complement[set_complement_code]: "set_fold1 f (Complement A) = Code.abort (STR ''set_fold1: Complement'') (\_. set_fold1 f (Complement A))" and "set_fold1 f (Collect_set P) = Code.abort (STR ''set_fold1: Collect_set'') (\_. set_fold1 f (Collect_set P))" and "set_fold1 f (Set_Monad (x # xs)) = fold (semilattice_set_apply f) xs x" (is "?Set_Monad") and "set_fold1 f' (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''set_fold1 DList_set: ceq = None'') (\_. set_fold1 f' (DList_set dxs)) | Some _ \ if DList_Set.null dxs then Code.abort (STR ''set_fold1 DList_set: empty set'') (\_. set_fold1 f' (DList_set dxs)) else DList_Set.fold (semilattice_set_apply f') (DList_Set.tl dxs) (DList_Set.hd dxs))" (is "?DList_set") and "set_fold1 f'' (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''set_fold1 RBT_set: ccompare = None'') (\_. set_fold1 f'' (RBT_set rbt)) | Some _ \ if RBT_Set2.is_empty rbt then Code.abort (STR ''set_fold1 RBT_set: empty set'') (\_. set_fold1 f'' (RBT_set rbt)) else RBT_Set2.fold1 (semilattice_set_apply f'') rbt)" (is "?RBT_set") proof - note fold_set_fold = comp_fun_idem_def' comp_fun_idem_on.fold_set_fold[OF _ subset_UNIV] show ?Set_Monad by(simp add: set_fold1_def semilattice_set.eq_fold fold_set_fold) show ?DList_set by(simp add: set_fold1_def semilattice_set.F_set_conv_fold fold_set_fold DList_set_def DList_Set.Collect_member split: option.split)(transfer, simp) show ?RBT_set by(simp add: set_fold1_def semilattice_set.F_set_conv_fold fold_set_fold RBT_set_def RBT_Set2.member_conv_keys RBT_Set2.fold1_conv_fold split: option.split) qed simp_all text \Implementation of set operations\ lemma Collect_code [code]: fixes P :: "'a :: cenum \ bool" shows "Collect P = (case ID CENUM('a) of None \ Collect_set P | Some (enum, _) \ Set_Monad (filter P enum))" by(auto split: option.split dest: in_cenum) lemma finite_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" and A :: "'c :: finite_UNIV set" and P :: "'c \ bool" shows "finite (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''finite DList_set: ceq = None'') (\_. finite (DList_set dxs)) | Some _ \ True)" "finite (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''finite RBT_set: ccompare = None'') (\_. finite (RBT_set rbt)) | Some _ \ True)" and finite_Complement [set_complement_code]: "finite (Complement A) \ (if of_phantom (finite_UNIV :: 'c finite_UNIV) then True else if finite A then False else Code.abort (STR ''finite Complement: infinite set'') (\_. finite (Complement A)))" and "finite (Set_Monad xs) = True" "finite (Collect_set P) \ of_phantom (finite_UNIV :: 'c finite_UNIV) \ Code.abort (STR ''finite Collect_set'') (\_. finite (Collect_set P))" by(auto simp add: DList_set_def RBT_set_def member_conv_keys card_gt_0_iff finite_UNIV split: option.split elim: finite_subset[rotated 1]) +lemma CARD_code [code_unfold]: + "CARD('a :: card_UNIV) = of_phantom (card_UNIV :: 'a card_UNIV)" +by(simp add: card_UNIV) + lemma card_code [code]: fixes dxs :: "'a :: ceq set_dlist" and xs :: "'a list" and rbt :: "'b :: ccompare set_rbt" and A :: "'c :: card_UNIV set" shows "card (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''card DList_set: ceq = None'') (\_. card (DList_set dxs)) | Some _ \ DList_Set.length dxs)" "card (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''card RBT_set: ccompare = None'') (\_. card (RBT_set rbt)) | Some _ \ length (RBT_Set2.keys rbt))" "card (Set_Monad xs) = (case ID CEQ('a) of None \ Code.abort (STR ''card Set_Monad: ceq = None'') (\_. card (Set_Monad xs)) | Some eq \ length (equal_base.list_remdups eq xs))" and card_Complement [set_complement_code]: "card (Complement A) = (let a = card A; s = CARD('c) in if s > 0 then s - a else if finite A then 0 else Code.abort (STR ''card Complement: infinite'') (\_. card (Complement A)))" by(auto simp add: RBT_set_def member_conv_keys distinct_card DList_set_def Let_def card_UNIV Compl_eq_Diff_UNIV card_Diff_subset_Int card_gt_0_iff finite_subset[of A UNIV] List.card_set dest: Collection_Eq.ID_ceq split: option.split) lemma is_UNIV_code [code]: fixes rbt :: "'a :: {cproper_interval, finite_UNIV} set_rbt" and A :: "'b :: card_UNIV set" shows "is_UNIV A \ (let a = CARD('b); b = card A in if a > 0 then a = b else if b > 0 then False else Code.abort (STR ''is_UNIV called on infinite type and set'') (\_. is_UNIV A))" (is ?generic) "is_UNIV (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''is_UNIV RBT_set: ccompare = None'') (\_. is_UNIV (RBT_set rbt)) | Some _ \ of_phantom (finite_UNIV :: 'a finite_UNIV) \ proper_intrvl.exhaustive_fusion cproper_interval rbt_keys_generator (RBT_Set2.init rbt))" (is ?rbt) proof - { fix c assume linorder: "ID CCOMPARE('a) = Some c" have "is_UNIV (RBT_set rbt) = (finite (UNIV :: 'a set) \ proper_intrvl.exhaustive cproper_interval (RBT_Set2.keys rbt))" (is "?lhs \ ?rhs") proof assume ?lhs have "finite (UNIV :: 'a set)" unfolding \?lhs\[unfolded is_UNIV_def, symmetric] using linorder by(simp add: finite_code) moreover hence "proper_intrvl.exhaustive cproper_interval (RBT_Set2.keys rbt)" using linorder \?lhs\ by(simp add: linorder_proper_interval.exhaustive_correct[OF ID_ccompare_interval[OF linorder]] sorted_RBT_Set_keys is_UNIV_def RBT_set_conv_keys) ultimately show ?rhs .. next assume ?rhs thus ?lhs using linorder by(auto simp add: linorder_proper_interval.exhaustive_correct[OF ID_ccompare_interval[OF linorder]] sorted_RBT_Set_keys is_UNIV_def RBT_set_conv_keys) qed } thus ?rbt by(auto simp add: finite_UNIV proper_intrvl.exhaustive_fusion_def unfoldr_rbt_keys_generator is_UNIV_def split: option.split) show ?generic by(auto simp add: Let_def is_UNIV_def dest: card_seteq[of UNIV A] dest!: card_ge_0_finite) qed lemma is_empty_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" and A :: "'c set" shows "Set.is_empty (Set_Monad xs) \ xs = []" "Set.is_empty (DList_set dxs) \ (case ID CEQ('a) of None \ Code.abort (STR ''is_empty DList_set: ceq = None'') (\_. Set.is_empty (DList_set dxs)) | Some _ \ DList_Set.null dxs)" (is ?DList_set) "Set.is_empty (RBT_set rbt) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''is_empty RBT_set: ccompare = None'') (\_. Set.is_empty (RBT_set rbt)) | Some _ \ RBT_Set2.is_empty rbt)" (is ?RBT_set) and is_empty_Complement [set_complement_code]: "Set.is_empty (Complement A) \ is_UNIV A" (is ?Complement) proof - show ?DList_set by(clarsimp simp add: DList_set_def Set.is_empty_def DList_Set.member_empty_empty split: option.split) show ?RBT_set by(clarsimp simp add: RBT_set_def Set.is_empty_def RBT_Set2.member_empty_empty[symmetric] fun_eq_iff simp del: RBT_Set2.member_empty_empty split: option.split) show ?Complement by(auto simp add: is_UNIV_def Set.is_empty_def) qed(simp_all add: Set.is_empty_def List.null_def) lemma Set_insert_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "\x. Set.insert x (Collect_set A) = (case ID CEQ('a) of None \ Code.abort (STR ''insert Collect_set: ceq = None'') (\_. Set.insert x (Collect_set A)) | Some eq \ Collect_set (equal_base.fun_upd eq A x True))" "\x. Set.insert x (Set_Monad xs) = Set_Monad (x # xs)" "\x. Set.insert x (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''insert DList_set: ceq = None'') (\_. Set.insert x (DList_set dxs)) | Some _ \ DList_set (DList_Set.insert x dxs))" "\x. Set.insert x (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''insert RBT_set: ccompare = None'') (\_. Set.insert x (RBT_set rbt)) | Some _ \ RBT_set (RBT_Set2.insert x rbt))" and insert_Complement [set_complement_code]: "\x. Set.insert x (Complement X) = Complement (Set.remove x X)" by(auto split: option.split dest: equal.equal_eq[OF ID_ceq] simp add: DList_set_def DList_Set.member_insert RBT_set_def) lemma Set_member_code [code]: fixes xs :: "'a :: ceq list" shows "\x. x \ Collect_set A \ A x" "\x. x \ DList_set dxs \ DList_Set.member dxs x" "\x. x \ RBT_set rbt \ RBT_Set2.member rbt x" and mem_Complement [set_complement_code]: "\x. x \ Complement X \ x \ X" and "\x. x \ Set_Monad xs \ (case ID CEQ('a) of None \ Code.abort (STR ''member Set_Monad: ceq = None'') (\_. x \ Set_Monad xs) | Some eq \ equal_base.list_member eq xs x)" by(auto simp add: DList_set_def RBT_set_def List.member_def split: option.split dest!: Collection_Eq.ID_ceq) lemma Set_remove_code [code]: fixes rbt :: "'a :: ccompare set_rbt" and dxs :: "'b :: ceq set_dlist" shows "\x. Set.remove x (Collect_set A) = (case ID CEQ('b) of None \ Code.abort (STR ''remove Collect: ceq = None'') (\_. Set.remove x (Collect_set A)) | Some eq \ Collect_set (equal_base.fun_upd eq A x False))" "\x. Set.remove x (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''remove DList_set: ceq = None'') (\_. Set.remove x (DList_set dxs)) | Some _ \ DList_set (DList_Set.remove x dxs))" "\x. Set.remove x (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''remove RBT_set: ccompare = None'') (\_. Set.remove x (RBT_set rbt)) | Some _ \ RBT_set (RBT_Set2.remove x rbt))" and remove_Complement [set_complement_code]: "\x A. Set.remove x (Complement A) = Complement (Set.insert x A)" by(auto split: option.split if_split_asm dest: equal.equal_eq[OF ID_ceq] simp add: DList_set_def DList_Set.member_remove RBT_set_def) lemma Set_uminus_code [code, set_complement_code]: "- A = Complement A" "- (Collect_set P) = Collect_set (\x. \ P x)" "- (Complement B) = B" by auto text \ These equations represent complements as true complements. If you want that the complement operations returns an explicit enumeration of the elements, use the following set of equations which use @{class cenum}. \ lemma Set_uminus_cenum: fixes A :: "'a :: cenum set" shows "- A = (case ID CENUM('a) of None \ Complement A | Some (enum, _) \ Set_Monad (filter (\x. x \ A) enum))" and "- (Complement B) = B" by(auto split: option.split dest: ID_cEnum) lemma Set_minus_code [code]: fixes rbt1 rbt2 :: "'a :: ccompare set_rbt" shows "A - B = A \ (- B)" "RBT_set rbt1 - RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''minus RBT_set RBT_set: ccompare = None'') (\_. RBT_set rbt1 - RBT_set rbt2) | Some _ \ RBT_set (RBT_Set2.minus rbt1 rbt2))" by (auto simp: Set_member_code(3) split: option.splits) lemma Set_union_code [code]: fixes rbt1 rbt2 :: "'a :: ccompare set_rbt" and rbt :: "'b :: {ccompare, ceq} set_rbt" and dxs :: "'b set_dlist" and dxs1 dxs2 :: "'c :: ceq set_dlist" shows "RBT_set rbt1 \ RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''union RBT_set RBT_set: ccompare = None'') (\_. RBT_set rbt1 \ RBT_set rbt2) | Some _ \ RBT_set (RBT_Set2.union rbt1 rbt2))" (is ?RBT_set_RBT_set) "RBT_set rbt \ DList_set dxs = (case ID CCOMPARE('b) of None \ Code.abort (STR ''union RBT_set DList_set: ccompare = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''union RBT_set DList_set: ceq = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ RBT_set (DList_Set.fold RBT_Set2.insert dxs rbt))" (is ?RBT_set_DList_set) "DList_set dxs \ RBT_set rbt = (case ID CCOMPARE('b) of None \ Code.abort (STR ''union DList_set RBT_set: ccompare = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''union DList_set RBT_set: ceq = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ RBT_set (DList_Set.fold RBT_Set2.insert dxs rbt))" (is ?DList_set_RBT_set) "DList_set dxs1 \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''union DList_set DList_set: ceq = None'') (\_. DList_set dxs1 \ DList_set dxs2) | Some _ \ DList_set (DList_Set.union dxs1 dxs2))" (is ?DList_set_DList_set) "Set_Monad zs \ RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''union Set_Monad RBT_set: ccompare = None'') (\_. Set_Monad zs \ RBT_set rbt2) | Some _ \ RBT_set (fold RBT_Set2.insert zs rbt2))" (is ?Set_Monad_RBT_set) "RBT_set rbt1 \ Set_Monad zs = (case ID CCOMPARE('a) of None \ Code.abort (STR ''union RBT_set Set_Monad: ccompare = None'') (\_. RBT_set rbt1 \ Set_Monad zs) | Some _ \ RBT_set (fold RBT_Set2.insert zs rbt1))" (is ?RBT_set_Set_Monad) "Set_Monad ws \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''union Set_Monad DList_set: ceq = None'') (\_. Set_Monad ws \ DList_set dxs2) | Some _ \ DList_set (fold DList_Set.insert ws dxs2))" (is ?Set_Monad_DList_set) "DList_set dxs1 \ Set_Monad ws = (case ID CEQ('c) of None \ Code.abort (STR ''union DList_set Set_Monad: ceq = None'') (\_. DList_set dxs1 \ Set_Monad ws) | Some _ \ DList_set (fold DList_Set.insert ws dxs1))" (is ?DList_set_Set_Monad) "Set_Monad xs \ Set_Monad ys = Set_Monad (xs @ ys)" "Collect_set A \ B = Collect_set (\x. A x \ x \ B)" "B \ Collect_set A = Collect_set (\x. A x \ x \ B)" and Set_union_Complement [set_complement_code]: "Complement B \ B' = Complement (B \ - B')" "B' \ Complement B = Complement (- B' \ B)" proof - show ?RBT_set_RBT_set ?Set_Monad_RBT_set ?RBT_set_Set_Monad by(auto split: option.split simp add: RBT_set_def) show ?RBT_set_DList_set ?DList_set_RBT_set by(auto split: option.split simp add: RBT_set_def DList_set_def DList_Set.fold_def DList_Set.member_def List.member_def dest: equal.equal_eq[OF ID_ceq]) show ?DList_set_Set_Monad ?Set_Monad_DList_set by(auto split: option.split simp add: DList_set_def DList_Set.member_fold_insert) show ?DList_set_DList_set by(auto split: option.split simp add: DList_set_def DList_Set.member_union) qed(auto) lemma Set_inter_code [code]: fixes rbt1 rbt2 :: "'a :: ccompare set_rbt" and rbt :: "'b :: {ccompare, ceq} set_rbt" and dxs :: "'b set_dlist" and dxs1 dxs2 :: "'c :: ceq set_dlist" and xs1 xs2 :: "'c list" shows "Collect_set A'' \ J = Collect_set (\x. A'' x \ x \ J)" (is ?collect1) "J \ Collect_set A'' = Collect_set (\x. A'' x \ x \ J)" (is ?collect2) "Set_Monad xs'' \ I = Set_Monad (filter (\x. x \ I) xs'')" (is ?monad1) "I \ Set_Monad xs'' = Set_Monad (filter (\x. x \ I) xs'')" (is ?monad2) "DList_set dxs1 \ H = (case ID CEQ('c) of None \ Code.abort (STR ''inter DList_set1: ceq = None'') (\_. DList_set dxs1 \ H) | Some eq \ DList_set (DList_Set.filter (\x. x \ H) dxs1))" (is ?dlist1) "H \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''inter DList_set2: ceq = None'') (\_. H \ DList_set dxs2) | Some eq \ DList_set (DList_Set.filter (\x. x \ H) dxs2))" (is ?dlist2) "RBT_set rbt1 \ G = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter RBT_set1: ccompare = None'') (\_. RBT_set rbt1 \ G) | Some _ \ RBT_set (RBT_Set2.filter (\x. x \ G) rbt1))" (is ?rbt1) "G \ RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter RBT_set2: ccompare = None'') (\_. G \ RBT_set rbt2) | Some _ \ RBT_set (RBT_Set2.filter (\x. x \ G) rbt2))" (is ?rbt2) and Set_inter_Complement [set_complement_code]: "Complement B'' \ Complement B''' = Complement (B'' \ B''')" (is ?complement) and "Set_Monad xs \ RBT_set rbt1 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter Set_Monad RBT_set: ccompare = None'') (\_. RBT_set rbt1 \ Set_Monad xs) | Some _ \ RBT_set (RBT_Set2.inter_list rbt1 xs))" (is ?monad_rbt) "Set_Monad xs' \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''inter Set_Monad DList_set: ceq = None'') (\_. Set_Monad xs' \ DList_set dxs2) | Some eq \ DList_set (DList_Set.filter (equal_base.list_member eq xs') dxs2))" (is ?monad_dlist) "Set_Monad xs1 \ Set_Monad xs2 = (case ID CEQ('c) of None \ Code.abort (STR ''inter Set_Monad Set_Monad: ceq = None'') (\_. Set_Monad xs1 \ Set_Monad xs2) | Some eq \ Set_Monad (filter (equal_base.list_member eq xs2) xs1))" (is ?monad) "DList_set dxs \ RBT_set rbt = (case ID CCOMPARE('b) of None \ Code.abort (STR ''inter DList_set RBT_set: ccompare = None'') (\_. DList_set dxs \ RBT_set rbt) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''inter DList_set RBT_set: ceq = None'') (\_. DList_set dxs \ RBT_set rbt) | Some _ \ RBT_set (RBT_Set2.inter_list rbt (list_of_dlist dxs)))" (is ?dlist_rbt) "DList_set dxs1 \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''inter DList_set DList_set: ceq = None'') (\_. DList_set dxs1 \ DList_set dxs2) | Some _ \ DList_set (DList_Set.filter (DList_Set.member dxs2) dxs1))" (is ?dlist) "DList_set dxs1 \ Set_Monad xs' = (case ID CEQ('c) of None \ Code.abort (STR ''inter DList_set Set_Monad: ceq = None'') (\_. DList_set dxs1 \ Set_Monad xs') | Some eq \ DList_set (DList_Set.filter (equal_base.list_member eq xs') dxs1))" (is ?dlist_monad) "RBT_set rbt1 \ RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter RBT_set RBT_set: ccompare = None'') (\_. RBT_set rbt1 \ RBT_set rbt2) | Some _ \ RBT_set (RBT_Set2.inter rbt1 rbt2))" (is ?rbt_rbt) "RBT_set rbt \ DList_set dxs = (case ID CCOMPARE('b) of None \ Code.abort (STR ''inter RBT_set DList_set: ccompare = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''inter RBT_set DList_set: ceq = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ RBT_set (RBT_Set2.inter_list rbt (list_of_dlist dxs)))" (is ?rbt_dlist) "RBT_set rbt1 \ Set_Monad xs = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter RBT_set Set_Monad: ccompare = None'') (\_. RBT_set rbt1 \ Set_Monad xs) | Some _ \ RBT_set (RBT_Set2.inter_list rbt1 xs))" (is ?rbt_monad) proof - show ?rbt_rbt ?rbt1 ?rbt2 ?rbt_dlist ?rbt_monad ?dlist_rbt ?monad_rbt by(auto simp add: RBT_set_def DList_set_def DList_Set.member_def List.member_def dest: equal.equal_eq[OF ID_ceq] split: option.split) show ?dlist ?dlist1 ?dlist2 ?dlist_monad ?monad_dlist ?monad ?monad1 ?monad2 ?collect1 ?collect2 ?complement by(auto simp add: DList_set_def List.member_def dest!: Collection_Eq.ID_ceq split: option.splits) qed lemma Set_bind_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "Set.bind (Set_Monad xs) f = fold ((\) \ f) xs (Set_Monad [])" (is ?Set_Monad) "Set.bind (DList_set dxs) f' = (case ID CEQ('a) of None \ Code.abort (STR ''bind DList_set: ceq = None'') (\_. Set.bind (DList_set dxs) f') | Some _ \ DList_Set.fold (union \ f') dxs {})" (is ?DList) "Set.bind (RBT_set rbt) f'' = (case ID CCOMPARE('b) of None \ Code.abort (STR ''bind RBT_set: ccompare = None'') (\_. Set.bind (RBT_set rbt) f'') | Some _ \ RBT_Set2.fold (union \ f'') rbt {})" (is ?RBT) proof - show ?Set_Monad by(simp add: set_bind_conv_fold) show ?DList by(auto simp add: DList_set_def DList_Set.member_def List.member_def List.member_def[abs_def] set_bind_conv_fold DList_Set.fold_def split: option.split dest: equal.equal_eq[OF ID_ceq] ID_ceq) show ?RBT by(clarsimp split: option.split simp add: RBT_set_def RBT_Set2.fold_conv_fold_keys RBT_Set2.member_conv_keys set_bind_conv_fold) qed lemma UNIV_code [code]: "UNIV = - {}" by(simp) lift_definition inf_sls :: "'a :: lattice semilattice_set" is "inf" by unfold_locales lemma Inf_fin_code [code]: "Inf_fin A = set_fold1 inf_sls A" by transfer(simp add: Inf_fin_def) lift_definition sup_sls :: "'a :: lattice semilattice_set" is "sup" by unfold_locales lemma Sup_fin_code [code]: "Sup_fin A = set_fold1 sup_sls A" by transfer(simp add: Sup_fin_def) lift_definition inf_cfi :: "('a :: lattice, 'a) comp_fun_idem" is "inf" by(rule comp_fun_idem_inf) lemma Inf_code: fixes A :: "'a :: complete_lattice set" shows "Inf A = (if finite A then set_fold_cfi inf_cfi top A else Code.abort (STR ''Inf: infinite'') (\_. Inf A))" by transfer(simp add: Inf_fold_inf) lift_definition sup_cfi :: "('a :: lattice, 'a) comp_fun_idem" is "sup" by(rule comp_fun_idem_sup) lemma Sup_code: fixes A :: "'a :: complete_lattice set" shows "Sup A = (if finite A then set_fold_cfi sup_cfi bot A else Code.abort (STR ''Sup: infinite'') (\_. Sup A))" by transfer(simp add: Sup_fold_sup) lemmas Inter_code [code] = Inf_code[where ?'a = "_ :: type set"] lemmas Union_code [code] = Sup_code[where ?'a = "_ :: type set"] lemmas Predicate_Inf_code [code] = Inf_code[where ?'a = "_ :: type Predicate.pred"] lemmas Predicate_Sup_code [code] = Sup_code[where ?'a = "_ :: type Predicate.pred"] lemmas Inf_fun_code [code] = Inf_code[where ?'a = "_ :: type \ _ :: complete_lattice"] lemmas Sup_fun_code [code] = Sup_code[where ?'a = "_ :: type \ _ :: complete_lattice"] lift_definition min_sls :: "'a :: linorder semilattice_set" is min by unfold_locales lemma Min_code [code]: "Min A = set_fold1 min_sls A" by transfer(simp add: Min_def) lift_definition max_sls :: "'a :: linorder semilattice_set" is max by unfold_locales lemma Max_code [code]: "Max A = set_fold1 max_sls A" by transfer(simp add: Max_def) text \ We do not implement @{term Ball}, @{term Bex}, and @{term sorted_list_of_set} for @{term Collect_set} using @{term cEnum}, because it should already have been converted to an explicit list of elements if that is possible. \ lemma Ball_code [code]: fixes rbt :: "'a :: ccompare set_rbt" and dxs :: "'b :: ceq set_dlist" shows "Ball (Set_Monad xs) P = list_all P xs" "Ball (DList_set dxs) P' = (case ID CEQ('b) of None \ Code.abort (STR ''Ball DList_set: ceq = None'') (\_. Ball (DList_set dxs) P') | Some _ \ DList_Set.dlist_all P' dxs)" "Ball (RBT_set rbt) P'' = (case ID CCOMPARE('a) of None \ Code.abort (STR ''Ball RBT_set: ccompare = None'') (\_. Ball (RBT_set rbt) P'') | Some _ \ RBT_Set2.all P'' rbt)" by(simp_all add: DList_set_def RBT_set_def list_all_iff dlist_all_conv_member RBT_Set2.all_conv_all_member split: option.splits) lemma Bex_code [code]: fixes rbt :: "'a :: ccompare set_rbt" and dxs :: "'b :: ceq set_dlist" shows "Bex (Set_Monad xs) P = list_ex P xs" "Bex (DList_set dxs) P' = (case ID CEQ('b) of None \ Code.abort (STR ''Bex DList_set: ceq = None'') (\_. Bex (DList_set dxs) P') | Some _ \ DList_Set.dlist_ex P' dxs)" "Bex (RBT_set rbt) P'' = (case ID CCOMPARE('a) of None \ Code.abort (STR ''Bex RBT_set: ccompare = None'') (\_. Bex (RBT_set rbt) P'') | Some _ \ RBT_Set2.ex P'' rbt)" by(simp_all add: DList_set_def RBT_set_def list_ex_iff dlist_ex_conv_member RBT_Set2.ex_conv_ex_member split: option.splits) lemma csorted_list_of_set_code [code]: fixes rbt :: "'a :: ccompare set_rbt" and dxs :: "'b :: {ccompare, ceq} set_dlist" and xs :: "'a :: ccompare list" shows "csorted_list_of_set (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''csorted_list_of_set RBT_set: ccompare = None'') (\_. csorted_list_of_set (RBT_set rbt)) | Some _ \ RBT_Set2.keys rbt)" "csorted_list_of_set (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''csorted_list_of_set DList_set: ceq = None'') (\_. csorted_list_of_set (DList_set dxs)) | Some _ \ case ID CCOMPARE('b) of None \ Code.abort (STR ''csorted_list_of_set DList_set: ccompare = None'') (\_. csorted_list_of_set (DList_set dxs)) | Some c \ ord.quicksort (lt_of_comp c) (list_of_dlist dxs))" "csorted_list_of_set (Set_Monad xs) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''csorted_list_of_set Set_Monad: ccompare = None'') (\_. csorted_list_of_set (Set_Monad xs)) | Some c \ ord.remdups_sorted (lt_of_comp c) (ord.quicksort (lt_of_comp c) xs))" by(auto split: option.split simp add: RBT_set_def DList_set_def DList_Set.Collect_member member_conv_keys sorted_RBT_Set_keys linorder.sorted_list_of_set_sort_remdups[OF ID_ccompare] linorder.quicksort_conv_sort[OF ID_ccompare] distinct_remdups_id distinct_list_of_dlist linorder.remdups_sorted_conv_remdups[OF ID_ccompare] linorder.sorted_sort[OF ID_ccompare] linorder.sort_remdups[OF ID_ccompare] csorted_list_of_set_def) lemma cless_set_code [code]: fixes rbt rbt' :: "'a :: ccompare set_rbt" and rbt1 rbt2 :: "'b :: cproper_interval set_rbt" and A B :: "'a set" and A' B' :: "'b set" shows "cless_set A B \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_set: ccompare = None'') (\_. cless_set A B) | Some c \ if finite A \ finite B then ord.lexordp (\x y. lt_of_comp c y x) (csorted_list_of_set A) (csorted_list_of_set B) else Code.abort (STR ''cless_set: infinite set'') (\_. cless_set A B))" (is "?fin_fin") and cless_set_Complement2 [set_complement_code]: "cless_set A' (Complement B') \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_set Complement2: ccompare = None'') (\_. cless_set A' (Complement B')) | Some c \ if finite A' \ finite B' then finite (UNIV :: 'b set) \ proper_intrvl.set_less_aux_Compl (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B') else Code.abort (STR ''cless_set Complement2: infinite set'') (\_. cless_set A' (Complement B')))" (is "?fin_Compl_fin") and cless_set_Complement1 [set_complement_code]: "cless_set (Complement A') B' \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_set Complement1: ccompare = None'') (\_. cless_set (Complement A') B') | Some c \ if finite A' \ finite B' then finite (UNIV :: 'b set) \ proper_intrvl.Compl_set_less_aux (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B') else Code.abort (STR ''cless_set Complement1: infinite set'') (\_. cless_set (Complement A') B'))" (is "?Compl_fin_fin") and cless_set_Complement12 [set_complement_code]: "cless_set (Complement A) (Complement B) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_set Complement Complement: ccompare = None'') (\_. cless_set (Complement A) (Complement B)) | Some _ \ cless B A)" (is ?Compl_Compl) and "cless_set (RBT_set rbt) (RBT_set rbt') \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_set RBT_set RBT_set: ccompare = None'') (\_. cless_set (RBT_set rbt) (RBT_set rbt')) | Some c \ ord.lexord_fusion (\x y. lt_of_comp c y x) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt) (RBT_Set2.init rbt'))" (is ?rbt_rbt) and cless_set_rbt_Complement2 [set_complement_code]: "cless_set (RBT_set rbt1) (Complement (RBT_set rbt2)) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_set RBT_set (Complement RBT_set): ccompare = None'') (\_. cless_set (RBT_set rbt1) (Complement (RBT_set rbt2))) | Some c \ finite (UNIV :: 'b set) \ proper_intrvl.set_less_aux_Compl_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?rbt_Compl) and cless_set_rbt_Complement1 [set_complement_code]: "cless_set (Complement (RBT_set rbt1)) (RBT_set rbt2) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_set (Complement RBT_set) RBT_set: ccompare = None'') (\_. cless_set (Complement (RBT_set rbt1)) (RBT_set rbt2)) | Some c \ finite (UNIV :: 'b set) \ proper_intrvl.Compl_set_less_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?Compl_rbt) proof - note [split] = option.split csorted_list_of_set_split and [simp] = le_of_comp_of_ords_linorder[OF ID_ccompare] lt_of_comp_of_ords finite_subset[OF subset_UNIV] ccompare_set_def ID_Some ord.lexord_fusion_def proper_intrvl.Compl_set_less_aux_fusion_def proper_intrvl.set_less_aux_Compl_fusion_def unfoldr_rbt_keys_generator RBT_set_def sorted_RBT_Set_keys member_conv_keys linorder.set_less_finite_iff[OF ID_ccompare] linorder.set_less_aux_code[OF ID_ccompare, symmetric] linorder.Compl_set_less_Compl[OF ID_ccompare] linorder.infinite_set_less_Complement[OF ID_ccompare] linorder.infinite_Complement_set_less[OF ID_ccompare] linorder_proper_interval.set_less_aux_Compl2_conv_set_less_aux_Compl[OF ID_ccompare_interval, symmetric] linorder_proper_interval.Compl1_set_less_aux_conv_Compl_set_less_aux[OF ID_ccompare_interval, symmetric] show ?Compl_Compl by simp show ?rbt_rbt by auto show ?rbt_Compl by(cases "finite (UNIV :: 'b set)") auto show ?Compl_rbt by(cases "finite (UNIV :: 'b set)") auto show ?fin_fin by auto show ?fin_Compl_fin by(cases "finite (UNIV :: 'b set)", auto) show ?Compl_fin_fin by(cases "finite (UNIV :: 'b set)") auto qed lemma le_of_comp_set_less_eq: "le_of_comp (comp_of_ords (ord.set_less_eq le) (ord.set_less le)) = ord.set_less_eq le" by (rule le_of_comp_of_ords_gen, simp add: ord.set_less_def) lemma cless_eq_set_code [code]: fixes rbt rbt' :: "'a :: ccompare set_rbt" and rbt1 rbt2 :: "'b :: cproper_interval set_rbt" and A B :: "'a set" and A' B' :: "'b set" shows "cless_eq_set A B \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_eq_set: ccompare = None'') (\_. cless_eq_set A B) | Some c \ if finite A \ finite B then ord.lexordp_eq (\x y. lt_of_comp c y x) (csorted_list_of_set A) (csorted_list_of_set B) else Code.abort (STR ''cless_eq_set: infinite set'') (\_. cless_eq_set A B))" (is "?fin_fin") and cless_eq_set_Complement2 [set_complement_code]: "cless_eq_set A' (Complement B') \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_eq_set Complement2: ccompare = None'') (\_. cless_eq_set A' (Complement B')) | Some c \ if finite A' \ finite B' then finite (UNIV :: 'b set) \ proper_intrvl.set_less_eq_aux_Compl (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B') else Code.abort (STR ''cless_eq_set Complement2: infinite set'') (\_. cless_eq_set A' (Complement B')))" (is "?fin_Compl_fin") and cless_eq_set_Complement1 [set_complement_code]: "cless_eq_set (Complement A') B' \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_eq_set Complement1: ccompare = None'') (\_. cless_eq_set (Complement A') B') | Some c \ if finite A' \ finite B' then finite (UNIV :: 'b set) \ proper_intrvl.Compl_set_less_eq_aux (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B') else Code.abort (STR ''cless_eq_set Complement1: infinite set'') (\_. cless_eq_set (Complement A') B'))" (is "?Compl_fin_fin") and cless_eq_set_Complement12 [set_complement_code]: "cless_eq_set (Complement A) (Complement B) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_eq_set Complement Complement: ccompare = None'') (\_. cless_eq (Complement A) (Complement B)) | Some c \ cless_eq_set B A)" (is ?Compl_Compl) "cless_eq_set (RBT_set rbt) (RBT_set rbt') \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_eq_set RBT_set RBT_set: ccompare = None'') (\_. cless_eq_set (RBT_set rbt) (RBT_set rbt')) | Some c \ ord.lexord_eq_fusion (\x y. lt_of_comp c y x) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt) (RBT_Set2.init rbt'))" (is ?rbt_rbt) and cless_eq_set_rbt_Complement2 [set_complement_code]: "cless_eq_set (RBT_set rbt1) (Complement (RBT_set rbt2)) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_eq_set RBT_set (Complement RBT_set): ccompare = None'') (\_. cless_eq_set (RBT_set rbt1) (Complement (RBT_set rbt2))) | Some c \ finite (UNIV :: 'b set) \ proper_intrvl.set_less_eq_aux_Compl_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?rbt_Compl) and cless_eq_set_rbt_Complement1 [set_complement_code]: "cless_eq_set (Complement (RBT_set rbt1)) (RBT_set rbt2) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_eq_set (Complement RBT_set) RBT_set: ccompare = None'') (\_. cless_eq_set (Complement (RBT_set rbt1)) (RBT_set rbt2)) | Some c \ finite (UNIV :: 'b set) \ proper_intrvl.Compl_set_less_eq_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?Compl_rbt) proof - note [split] = option.split csorted_list_of_set_split and [simp] = le_of_comp_set_less_eq finite_subset[OF subset_UNIV] ccompare_set_def ID_Some ord.lexord_eq_fusion_def proper_intrvl.Compl_set_less_eq_aux_fusion_def proper_intrvl.set_less_eq_aux_Compl_fusion_def unfoldr_rbt_keys_generator RBT_set_def sorted_RBT_Set_keys member_conv_keys linorder.set_less_eq_finite_iff[OF ID_ccompare] linorder.set_less_eq_aux_code[OF ID_ccompare, symmetric] linorder.Compl_set_less_eq_Compl[OF ID_ccompare] linorder.infinite_set_less_eq_Complement[OF ID_ccompare] linorder.infinite_Complement_set_less_eq[OF ID_ccompare] linorder_proper_interval.set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl[OF ID_ccompare_interval, symmetric] linorder_proper_interval.Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux[OF ID_ccompare_interval, symmetric] show ?Compl_Compl by simp show ?rbt_rbt by auto show ?rbt_Compl by(cases "finite (UNIV :: 'b set)") auto show ?Compl_rbt by(cases "finite (UNIV :: 'b set)") auto show ?fin_fin by auto show ?fin_Compl_fin by (cases "finite (UNIV :: 'b set)", auto) show ?Compl_fin_fin by(cases "finite (UNIV :: 'b set)") auto qed lemma cproper_interval_set_Some_Some_code [code]: fixes rbt1 rbt2 :: "'a :: cproper_interval set_rbt" and A B :: "'a set" shows "cproper_interval (Some A) (Some B) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval: ccompare = None'') (\_. cproper_interval (Some A) (Some B)) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_set_aux (lt_of_comp c) cproper_interval (csorted_list_of_set A) (csorted_list_of_set B))" (is ?fin_fin) and cproper_interval_set_Some_Some_Complement [set_complement_code]: "cproper_interval (Some A) (Some (Complement B)) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval Complement2: ccompare = None'') (\_. cproper_interval (Some A) (Some (Complement B))) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_set_Compl_aux (lt_of_comp c) cproper_interval None 0 (csorted_list_of_set A) (csorted_list_of_set B))" (is ?fin_Compl_fin) and cproper_interval_set_Some_Complement_Some [set_complement_code]: "cproper_interval (Some (Complement A)) (Some B) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval Complement1: ccompare = None'') (\_. cproper_interval (Some (Complement A)) (Some B)) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_Compl_set_aux (lt_of_comp c) cproper_interval None (csorted_list_of_set A) (csorted_list_of_set B))" (is ?Compl_fin_fin) and cproper_interval_set_Some_Complement_Some_Complement [set_complement_code]: "cproper_interval (Some (Complement A)) (Some (Complement B)) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval Complement Complement: ccompare = None'') (\_. cproper_interval (Some (Complement A)) (Some (Complement B))) | Some _ \ cproper_interval (Some B) (Some A))" (is ?Compl_Compl) "cproper_interval (Some (RBT_set rbt1)) (Some (RBT_set rbt2)) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval RBT_set RBT_set: ccompare = None'') (\_. cproper_interval (Some (RBT_set rbt1)) (Some (RBT_set rbt2))) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_set_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?rbt_rbt) and cproper_interval_set_Some_rbt_Some_Complement [set_complement_code]: "cproper_interval (Some (RBT_set rbt1)) (Some (Complement (RBT_set rbt2))) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval RBT_set (Complement RBT_set): ccompare = None'') (\_. cproper_interval (Some (RBT_set rbt1)) (Some (Complement (RBT_set rbt2)))) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_set_Compl_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None 0 (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?rbt_Compl_rbt) and cproper_interval_set_Some_Complement_Some_rbt [set_complement_code]: "cproper_interval (Some (Complement (RBT_set rbt1))) (Some (RBT_set rbt2)) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval (Complement RBT_set) RBT_set: ccompare = None'') (\_. cproper_interval (Some (Complement (RBT_set rbt1))) (Some (RBT_set rbt2))) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_Compl_set_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?Compl_rbt_rbt) proof - note [split] = option.split csorted_list_of_set_split and [simp] = lt_of_comp_of_ords finite_subset[OF subset_UNIV] ccompare_set_def ID_Some linorder.set_less_finite_iff[OF ID_ccompare] RBT_set_def sorted_RBT_Set_keys member_conv_keys linorder.distinct_entries[OF ID_ccompare] unfoldr_rbt_keys_generator proper_intrvl.proper_interval_set_aux_fusion_def proper_intrvl.proper_interval_set_Compl_aux_fusion_def proper_intrvl.proper_interval_Compl_set_aux_fusion_def linorder_proper_interval.proper_interval_set_aux[OF ID_ccompare_interval] linorder_proper_interval.proper_interval_set_Compl_aux[OF ID_ccompare_interval] linorder_proper_interval.proper_interval_Compl_set_aux[OF ID_ccompare_interval] and [cong] = conj_cong show ?Compl_Compl by(clarsimp simp add: Complement_cproper_interval_set_Complement simp del: cproper_interval_set_Some_Some) show ?rbt_rbt ?rbt_Compl_rbt ?Compl_rbt_rbt by auto show ?fin_fin ?fin_Compl_fin ?Compl_fin_fin by auto qed context ord begin fun sorted_list_subset :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" where "sorted_list_subset eq [] ys = True" | "sorted_list_subset eq (x # xs) [] = False" | "sorted_list_subset eq (x # xs) (y # ys) \ (if eq x y then sorted_list_subset eq xs ys else x > y \ sorted_list_subset eq (x # xs) ys)" end context linorder begin lemma sorted_list_subset_correct: "\ sorted xs; distinct xs; sorted ys; distinct ys \ \ sorted_list_subset (=) xs ys \ set xs \ set ys" apply(induct "(=) :: 'a \ 'a \ bool" xs ys rule: sorted_list_subset.induct) apply(auto 6 2) using order_antisym apply auto done end context ord begin definition sorted_list_subset_fusion :: "('a \ 'a \ bool) \ ('a, 's1) generator \ ('a, 's2) generator \ 's1 \ 's2 \ bool" where "sorted_list_subset_fusion eq g1 g2 s1 s2 = sorted_list_subset eq (list.unfoldr g1 s1) (list.unfoldr g2 s2)" lemma sorted_list_subset_fusion_code: "sorted_list_subset_fusion eq g1 g2 s1 s2 = (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in list.has_next g2 s2 \ ( let (y, s2') = list.next g2 s2 in if eq x y then sorted_list_subset_fusion eq g1 g2 s1' s2' else y < x \ sorted_list_subset_fusion eq g1 g2 s1 s2') else True)" unfolding sorted_list_subset_fusion_def by(subst (1 2 5) list.unfoldr.simps)(simp add: split_beta Let_def) end lemmas [code] = ord.sorted_list_subset_fusion_code -text \ - Define a new constant for the subset operation - because @{theory "HOL-Library.Cardinality"} introduces @{const "Cardinality.subset'"} - and rewrites @{const "subset"} to @{const "Cardinality.subset'"} - based on the sort of the element type. -\ - -definition subset_eq :: "'a set \ 'a set \ bool" -where [simp, code del]: "subset_eq = (\)" - -lemma subseteq_code [code]: "(\) = subset_eq" -by simp - -lemma subset'_code [code]: "Cardinality.subset' = subset_eq" -by simp - -lemma subset_eq_code [folded subset_eq_def, code]: +lemma subset_eq_code [code]: fixes A1 A2 :: "'a set" and rbt :: "'b :: ccompare set_rbt" and rbt1 rbt2 :: "'d :: {ccompare, ceq} set_rbt" and dxs :: "'c :: ceq set_dlist" and xs :: "'c list" shows "RBT_set rbt \ B \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''subset RBT_set1: ccompare = None'') (\_. RBT_set rbt \ B) | Some _ \ list_all_fusion rbt_keys_generator (\x. x \ B) (RBT_Set2.init rbt))" (is ?rbt) "DList_set dxs \ C \ (case ID CEQ('c) of None \ Code.abort (STR ''subset DList_set1: ceq = None'') (\_. DList_set dxs \ C) | Some _ \ DList_Set.dlist_all (\x. x \ C) dxs)" (is ?dlist) "Set_Monad xs \ C \ list_all (\x. x \ C) xs" (is ?Set_Monad) - and Collect_subset_eq_Complement [folded subset_eq_def, set_complement_code]: + and Collect_subset_eq_Complement [set_complement_code]: "Collect_set P \ Complement A \ A \ {x. \ P x}" (is ?Collect_set_Compl) - and Complement_subset_eq_Complement [folded subset_eq_def, set_complement_code]: + and Complement_subset_eq_Complement [set_complement_code]: "Complement A1 \ Complement A2 \ A2 \ A1" (is ?Compl) and "RBT_set rbt1 \ RBT_set rbt2 \ (case ID CCOMPARE('d) of None \ Code.abort (STR ''subset RBT_set RBT_set: ccompare = None'') (\_. RBT_set rbt1 \ RBT_set rbt2) | Some c \ (case ID CEQ('d) of None \ ord.sorted_list_subset_fusion (lt_of_comp c) (\ x y. c x y = Eq) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2) | Some eq \ ord.sorted_list_subset_fusion (lt_of_comp c) eq rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2)))" (is ?rbt_rbt) proof - show ?rbt_rbt by (auto simp add: comparator.eq[OF ID_ccompare'] RBT_set_def member_conv_keys unfoldr_rbt_keys_generator ord.sorted_list_subset_fusion_def linorder.sorted_list_subset_correct[OF ID_ccompare] sorted_RBT_Set_keys split: option.split dest!: ID_ceq[THEN equal.equal_eq] del: iffI) show ?rbt by(auto simp add: RBT_set_def member_conv_keys list_all_fusion_def unfoldr_rbt_keys_generator keys.rep_eq list_all_iff split: option.split) show ?dlist by(auto simp add: DList_set_def dlist_all_conv_member split: option.split) show ?Set_Monad by(auto simp add: list_all_iff split: option.split) show ?Collect_set_Compl ?Compl by auto qed -hide_const (open) subset_eq -hide_fact (open) subset_eq_def - -lemma eq_set_code [code]: "Cardinality.eq_set = set_eq" -by(simp add: set_eq_def) - lemma set_eq_code [code]: fixes rbt1 rbt2 :: "'b :: {ccompare, ceq} set_rbt" shows "set_eq A B \ A \ B \ B \ A" and set_eq_Complement_Complement [set_complement_code]: "set_eq (Complement A) (Complement B) = set_eq A B" and "set_eq (RBT_set rbt1) (RBT_set rbt2) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''set_eq RBT_set RBT_set: ccompare = None'') (\_. set_eq (RBT_set rbt1) (RBT_set rbt2)) | Some c \ (case ID CEQ('b) of None \ list_all2_fusion (\ x y. c x y = Eq) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2) | Some eq \ list_all2_fusion eq rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2)))" (is ?rbt_rbt) proof - show ?rbt_rbt by (auto 4 3 split: option.split simp add: comparator.eq[OF ID_ccompare'] sorted_RBT_Set_keys list_all2_fusion_def unfoldr_rbt_keys_generator RBT_set_conv_keys set_eq_def list.rel_eq dest!: ID_ceq[THEN equal.equal_eq] intro: linorder.sorted_distinct_set_unique[OF ID_ccompare]) qed(auto simp add: set_eq_def) lemma Set_project_code [code]: "Set.filter P A = A \ Collect_set P" by(auto simp add: Set.filter_def) lemma Set_image_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "image f (Set_Monad xs) = Set_Monad (map f xs)" "image f (Collect_set A) = Code.abort (STR ''image Collect_set'') (\_. image f (Collect_set A))" and image_Complement_Complement [set_complement_code]: "image f (Complement (Complement B)) = image f B" and "image g (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''image DList_set: ceq = None'') (\_. image g (DList_set dxs)) | Some _ \ DList_Set.fold (insert \ g) dxs {})" (is ?dlist) "image h (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''image RBT_set: ccompare = None'') (\_. image h (RBT_set rbt)) | Some _ \ RBT_Set2.fold (insert \ h) rbt {})" (is ?rbt) proof - { fix xs have "fold (insert \ g) xs {} = g ` set xs" by(induct xs rule: rev_induct) simp_all } thus ?dlist by(simp add: DList_set_def DList_Set.fold_def DList_Set.Collect_member split: option.split) { fix xs have "fold (insert \ h) xs {} = h ` set xs" by(induct xs rule: rev_induct) simp_all } thus ?rbt by(auto simp add: RBT_set_def fold_conv_fold_keys member_conv_keys split: option.split) qed simp_all lemma the_elem_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "the_elem (Set_Monad [x]) = x" "the_elem (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''the_elem DList_set: ceq = None'') (\_. the_elem (DList_set dxs)) | Some _ \ case list_of_dlist dxs of [x] \ x | _ \ Code.abort (STR ''the_elem DList_set: not unique'') (\_. the_elem (DList_set dxs)))" "the_elem (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''the_elem RBT_set: ccompare = None'') (\_. the_elem (RBT_set rbt)) | Some _ \ case RBT_Mapping2.impl_of rbt of RBT_Impl.Branch _ RBT_Impl.Empty x _ RBT_Impl.Empty \ x | _ \ Code.abort (STR ''the_elem RBT_set: not unique'') (\_. the_elem (RBT_set rbt)))" by(auto simp add: RBT_set_def DList_set_def DList_Set.Collect_member the_elem_def member_conv_keys split: option.split list.split rbt.split)(simp add: RBT_Set2.keys_def) lemma Pow_set_conv_fold: "Pow (set xs \ A) = fold (\x A. A \ insert x ` A) xs (Pow A)" by(induct xs rule: rev_induct)(auto simp add: Pow_insert) lemma Pow_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "Pow A = Collect_set (\B. B \ A)" "Pow (Set_Monad xs) = fold (\x A. A \ insert x ` A) xs {{}}" "Pow (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''Pow DList_set: ceq = None'') (\_. Pow (DList_set dxs)) | Some _ \ DList_Set.fold (\x A. A \ insert x ` A) dxs {{}})" "Pow (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''Pow RBT_set: ccompare = None'') (\_. Pow (RBT_set rbt)) | Some _ \ RBT_Set2.fold (\x A. A \ insert x ` A) rbt {{}})" by(auto simp add: DList_set_def DList_Set.Collect_member DList_Set.fold_def RBT_set_def fold_conv_fold_keys member_conv_keys Pow_set_conv_fold[where A="{}", simplified] split: option.split) lemma fold_singleton: "Finite_Set.fold f x {y} = f y x" by(fastforce simp add: Finite_Set.fold_def intro: fold_graph.intros elim: fold_graph.cases) lift_definition sum_cfc :: "('a \ 'b :: comm_monoid_add) \ ('a, 'b) comp_fun_commute" is "\f :: 'a \ 'b. plus \ f" by(unfold_locales)(simp add: fun_eq_iff add.left_commute) lemma sum_code [code]: "sum f A = (if finite A then set_fold_cfc (sum_cfc f) 0 A else 0)" by transfer(simp add: sum.eq_fold) lemma product_code [code]: fixes dxs :: "'a :: ceq set_dlist" and dys :: "'b :: ceq set_dlist" and rbt1 :: "'c :: ccompare set_rbt" and rbt2 :: "'d :: ccompare set_rbt" shows "Product_Type.product A B = Collect_set (\(x, y). x \ A \ y \ B)" "Product_Type.product (Set_Monad xs) (Set_Monad ys) = Set_Monad (fold (\x. fold (\y rest. (x, y) # rest) ys) xs [])" (is ?Set_Monad) "Product_Type.product (DList_set dxs) B1 = (case ID CEQ('a) of None \ Code.abort (STR ''product DList_set1: ceq = None'') (\_. Product_Type.product (DList_set dxs) B1) | Some _ \ DList_Set.fold (\x rest. Pair x ` B1 \ rest) dxs {})" (is "?dlist1") "Product_Type.product A1 (DList_set dys) = (case ID CEQ('b) of None \ Code.abort (STR ''product DList_set2: ceq = None'') (\_. Product_Type.product A1 (DList_set dys)) | Some _ \ DList_Set.fold (\y rest. (\x. (x, y)) ` A1 \ rest) dys {})" (is "?dlist2") "Product_Type.product (DList_set dxs) (DList_set dys) = (case ID CEQ('a) of None \ Code.abort (STR ''product DList_set DList_set: ceq1 = None'') (\_. Product_Type.product (DList_set dxs) (DList_set dys)) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''product DList_set DList_set: ceq2 = None'') (\_. Product_Type.product (DList_set dxs) (DList_set dys)) | Some _ \ DList_set (DList_Set.product dxs dys))" "Product_Type.product (RBT_set rbt1) B2 = (case ID CCOMPARE('c) of None \ Code.abort (STR ''product RBT_set: ccompare1 = None'') (\_. Product_Type.product (RBT_set rbt1) B2) | Some _ \ RBT_Set2.fold (\x rest. Pair x ` B2 \ rest) rbt1 {})" (is "?rbt1") "Product_Type.product A2 (RBT_set rbt2) = (case ID CCOMPARE('d) of None \ Code.abort (STR ''product RBT_set: ccompare2 = None'') (\_. Product_Type.product A2 (RBT_set rbt2)) | Some _ \ RBT_Set2.fold (\y rest. (\x. (x, y)) ` A2 \ rest) rbt2 {})" (is "?rbt2") "Product_Type.product (RBT_set rbt1) (RBT_set rbt2) = (case ID CCOMPARE('c) of None \ Code.abort (STR ''product RBT_set RBT_set: ccompare1 = None'') (\_. Product_Type.product (RBT_set rbt1) (RBT_set rbt2)) | Some _ \ case ID CCOMPARE('d) of None \ Code.abort (STR ''product RBT_set RBT_set: ccompare2 = None'') (\_. Product_Type.product (RBT_set rbt1) (RBT_set rbt2)) | Some _ \ RBT_set (RBT_Set2.product rbt1 rbt2))" proof - have [simp]: "\a zs. fold (\y. (#) (a, y)) ys zs = rev (map (Pair a) ys) @ zs" by(induct ys) simp_all have [simp]: "\zs. fold (\x. fold (\y rest. (x, y) # rest) ys) xs zs = rev (concat (map (\x. map (Pair x) ys) xs)) @ zs" by(induct xs) simp_all show ?Set_Monad by(auto simp add: Product_Type.product_def) { fix xs :: "'a list" have "fold (\x. (\) (Pair x ` B1)) xs {} = set xs \ B1" by(induct xs rule: rev_induct) auto } thus ?dlist1 by(simp add: Product_Type.product_def DList_set_def DList_Set.fold.rep_eq DList_Set.Collect_member split: option.split) { fix ys :: "'b list" have "fold (\y. (\) ((\x. (x, y)) ` A1)) ys {} = A1 \ set ys" by(induct ys rule: rev_induct) auto } thus ?dlist2 by(simp add: Product_Type.product_def DList_set_def DList_Set.fold.rep_eq DList_Set.Collect_member split: option.split) { fix xs :: "'c list" have "fold (\x. (\) (Pair x ` B2)) xs {} = set xs \ B2" by(induct xs rule: rev_induct) auto } thus ?rbt1 by(simp add: Product_Type.product_def RBT_set_def RBT_Set2.member_product RBT_Set2.member_conv_keys fold_conv_fold_keys split: option.split) { fix ys :: "'d list" have "fold (\y. (\) ((\x. (x, y)) ` A2)) ys {} = A2 \ set ys" by(induct ys rule: rev_induct) auto } thus ?rbt2 by(simp add: Product_Type.product_def RBT_set_def RBT_Set2.member_product RBT_Set2.member_conv_keys fold_conv_fold_keys split: option.split) qed(auto simp add: RBT_set_def DList_set_def Product_Type.product_def DList_Set.product_member RBT_Set2.member_product split: option.split) lemma Id_on_code [code]: fixes A :: "'a :: ceq set" and dxs :: "'a set_dlist" and P :: "'a \ bool" and rbt :: "'b :: ccompare set_rbt" shows "Id_on B = (\x. (x, x)) ` B" and Id_on_Complement [set_complement_code]: "Id_on (Complement A) = (case ID CEQ('a) of None \ Code.abort (STR ''Id_on Complement: ceq = None'') (\_. Id_on (Complement A)) | Some eq \ Collect_set (\(x, y). eq x y \ x \ A))" and "Id_on (Collect_set P) = (case ID CEQ('a) of None \ Code.abort (STR ''Id_on Collect_set: ceq = None'') (\_. Id_on (Collect_set P)) | Some eq \ Collect_set (\(x, y). eq x y \ P x))" "Id_on (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''Id_on DList_set: ceq = None'') (\_. Id_on (DList_set dxs)) | Some _ \ DList_set (DList_Set.Id_on dxs))" "Id_on (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''Id_on RBT_set: ccompare = None'') (\_. Id_on (RBT_set rbt)) | Some _ \ RBT_set (RBT_Set2.Id_on rbt))" by(auto simp add: DList_set_def RBT_set_def DList_Set.member_Id_on RBT_Set2.member_Id_on dest: equal.equal_eq[OF ID_ceq] split: option.split) lemma Image_code [code]: fixes dxs :: "('a :: ceq \ 'b :: ceq) set_dlist" and rbt :: "('c :: ccompare \ 'd :: ccompare) set_rbt" shows "X `` Y = snd ` Set.filter (\(x, y). x \ Y) X" (is ?generic) "Set_Monad rxs `` A = Set_Monad (fold (\(x, y) rest. if x \ A then y # rest else rest) rxs [])" (is ?Set_Monad) "DList_set dxs `` B = (case ID CEQ('a) of None \ Code.abort (STR ''Image DList_set: ceq1 = None'') (\_. DList_set dxs `` B) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''Image DList_set: ceq2 = None'') (\_. DList_set dxs `` B) | Some _ \ DList_Set.fold (\(x, y) acc. if x \ B then insert y acc else acc) dxs {})" (is ?DList_set) "RBT_set rbt `` C = (case ID CCOMPARE('c) of None \ Code.abort (STR ''Image RBT_set: ccompare1 = None'') (\_. RBT_set rbt `` C) | Some _ \ case ID CCOMPARE('d) of None \ Code.abort (STR ''Image RBT_set: ccompare2 = None'') (\_. RBT_set rbt `` C) | Some _ \ RBT_Set2.fold (\(x, y) acc. if x \ C then insert y acc else acc) rbt {})" (is ?RBT_set) proof - show ?generic by(auto intro: rev_image_eqI) have "set (fold (\(x, y) rest. if x \ A then y # rest else rest) rxs []) = set rxs `` A" by(induct rxs rule: rev_induct)(auto split: if_split_asm) thus ?Set_Monad by(auto) { fix dxs :: "('a \ 'b) list" have "fold (\(x, y) acc. if x \ B then insert y acc else acc) dxs {} = set dxs `` B" by(induct dxs rule: rev_induct)(auto split: if_split_asm) } thus ?DList_set by(clarsimp simp add: DList_set_def Collect_member ceq_prod_def ID_Some DList_Set.fold.rep_eq split: option.split) { fix rbt :: "(('c \ 'd) \ unit) list" have "fold (\(a, _). case a of (x, y) \ \acc. if x \ C then insert y acc else acc) rbt {} = (fst ` set rbt) `` C" by(induct rbt rule: rev_induct)(auto simp add: split_beta split: if_split_asm) } thus ?RBT_set by(clarsimp simp add: RBT_set_def ccompare_prod_def ID_Some RBT_Set2.fold.rep_eq member_conv_keys RBT_Set2.keys.rep_eq RBT_Impl.fold_def RBT_Impl.keys_def split: option.split) qed lemma insert_relcomp: "insert (a, b) A O B = A O B \ {a} \ {c. (b, c) \ B}" by auto lemma trancl_code [code]: "trancl A = (if finite A then ntrancl (card A - 1) A else Code.abort (STR ''trancl: infinite set'') (\_. trancl A))" by (simp add: finite_trancl_ntranl) lemma set_relcomp_set: "set xs O set ys = fold (\(x, y). fold (\(y', z) A. if y = y' then insert (x, z) A else A) ys) xs {}" proof(induct xs rule: rev_induct) case Nil show ?case by simp next case (snoc x xs) note [[show_types]] { fix a :: 'a and b :: 'c and X :: "('a \ 'b) set" have "fold (\(y', z) A. if b = y' then insert (a, z) A else A) ys X = X \ {a} \ {c. (b, c) \ set ys}" by(induct ys arbitrary: X rule: rev_induct)(auto split: if_split_asm) } thus ?case using snoc by(cases x)(simp add: insert_relcomp) qed lemma If_not: "(if \ a then b else c) = (if a then c else b)" by auto lemma relcomp_code [code]: fixes rbt1 :: "('a :: ccompare \ 'b :: ccompare) set_rbt" and rbt2 :: "('b \ 'c :: ccompare) set_rbt" and rbt3 :: "('a \ 'd :: {ccompare, ceq}) set_rbt" and rbt4 :: "('d \ 'a) set_rbt" and rbt5 :: "('b \ 'a) set_rbt" and dxs1 :: "('d \ 'e :: ceq) set_dlist" and dxs2 :: "('e \ 'd) set_dlist" and dxs3 :: "('e \ 'f :: ceq) set_dlist" and dxs4 :: "('f \ 'g :: ceq) set_dlist" and xs1 :: "('h \ 'i :: ceq) list" and xs2 :: "('i \ 'j) list" and xs3 :: "('b \ 'h) list" and xs4 :: "('h \ 'b) list" and xs5 :: "('f \ 'h) list" and xs6 :: "('h \ 'f) list" shows "RBT_set rbt1 O RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp RBT_set RBT_set: ccompare1 = None'') (\_. RBT_set rbt1 O RBT_set rbt2) | Some _ \ case ID CCOMPARE('b) of None \ Code.abort (STR ''relcomp RBT_set RBT_set: ccompare2 = None'') (\_. RBT_set rbt1 O RBT_set rbt2) | Some c_b \ case ID CCOMPARE('c) of None \ Code.abort (STR ''relcomp RBT_set RBT_set: ccompare3 = None'') (\_. RBT_set rbt1 O RBT_set rbt2) | Some _ \ RBT_Set2.fold (\(x, y). RBT_Set2.fold (\(y', z) A. if c_b y y' \ Eq then A else insert (x, z) A) rbt2) rbt1 {})" (is ?rbt_rbt) "RBT_set rbt3 O DList_set dxs1 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp RBT_set DList_set: ccompare1 = None'') (\_. RBT_set rbt3 O DList_set dxs1) | Some _ \ case ID CCOMPARE('d) of None \ Code.abort (STR ''relcomp RBT_set DList_set: ccompare2 = None'') (\_. RBT_set rbt3 O DList_set dxs1) | Some _ \ case ID CEQ('d) of None \ Code.abort (STR ''relcomp RBT_set DList_set: ceq2 = None'') (\_. RBT_set rbt3 O DList_set dxs1) | Some eq \ case ID CEQ('e) of None \ Code.abort (STR ''relcomp RBT_set DList_set: ceq3 = None'') (\_. RBT_set rbt3 O DList_set dxs1) | Some _ \ RBT_Set2.fold (\(x, y). DList_Set.fold (\(y', z) A. if eq y y' then insert (x, z) A else A) dxs1) rbt3 {})" (is ?rbt_dlist) "DList_set dxs2 O RBT_set rbt4 = (case ID CEQ('e) of None \ Code.abort (STR ''relcomp DList_set RBT_set: ceq1 = None'') (\_. DList_set dxs2 O RBT_set rbt4) | Some _ \ case ID CCOMPARE('d) of None \ Code.abort (STR ''relcomp DList_set RBT_set: ceq2 = None'') (\_. DList_set dxs2 O RBT_set rbt4) | Some _ \ case ID CEQ('d) of None \ Code.abort (STR ''relcomp DList_set RBT_set: ccompare2 = None'') (\_. DList_set dxs2 O RBT_set rbt4) | Some eq \ case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp DList_set RBT_set: ccompare3 = None'') (\_. DList_set dxs2 O RBT_set rbt4) | Some _ \ DList_Set.fold (\(x, y). RBT_Set2.fold (\(y', z) A. if eq y y' then insert (x, z) A else A) rbt4) dxs2 {})" (is ?dlist_rbt) "DList_set dxs3 O DList_set dxs4 = (case ID CEQ('e) of None \ Code.abort (STR ''relcomp DList_set DList_set: ceq1 = None'') (\_. DList_set dxs3 O DList_set dxs4) | Some _ \ case ID CEQ('f) of None \ Code.abort (STR ''relcomp DList_set DList_set: ceq2 = None'') (\_. DList_set dxs3 O DList_set dxs4) | Some eq \ case ID CEQ('g) of None \ Code.abort (STR ''relcomp DList_set DList_set: ceq3 = None'') (\_. DList_set dxs3 O DList_set dxs4) | Some _ \ DList_Set.fold (\(x, y). DList_Set.fold (\(y', z) A. if eq y y' then insert (x, z) A else A) dxs4) dxs3 {})" (is ?dlist_dlist) "Set_Monad xs1 O Set_Monad xs2 = (case ID CEQ('i) of None \ Code.abort (STR ''relcomp Set_Monad Set_Monad: ceq = None'') (\_. Set_Monad xs1 O Set_Monad xs2) | Some eq \ fold (\(x, y). fold (\(y', z) A. if eq y y' then insert (x, z) A else A) xs2) xs1 {})" (is ?monad_monad) "RBT_set rbt1 O Set_Monad xs3 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp RBT_set Set_Monad: ccompare1 = None'') (\_. RBT_set rbt1 O Set_Monad xs3) | Some _ \ case ID CCOMPARE('b) of None \ Code.abort (STR ''relcomp RBT_set Set_Monad: ccompare2 = None'') (\_. RBT_set rbt1 O Set_Monad xs3) | Some c_b \ RBT_Set2.fold (\(x, y). fold (\(y', z) A. if c_b y y' \ Eq then A else insert (x, z) A) xs3) rbt1 {})" (is ?rbt_monad) "Set_Monad xs4 O RBT_set rbt5 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp Set_Monad RBT_set: ccompare1 = None'') (\_. Set_Monad xs4 O RBT_set rbt5) | Some _ \ case ID CCOMPARE('b) of None \ Code.abort (STR ''relcomp Set_Monad RBT_set: ccompare2 = None'') (\_. Set_Monad xs4 O RBT_set rbt5) | Some c_b \ fold (\(x, y). RBT_Set2.fold (\(y', z) A. if c_b y y' \ Eq then A else insert (x, z) A) rbt5) xs4 {})" (is ?monad_rbt) "DList_set dxs3 O Set_Monad xs5 = (case ID CEQ('e) of None \ Code.abort (STR ''relcomp DList_set Set_Monad: ceq1 = None'') (\_. DList_set dxs3 O Set_Monad xs5) | Some _ \ case ID CEQ('f) of None \ Code.abort (STR ''relcomp DList_set Set_Monad: ceq2 = None'') (\_. DList_set dxs3 O Set_Monad xs5) | Some eq \ DList_Set.fold (\(x, y). fold (\(y', z) A. if eq y y' then insert (x, z) A else A) xs5) dxs3 {})" (is ?dlist_monad) "Set_Monad xs6 O DList_set dxs4 = (case ID CEQ('f) of None \ Code.abort (STR ''relcomp Set_Monad DList_set: ceq1 = None'') (\_. Set_Monad xs6 O DList_set dxs4) | Some eq \ case ID CEQ('g) of None \ Code.abort (STR ''relcomp Set_Monad DList_set: ceq2 = None'') (\_. Set_Monad xs6 O DList_set dxs4) | Some _ \ fold (\(x, y). DList_Set.fold (\(y', z) A. if eq y y' then insert (x, z) A else A) dxs4) xs6 {})" (is ?monad_dlist) proof - show ?rbt_rbt ?rbt_monad ?monad_rbt by(auto simp add: comparator.eq[OF ID_ccompare'] RBT_set_def ccompare_prod_def member_conv_keys ID_Some RBT_Set2.fold_conv_fold_keys' RBT_Set2.keys.rep_eq If_not set_relcomp_set split: option.split del: equalityI) show ?rbt_dlist ?dlist_rbt ?dlist_dlist ?monad_monad ?dlist_monad ?monad_dlist by(auto simp add: RBT_set_def DList_set_def member_conv_keys ID_Some ccompare_prod_def ceq_prod_def Collect_member RBT_Set2.fold_conv_fold_keys' RBT_Set2.keys.rep_eq DList_Set.fold.rep_eq set_relcomp_set dest: equal.equal_eq[OF ID_ceq] split: option.split del: equalityI) qed lemma irrefl_code [code]: fixes r :: "('a :: {ceq, ccompare} \ 'a) set" shows "irrefl r \ (case ID CEQ('a) of Some eq \ (\(x, y) \ r. \ eq x y) | None \ case ID CCOMPARE('a) of None \ Code.abort (STR ''irrefl: ceq = None & ccompare = None'') (\_. irrefl r) | Some c \ (\(x, y) \ r. c x y \ Eq))" apply(auto simp add: irrefl_distinct comparator.eq[OF ID_ccompare'] split: option.split dest!: ID_ceq[THEN equal.equal_eq]) done lemma wf_code [code]: fixes rbt :: "('a :: ccompare \ 'a) set_rbt" and dxs :: "('b :: ceq \ 'b) set_dlist" shows "wf (Set_Monad xs) = acyclic (Set_Monad xs)" "wf (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''wf RBT_set: ccompare = None'') (\_. wf (RBT_set rbt)) | Some _ \ acyclic (RBT_set rbt))" "wf (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''wf DList_set: ceq = None'') (\_. wf (DList_set dxs)) | Some _ \ acyclic (DList_set dxs))" by(auto simp add: wf_iff_acyclic_if_finite split: option.split del: iffI)(simp_all add: wf_iff_acyclic_if_finite finite_code ccompare_prod_def ceq_prod_def ID_Some) lemma bacc_code [code]: "bacc R 0 = - snd ` R" "bacc R (Suc n) = (let rec = bacc R n in rec \ - snd ` (Set.filter (\(y, x). y \ rec) R))" by(auto intro: rev_image_eqI simp add: Let_def) (* TODO: acc could also be computed for infinite universes if r is finite *) lemma acc_code [code]: fixes A :: "('a :: {finite, card_UNIV} \ 'a) set" shows "Wellfounded.acc A = bacc A (of_phantom (card_UNIV :: 'a card_UNIV))" by(simp add: card_UNIV acc_bacc_eq) lemma sorted_list_of_set_code [code]: fixes dxs :: "'a :: {linorder, ceq} set_dlist" and rbt :: "'b :: {linorder, ccompare} set_rbt" shows "sorted_list_of_set (Set_Monad xs) = sort (remdups xs)" "sorted_list_of_set (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''sorted_list_of_set DList_set: ceq = None'') (\_. sorted_list_of_set (DList_set dxs)) | Some _ \ sort (list_of_dlist dxs))" "sorted_list_of_set (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''sorted_list_of_set RBT_set: ccompare = None'') (\_. sorted_list_of_set (RBT_set rbt)) | Some _ \ sort (RBT_Set2.keys rbt))" \ \We must sort the keys because @{term ccompare}'s ordering need not coincide with @{term linorder}'s.\ by(auto simp add: DList_set_def RBT_set_def sorted_list_of_set_sort_remdups Collect_member distinct_remdups_id distinct_list_of_dlist member_conv_keys split: option.split) lemma map_project_set: "List.map_project f (set xs) = set (List.map_filter f xs)" by(auto simp add: List.map_project_def List.map_filter_def intro: rev_image_eqI) lemma map_project_simps: shows map_project_empty: "List.map_project f {} = {}" and map_project_insert: "List.map_project f (insert x A) = (case f x of None \ List.map_project f A | Some y \ insert y (List.map_project f A))" by(auto simp add: List.map_project_def split: option.split) lemma map_project_conv_fold: "List.map_project f (set xs) = fold (\x A. case f x of None \ A | Some y \ insert y A) xs {}" by(induct xs rule: rev_induct)(simp_all add: map_project_simps cong: option.case_cong) lemma map_project_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "List.map_project f (Set_Monad xs) = Set_Monad (List.map_filter f xs)" "List.map_project g (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''map_project DList_set: ceq = None'') (\_. List.map_project g (DList_set dxs)) | Some _ \ DList_Set.fold (\x A. case g x of None \ A | Some y \ insert y A) dxs {})" (is ?dlist) "List.map_project h (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''map_project RBT_set: ccompare = None'') (\_. List.map_project h (RBT_set rbt)) | Some _ \ RBT_Set2.fold (\x A. case h x of None \ A | Some y \ insert y A) rbt {})" (is ?rbt) proof - show ?dlist ?rbt by(auto split: option.split simp add: RBT_set_def DList_set_def DList_Set.fold.rep_eq Collect_member map_project_conv_fold RBT_Set2.fold_conv_fold_keys member_conv_keys del: equalityI) qed(auto simp add: List.map_project_def List.map_filter_def intro: rev_image_eqI) lemma Bleast_code [code]: "Bleast A P = (if finite A then case filter P (sorted_list_of_set A) of [] \ abort_Bleast A P | x # xs \ x else abort_Bleast A P)" proof(cases "finite A") case True hence *: "A = set (sorted_list_of_set A)" by(simp add: sorted_list_of_set) show ?thesis using True by(subst (1 3) *)(unfold Bleast_code, simp add: sorted_sort_id) qed(simp add: abort_Bleast_def Bleast_def) lemma can_select_code [code]: fixes xs :: "'a :: ceq list" and dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "can_select P (Set_Monad xs) = (case ID CEQ('a) of None \ Code.abort (STR ''can_select Set_Monad: ceq = None'') (\_. can_select P (Set_Monad xs)) | Some eq \ case filter P xs of Nil \ False | x # xs \ list_all (eq x) xs)" (is ?Set_Monad) "can_select Q (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''can_select DList_set: ceq = None'') (\_. can_select Q (DList_set dxs)) | Some _ \ DList_Set.length (DList_Set.filter Q dxs) = 1)" (is ?dlist) "can_select R (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''can_select RBT_set: ccompare = None'') (\_. can_select R (RBT_set rbt)) | Some _ \ singleton_list_fusion (filter_generator R rbt_keys_generator) (RBT_Set2.init rbt))" (is ?rbt) proof - show ?Set_Monad apply(auto split: option.split list.split dest!: ID_ceq[THEN equal.equal_eq] dest: filter_eq_ConsD simp add: can_select_def filter_empty_conv list_all_iff) apply(drule filter_eq_ConsD, fastforce) apply(drule filter_eq_ConsD, clarsimp, blast) done show ?dlist by(clarsimp simp add: can_select_def card_eq_length[symmetric] Set_member_code card_eq_Suc_0_ex1 simp del: card_eq_length split: option.split) note [simp del] = distinct_keys show ?rbt using distinct_keys[of rbt] apply(auto simp add: can_select_def singleton_list_fusion_def unfoldr_filter_generator unfoldr_rbt_keys_generator Set_member_code member_conv_keys filter_empty_conv empty_filter_conv split: option.split list.split dest: filter_eq_ConsD) apply(drule filter_eq_ConsD, fastforce) apply(drule filter_eq_ConsD, fastforce simp add: empty_filter_conv) apply(drule filter_eq_ConsD) apply clarsimp apply(drule Cons_eq_filterD) apply clarify apply(simp (no_asm_use)) apply blast done qed lemma pred_of_set_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "pred_of_set (Set_Monad xs) = fold (sup \ Predicate.single) xs bot" "pred_of_set (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''pred_of_set DList_set: ceq = None'') (\_. pred_of_set (DList_set dxs)) | Some _ \ DList_Set.fold (sup \ Predicate.single) dxs bot)" "pred_of_set (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''pred_of_set RBT_set: ccompare = None'') (\_. pred_of_set (RBT_set rbt)) | Some _ \ RBT_Set2.fold (sup \ Predicate.single) rbt bot)" by(auto simp add: pred_of_set_set_fold_sup fold_map DList_set_def RBT_set_def Collect_member member_conv_keys DList_Set.fold.rep_eq fold_conv_fold_keys split: option.split) text \ @{typ "'a Predicate.pred"} is implemented as a monad, so we keep the monad when converting to @{typ "'a set"}. For this case, @{term insert_monad} and @{term union_monad} avoid the unnecessary dictionary construction. \ definition insert_monad :: "'a \ 'a set \ 'a set" where [simp]: "insert_monad = insert" definition union_monad :: "'a set \ 'a set \ 'a set" where [simp]: "union_monad = (\)" lemma insert_monad_code [code]: "insert_monad x (Set_Monad xs) = Set_Monad (x # xs)" by simp lemma union_monad_code [code]: "union_monad (Set_Monad xs) (Set_Monad ys) = Set_Monad (xs @ ys)" by(simp) lemma set_of_pred_code [code]: "set_of_pred (Predicate.Seq f) = (case f () of seq.Empty \ Set_Monad [] | seq.Insert x P \ insert_monad x (set_of_pred P) | seq.Join P xq \ union_monad (set_of_pred P) (set_of_seq xq))" by(simp add: of_pred_code cong: seq.case_cong) lemma set_of_seq_code [code]: "set_of_seq seq.Empty = Set_Monad []" "set_of_seq (seq.Insert x P) = insert_monad x (set_of_pred P)" "set_of_seq (seq.Join P xq) = union_monad (set_of_pred P) (set_of_seq xq)" by(simp_all add: of_seq_code) hide_const (open) insert_monad union_monad subsection \Type class instantiations\ datatype set_impl = Set_IMPL declare set_impl.eq.simps [code del] set_impl.size [code del] set_impl.rec [code del] set_impl.case [code del] lemma [code]: fixes x :: set_impl shows "size x = 0" and "size_set_impl x = 0" by(case_tac [!] x) simp_all definition set_Choose :: set_impl where [simp]: "set_Choose = Set_IMPL" definition set_Collect :: set_impl where [simp]: "set_Collect = Set_IMPL" definition set_DList :: set_impl where [simp]: "set_DList = Set_IMPL" definition set_RBT :: set_impl where [simp]: "set_RBT = Set_IMPL" definition set_Monad :: set_impl where [simp]: "set_Monad = Set_IMPL" code_datatype set_Choose set_Collect set_DList set_RBT set_Monad definition set_empty_choose :: "'a set" where [simp]: "set_empty_choose = {}" lemma set_empty_choose_code [code]: "(set_empty_choose :: 'a :: {ceq, ccompare} set) = (case CCOMPARE('a) of Some _ \ RBT_set RBT_Set2.empty | None \ case CEQ('a) of None \ Set_Monad [] | Some _ \ DList_set (DList_Set.empty))" by(simp split: option.split) definition set_impl_choose2 :: "set_impl \ set_impl \ set_impl" where [simp]: "set_impl_choose2 = (\_ _. Set_IMPL)" lemma set_impl_choose2_code [code]: "set_impl_choose2 x y = set_Choose" "set_impl_choose2 set_Collect set_Collect = set_Collect" "set_impl_choose2 set_DList set_DList = set_DList" "set_impl_choose2 set_RBT set_RBT = set_RBT" "set_impl_choose2 set_Monad set_Monad = set_Monad" by(simp_all) definition set_empty :: "set_impl \ 'a set" where [simp]: "set_empty = (\_. {})" lemma set_empty_code [code]: "set_empty set_Collect = Collect_set (\_. False)" "set_empty set_DList = DList_set DList_Set.empty" "set_empty set_RBT = RBT_set RBT_Set2.empty" "set_empty set_Monad = Set_Monad []" "set_empty set_Choose = set_empty_choose" by(simp_all) class set_impl = fixes set_impl :: "('a, set_impl) phantom" syntax (input) "_SET_IMPL" :: "type => logic" ("(1SET'_IMPL/(1'(_')))") parse_translation \ let fun set_impl_tr [ty] = (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "set_impl"} $ (Syntax.const @{type_syntax phantom} $ ty $ Syntax.const @{type_syntax set_impl})) | set_impl_tr ts = raise TERM ("set_impl_tr", ts); in [(@{syntax_const "_SET_IMPL"}, K set_impl_tr)] end \ declare [[code drop: "{}"]] lemma empty_code [code, code_unfold]: "({} :: 'a :: set_impl set) = set_empty (of_phantom SET_IMPL('a))" by simp subsection \Generator for the @{class set_impl}-class\ text \ This generator registers itself at the derive-manager for the classes @{class set_impl}. Here, one can choose the desired implementation via the parameter. \begin{itemize} \item \texttt{instantiation type :: (type,\ldots,type) (rbt,dlist,collect,monad,choose, or arbitrary constant name) set-impl} \end{itemize} \ text \ This generator can be used for arbitrary types, not just datatypes. \ ML_file \set_impl_generator.ML\ derive (dlist) set_impl unit bool derive (rbt) set_impl nat derive (set_RBT) set_impl int (* shows usage of constant names *) derive (dlist) set_impl Enum.finite_1 Enum.finite_2 Enum.finite_3 derive (rbt) set_impl integer natural derive (rbt) set_impl char instantiation sum :: (set_impl, set_impl) set_impl begin definition "SET_IMPL('a + 'b) = Phantom('a + 'b) (set_impl_choose2 (of_phantom SET_IMPL('a)) (of_phantom SET_IMPL('b)))" instance .. end instantiation prod :: (set_impl, set_impl) set_impl begin definition "SET_IMPL('a * 'b) = Phantom('a * 'b) (set_impl_choose2 (of_phantom SET_IMPL('a)) (of_phantom SET_IMPL('b)))" instance .. end derive (choose) set_impl list derive (rbt) set_impl String.literal instantiation option :: (set_impl) set_impl begin definition "SET_IMPL('a option) = Phantom('a option) (of_phantom SET_IMPL('a))" instance .. end derive (monad) set_impl "fun" derive (choose) set_impl set instantiation phantom :: (type, set_impl) set_impl begin definition "SET_IMPL(('a, 'b) phantom) = Phantom (('a, 'b) phantom) (of_phantom SET_IMPL('b))" instance .. end text \ We enable automatic implementation selection for sets constructed by @{const set}, although they could be directly converted using @{const Set_Monad} in constant time. However, then it is more likely that the parameters of binary operators have different implementations, which can lead to less efficient execution. However, we test whether automatic selection picks @{const Set_Monad} anyway and take a short-cut. \ definition set_aux :: "set_impl \ 'a list \ 'a set" where [simp, code del]: "set_aux _ = set" lemma set_aux_code [code]: defines "conv \ foldl (\s (x :: 'a). insert x s)" shows "set_aux impl = conv (set_empty impl)" (is "?thesis1") "set_aux set_Choose = (case CCOMPARE('a :: {ccompare, ceq}) of Some _ \ conv (RBT_set RBT_Set2.empty) | None \ case CEQ('a) of None \ Set_Monad | Some _ \ conv (DList_set DList_Set.empty))" (is "?thesis2") "set_aux set_Monad = Set_Monad" proof - have "conv {} = set" by(rule ext)(induct_tac x rule: rev_induct, simp_all add: conv_def) thus ?thesis1 ?thesis2 by(simp_all split: option.split) qed simp lemma set_code [code]: fixes xs :: "'a :: set_impl list" shows "set xs = set_aux (of_phantom (ID SET_IMPL('a))) xs" by(simp) subsection \Pretty printing for sets\ text \ @{term code_post} marks contexts (as hypothesis) in which we use code\_post as a decision procedure rather than a pretty-printing engine. The intended use is to enable more rules when proving assumptions of rewrite rules. \ definition code_post :: bool where "code_post = True" lemma conj_code_post [code_post]: assumes code_post shows "True & x \ x" "False & x \ False" by simp_all text \ A flag to switch post-processing of sets on and off. Use \verb$declare pretty_sets[code_post del]$ to disable pretty printing of sets in value. \ definition code_post_set :: bool where pretty_sets [code_post, simp]: "code_post_set = True" definition collapse_RBT_set :: "'a set_rbt \ 'a :: ccompare set \ 'a set" where "collapse_RBT_set r M = set (RBT_Set2.keys r) \ M" lemma RBT_set_collapse_RBT_set [code_post]: fixes r :: "'a :: ccompare set_rbt" assumes "code_post \ is_ccompare TYPE('a)" and code_post_set shows "RBT_set r = collapse_RBT_set r {}" using assms by(clarsimp simp add: code_post_def is_ccompare_def RBT_set_def member_conv_keys collapse_RBT_set_def) lemma collapse_RBT_set_Branch [code_post]: "collapse_RBT_set (Mapping_RBT (Branch c l x v r)) M = collapse_RBT_set (Mapping_RBT l) (insert x (collapse_RBT_set (Mapping_RBT r) M))" unfolding collapse_RBT_set_def by(auto simp add: is_ccompare_def set_keys_Mapping_RBT) lemma collapse_RBT_set_Empty [code_post]: "collapse_RBT_set (Mapping_RBT rbt.Empty) M = M" by(auto simp add: collapse_RBT_set_def set_keys_Mapping_RBT) definition collapse_DList_set :: "'a :: ceq set_dlist \ 'a set" where "collapse_DList_set dxs = set (DList_Set.list_of_dlist dxs)" lemma DList_set_collapse_DList_set [code_post]: fixes dxs :: "'a :: ceq set_dlist" assumes "code_post \ is_ceq TYPE('a)" and code_post_set shows "DList_set dxs = collapse_DList_set dxs" using assms by(clarsimp simp add: code_post_def DList_set_def is_ceq_def collapse_DList_set_def Collect_member) lemma collapse_DList_set_empty [code_post]: "collapse_DList_set (Abs_dlist []) = {}" by(simp add: collapse_DList_set_def Abs_dlist_inverse) lemma collapse_DList_set_Cons [code_post]: "collapse_DList_set (Abs_dlist (x # xs)) = insert x (collapse_DList_set (Abs_dlist xs))" by(simp add: collapse_DList_set_def set_list_of_dlist_Abs_dlist) lemma Set_Monad_code_post [code_post]: assumes code_post_set shows "Set_Monad [] = {}" and "Set_Monad (x#xs) = insert x (Set_Monad xs)" by simp_all end diff --git a/thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy b/thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy --- a/thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy +++ b/thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy @@ -1,44 +1,44 @@ section\Sets\ text\While the default code generator setup for sets works fine, it does not make for particularly readable code. The reason for this is that the default setup needs to work with potentially infinite sets. All of the sets we need to use here are finite so we present an alternative setup for the basic set operations which generates much cleaner code.\ theory Code_Target_Set - imports "HOL-Library.Cardinality" + imports "HOL-Library.Code_Cardinality" begin code_datatype set declare List.union_coset_filter [code del] declare insert_code [code del] declare remove_code [code del] declare card_coset_error [code del] declare coset_subseteq_set_code [code del] declare eq_set_code(1) [code del] declare eq_set_code(2) [code del] declare eq_set_code(4) [code del] declare List.subset_code [code del] declare inter_coset_fold [code del] -declare Cardinality.subset'_code [code del] +declare Code_Cardinality.subset'_code [code del] declare subset_eq [code] (* Get rid of that one unnamed lemma *) lemma [code del]: "x \ List.coset xs \ \ List.member xs x" by (simp add: member_def) lemma sup_set_append[code]: "(set x) \ (set y) = set (x @ y)" by simp declare product_concat_map [code] lemma [code]: "insert x (set s) = (if x \ set s then set s else set (x#s))" apply (simp) by auto lemma [code]: - "Cardinality.subset' (set l1) (set l2) = ((list_all (\x. List.member l2 x)) l1)" + "Code_Cardinality.subset' (set l1) (set l2) = ((list_all (\x. List.member l2 x)) l1)" by (meson in_set_member list.pred_set subset'_code(2)) end diff --git a/thys/Gauss_Jordan/Code_Set.thy b/thys/Gauss_Jordan/Code_Set.thy --- a/thys/Gauss_Jordan/Code_Set.thy +++ b/thys/Gauss_Jordan/Code_Set.thy @@ -1,42 +1,42 @@ (* Title: Code_Set.thy Author: Jose Divasón Author: Jesús Aransay *) section "Code set" theory Code_Set imports - "HOL-Library.Cardinality" + "HOL-Library.Code_Cardinality" begin text\The following setup could help to get code generation for List.coset, but it neither works correctly it complains that code equations for remove are missed, even when List.coset should be rewritten to an enum:\ declare minus_coset_filter [code del] declare remove_code(2) [code del] declare insert_code(2) [code del] declare inter_coset_fold [code del] declare compl_coset[code del] -declare Cardinality.card'_code(2)[code del] +declare Code_Cardinality.card'_code(2)[code del] code_datatype set text\The following code equation could be useful to avoid the problem of code generation for List.coset []:\ lemma [code]: "List.coset (l::'a::enum list) = set (enum_class.enum) - set l" by (metis Compl_eq_Diff_UNIV coset_def enum_UNIV) text\Now the following examples work:\ value "UNIV::bool set" value "List.coset ([]::bool list)" value "UNIV::Enum.finite_2 set" value "List.coset ([]::Enum.finite_2 list)" value "List.coset ([]::Enum.finite_5 list)" end diff --git a/thys/JinjaThreads/Execute/Code_Generation.thy b/thys/JinjaThreads/Execute/Code_Generation.thy --- a/thys/JinjaThreads/Execute/Code_Generation.thy +++ b/thys/JinjaThreads/Execute/Code_Generation.thy @@ -1,168 +1,169 @@ (* Title: JinjaThreads/Execute/Code_Generation.thy Author: Andreas Lochbihler *) section \Code generator setup\ theory Code_Generation imports J_Execute JVM_Execute2 "../Compiler/Preprocessor" "../BV/BCVExec" "../Compiler/Compiler" Coinductive.Lazy_TLList + "HOL-Library.Code_Cardinality" "HOL-Library.Code_Target_Int" "HOL-Library.Code_Target_Numeral" begin text \Avoid module dependency cycles.\ (* FIXME: Eliminate dependency cycle in Isabelle library *) code_identifier code_module More_Set \ (SML) Set | code_module Set \ (SML) Set | code_module Complete_Lattices \ (SML) Set | code_module Complete_Partial_Order \ (SML) Set text \new code equation for @{term "insort_insert_key"} to avoid module dependency cycle with @{term "set"}.\ lemma insort_insert_key_code [code]: "insort_insert_key f x xs = (if List.member (map f xs) (f x) then xs else insort_key f x xs)" by(simp add: insort_insert_key_def List.member_def split del: if_split) text \equations on predicate operations for code inlining\ lemma eq_i_o_conv_single: "eq_i_o = Predicate.single" by(rule ext)(simp add: Predicate.single_bind eq.equation) lemma eq_o_i_conv_single: "eq_o_i = Predicate.single" by(rule ext)(simp add: Predicate.single_bind eq.equation) lemma sup_case_exp_case_exp_same: "sup_class.sup (case_exp cNew cNewArray cCast cInstanceOf cVal cBinOp cVar cLAss cAAcc cAAss cALen cFAcc cFAss cCAS cCall cBlock cSync cInSync cSeq cCond cWhile cThrow cTry e) (case_exp cNew' cNewArray' cCast' cInstanceOf' cVal' cBinOp' cVar' cLAss' cAAcc' cAAss' cALen' cFAcc' cFAss' cCAS' cCall' cBlock' cSync' cInSync' cSeq' cCond' cWhile' cThrow' cTry' e) = (case e of new C \ sup_class.sup (cNew C) (cNew' C) | newArray T e \ sup_class.sup (cNewArray T e) (cNewArray' T e) | Cast T e \ sup_class.sup (cCast T e) (cCast' T e) | InstanceOf e T \ sup_class.sup (cInstanceOf e T) (cInstanceOf' e T) | Val v \ sup_class.sup (cVal v) (cVal' v) | BinOp e bop e' \ sup_class.sup (cBinOp e bop e') (cBinOp' e bop e') | Var V \ sup_class.sup (cVar V) (cVar' V) | LAss V e \ sup_class.sup (cLAss V e) (cLAss' V e) | AAcc a e \ sup_class.sup (cAAcc a e) (cAAcc' a e) | AAss a i e \ sup_class.sup (cAAss a i e) (cAAss' a i e) | ALen a \ sup_class.sup (cALen a) (cALen' a) | FAcc e F D \ sup_class.sup (cFAcc e F D) (cFAcc' e F D) | FAss e F D e' \ sup_class.sup (cFAss e F D e') (cFAss' e F D e') | CompareAndSwap e D F e' e'' \ sup_class.sup (cCAS e D F e' e'') (cCAS' e D F e' e'') | Call e M es \ sup_class.sup (cCall e M es) (cCall' e M es) | Block V T vo e \ sup_class.sup (cBlock V T vo e) (cBlock' V T vo e) | Synchronized v e e' \ sup_class.sup (cSync v e e') (cSync' v e e') | InSynchronized v a e \ sup_class.sup (cInSync v a e) (cInSync' v a e) | Seq e e' \ sup_class.sup (cSeq e e') (cSeq' e e') | Cond b e e' \ sup_class.sup (cCond b e e') (cCond' b e e') | While b e \ sup_class.sup (cWhile b e) (cWhile' b e) | throw e \ sup_class.sup (cThrow e) (cThrow' e) | TryCatch e C V e' \ sup_class.sup (cTry e C V e') (cTry' e C V e'))" apply(cases e) apply(simp_all) done lemma sup_case_exp_case_exp_other: fixes p :: "'a :: semilattice_sup" shows "sup_class.sup (case_exp cNew cNewArray cCast cInstanceOf cVal cBinOp cVar cLAss cAAcc cAAss cALen cFAcc cFAss cCAS cCall cBlock cSync cInSync cSeq cCond cWhile cThrow cTry e) (sup_class.sup (case_exp cNew' cNewArray' cCast' cInstanceOf' cVal' cBinOp' cVar' cLAss' cAAcc' cAAss' cALen' cFAcc' cFAss' cCAS' cCall' cBlock' cSync' cInSync' cSeq' cCond' cWhile' cThrow' cTry' e) p) = sup_class.sup (case e of new C \ sup_class.sup (cNew C) (cNew' C) | newArray T e \ sup_class.sup (cNewArray T e) (cNewArray' T e) | Cast T e \ sup_class.sup (cCast T e) (cCast' T e) | InstanceOf e T \ sup_class.sup (cInstanceOf e T) (cInstanceOf' e T) | Val v \ sup_class.sup (cVal v) (cVal' v) | BinOp e bop e' \ sup_class.sup (cBinOp e bop e') (cBinOp' e bop e') | Var V \ sup_class.sup (cVar V) (cVar' V) | LAss V e \ sup_class.sup (cLAss V e) (cLAss' V e) | AAcc a e \ sup_class.sup (cAAcc a e) (cAAcc' a e) | AAss a i e \ sup_class.sup (cAAss a i e) (cAAss' a i e) | ALen a \ sup_class.sup (cALen a) (cALen' a) | FAcc e F D \ sup_class.sup (cFAcc e F D) (cFAcc' e F D) | FAss e F D e' \ sup_class.sup (cFAss e F D e') (cFAss' e F D e') | CompareAndSwap e D F e' e'' \ sup_class.sup (cCAS e D F e' e'') (cCAS' e D F e' e'') | Call e M es \ sup_class.sup (cCall e M es) (cCall' e M es) | Block V T vo e \ sup_class.sup (cBlock V T vo e) (cBlock' V T vo e) | Synchronized v e e' \ sup_class.sup (cSync v e e') (cSync' v e e') | InSynchronized v a e \ sup_class.sup (cInSync v a e) (cInSync' v a e) | Seq e e' \ sup_class.sup (cSeq e e') (cSeq' e e') | Cond b e e' \ sup_class.sup (cCond b e e') (cCond' b e e') | While b e \ sup_class.sup (cWhile b e) (cWhile' b e) | throw e \ sup_class.sup (cThrow e) (cThrow' e) | TryCatch e C V e' \ sup_class.sup (cTry e C V e') (cTry' e C V e')) p" apply(cases e) apply(simp_all add: inf_sup_aci sup.assoc) done lemma sup_bot1: "sup_class.sup bot a = (a :: 'a :: {semilattice_sup, order_bot})" by(rule sup_absorb2)auto lemma sup_bot2: "sup_class.sup a bot = (a :: 'a :: {semilattice_sup, order_bot})" by(rule sup_absorb1) auto lemma sup_case_val_case_val_same: "sup_class.sup (case_val cUnit cNull cBool cIntg cAddr v) (case_val cUnit' cNull' cBool' cIntg' cAddr' v) = (case v of Unit \ sup_class.sup cUnit cUnit' | Null \ sup_class.sup cNull cNull' | Bool b \ sup_class.sup (cBool b) (cBool' b) | Intg i \ sup_class.sup (cIntg i) (cIntg' i) | Addr a \ sup_class.sup (cAddr a) (cAddr' a))" apply(cases v) apply simp_all done lemma sup_case_bool_case_bool_same: "sup_class.sup (case_bool t f b) (case_bool t' f' b) = (if b then sup_class.sup t t' else sup_class.sup f f')" by simp lemmas predicate_code_inline [code_unfold] = Predicate.single_bind Predicate.bind_single split eq_i_o_conv_single eq_o_i_conv_single sup_case_exp_case_exp_same sup_case_exp_case_exp_other unit.case sup_bot1 sup_bot2 sup_case_val_case_val_same sup_case_bool_case_bool_same lemma op_case_ty_case_ty_same: "f (case_ty cVoid cBoolean cInteger cNT cClass cArray e) (case_ty cVoid' cBoolean' cInteger' cNT' cClass' cArray' e) = (case e of Void \ f cVoid cVoid' | Boolean \ f cBoolean cBoolean' | Integer \ f cInteger cInteger' | NT \ f cNT cNT' | Class C \ f (cClass C) (cClass' C) | Array T \ f (cArray T) (cArray' T))" by(simp split: ty.split) declare op_case_ty_case_ty_same[where f="sup_class.sup", code_unfold] lemma op_case_bop_case_bop_same: "f (case_bop cEq cNotEq cLessThan cLessOrEqual cGreaterThan cGreaterOrEqual cAdd cSubtract cMult cDiv cMod cBinAnd cBinOr cBinXor cShiftLeft cShiftRightZeros cShiftRightSigned bop) (case_bop cEq' cNotEq' cLessThan' cLessOrEqual' cGreaterThan' cGreaterOrEqual' cAdd' cSubtract' cMult' cDiv' cMod' cBinAnd' cBinOr' cBinXor' cShiftLeft' cShiftRightZeros' cShiftRightSigned' bop) = case_bop (f cEq cEq') (f cNotEq cNotEq') (f cLessThan cLessThan') (f cLessOrEqual cLessOrEqual') (f cGreaterThan cGreaterThan') (f cGreaterOrEqual cGreaterOrEqual') (f cAdd cAdd') (f cSubtract cSubtract') (f cMult cMult') (f cDiv cDiv') (f cMod cMod') (f cBinAnd cBinAnd') (f cBinOr cBinOr') (f cBinXor cBinXor') (f cShiftLeft cShiftLeft') (f cShiftRightZeros cShiftRightZeros') (f cShiftRightSigned cShiftRightSigned') bop" by(simp split: bop.split) lemma sup_case_bop_case_bop_other [code_unfold]: fixes p :: "'a :: semilattice_sup" shows "sup_class.sup (case_bop cEq cNotEq cLessThan cLessOrEqual cGreaterThan cGreaterOrEqual cAdd cSubtract cMult cDiv cMod cBinAnd cBinOr cBinXor cShiftLeft cShiftRightZeros cShiftRightSigned bop) (sup_class.sup (case_bop cEq' cNotEq' cLessThan' cLessOrEqual' cGreaterThan' cGreaterOrEqual' cAdd' cSubtract' cMult' cDiv' cMod' cBinAnd' cBinOr' cBinXor' cShiftLeft' cShiftRightZeros' cShiftRightSigned' bop) p) = sup_class.sup (case_bop (sup_class.sup cEq cEq') (sup_class.sup cNotEq cNotEq') (sup_class.sup cLessThan cLessThan') (sup_class.sup cLessOrEqual cLessOrEqual') (sup_class.sup cGreaterThan cGreaterThan') (sup_class.sup cGreaterOrEqual cGreaterOrEqual') (sup_class.sup cAdd cAdd') (sup_class.sup cSubtract cSubtract') (sup_class.sup cMult cMult') (sup_class.sup cDiv cDiv') (sup_class.sup cMod cMod') (sup_class.sup cBinAnd cBinAnd') (sup_class.sup cBinOr cBinOr') (sup_class.sup cBinXor cBinXor') (sup_class.sup cShiftLeft cShiftLeft') (sup_class.sup cShiftRightZeros cShiftRightZeros') (sup_class.sup cShiftRightSigned cShiftRightSigned') bop) p" apply(cases bop) apply(simp_all add: inf_sup_aci sup.assoc) done declare op_case_bop_case_bop_same[where f="sup_class.sup", code_unfold] end diff --git a/thys/JinjaThreads/Execute/Java2Jinja.thy b/thys/JinjaThreads/Execute/Java2Jinja.thy --- a/thys/JinjaThreads/Execute/Java2Jinja.thy +++ b/thys/JinjaThreads/Execute/Java2Jinja.thy @@ -1,89 +1,90 @@ (* Title: JinjaThreads/Execute/Java2Jinja.thy Author: Andreas Lochbihler *) section \Setup for converter Java2Jinja\ theory Java2Jinja imports Code_Generation ToString begin code_identifier code_module Java2Jinja \ (SML) Code_Generation definition j_Program :: "addr J_mb cdecl list \ addr J_prog" where "j_Program = Program" export_code wf_J_prog' j_Program in SML file \JWellForm.ML\ text \Functions for extracting calls to the native print method\ definition purge where "\run. purge run = lmap (\obs. case obs of ExternalCall _ _ (Cons (Intg i) _) v \ i) (lfilter (\obs. case obs of ExternalCall _ M (Cons (Intg i) Nil) _ \ M = print | _ \ False) (lconcat (lmap (llist_of \ snd) (llist_of_tllist run))))" text \Various other functions\ instantiation heapobj :: toString begin primrec toString_heapobj :: "heapobj \ String.literal" where "toString (Obj C fs) = sum_list [STR ''(Obj '', toString C, STR '', '', toString fs, STR '')'']" | "toString (Arr T si fs el) = sum_list [STR ''(['', toString si, STR '']'', toString T, STR '', '', toString fs, STR '', '', toString (map snd (rm_to_list el)), STR '')'']" instance proof qed end definition case_llist' where "case_llist' = case_llist" definition case_tllist' where "case_tllist' = case_tllist" definition terminal' where "terminal' = terminal" definition llist_of_tllist' where "llist_of_tllist' = llist_of_tllist" definition thr' where "thr' = thr" definition shr' where "shr' = shr" definition heap_toString :: "heap \ String.literal" where "heap_toString = toString" definition thread_toString :: "(thread_id, (addr expr \ addr locals) \ (addr \f nat)) rbt \ String.literal" where "thread_toString = toString" definition thread_toString' :: "(thread_id, addr jvm_thread_state' \ (addr \f nat)) rbt \ String.literal" where "thread_toString' = toString" definition trace_toString :: "thread_id \ (addr, thread_id) obs_event list \ String.literal" where "trace_toString = toString" code_identifier code_module Cardinality \ (SML) Set +| code_module Code_Cardinality \ (SML) Set | code_module Conditionally_Complete_Lattices \ (SML) Set | code_module List \ (SML) Set | code_module Predicate \ (SML) Set | code_module Parity \ (SML) Bit_Operations | type_class semiring_parity \ (SML) Bit_Operations.semiring_parity | class_instance int :: semiring_parity \ (SML) Bit_Operations.semiring_parity_int | class_instance int :: ring_parity \ (SML) Bit_Operations.semiring_parity_int | constant member_i_i \ (SML) Set.member_i_i export_code wf_J_prog' exec_J_rr exec_J_rnd j_Program purge case_llist' case_tllist' terminal' llist_of_tllist' thr' shr' heap_toString thread_toString trace_toString in SML file \J_Execute.ML\ definition j2jvm :: "addr J_prog \ addr jvm_prog" where "j2jvm = J2JVM" export_code wf_jvm_prog' exec_JVM_rr exec_JVM_rnd j2jvm j_Program purge case_llist' case_tllist' terminal' llist_of_tllist' thr' shr' heap_toString thread_toString' trace_toString in SML file \JVM_Execute2.ML\ end diff --git a/thys/MFODL_Monitor_Optimized/Monitor_Impl.thy b/thys/MFODL_Monitor_Optimized/Monitor_Impl.thy --- a/thys/MFODL_Monitor_Optimized/Monitor_Impl.thy +++ b/thys/MFODL_Monitor_Optimized/Monitor_Impl.thy @@ -1,489 +1,484 @@ (*<*) theory Monitor_Impl imports Monitor Optimized_MTL "HOL-Library.Code_Target_Nat" Containers.Containers begin (*>*) section \Instantiation of the generic algorithm and code setup\ -lemma [code_unfold del, symmetric, code_post del]: "card \ Cardinality.card'" by simp declare [[code drop: card]] Set_Impl.card_code[code] instantiation enat :: set_impl begin definition set_impl_enat :: "(enat, set_impl) phantom" where "set_impl_enat = phantom set_RBT" instance .. end derive ccompare Formula.trm derive (eq) ceq Formula.trm derive (rbt) set_impl Formula.trm derive (eq) ceq Monitor.mregex derive ccompare Monitor.mregex derive (rbt) set_impl Monitor.mregex derive (rbt) mapping_impl Monitor.mregex derive (no) cenum Monitor.mregex derive (rbt) set_impl event_data derive (rbt) mapping_impl event_data definition add_new_mmuaux' :: "args \ event_data table \ event_data table \ ts \ event_data mmuaux \ event_data mmuaux" where "add_new_mmuaux' = add_new_mmuaux" interpretation muaux valid_mmuaux init_mmuaux add_new_mmuaux' length_mmuaux eval_mmuaux using valid_init_mmuaux valid_add_new_mmuaux valid_length_mmuaux valid_eval_mmuaux unfolding add_new_mmuaux'_def by unfold_locales assumption+ type_synonym 'a vmsaux = "nat \ (nat \ 'a table) list" definition valid_vmsaux :: "args \ nat \ event_data vmsaux \ (nat \ event_data table) list \ bool" where "valid_vmsaux = (\_ cur (t, aux) auxlist. t = cur \ aux = auxlist)" definition init_vmsaux :: "args \ event_data vmsaux" where "init_vmsaux = (\_. (0, []))" definition add_new_ts_vmsaux :: "args \ nat \ event_data vmsaux \ event_data vmsaux" where "add_new_ts_vmsaux = (\args nt (t, auxlist). (nt, filter (\(t, rel). enat (nt - t) \ right (args_ivl args)) auxlist))" definition join_vmsaux :: "args \ event_data table \ event_data vmsaux \ event_data vmsaux" where "join_vmsaux = (\args rel1 (t, auxlist). (t, map (\(t, rel). (t, join rel (args_pos args) rel1)) auxlist))" definition add_new_table_vmsaux :: "args \ event_data table \ event_data vmsaux \ event_data vmsaux" where "add_new_table_vmsaux = (\args rel2 (cur, auxlist). (cur, (case auxlist of [] => [(cur, rel2)] | ((t, y) # ts) \ if t = cur then (t, y \ rel2) # ts else (cur, rel2) # auxlist)))" definition result_vmsaux :: "args \ event_data vmsaux \ event_data table" where "result_vmsaux = (\args (cur, auxlist). foldr (\) [rel. (t, rel) \ auxlist, left (args_ivl args) \ cur - t] {})" type_synonym 'a vmuaux = "nat \ (nat \ 'a table \ 'a table) list" definition valid_vmuaux :: "args \ nat \ event_data vmuaux \ (nat \ event_data table \ event_data table) list \ bool" where "valid_vmuaux = (\_ cur (t, aux) auxlist. t = cur \ aux = auxlist)" definition init_vmuaux :: "args \ event_data vmuaux" where "init_vmuaux = (\_. (0, []))" definition add_new_vmuaux :: "args \ event_data table \ event_data table \ nat \ event_data vmuaux \ event_data vmuaux" where "add_new_vmuaux = (\args rel1 rel2 nt (t, auxlist). (nt, update_until args rel1 rel2 nt auxlist))" definition length_vmuaux :: "args \ event_data vmuaux \ nat" where "length_vmuaux = (\_ (_, auxlist). length auxlist)" definition eval_vmuaux :: "args \ nat \ event_data vmuaux \ event_data table list \ event_data vmuaux" where "eval_vmuaux = (\args nt (t, auxlist). (let (res, auxlist') = eval_until (args_ivl args) nt auxlist in (res, (t, auxlist'))))" global_interpretation verimon_maux: maux valid_vmsaux init_vmsaux add_new_ts_vmsaux join_vmsaux add_new_table_vmsaux result_vmsaux valid_vmuaux init_vmuaux add_new_vmuaux length_vmuaux eval_vmuaux defines vminit0 = "maux.minit0 (init_vmsaux :: _ \ event_data vmsaux) (init_vmuaux :: _ \ event_data vmuaux) :: _ \ Formula.formula \ _" and vminit = "maux.minit (init_vmsaux :: _ \ event_data vmsaux) (init_vmuaux :: _ \ event_data vmuaux) :: Formula.formula \ _" and vminit_safe = "maux.minit_safe (init_vmsaux :: _ \ event_data vmsaux) (init_vmuaux :: _ \ event_data vmuaux) :: Formula.formula \ _" and vmupdate_since = "maux.update_since add_new_ts_vmsaux join_vmsaux add_new_table_vmsaux (result_vmsaux :: _ \ event_data vmsaux \ event_data table)" and vmeval = "maux.meval add_new_ts_vmsaux join_vmsaux add_new_table_vmsaux (result_vmsaux :: _ \ event_data vmsaux \ _) add_new_vmuaux (eval_vmuaux :: _ \ _ \ event_data vmuaux \ _)" and vmstep = "maux.mstep add_new_ts_vmsaux join_vmsaux add_new_table_vmsaux (result_vmsaux :: _ \ event_data vmsaux \ _) add_new_vmuaux (eval_vmuaux :: _ \ _ \ event_data vmuaux \ _)" and vmsteps0_stateless = "maux.msteps0_stateless add_new_ts_vmsaux join_vmsaux add_new_table_vmsaux (result_vmsaux :: _ \ event_data vmsaux \ _) add_new_vmuaux (eval_vmuaux :: _ \ _ \ event_data vmuaux \ _)" and vmsteps_stateless = "maux.msteps_stateless add_new_ts_vmsaux join_vmsaux add_new_table_vmsaux (result_vmsaux :: _ \ event_data vmsaux \ _) add_new_vmuaux (eval_vmuaux :: _ \ _ \ event_data vmuaux \ _)" and vmonitor = "maux.monitor init_vmsaux add_new_ts_vmsaux join_vmsaux add_new_table_vmsaux (result_vmsaux :: _ \ event_data vmsaux \ _) init_vmuaux add_new_vmuaux (eval_vmuaux :: _ \ _ \ event_data vmuaux \ _)" unfolding valid_vmsaux_def init_vmsaux_def add_new_ts_vmsaux_def join_vmsaux_def add_new_table_vmsaux_def result_vmsaux_def valid_vmuaux_def init_vmuaux_def add_new_vmuaux_def length_vmuaux_def eval_vmuaux_def by unfold_locales auto global_interpretation default_maux: maux valid_mmsaux "init_mmsaux :: _ \ event_data mmsaux" add_new_ts_mmsaux gc_join_mmsaux add_new_table_mmsaux result_mmsaux valid_mmuaux "init_mmuaux :: _ \ event_data mmuaux" add_new_mmuaux' length_mmuaux eval_mmuaux defines minit0 = "maux.minit0 (init_mmsaux :: _ \ event_data mmsaux) (init_mmuaux :: _ \ event_data mmuaux) :: _ \ Formula.formula \ _" and minit = "maux.minit (init_mmsaux :: _ \ event_data mmsaux) (init_mmuaux :: _ \ event_data mmuaux) :: Formula.formula \ _" and minit_safe = "maux.minit_safe (init_mmsaux :: _ \ event_data mmsaux) (init_mmuaux :: _ \ event_data mmuaux) :: Formula.formula \ _" and mupdate_since = "maux.update_since add_new_ts_mmsaux gc_join_mmsaux add_new_table_mmsaux (result_mmsaux :: _ \ event_data mmsaux \ event_data table)" and meval = "maux.meval add_new_ts_mmsaux gc_join_mmsaux add_new_table_mmsaux (result_mmsaux :: _ \ event_data mmsaux \ _) add_new_mmuaux' (eval_mmuaux :: _ \ _ \ event_data mmuaux \ _)" and mstep = "maux.mstep add_new_ts_mmsaux gc_join_mmsaux add_new_table_mmsaux (result_mmsaux :: _ \ event_data mmsaux \ _) add_new_mmuaux' (eval_mmuaux :: _ \ _ \ event_data mmuaux \ _)" and msteps0_stateless = "maux.msteps0_stateless add_new_ts_mmsaux gc_join_mmsaux add_new_table_mmsaux (result_mmsaux :: _ \ event_data mmsaux \ _) add_new_mmuaux' (eval_mmuaux :: _ \ _ \ event_data mmuaux \ _)" and msteps_stateless = "maux.msteps_stateless add_new_ts_mmsaux gc_join_mmsaux add_new_table_mmsaux (result_mmsaux :: _ \ event_data mmsaux \ _) add_new_mmuaux' (eval_mmuaux :: _ \ _ \ event_data mmuaux \ _)" and monitor = "maux.monitor init_mmsaux add_new_ts_mmsaux gc_join_mmsaux add_new_table_mmsaux (result_mmsaux :: _ \ event_data mmsaux \ _) init_mmuaux add_new_mmuaux' (eval_mmuaux :: _ \ _ \ event_data mmuaux \ _)" by unfold_locales lemma image_these: "f ` Option.these X = Option.these (map_option f ` X)" by (force simp: in_these_eq Bex_def image_iff map_option_case split: option.splits) thm default_maux.meval.simps(2) lemma meval_MPred: "meval n t db (MPred e ts) = (case Mapping.lookup db e of None \ [{}] | Some Xs \ map (\X. \v \ X. (set_option (map_option (\f. Table.tabulate f 0 n) (match ts v)))) Xs, MPred e ts)" by (force split: option.splits simp: Option.these_def image_iff) lemmas meval_code[code] = default_maux.meval.simps(1) meval_MPred default_maux.meval.simps(3-) definition mk_db :: "(Formula.name \ event_data list set) list \ _" where "mk_db t = Monitor.mk_db (\n \ set (map fst t). (\v. (n, v)) ` the (map_of t n))" definition rbt_fold :: "_ \ event_data tuple set_rbt \ _ \ _" where "rbt_fold = RBT_Set2.fold" definition rbt_empty :: "event_data list set_rbt" where "rbt_empty = RBT_Set2.empty" definition rbt_insert :: "_ \ _ \ event_data list set_rbt" where "rbt_insert = RBT_Set2.insert" lemma saturate_commute: assumes "\s. r \ g s" "\s. g (insert r s) = g s" "\s. r \ s \ h s = g s" and terminates: "mono g" "\X. X \ C \ g X \ C" "finite C" shows "saturate g {} = saturate h {r}" proof (cases "g {} = {r}") case True with assms have "g {r} = {r}" "h {r} = {r}" by auto with True show ?thesis by (subst (1 2) saturate_code; subst saturate_code) (simp add: Let_def) next case False then show ?thesis unfolding saturate_def while_def using while_option_finite_subset_Some[OF terminates] assms(1-3) by (subst while_option_commute_invariant[of "\S. S = {} \ r \ S" "\S. g S \ S" g "\S. h S \ S" "insert r" h "{}", symmetric]) (auto 4 4 dest: while_option_stop[of "\S. g S \ S" g "{}"]) qed definition "RPDs_aux = saturate (\S. S \ \ (RPD ` S))" lemma RPDs_aux_code[code]: "RPDs_aux S = (let S' = S \ Set.bind S RPD in if S' \ S then S else RPDs_aux S')" unfolding RPDs_aux_def bind_UNION by (subst saturate_code) auto declare RPDs_code[code del] lemma RPDs_code[code]: "RPDs r = RPDs_aux {r}" unfolding RPDs_aux_def RPDs_code by (rule saturate_commute[where C="RPDs r"]) (auto 0 3 simp: mono_def subset_singleton_iff RPDs_refl RPDs_trans finite_RPDs) definition "LPDs_aux = saturate (\S. S \ \ (LPD ` S))" lemma LPDs_aux_code[code]: "LPDs_aux S = (let S' = S \ Set.bind S LPD in if S' \ S then S else LPDs_aux S')" unfolding LPDs_aux_def bind_UNION by (subst saturate_code) auto declare LPDs_code[code del] lemma LPDs_code[code]: "LPDs r = LPDs_aux {r}" unfolding LPDs_aux_def LPDs_code by (rule saturate_commute[where C="LPDs r"]) (auto 0 3 simp: mono_def subset_singleton_iff LPDs_refl LPDs_trans finite_LPDs) lemma is_empty_table_unfold [code_unfold]: "X = empty_table \ Set.is_empty X" "empty_table = X \ Set.is_empty X" - "Cardinality.eq_set X empty_table \ Set.is_empty X" - "Cardinality.eq_set empty_table X \ Set.is_empty X" "set_eq X empty_table \ Set.is_empty X" "set_eq empty_table X \ Set.is_empty X" "X = (set_empty impl) \ Set.is_empty X" "(set_empty impl) = X \ Set.is_empty X" - "Cardinality.eq_set X (set_empty impl) \ Set.is_empty X" - "Cardinality.eq_set (set_empty impl) X \ Set.is_empty X" "set_eq X (set_empty impl) \ Set.is_empty X" "set_eq (set_empty impl) X \ Set.is_empty X" - unfolding set_eq_def set_empty_def empty_table_def Set.is_empty_def Cardinality.eq_set_def by auto + unfolding set_eq_def set_empty_def empty_table_def Set.is_empty_def by auto lemma tabulate_rbt_code[code]: "Monitor.mrtabulate (xs :: mregex list) f = (case ID CCOMPARE(mregex) of None \ Code.abort (STR ''tabulate RBT_Mapping: ccompare = None'') (\_. Monitor.mrtabulate (xs :: mregex list) f) | _ \ RBT_Mapping (RBT_Mapping2.bulkload (List.map_filter (\k. let fk = f k in if fk = empty_table then None else Some (k, fk)) xs)))" unfolding mrtabulate.abs_eq RBT_Mapping_def by (auto split: option.splits) lemma combine_Mapping[code]: fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows "Mapping.combine f (RBT_Mapping t) (RBT_Mapping u) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''combine RBT_Mapping: ccompare = None'') (\_. Mapping.combine f (RBT_Mapping t) (RBT_Mapping u)) | Some _ \ RBT_Mapping (RBT_Mapping2.join (\_. f) t u))" by (auto simp add: Mapping.combine.abs_eq Mapping_inject lookup_join split: option.split) lemma upd_set_empty[simp]: "upd_set m f {} = m" by transfer auto lemma upd_set_insert[simp]: "upd_set m f (insert x A) = Mapping.update x (f x) (upd_set m f A)" by (rule mapping_eqI) (auto simp: Mapping_lookup_upd_set Mapping.lookup_update') lemma upd_set_fold: assumes "finite A" shows "upd_set m f A = Finite_Set.fold (\a. Mapping.update a (f a)) m A" proof - interpret comp_fun_idem "\a. Mapping.update a (f a)" by unfold_locales (transfer; auto simp: fun_eq_iff)+ from assms show ?thesis by (induct A arbitrary: m rule: finite.induct) auto qed lift_definition upd_cfi :: "('a \ 'b) \ ('a, ('a, 'b) mapping) comp_fun_idem" is "\f a m. Mapping.update a (f a) m" by unfold_locales (transfer; auto simp: fun_eq_iff)+ lemma upd_set_code[code]: "upd_set m f A = (if finite A then set_fold_cfi (upd_cfi f) m A else Code.abort (STR ''upd_set: infinite'') (\_. upd_set m f A))" by (transfer fixing: m) (auto simp: upd_set_fold) lemma lexordp_eq_code[code]: "lexordp_eq xs ys \ (case xs of [] \ True | x # xs \ (case ys of [] \ False | y # ys \ if x < y then True else if x > y then False else lexordp_eq xs ys))" by (subst lexordp_eq.simps) (auto split: list.split) definition "filter_set m X t = Mapping.filter (filter_cond X m t) m" declare [[code drop: shift_end]] declare shift_end.simps[folded filter_set_def, code] lemma upd_set'_empty[simp]: "upd_set' m d f {} = m" by (rule mapping_eqI) (auto simp add: upd_set'_lookup) lemma upd_set'_insert: "d = f d \ (\x. f (f x) = f x) \ upd_set' m d f (insert x A) = (let m' = (upd_set' m d f A) in case Mapping.lookup m' x of None \ Mapping.update x d m' | Some v \ Mapping.update x (f v) m')" by (rule mapping_eqI) (auto simp: upd_set'_lookup Mapping.lookup_update' split: option.splits) lemma upd_set'_aux1: "upd_set' Mapping.empty d f {b. b = k \ (a, b) \ A} = Mapping.update k d (upd_set' Mapping.empty d f {b. (a, b) \ A})" by (rule mapping_eqI) (auto simp add: Let_def upd_set'_lookup Mapping.lookup_update' Mapping.lookup_empty split: option.splits) lemma upd_set'_aux2: "Mapping.lookup m k = None \ upd_set' m d f {b. b = k \ (a, b) \ A} = Mapping.update k d (upd_set' m d f {b. (a, b) \ A})" by (rule mapping_eqI) (auto simp add: upd_set'_lookup Mapping.lookup_update' split: option.splits) lemma upd_set'_aux3: "Mapping.lookup m k = Some v \ upd_set' m d f {b. b = k \ (a, b) \ A} = Mapping.update k (f v) (upd_set' m d f {b. (a, b) \ A})" by (rule mapping_eqI) (auto simp add: upd_set'_lookup Mapping.lookup_update' split: option.splits) lemma upd_set'_aux4: "k \ fst ` A \ upd_set' Mapping.empty d f {b. (k, b) \ A} = Mapping.empty" by (rule mapping_eqI) (auto simp add: upd_set'_lookup Mapping.lookup_update' Domain.DomainI fst_eq_Domain split: option.splits) lemma upd_nested_empty[simp]: "upd_nested m d f {} = m" by (rule mapping_eqI) (auto simp add: upd_nested_lookup split: option.splits) definition upd_nested_step :: "'c \ ('c \ 'c) \ 'a \ 'b \ ('a, ('b, 'c) mapping) mapping \ ('a, ('b, 'c) mapping) mapping" where "upd_nested_step d f x m = (case x of (k, k') \ (case Mapping.lookup m k of Some m' \ (case Mapping.lookup m' k' of Some v \ Mapping.update k (Mapping.update k' (f v) m') m | None \ Mapping.update k (Mapping.update k' d m') m) | None \ Mapping.update k (Mapping.update k' d Mapping.empty) m))" lemma upd_nested_insert: "d = f d \ (\x. f (f x) = f x) \ upd_nested m d f (insert x A) = upd_nested_step d f x (upd_nested m d f A)" unfolding upd_nested_step_def using upd_set'_aux1[of d f _ _ A] upd_set'_aux2[of _ _ d f _ A] upd_set'_aux3[of _ _ _ d f _ A] upd_set'_aux4[of _ A d f] by (auto simp add: Let_def upd_nested_lookup upd_set'_lookup Mapping.lookup_update' Mapping.lookup_empty split: option.splits prod.splits if_splits intro!: mapping_eqI) definition upd_nested_max_tstp where "upd_nested_max_tstp m d X = upd_nested m d (max_tstp d) X" lemma upd_nested_max_tstp_fold: assumes "finite X" shows "upd_nested_max_tstp m d X = Finite_Set.fold (upd_nested_step d (max_tstp d)) m X" proof - interpret comp_fun_idem "upd_nested_step d (max_tstp d)" by (unfold_locales; rule ext) (auto simp add: comp_def upd_nested_step_def Mapping.lookup_update' Mapping.lookup_empty update_update max_tstp_d_d max_tstp_idem' split: option.splits) note upd_nested_insert' = upd_nested_insert[of d "max_tstp d", OF max_tstp_d_d[symmetric] max_tstp_idem'] show ?thesis using assms by (induct X arbitrary: m rule: finite.induct) (auto simp add: upd_nested_max_tstp_def upd_nested_insert') qed lift_definition upd_nested_max_tstp_cfi :: "ts + tp \ ('a \ 'b, ('a, ('b, ts + tp) mapping) mapping) comp_fun_idem" is "\d. upd_nested_step d (max_tstp d)" by (unfold_locales; rule ext) (auto simp add: comp_def upd_nested_step_def Mapping.lookup_update' Mapping.lookup_empty update_update max_tstp_d_d max_tstp_idem' split: option.splits) lemma upd_nested_max_tstp_code[code]: "upd_nested_max_tstp m d X = (if finite X then set_fold_cfi (upd_nested_max_tstp_cfi d) m X else Code.abort (STR ''upd_nested_max_tstp: infinite'') (\_. upd_nested_max_tstp m d X))" by transfer (auto simp add: upd_nested_max_tstp_fold) declare [[code drop: add_new_mmuaux']] declare add_new_mmuaux'_def[unfolded add_new_mmuaux.simps, folded upd_nested_max_tstp_def, code] lemma filter_set_empty[simp]: "filter_set m {} t = m" unfolding filter_set_def by transfer (auto simp: fun_eq_iff split: option.splits) lemma filter_set_insert[simp]: "filter_set m (insert x A) t = (let m' = filter_set m A t in case Mapping.lookup m' x of Some u \ if t = u then Mapping.delete x m' else m' | _ \ m')" unfolding filter_set_def by transfer (auto simp: fun_eq_iff Let_def Map_To_Mapping.map_apply_def split: option.splits) lemma filter_set_fold: assumes "finite A" shows "filter_set m A t = Finite_Set.fold (\a m. case Mapping.lookup m a of Some u \ if t = u then Mapping.delete a m else m | _ \ m) m A" proof - interpret comp_fun_idem "\a m. case Mapping.lookup m a of Some u \ if t = u then Mapping.delete a m else m | _ \ m" by unfold_locales (transfer; auto simp: fun_eq_iff Map_To_Mapping.map_apply_def split: option.splits)+ from assms show ?thesis by (induct A arbitrary: m rule: finite.induct) (auto simp: Let_def) qed lift_definition filter_cfi :: "'b \ ('a, ('a, 'b) mapping) comp_fun_idem" is "\t a m. case Mapping.lookup m a of Some u \ if t = u then Mapping.delete a m else m | _ \ m" by unfold_locales (transfer; auto simp: fun_eq_iff Map_To_Mapping.map_apply_def split: option.splits)+ lemma filter_set_code[code]: "filter_set m A t = (if finite A then set_fold_cfi (filter_cfi t) m A else Code.abort (STR ''upd_set: infinite'') (\_. filter_set m A t))" by (transfer fixing: m) (auto simp: filter_set_fold) lemma filter_Mapping[code]: fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows "Mapping.filter P (RBT_Mapping t) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''filter RBT_Mapping: ccompare = None'') (\_. Mapping.filter P (RBT_Mapping t)) | Some _ \ RBT_Mapping (RBT_Mapping2.filter (case_prod P) t))" by (auto simp add: Mapping.filter.abs_eq Mapping_inject split: option.split) definition "filter_join pos X m = Mapping.filter (join_filter_cond pos X) m" declare [[code drop: join_mmsaux]] declare join_mmsaux.simps[folded filter_join_def, code] lemma filter_join_False_empty: "filter_join False {} m = m" unfolding filter_join_def by transfer (auto split: option.splits) lemma filter_join_False_insert: "filter_join False (insert a A) m = filter_join False A (Mapping.delete a m)" proof - { fix x have "Mapping.lookup (filter_join False (insert a A) m) x = Mapping.lookup (filter_join False A (Mapping.delete a m)) x" by (auto simp add: filter_join_def Mapping.lookup_filter Mapping_lookup_delete split: option.splits) } then show ?thesis by (simp add: mapping_eqI) qed lemma filter_join_False: assumes "finite A" shows "filter_join False A m = Finite_Set.fold Mapping.delete m A" proof - interpret comp_fun_idem "Mapping.delete" by (unfold_locales; transfer) (fastforce simp add: comp_def)+ from assms show ?thesis by (induction A arbitrary: m rule: finite.induct) (auto simp add: filter_join_False_empty filter_join_False_insert fold_fun_left_comm) qed lift_definition filter_not_in_cfi :: "('a, ('a, 'b) mapping) comp_fun_idem" is "Mapping.delete" by (unfold_locales; transfer) (fastforce simp add: comp_def)+ lemma filter_join_code[code]: "filter_join pos A m = (if \pos \ finite A \ card A < Mapping.size m then set_fold_cfi filter_not_in_cfi m A else Mapping.filter (join_filter_cond pos A) m)" unfolding filter_join_def by (transfer fixing: m) (use filter_join_False in \auto simp add: filter_join_def\) definition set_minus :: "'a set \ 'a set \ 'a set" where "set_minus X Y = X - Y" lift_definition remove_cfi :: "('a, 'a set) comp_fun_idem" is "\b a. a - {b}" by unfold_locales auto lemma set_minus_finite: assumes fin: "finite Y" shows "set_minus X Y = Finite_Set.fold (\a X. X - {a}) X Y" proof - interpret comp_fun_idem "\a X. X - {a}" by unfold_locales auto from assms show ?thesis by (induction Y arbitrary: X rule: finite.induct) (auto simp add: set_minus_def) qed lemma set_minus_code[code]: "set_minus X Y = (if finite Y \ card Y < card X then set_fold_cfi remove_cfi X Y else X - Y)" by transfer (use set_minus_finite in \auto simp add: set_minus_def\) declare [[code drop: bin_join]] declare bin_join.simps[folded set_minus_def, code] definition remove_Union where "remove_Union A X B = A - (\x \ X. B x)" lemma remove_Union_finite: assumes "finite X" shows "remove_Union A X B = Finite_Set.fold (\x A. A - B x) A X" proof - interpret comp_fun_idem "\x A. A - B x" by unfold_locales auto from assms show ?thesis by (induct X arbitrary: A rule: finite_induct) (auto simp: remove_Union_def) qed lift_definition remove_Union_cfi :: "('a \ 'b set) \ ('a, 'b set) comp_fun_idem" is "\B x A. A - B x" by unfold_locales auto lemma remove_Union_code[code]: "remove_Union A X B = (if finite X then set_fold_cfi (remove_Union_cfi B) A X else A - (\x \ X. B x))" by (transfer fixing: A X B) (use remove_Union_finite[of X A B] in \auto simp add: remove_Union_def\) lemma tabulate_remdups: "Mapping.tabulate xs f = Mapping.tabulate (remdups xs) f" by (transfer fixing: xs f) (auto simp: map_of_map_restrict) lift_definition clearjunk :: "(String.literal \ event_data list set) list \ (String.literal, event_data list set list) alist" is "\t. List.map_filter (\(p, X). if X = {} then None else Some (p, [X])) (AList.clearjunk t)" unfolding map_filter_def o_def list.map_comp by (subst map_cong[OF refl, of _ _ fst]) (auto simp: map_filter_def distinct_map_fst_filter split: if_splits) lemma map_filter_snd_map_filter: "List.map_filter (\(a, b). if P b then None else Some (f a b)) xs = map (\(a, b). f a b) (filter (\x. \ P (snd x)) xs)" by (simp add: map_filter_def prod.case_eq_if) lemma mk_db_code_alist: "mk_db t = Assoc_List_Mapping (clearjunk t)" unfolding mk_db_def Assoc_List_Mapping_def by (transfer' fixing: t) (auto simp: map_filter_snd_map_filter fun_eq_iff map_of_map image_iff map_of_clearjunk map_of_filter_apply dest: weak_map_of_SomeI intro!: bexI[rotated, OF map_of_SomeD] split: if_splits option.splits) lemma mk_db_code[code]: "mk_db t = Mapping.of_alist (List.map_filter (\(p, X). if X = {} then None else Some (p, [X])) (AList.clearjunk t))" unfolding mk_db_def by (transfer' fixing: t) (auto simp: map_filter_snd_map_filter fun_eq_iff map_of_map image_iff map_of_clearjunk map_of_filter_apply dest: weak_map_of_SomeI intro!: bexI[rotated, OF map_of_SomeD] split: if_splits option.splits) declare [[code drop: New_max_getIJ_genericJoin New_max_getIJ_wrapperGenericJoin]] declare New_max.genericJoin.simps[folded remove_Union_def, code] declare New_max.wrapperGenericJoin.simps[folded remove_Union_def, code] (*<*) end (*>*) diff --git a/thys/Physical_Quantities/Enum_extra.thy b/thys/Physical_Quantities/Enum_extra.thy --- a/thys/Physical_Quantities/Enum_extra.thy +++ b/thys/Physical_Quantities/Enum_extra.thy @@ -1,94 +1,94 @@ section \ Enumeration Extras \ theory Enum_extra - imports "HOL-Library.Cardinality" + imports "HOL-Library.Code_Cardinality" begin subsection \ First Index Function \ text \ The following function extracts the index of the first occurrence of an element in a list, assuming it is indeed an element. \ fun first_ind :: "'a list \ 'a \ nat \ nat" where "first_ind [] y i = undefined" | "first_ind (x # xs) y i = (if (x = y) then i else first_ind xs y (Suc i))" lemma first_ind_length: "x \ set(xs) \ first_ind xs x i < length(xs) + i" by (induct xs arbitrary: i, auto, metis add_Suc_right) lemma nth_first_ind: "\ distinct xs; x \ set(xs) \ \ xs ! (first_ind xs x i - i) = x" apply (induct xs arbitrary: i) apply (auto) apply (metis One_nat_def add.right_neutral add_Suc_right add_diff_cancel_left' diff_diff_left empty_iff first_ind.simps(2) list.set(1) nat.simps(3) neq_Nil_conv nth_Cons' zero_diff) done lemma first_ind_nth: "\ distinct xs; i < length xs \ \ first_ind xs (xs ! i) j = i + j" apply (induct xs arbitrary: i j) apply (auto) apply (metis less_Suc_eq_le nth_equal_first_eq) using less_Suc_eq_0_disj apply auto done subsection \ Enumeration Indices \ syntax "_ENUM" :: "type \ logic" ("ENUM'(_')") translations "ENUM('a)" => "CONST Enum.enum :: ('a::enum) list" text \ Extract a unique natural number associated with an enumerated value by using its index in the characteristic list \<^term>\ENUM('a)\. \ definition enum_ind :: "'a::enum \ nat" where "enum_ind (x :: 'a::enum) = first_ind ENUM('a) x 0" lemma length_enum_CARD: "length ENUM('a) = CARD('a)" by (simp add: UNIV_enum distinct_card enum_distinct) lemma CARD_length_enum: "CARD('a) = length ENUM('a)" by (simp add: length_enum_CARD) lemma enum_ind_less_CARD [simp]: "enum_ind (x :: 'a::enum) < CARD('a)" using first_ind_length[of x, OF in_enum, of 0] by (simp add: enum_ind_def CARD_length_enum) lemma enum_nth_ind [simp]: "Enum.enum ! (enum_ind x) = x" using nth_first_ind[of Enum.enum x 0, OF enum_distinct in_enum] by (simp add: enum_ind_def) lemma enum_distinct_conv_nth: assumes "i < CARD('a)" "j < CARD('a)" "ENUM('a) ! i = ENUM('a) ! j" shows "i = j" proof - have "(\ij j \ ENUM('a) ! i \ ENUM('a) ! j)" using distinct_conv_nth[of "ENUM('a)", THEN sym] by (simp add: enum_distinct) with assms show ?thesis by (auto simp add: CARD_length_enum) qed lemma enum_ind_nth [simp]: assumes "i < CARD('a::enum)" shows "enum_ind (ENUM('a) ! i) = i" using assms first_ind_nth[of "ENUM('a)" i 0, OF enum_distinct] by (simp add: enum_ind_def CARD_length_enum) lemma enum_ind_spec: "enum_ind (x :: 'a::enum) = (THE i. i < CARD('a) \ Enum.enum ! i = x)" proof (rule sym, rule the_equality, safe) show "enum_ind x < CARD('a)" by (simp add: enum_ind_less_CARD[of x]) show "enum_class.enum ! enum_ind x = x" by simp show "\i. i < CARD('a) \ x = ENUM('a) ! i \ i = enum_ind (ENUM('a) ! i)" by (simp add: enum_ind_nth) qed lemma enum_ind_inj: "inj (enum_ind :: 'a::enum \ nat)" by (rule inj_on_inverseI[of _ "\ i. ENUM('a) ! i"], simp) lemma enum_ind_neq [simp]: "x \ y \ enum_ind x \ enum_ind y" by (simp add: enum_ind_inj inj_eq) end \ No newline at end of file