# HG changeset patch # User Cezary Kaliszyk # Date 1271932431 -7200 # Node ID 266abc3ee228258745d4b71c010f79e674f6752f # Parent 8f6e68dc6cbc27eb0a8609d48c6b755f7c5851f3 Moved working Fset3 properties to FSet. diff -r 8f6e68dc6cbc -r 266abc3ee228 Attic/Quot/Examples/FSet3.thy --- a/Attic/Quot/Examples/FSet3.thy Thu Apr 22 06:44:24 2010 +0200 +++ b/Attic/Quot/Examples/FSet3.thy Thu Apr 22 12:33:51 2010 +0200 @@ -2,246 +2,6 @@ imports "../../../Nominal/FSet" begin -notation - list_eq (infix "\" 50) - -lemma fset_exhaust[case_names fempty finsert, cases type: fset]: - shows "\S = {||} \ P; \x S'. S = finsert x S' \ P\ \ P" - by (lifting list.exhaust) - -lemma list_rel_find_element: - assumes a: "x \ set a" - and b: "list_rel R a b" - shows "\y. (y \ set b \ R x y)" -proof - - have "length a = length b" using b by (rule list_rel_len) - then show ?thesis using a b proof (induct a b rule: list_induct2) - case Nil - show ?case using Nil.prems by simp - next - case (Cons x xs y ys) - show ?case using Cons by auto - qed -qed - -lemma concat_rsp_pre: - assumes a: "list_rel op \ x x'" - and b: "x' \ y'" - and c: "list_rel op \ y' y" - and d: "\x\set x. xa \ set x" - shows "\x\set y. xa \ set x" -proof - - obtain xb where e: "xb \ set x" and f: "xa \ set xb" using d by auto - have "\y. y \ set x' \ xb \ y" by (rule list_rel_find_element[OF e a]) - then obtain ya where h: "ya \ set x'" and i: "xb \ ya" by auto - have j: "ya \ set y'" using b h by simp - have "\yb. yb \ set y \ ya \ yb" by (rule list_rel_find_element[OF j c]) - then show ?thesis using f i by auto -qed - -lemma fun_relI [intro]: - assumes "\a b. P a b \ Q (x a) (y b)" - shows "(P ===> Q) x y" - using assms by (simp add: fun_rel_def) - -lemma [quot_respect]: - shows "(list_rel op \ OOO op \ ===> op \) concat concat" -proof (rule fun_relI, elim pred_compE) - fix a b ba bb - assume a: "list_rel op \ a ba" - assume b: "ba \ bb" - assume c: "list_rel op \ bb b" - have "\x. (\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof - fix x - show "(\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof - assume d: "\xa\set a. x \ set xa" - show "\xa\set b. x \ set xa" by (rule concat_rsp_pre[OF a b c d]) - next - assume e: "\xa\set b. x \ set xa" - have a': "list_rel op \ ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) - have b': "bb \ ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) - have c': "list_rel op \ b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) - show "\xa\set a. x \ set xa" by (rule concat_rsp_pre[OF c' b' a' e]) - qed - qed - then show "concat a \ concat b" by simp -qed - -lemma nil_rsp2[quot_respect]: "(list_rel op \ OOO op \) [] []" - by (metis nil_rsp list_rel.simps(1) pred_compI) - -lemma set_in_eq: "(\e. ((e \ A) \ (e \ B))) \ A = B" - by (rule eq_reflection) auto - -lemma map_rel_cong: "b \ ba \ map f b \ map f ba" - unfolding list_eq.simps - by (simp only: set_map set_in_eq) - -lemma compose_list_refl: - shows "(list_rel op \ OOO op \) r r" -proof - show c: "list_rel op \ r r" by (rule list_rel_refl) (metis equivp_def fset_equivp) - have d: "r \ r" by (rule equivp_reflp[OF fset_equivp]) - show b: "(op \ OO list_rel op \) r r" by (rule pred_compI) (rule d, rule c) -qed - -lemma list_rel_refl: - shows "(list_rel op \) r r" - by (rule list_rel_refl)(metis equivp_def fset_equivp) - -lemma Quotient_fset_list: - shows "Quotient (list_rel op \) (map abs_fset) (map rep_fset)" - by (fact list_quotient[OF Quotient_fset]) - -lemma quotient_compose_list[quot_thm]: - shows "Quotient ((list_rel op \) OOO (op \)) - (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" - unfolding Quotient_def comp_def -proof (intro conjI allI) - fix a r s - show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a" - by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id) - have b: "list_rel op \ (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" - by (rule list_rel_refl) - have c: "(op \ OO list_rel op \) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" - by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) - show "(list_rel op \ OOO op \) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" - by (rule, rule list_rel_refl) (rule c) - show "(list_rel op \ OOO op \) r s = ((list_rel op \ OOO op \) r r \ - (list_rel op \ OOO op \) s s \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" - proof (intro iffI conjI) - show "(list_rel op \ OOO op \) r r" by (rule compose_list_refl) - show "(list_rel op \ OOO op \) s s" by (rule compose_list_refl) - next - assume a: "(list_rel op \ OOO op \) r s" - then have b: "map abs_fset r \ map abs_fset s" proof (elim pred_compE) - fix b ba - assume c: "list_rel op \ r b" - assume d: "b \ ba" - assume e: "list_rel op \ ba s" - have f: "map abs_fset r = map abs_fset b" - by (metis Quotient_rel[OF Quotient_fset_list] c) - have g: "map abs_fset s = map abs_fset ba" - by (metis Quotient_rel[OF Quotient_fset_list] e) - show "map abs_fset r \ map abs_fset s" using d f g map_rel_cong by simp - qed - then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" - by (metis Quotient_rel[OF Quotient_fset]) - next - assume a: "(list_rel op \ OOO op \) r r \ (list_rel op \ OOO op \) s s - \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" - then have s: "(list_rel op \ OOO op \) s s" by simp - have d: "map abs_fset r \ map abs_fset s" - by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) - have b: "map rep_fset (map abs_fset r) \ map rep_fset (map abs_fset s)" - by (rule map_rel_cong[OF d]) - have y: "list_rel op \ (map rep_fset (map abs_fset s)) s" - by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]]) - have c: "(op \ OO list_rel op \) (map rep_fset (map abs_fset r)) s" - by (rule pred_compI) (rule b, rule y) - have z: "list_rel op \ r (map rep_fset (map abs_fset r))" - by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]]) - then show "(list_rel op \ OOO op \) r s" - using a c pred_compI by simp - qed -qed - -lemma nil_prs2[quot_preserve]: "(abs_fset \ map f) [] = abs_fset []" - by simp - -lemma fconcat_empty: - shows "fconcat {||} = {||}" - by (lifting concat.simps(1)) - -lemma insert_rsp2[quot_respect]: - "(op \ ===> list_rel op \ OOO op \ ===> list_rel op \ OOO op \) op # op #" - apply auto - apply (simp add: set_in_eq) - apply (rule_tac b="x # b" in pred_compI) - apply auto - apply (rule_tac b="x # ba" in pred_compI) - apply auto - done - -lemma append_rsp[quot_respect]: - "(op \ ===> op \ ===> op \) op @ op @" - by (auto) - -lemma insert_prs2[quot_preserve]: - "(rep_fset ---> (map rep_fset \ rep_fset) ---> (abs_fset \ map abs_fset)) op # = finsert" - by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] - abs_o_rep[OF Quotient_fset] map_id finsert_def) - -lemma fconcat_insert: - shows "fconcat (finsert x S) = x |\| fconcat S" - by (lifting concat.simps(2)) - -lemma append_prs2[quot_preserve]: - "((map rep_fset \ rep_fset) ---> (map rep_fset \ rep_fset) ---> abs_fset \ map abs_fset) op @ = funion" - by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] - abs_o_rep[OF Quotient_fset] map_id sup_fset_def) - -lemma list_rel_app_l: - assumes a: "reflp R" - and b: "list_rel R l r" - shows "list_rel R (z @ l) (z @ r)" - by (induct z) (simp_all add: b, metis a reflp_def) - -lemma append_rsp2_pre0: - assumes a:"list_rel op \ x x'" - shows "list_rel op \ (x @ z) (x' @ z)" - using a apply (induct x x' rule: list_induct2') - apply simp_all - apply (rule list_rel_refl) - done - -lemma append_rsp2_pre1: - assumes a:"list_rel op \ x x'" - shows "list_rel op \ (z @ x) (z @ x')" - using a apply (induct x x' arbitrary: z rule: list_induct2') - apply (rule list_rel_refl) - apply (simp_all del: list_eq.simps) - apply (rule list_rel_app_l) - apply (simp_all add: reflp_def) - done - -lemma append_rsp2_pre: - assumes a:"list_rel op \ x x'" - and b: "list_rel op \ z z'" - shows "list_rel op \ (x @ z) (x' @ z')" - apply (rule list_rel_transp[OF fset_equivp]) - apply (rule append_rsp2_pre0) - apply (rule a) - using b apply (induct z z' rule: list_induct2') - apply (simp_all only: append_Nil2) - apply (rule list_rel_refl) - apply simp_all - apply (rule append_rsp2_pre1) - apply simp - done - -lemma append_rsp2[quot_respect]: - "(list_rel op \ OOO op \ ===> list_rel op \ OOO op \ ===> list_rel op \ OOO op \) op @ op @" -proof (intro fun_relI, elim pred_compE) - fix x y z w x' z' y' w' :: "'a list list" - assume a:"list_rel op \ x x'" - and b: "x' \ y'" - and c: "list_rel op \ y' y" - assume aa: "list_rel op \ z z'" - and bb: "z' \ w'" - and cc: "list_rel op \ w' w" - have a': "list_rel op \ (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto - have b': "x' @ z' \ y' @ w'" using b bb by simp - have c': "list_rel op \ (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto - have d': "(op \ OO list_rel op \) (x' @ z') (y @ w)" - by (rule pred_compI) (rule b', rule c') - show "(list_rel op \ OOO op \) (x @ z) (y @ w)" - by (rule pred_compI) (rule a', rule d') -qed - -lemma "fconcat (xs |\| ys) = fconcat xs |\| fconcat ys" - by (lifting concat_append) - (* TBD *) text {* syntax for fset comprehensions (adapted from lists) *} diff -r 8f6e68dc6cbc -r 266abc3ee228 Nominal/FSet.thy --- a/Nominal/FSet.thy Thu Apr 22 06:44:24 2010 +0200 +++ b/Nominal/FSet.thy Thu Apr 22 12:33:51 2010 +0200 @@ -71,6 +71,84 @@ else f a (ffold_raw f z A) else z)" +text {* Composition Quotient *} + +lemma compose_list_refl: + shows "(list_rel op \ OOO op \) r r" +proof + show c: "list_rel op \ r r" by (rule list_rel_refl) (metis equivp_def fset_equivp) + have d: "r \ r" by (rule equivp_reflp[OF fset_equivp]) + show b: "(op \ OO list_rel op \) r r" by (rule pred_compI) (rule d, rule c) +qed + +lemma list_rel_refl: + shows "(list_rel op \) r r" + by (rule list_rel_refl)(metis equivp_def fset_equivp) + +lemma Quotient_fset_list: + shows "Quotient (list_rel op \) (map abs_fset) (map rep_fset)" + by (fact list_quotient[OF Quotient_fset]) + +lemma set_in_eq: "(\e. ((e \ A) \ (e \ B))) \ A = B" + by (rule eq_reflection) auto + +lemma map_rel_cong: "b \ ba \ map f b \ map f ba" + unfolding list_eq.simps + by (simp only: set_map set_in_eq) + +lemma quotient_compose_list[quot_thm]: + shows "Quotient ((list_rel op \) OOO (op \)) + (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" + unfolding Quotient_def comp_def +proof (intro conjI allI) + fix a r s + show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a" + by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id) + have b: "list_rel op \ (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" + by (rule list_rel_refl) + have c: "(op \ OO list_rel op \) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" + by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) + show "(list_rel op \ OOO op \) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" + by (rule, rule list_rel_refl) (rule c) + show "(list_rel op \ OOO op \) r s = ((list_rel op \ OOO op \) r r \ + (list_rel op \ OOO op \) s s \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" + proof (intro iffI conjI) + show "(list_rel op \ OOO op \) r r" by (rule compose_list_refl) + show "(list_rel op \ OOO op \) s s" by (rule compose_list_refl) + next + assume a: "(list_rel op \ OOO op \) r s" + then have b: "map abs_fset r \ map abs_fset s" proof (elim pred_compE) + fix b ba + assume c: "list_rel op \ r b" + assume d: "b \ ba" + assume e: "list_rel op \ ba s" + have f: "map abs_fset r = map abs_fset b" + by (metis Quotient_rel[OF Quotient_fset_list] c) + have g: "map abs_fset s = map abs_fset ba" + by (metis Quotient_rel[OF Quotient_fset_list] e) + show "map abs_fset r \ map abs_fset s" using d f g map_rel_cong by simp + qed + then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" + by (metis Quotient_rel[OF Quotient_fset]) + next + assume a: "(list_rel op \ OOO op \) r r \ (list_rel op \ OOO op \) s s + \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" + then have s: "(list_rel op \ OOO op \) s s" by simp + have d: "map abs_fset r \ map abs_fset s" + by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) + have b: "map rep_fset (map abs_fset r) \ map rep_fset (map abs_fset s)" + by (rule map_rel_cong[OF d]) + have y: "list_rel op \ (map rep_fset (map abs_fset s)) s" + by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]]) + have c: "(op \ OO list_rel op \) (map rep_fset (map abs_fset r)) s" + by (rule pred_compI) (rule b, rule y) + have z: "list_rel op \ r (map rep_fset (map abs_fset r))" + by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]]) + then show "(list_rel op \ OOO op \) r s" + using a c pred_compI by simp + qed +qed + text {* Respectfullness *} lemma [quot_respect]: @@ -217,6 +295,44 @@ "(op = ===> op = ===> op \ ===> op =) ffold_raw ffold_raw" by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) +lemma concat_rsp_pre: + assumes a: "list_rel op \ x x'" + and b: "x' \ y'" + and c: "list_rel op \ y' y" + and d: "\x\set x. xa \ set x" + shows "\x\set y. xa \ set x" +proof - + obtain xb where e: "xb \ set x" and f: "xa \ set xb" using d by auto + have "\y. y \ set x' \ xb \ y" by (rule list_rel_find_element[OF e a]) + then obtain ya where h: "ya \ set x'" and i: "xb \ ya" by auto + have j: "ya \ set y'" using b h by simp + have "\yb. yb \ set y \ ya \ yb" by (rule list_rel_find_element[OF j c]) + then show ?thesis using f i by auto +qed + +lemma [quot_respect]: + shows "(list_rel op \ OOO op \ ===> op \) concat concat" +proof (rule fun_relI, elim pred_compE) + fix a b ba bb + assume a: "list_rel op \ a ba" + assume b: "ba \ bb" + assume c: "list_rel op \ bb b" + have "\x. (\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof + fix x + show "(\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof + assume d: "\xa\set a. x \ set xa" + show "\xa\set b. x \ set xa" by (rule concat_rsp_pre[OF a b c d]) + next + assume e: "\xa\set b. x \ set xa" + have a': "list_rel op \ ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) + have b': "bb \ ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) + have c': "list_rel op \ b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) + show "\xa\set a. x \ set xa" by (rule concat_rsp_pre[OF c' b' a' e]) + qed + qed + then show "concat a \ concat b" by simp +qed + text {* Distributive lattice with bot *} lemma sub_list_not_eq: @@ -379,7 +495,122 @@ where "x |\| S \ \ (x |\| S)" -section {* Augmenting an fset -- @{const finsert} *} +section {* Other constants on the Quotient Type *} + +quotient_definition + "fcard :: 'a fset \ nat" +is + "fcard_raw" + +quotient_definition + "fmap :: ('a \ 'b) \ 'a fset \ 'b fset" +is + "map" + +quotient_definition + "fdelete :: 'a fset \ 'a \ 'a fset" + is "delete_raw" + +quotient_definition + "fset_to_set :: 'a fset \ 'a set" + is "set" + +quotient_definition + "ffold :: ('a \ 'b \ 'b) \ 'b \ 'a fset \ 'b" + is "ffold_raw" + +quotient_definition + "fconcat :: ('a fset) fset \ 'a fset" +is + "concat" + +text {* Compositional Respectfullness and Preservation *} + +lemma [quot_respect]: "(list_rel op \ OOO op \) [] []" + by (metis nil_rsp list_rel.simps(1) pred_compI) + +lemma [quot_preserve]: "(abs_fset \ map f) [] = abs_fset []" + by simp + +lemma [quot_respect]: + "(op \ ===> list_rel op \ OOO op \ ===> list_rel op \ OOO op \) op # op #" + apply auto + apply (simp add: set_in_eq) + apply (rule_tac b="x # b" in pred_compI) + apply auto + apply (rule_tac b="x # ba" in pred_compI) + apply auto + done + +lemma [quot_preserve]: + "(rep_fset ---> (map rep_fset \ rep_fset) ---> (abs_fset \ map abs_fset)) op # = finsert" + by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] + abs_o_rep[OF Quotient_fset] map_id finsert_def) + +lemma [quot_preserve]: + "((map rep_fset \ rep_fset) ---> (map rep_fset \ rep_fset) ---> abs_fset \ map abs_fset) op @ = funion" + by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] + abs_o_rep[OF Quotient_fset] map_id sup_fset_def) + +lemma list_rel_app_l: + assumes a: "reflp R" + and b: "list_rel R l r" + shows "list_rel R (z @ l) (z @ r)" + by (induct z) (simp_all add: b, metis a reflp_def) + +lemma append_rsp2_pre0: + assumes a:"list_rel op \ x x'" + shows "list_rel op \ (x @ z) (x' @ z)" + using a apply (induct x x' rule: list_induct2') + apply simp_all + apply (rule list_rel_refl) + done + +lemma append_rsp2_pre1: + assumes a:"list_rel op \ x x'" + shows "list_rel op \ (z @ x) (z @ x')" + using a apply (induct x x' arbitrary: z rule: list_induct2') + apply (rule list_rel_refl) + apply (simp_all del: list_eq.simps) + apply (rule list_rel_app_l) + apply (simp_all add: reflp_def) + done + +lemma append_rsp2_pre: + assumes a:"list_rel op \ x x'" + and b: "list_rel op \ z z'" + shows "list_rel op \ (x @ z) (x' @ z')" + apply (rule list_rel_transp[OF fset_equivp]) + apply (rule append_rsp2_pre0) + apply (rule a) + using b apply (induct z z' rule: list_induct2') + apply (simp_all only: append_Nil2) + apply (rule list_rel_refl) + apply simp_all + apply (rule append_rsp2_pre1) + apply simp + done + +lemma [quot_respect]: + "(list_rel op \ OOO op \ ===> list_rel op \ OOO op \ ===> list_rel op \ OOO op \) op @ op @" +proof (intro fun_relI, elim pred_compE) + fix x y z w x' z' y' w' :: "'a list list" + assume a:"list_rel op \ x x'" + and b: "x' \ y'" + and c: "list_rel op \ y' y" + assume aa: "list_rel op \ z z'" + and bb: "z' \ w'" + and cc: "list_rel op \ w' w" + have a': "list_rel op \ (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto + have b': "x' @ z' \ y' @ w'" using b bb by simp + have c': "list_rel op \ (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto + have d': "(op \ OO list_rel op \) (x' @ z') (y @ w)" + by (rule pred_compI) (rule b', rule c') + show "(list_rel op \ OOO op \) (x @ z) (y @ w)" + by (rule pred_compI) (rule a', rule d') +qed + +text {* Raw theorems. Finsert, memb, singleron, sub_list *} lemma nil_not_cons: shows "\ ([] \ x # xs)" @@ -398,30 +629,20 @@ shows "memb x xs \ memb x (y # xs)" by (simp add: memb_def) -section {* Singletons *} - lemma singleton_list_eq: shows "[x] \ [y] \ x = y" by (simp add: id_simps) auto -section {* sub_list *} - lemma sub_list_cons: "sub_list (x # xs) ys = (memb x ys \ sub_list xs ys)" by (auto simp add: memb_def sub_list_def) -section {* Cardinality of finite sets *} - -quotient_definition - "fcard :: 'a fset \ nat" -is - "fcard_raw" +text {* Cardinality of finite sets *} lemma fcard_raw_0: shows "fcard_raw xs = 0 \ xs \ []" by (induct xs) (auto simp add: memb_def) - lemma fcard_raw_not_memb: shows "\ memb x xs \ fcard_raw (x # xs) = Suc (fcard_raw xs)" by auto @@ -432,7 +653,7 @@ using a by (induct xs) (auto simp add: memb_def split: if_splits) -lemma singleton_fcard_1: +lemma singleton_fcard_1: shows "set xs = {x} \ fcard_raw xs = 1" by (induct xs) (auto simp add: memb_def subset_insert) @@ -466,12 +687,7 @@ then show ?thesis using fcard_raw_0[of A] by simp qed -section {* fmap *} - -quotient_definition - "fmap :: ('a \ 'b) \ 'a fset \ 'b fset" -is - "map" +text {* fmap *} lemma map_append: "map f (xs @ ys) \ (map f xs) @ (map f ys)" @@ -526,28 +742,10 @@ "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" by (simp add: fdelete_raw_filter fcard_raw_delete_one) - - - - lemma finter_raw_empty: "finter_raw l [] = []" by (induct l) (simp_all add: not_memb_nil) -section {* Constants on the Quotient Type *} - -quotient_definition - "fdelete :: 'a fset \ 'a \ 'a fset" - is "delete_raw" - -quotient_definition - "fset_to_set :: 'a fset \ 'a set" - is "set" - -quotient_definition - "ffold :: ('a \ 'b \ 'b) \ 'b \ 'a fset \ 'b" - is "ffold_raw" - lemma set_cong: shows "(set x = set y) = (x \ y)" by auto @@ -556,12 +754,6 @@ "inj f \ (map f l \ map f m) = (l \ m)" by (simp add: expand_set_eq[symmetric] inj_image_eq_iff) -quotient_definition - "fconcat :: ('a fset) fset \ 'a fset" -is - "concat" - - text {* alternate formulation with a different decomposition principle and a proof of equivalence *} @@ -641,7 +833,7 @@ show "l \ r \ list_eq2 l r" using list_eq2_equiv_aux by blast qed -section {* lifted part *} +text {* Lifted theorems *} lemma not_fin_fnil: "x |\| {||}" by (lifting not_memb_nil) @@ -913,6 +1105,19 @@ using assms by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) +text {* concat *} + +lemma fconcat_empty: + shows "fconcat {||} = {||}" + by (lifting concat.simps(1)) + +lemma fconcat_insert: + shows "fconcat (finsert x S) = x |\| fconcat S" + by (lifting concat.simps(2)) + +lemma "fconcat (xs |\| ys) = fconcat xs |\| fconcat ys" + by (lifting concat_append) + ML {* fun dest_fsetT (Type ("FSet.fset", [T])) = T | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);