# HG changeset patch # User Christian Urban # Date 1287026062 -3600 # Node ID 693562f03eeed1778fb69375dc18fde0f36b7095 # Parent e903c32ec24feabd8c45a3ed2b4af8cd986a8fae major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) diff -r e903c32ec24f -r 693562f03eee IsaMakefile --- a/IsaMakefile Wed Oct 13 22:55:58 2010 +0100 +++ b/IsaMakefile Thu Oct 14 04:14:22 2010 +0100 @@ -1,10 +1,10 @@ ## targets -default: test +default: tests images: -all: tests paper pearl pearl-jv qpaper +all: tests paper pearl pearl-jv qpaper slides ## global settings @@ -107,7 +107,7 @@ cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf -slides: slides4 +slides: slides1 slides2 slides3 slides4 diff -r e903c32ec24f -r 693562f03eee Nominal/Equivp.thy --- a/Nominal/Equivp.thy Wed Oct 13 22:55:58 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,185 +0,0 @@ -theory Equivp -imports "Abs" "Perm" "Tacs" "Rsp" -begin - -lemma not_in_union: "c \ a \ b \ (c \ a \ c \ b)" -by auto - -ML {* -fun supports_tac perm = - simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( - REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN' - asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] - swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh - supp_fset_to_set supp_fmap_atom})) -*} - -ML {* -fun mk_supp ty x = - Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x -*} - -ML {* -fun mk_supports_eq thy cnstr = -let - val (tys, ty) = (strip_type o fastype_of) cnstr - val names = Datatype_Prop.make_tnames tys - val frees = map Free (names ~~ tys) - val rhs = list_comb (cnstr, frees) - - fun mk_supp_arg (x, ty) = - if is_atom thy ty then mk_supp @{typ atom} (mk_atom_ty ty x) else - if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else - if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) - else mk_supp ty x - val lhss = map mk_supp_arg (frees ~~ tys) - val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) - val eq = HOLogic.mk_Trueprop (supports $ fold_union lhss $ rhs) -in - (names, eq) -end -*} - -ML {* -fun prove_supports ctxt perms cnst = -let - val (names, eq) = mk_supports_eq ctxt cnst -in - Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) -end -*} - -ML {* -fun mk_fs tys = -let - val names = Datatype_Prop.make_tnames tys - val frees = map Free (names ~~ tys) - val supps = map2 mk_supp tys frees - val fin_supps = map (fn x => @{term "finite :: atom set \ bool"} $ x) supps -in - (names, HOLogic.mk_Trueprop (mk_conjl fin_supps)) -end -*} - -ML {* -fun fs_tac induct supports = rtac induct THEN_ALL_NEW ( - rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set - supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp}) -*} - -ML {* -fun prove_fs ctxt induct supports tys = -let - val (names, eq) = mk_fs tys -in - Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1) -end -*} - -ML {* -fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x; - -fun mk_supp_neq arg (fv, alpha) = -let - val collect = Const ("Collect", @{typ "(atom \ bool) \ atom \ bool"}); - val ty = fastype_of arg; - val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty); - val finite = @{term "finite :: atom set \ bool"} - val rhs = collect $ Abs ("a", @{typ atom}, - HOLogic.mk_not (finite $ - (collect $ Abs ("b", @{typ atom}, - HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg))))) -in - HOLogic.mk_eq (fv $ arg, rhs) -end; - -fun supp_eq fv_alphas_lst = -let - val (fvs_alphas, ls) = split_list fv_alphas_lst; - val (fv_ts, _) = split_list fvs_alphas; - val tys = map (domain_type o fastype_of) fv_ts; - val names = Datatype_Prop.make_tnames tys; - val args = map Free (names ~~ tys); - fun supp_eq_arg ((fv, arg), l) = - mk_conjl - ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) :: - (map (mk_supp_neq arg) l)) - val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls)) -in - (names, HOLogic.mk_Trueprop eqs) -end -*} - -ML {* -fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos = -if length fv_ts_bn < length alpha_ts_bn then - (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) []) -else let - val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1); - fun filter_fn i (x, j) = if j = i then SOME x else NONE; - val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos; - val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos; -in - (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all -end -*} - -(* TODO: this is a hack, it assumes that only one type of Abs's is present - in the type and chooses this supp_abs. Additionally single atoms are - treated properly. *) -ML {* -fun choose_alpha_abs eqiff = -let - fun exists_subterms f ts = member (op =) (map (exists_subterm f) ts) true; - val terms = map prop_of eqiff; - fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms - val no = - if check @{const_name alpha_lst} then 2 else - if check @{const_name alpha_res} then 1 else - if check @{const_name alpha_gen} then 0 else - error "Failure choosing supp_abs" -in - nth @{thms supp_abs[symmetric]} no -end -*} -lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}" -by (rule supp_abs(1)) - -lemma supp_abs_sum: - "supp (Abs x (a :: 'a :: fs)) \ supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" - "supp (Abs_res x (a :: 'a :: fs)) \ supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))" - "supp (Abs_lst y (a :: 'a :: fs)) \ supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))" - apply (simp_all add: supp_abs supp_Pair) - apply blast+ - done - - -ML {* -fun supp_eq_tac ind fv perm eqiff ctxt = - rtac ind THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW - simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) -*} - - - - - -end diff -r e903c32ec24f -r 693562f03eee Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Wed Oct 13 22:55:58 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Thu Oct 14 04:14:22 2010 +0100 @@ -157,10 +157,7 @@ apply(simp add: finite_supp) apply(simp add: finite_supp) oops - (*apply(simp add: Abs_fresh_star)*) -sorry - -done + end diff -r e903c32ec24f -r 693562f03eee Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Wed Oct 13 22:55:58 2010 +0100 +++ b/Nominal/Ex/TypeSchemes.thy Thu Oct 14 04:14:22 2010 +0100 @@ -56,7 +56,7 @@ lemma strong_induct: assumes a1: "\name b. P b (Var name)" and a2: "\t1 t2 b. \\c. P c t1; \c. P c t2\ \ P b (Fun t1 t2)" - and a3: "\fset t b. \\c. P c t; fset_to_set (fmap atom fset) \* b\ \ P' b (All fset t)" + and a3: "\fset t b. \\c. P c t; fset (fmap atom fset) \* b\ \ P' b (All fset t)" shows "P (a :: 'a :: pt) t \ P' (d :: 'b :: {fs}) ts " proof - have " (\p a. P a (p \ t)) \ (\p d. P' d (p \ ts))" @@ -69,7 +69,7 @@ apply simp apply (rule allI) apply (rule allI) - apply(subgoal_tac "\pa. ((pa \ (fset_to_set (fmap atom (p \ fset)))) \* d \ supp (p \ All fset ty) \* pa)") + apply(subgoal_tac "\pa. ((pa \ (fset (fmap atom (p \ fset)))) \* d \ supp (p \ All fset ty) \* pa)") apply clarify apply(rule_tac t="p \ All fset ty" and s="pa \ (p \ All fset ty)" in subst) @@ -81,7 +81,7 @@ apply simp apply (simp add: eqvts eqvts_raw) apply (rule at_set_avoiding2) - apply (simp add: fin_fset_to_set) + apply (simp add: fin_fset) apply (simp add: finite_supp) apply (simp add: eqvts finite_supp) apply (rule_tac p=" -p" in permute_boolE) @@ -142,7 +142,7 @@ assumes s1: "subst \ (Var n) = lookup \ n" and s2: "subst \ (Fun l r) = Fun (subst \ l) (subst \ r)" -and s3: "fset_to_set (fmap atom xs) \* \ \ substs \ (All xs t) = All xs (subst \ t)" +and s3: "fset (fmap atom xs) \* \ \ substs \ (All xs t) = All xs (subst \ t)" begin lemma subst_ty: @@ -163,7 +163,7 @@ apply (simp_all add: fresh_star_prod_elim) apply (drule fresh_star_atom) apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp]) - apply (subgoal_tac "atom a \ fset_to_set (fmap atom fset)") + apply (subgoal_tac "atom a \ fset (fmap atom fset)") apply blast apply (metis supp_finite_atom_set finite_fset) done @@ -197,7 +197,7 @@ apply (fold fresh_def)[1] apply (rule mp[OF subst_lemma_pre]) apply (simp add: fresh_Pair) - apply (subgoal_tac "atom a \ (fset_to_set (fmap atom fset))") + apply (subgoal_tac "atom a \ (fset (fmap atom fset))") apply blast apply (metis supp_finite_atom_set finite_fset) done diff -r e903c32ec24f -r 693562f03eee Nominal/FSet.thy --- a/Nominal/FSet.thy Wed Oct 13 22:55:58 2010 +0100 +++ b/Nominal/FSet.thy Thu Oct 14 04:14:22 2010 +0100 @@ -14,7 +14,7 @@ fun list_eq :: "'a list \ 'a list \ bool" (infix "\" 50) where - "list_eq xs ys = (\x. x \ set xs \ x \ set ys)" + "list_eq xs ys = (set xs = set ys)" lemma list_eq_equivp: shows "equivp list_eq" @@ -38,34 +38,25 @@ definition sub_list :: "'a list \ 'a list \ bool" where - "sub_list xs ys \ (\x. x \ set xs \ x \ set ys)" + "sub_list xs ys \ set xs \ set ys" -fun +definition fcard_raw :: "'a list \ nat" where - fcard_raw_nil: "fcard_raw [] = 0" -| fcard_raw_cons: "fcard_raw (x # xs) = - (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))" + "fcard_raw xs = card (set xs)" primrec finter_raw :: "'a list \ 'a list \ 'a list" where - "finter_raw [] l = []" -| "finter_raw (h # t) l = - (if memb h l then h # (finter_raw t l) else finter_raw t l)" - -primrec - delete_raw :: "'a list \ 'a \ 'a list" -where - "delete_raw [] x = []" -| "delete_raw (a # xs) x = - (if (a = x) then delete_raw xs x else a # (delete_raw xs x))" + "finter_raw [] ys = []" +| "finter_raw (x # xs) ys = + (if x \ set ys then x # (finter_raw xs ys) else finter_raw xs ys)" primrec fminus_raw :: "'a list \ 'a list \ 'a list" where - "fminus_raw l [] = l" -| "fminus_raw l (h # t) = fminus_raw (delete_raw l h) t" + "fminus_raw ys [] = ys" +| "fminus_raw ys (x # xs) = fminus_raw (removeAll x ys) xs" definition rsp_fold @@ -78,7 +69,7 @@ "ffold_raw f z [] = z" | "ffold_raw f z (a # xs) = (if (rsp_fold f) then - if memb a xs then ffold_raw f z xs + if a \ set xs then ffold_raw f z xs else f a (ffold_raw f z xs) else z)" @@ -100,12 +91,14 @@ shows "Quotient (list_all2 op \) (map abs_fset) (map rep_fset)" by (fact list_quotient[OF Quotient_fset]) +(* lemma set_in_eq: "(\e. ((e \ xs) \ (e \ ys))) \ xs = ys" 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) + by (simp only: set_map) lemma quotient_compose_list[quot_thm]: shows "Quotient ((list_all2 op \) OOO (op \)) @@ -165,13 +158,14 @@ text {* Respectfullness *} lemma append_rsp[quot_respect]: - shows "(op \ ===> op \ ===> op \) op @ op @" - apply(simp del: list_eq.simps) - by auto + shows "(op \ ===> op \ ===> op \) append append" + by (simp) +(* lemma append_rsp_unfolded: "\x \ y; v \ w\ \ x @ v \ y @ w" by auto +*) lemma [quot_respect]: shows "(op \ ===> op \ ===> op =) sub_list sub_list" @@ -186,7 +180,7 @@ by simp lemma cons_rsp[quot_respect]: - shows "(op = ===> op \ ===> op \) op # op #" + shows "(op = ===> op \ ===> op \) Cons Cons" by simp lemma map_rsp[quot_respect]: @@ -209,84 +203,35 @@ shows "memb x (y # xs) = (x = y \ memb x xs)" by (induct xs) (auto simp add: memb_def) -lemma memb_finter_raw: - "memb x (finter_raw xs ys) \ memb x xs \ memb x ys" - by (induct xs) (auto simp add: not_memb_nil memb_cons_iff) - -lemma [quot_respect]: - "(op \ ===> op \ ===> op \) finter_raw finter_raw" - by (simp add: memb_def[symmetric] memb_finter_raw) - -lemma memb_delete_raw: - "memb x (delete_raw xs y) = (memb x xs \ x \ y)" - by (induct xs arbitrary: x y) (auto simp add: memb_def) - -lemma [quot_respect]: - "(op \ ===> op = ===> op \) delete_raw delete_raw" - by (simp add: memb_def[symmetric] memb_delete_raw) - -lemma fminus_raw_memb: "memb x (fminus_raw xs ys) = (memb x xs \ \ memb x ys)" - by (induct ys arbitrary: xs) - (simp_all add: not_memb_nil memb_delete_raw memb_cons_iff) +lemma set_finter_raw[simp]: + "set (finter_raw xs ys) = set xs \ set ys" + by (induct xs) (auto simp add: memb_def) lemma [quot_respect]: - "(op \ ===> op \ ===> op \) fminus_raw fminus_raw" - by (simp add: memb_def[symmetric] fminus_raw_memb) + shows "(op \ ===> op \ ===> op \) finter_raw finter_raw" + by (simp) -lemma fcard_raw_gt_0: - assumes a: "x \ set xs" - shows "0 < fcard_raw xs" - using a by (induct xs) (auto simp add: memb_def) - -lemma fcard_raw_delete_one: - shows "fcard_raw ([x \ xs. x \ y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" - by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def) +(* +lemma memb_removeAll: + "memb x (removeAll y xs) \ memb x xs \ x \ y" + by (induct xs arbitrary: x y) (auto simp add: memb_def) +*) -lemma fcard_raw_rsp_aux: - assumes a: "xs \ ys" - shows "fcard_raw xs = fcard_raw ys" - using a - proof (induct xs arbitrary: ys) - case Nil - show ?case using Nil.prems by simp - next - case (Cons a xs) - have a: "a # xs \ ys" by fact - have b: "\ys. xs \ ys \ fcard_raw xs = fcard_raw ys" by fact - show ?case proof (cases "a \ set xs") - assume c: "a \ set xs" - have "\x. (x \ set xs) = (x \ set ys)" - proof (intro allI iffI) - fix x - assume "x \ set xs" - then show "x \ set ys" using a by auto - next - fix x - assume d: "x \ set ys" - have e: "(x \ set (a # xs)) = (x \ set ys)" using a by simp - show "x \ set xs" using c d e unfolding list_eq.simps by simp blast - qed - then show ?thesis using b c by (simp add: memb_def) - next - assume c: "a \ set xs" - have d: "xs \ [x\ys . x \ a] \ fcard_raw xs = fcard_raw [x\ys . x \ a]" using b by simp - have "Suc (fcard_raw xs) = fcard_raw ys" - proof (cases "a \ set ys") - assume e: "a \ set ys" - have f: "\x. (x \ set xs) = (x \ set ys \ x \ a)" using a c - by (auto simp add: fcard_raw_delete_one) - have "fcard_raw ys = Suc (fcard_raw ys - 1)" by (rule Suc_pred'[OF fcard_raw_gt_0]) (rule e) - then show ?thesis using d e f by (simp_all add: fcard_raw_delete_one memb_def) - next - case False then show ?thesis using a c d by auto - qed - then show ?thesis using a c d by (simp add: memb_def) - qed -qed +lemma [quot_respect]: + shows "(op = ===> op \ ===> op \) removeAll removeAll" + by (simp) + +lemma set_fminus_raw[simp]: + "set (fminus_raw xs ys) = (set xs - set ys)" + by (induct ys arbitrary: xs) (auto) + +lemma [quot_respect]: + shows "(op \ ===> op \ ===> op \) fminus_raw fminus_raw" + by simp lemma fcard_raw_rsp[quot_respect]: shows "(op \ ===> op =) fcard_raw fcard_raw" - by (simp add: fcard_raw_rsp_aux) + by (simp add: fcard_raw_def) lemma memb_absorb: shows "memb x xs \ x # xs \ xs" @@ -296,53 +241,39 @@ "(\x. \ memb x xs) = (xs \ [])" by (simp add: memb_def) -lemma not_memb_delete_raw_ident: - shows "\ memb x xs \ delete_raw xs x = xs" +lemma not_memb_removeAll_ident: + shows "\ memb x xs \ removeAll x xs = xs" by (induct xs) (auto simp add: memb_def) lemma memb_commute_ffold_raw: - "rsp_fold f \ memb h b \ ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))" + "rsp_fold f \ h \ set b \ ffold_raw f z b = f h (ffold_raw f z (removeAll h b))" apply (induct b) - apply (simp_all add: not_memb_nil) - apply (auto) - apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff) + apply (auto simp add: rsp_fold_def) done lemma ffold_raw_rsp_pre: - "\e. memb e a = memb e b \ ffold_raw f z a = ffold_raw f z b" + "set a = set b \ ffold_raw f z a = ffold_raw f z b" apply (induct a arbitrary: b) - apply (simp add: memb_absorb memb_def none_memb_nil) apply (simp) + apply (simp (no_asm_use)) apply (rule conjI) apply (rule_tac [!] impI) apply (rule_tac [!] conjI) apply (rule_tac [!] impI) - apply (subgoal_tac "\e. memb e a2 = memb e b") - apply (simp) - apply (simp add: memb_cons_iff memb_def) - apply (auto)[1] - apply (drule_tac x="e" in spec) - apply (blast) - apply (case_tac b) - apply (simp_all) - apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") - apply (simp only:) - apply (rule_tac f="f a1" in arg_cong) - apply (subgoal_tac "\e. memb e a2 = memb e (delete_raw b a1)") - apply (simp) - apply (simp add: memb_delete_raw) - apply (auto simp add: memb_cons_iff)[1] - apply (erule memb_commute_ffold_raw) - apply (drule_tac x="a1" in spec) - apply (simp add: memb_cons_iff) - apply (simp add: memb_cons_iff) - apply (case_tac b) - apply (simp_all) - done + apply (metis insert_absorb) + apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_raw.simps(2)) + apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_raw set_removeAll) + apply(drule_tac x="removeAll a1 b" in meta_spec) + apply(auto) + apply(drule meta_mp) + apply(blast) + by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def) lemma [quot_respect]: - "(op = ===> op = ===> op \ ===> op =) ffold_raw ffold_raw" - by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) + shows "(op = ===> op = ===> op \ ===> op =) ffold_raw ffold_raw" + unfolding fun_rel_def + apply(auto intro: ffold_raw_rsp_pre) + done lemma concat_rsp_pre: assumes a: "list_all2 op \ x x'" @@ -366,9 +297,11 @@ assume a: "list_all2 op \ a ba" assume b: "ba \ bb" assume c: "list_all2 op \ bb b" - have "\x. (\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof + 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 + 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 @@ -379,11 +312,10 @@ 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 + then show "concat a \ concat b" by auto qed - lemma concat_rsp_unfolded: "\list_all2 op \ a ba; ba \ bb; list_all2 op \ bb b\ \ concat a \ concat b" proof - @@ -404,11 +336,11 @@ 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 + then show "concat a \ concat b" by auto qed lemma [quot_respect]: - "((op =) ===> op \ ===> op \) filter filter" + shows "((op =) ===> op \ ===> op \) filter filter" by auto text {* Distributive lattice with bot *} @@ -439,11 +371,11 @@ lemma sub_list_inter_left: shows "sub_list (finter_raw x y) x" - by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw) + by (simp add: sub_list_def) lemma sub_list_inter_right: shows "sub_list (finter_raw x y) y" - by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw) + by (simp add: sub_list_def) lemma sub_list_list_eq: "sub_list x y \ sub_list y x \ list_eq x y" @@ -455,14 +387,12 @@ lemma sub_list_inter: "sub_list x y \ sub_list x z \ sub_list x (finter_raw y z)" - by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw) + by (simp add: sub_list_def) lemma append_inter_distrib: "x @ (finter_raw y z) \ finter_raw (x @ y) (x @ z)" apply (induct x) - apply (simp_all add: memb_def) - apply (simp add: memb_def[symmetric] memb_finter_raw) - apply (auto simp add: memb_def) + apply (auto) done instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}" @@ -487,44 +417,45 @@ "xs |\| ys \ xs \ ys" definition - less_fset: - "(xs :: 'a fset) < ys \ xs \ ys \ xs \ ys" + less_fset :: "'a fset \ 'a fset \ bool" +where + "xs < ys \ xs \ ys \ xs \ (ys::'a fset)" abbreviation - f_subset :: "'a fset \ 'a fset \ bool" (infix "|\|" 50) + fsubset :: "'a fset \ 'a fset \ bool" (infix "|\|" 50) where "xs |\| ys \ xs < ys" quotient_definition - "sup \ ('a fset \ 'a fset \ 'a fset)" + "sup :: 'a fset \ 'a fset \ 'a fset" is - "(op @) \ ('a list \ 'a list \ 'a list)" + "append :: 'a list \ 'a list \ 'a list" abbreviation funion (infixl "|\|" 65) where - "xs |\| ys \ sup (xs :: 'a fset) ys" + "xs |\| ys \ sup xs (ys::'a fset)" quotient_definition - "inf \ ('a fset \ 'a fset \ 'a fset)" + "inf :: 'a fset \ 'a fset \ 'a fset" is - "finter_raw \ ('a list \ 'a list \ 'a list)" + "finter_raw :: 'a list \ 'a list \ 'a list" abbreviation finter (infixl "|\|" 65) where - "xs |\| ys \ inf (xs :: 'a fset) ys" + "xs |\| ys \ inf xs (ys::'a fset)" quotient_definition - "minus \ ('a fset \ 'a fset \ 'a fset)" + "minus :: 'a fset \ 'a fset \ 'a fset" is - "fminus_raw \ ('a list \ 'a list \ 'a list)" + "fminus_raw :: 'a list \ 'a list \ 'a list" instance proof fix x y z :: "'a fset" show "(x |\| y) = (x |\| y \ \ y |\| x)" - unfolding less_fset by (lifting sub_list_not_eq) + unfolding less_fset_def by (lifting sub_list_not_eq) show "x |\| x" by (lifting sub_list_refl) show "{||} |\| x" by (lifting sub_list_empty) show "x |\| x |\| y" by (lifting sub_list_append_left) @@ -560,7 +491,7 @@ quotient_definition "finsert :: 'a \ 'a fset \ 'a fset" -is "op #" +is "Cons" syntax "@Finset" :: "args => 'a fset" ("{|(_)|}") @@ -583,20 +514,18 @@ quotient_definition "fcard :: 'a fset \ nat" -is - "fcard_raw" + is fcard_raw quotient_definition "fmap :: ('a \ 'b) \ 'a fset \ 'b fset" -is - "map" + is map quotient_definition - "fdelete :: 'a fset \ 'a \ 'a fset" - is "delete_raw" + "fdelete :: 'a \ 'a fset \ 'a fset" + is removeAll quotient_definition - "fset_to_set :: 'a fset \ 'a set" + "fset :: 'a fset \ 'a set" is "set" quotient_definition @@ -622,9 +551,8 @@ by simp lemma [quot_respect]: - "(op \ ===> list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \) op # op #" + shows "(op \ ===> list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \) Cons Cons" 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) @@ -723,53 +651,25 @@ lemma singleton_list_eq: shows "[x] \ [y] \ x = y" - by (simp add:) auto + by (simp) 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) -lemma fminus_raw_red: "fminus_raw (x # xs) ys = (if memb x ys then fminus_raw xs ys else x # (fminus_raw xs ys))" - by (induct ys arbitrary: xs x) - (simp_all add: not_memb_nil memb_delete_raw memb_cons_iff) +lemma fminus_raw_red: + "fminus_raw (x # xs) ys = (if x \ set ys then fminus_raw xs ys else x # (fminus_raw xs ys))" + by (induct ys arbitrary: xs x) (simp_all) text {* Cardinality of finite sets *} +(* used in memb_card_not_0 *) 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 - -lemma fcard_raw_suc: - assumes a: "fcard_raw xs = Suc n" - shows "\x ys. \ (memb x ys) \ xs \ (x # ys) \ fcard_raw ys = n" - using a - by (induct xs) (auto simp add: memb_def split_ifs) - -lemma singleton_fcard_1: - shows "set xs = {x} \ fcard_raw xs = 1" - by (induct xs) (auto simp add: memb_def subset_insert) + unfolding fcard_raw_def + by (induct xs) (auto) -lemma fcard_raw_1: - shows "fcard_raw xs = 1 \ (\x. xs \ [x])" - apply (auto dest!: fcard_raw_suc) - apply (simp add: fcard_raw_0) - apply (rule_tac x="x" in exI) - apply simp - apply (subgoal_tac "set xs = {x}") - apply (drule singleton_fcard_1) - apply auto - done - -lemma fcard_raw_suc_memb: - assumes a: "fcard_raw A = Suc n" - shows "\a. memb a A" - using a - by (induct A) (auto simp add: memb_def) - +(* used in list_eq2_equiv *) lemma memb_card_not_0: assumes a: "memb a A" shows "\(fcard_raw A = 0)" @@ -779,7 +679,11 @@ then show ?thesis using fcard_raw_0[of A] by simp qed -text {* fmap *} + + +section {* fmap *} + +(* there is another fmap section below *) lemma map_append: "map f (xs @ ys) \ (map f xs) @ (map f ys)" @@ -830,32 +734,29 @@ then show thesis using a c by blast qed + section {* deletion *} -lemma memb_delete_raw_ident: - shows "\ memb x (delete_raw xs x)" +lemma memb_removeAll_ident: + shows "\ memb x (removeAll x xs)" by (induct xs) (auto simp add: memb_def) -lemma fset_raw_delete_raw_cases: - "xs = [] \ (\x. memb x xs \ xs \ x # delete_raw xs x)" +lemma fset_raw_removeAll_cases: + "xs = [] \ (\x. memb x xs \ xs \ x # removeAll x xs)" by (induct xs) (auto simp add: memb_def) -lemma fdelete_raw_filter: - "delete_raw xs y = [x \ xs. x \ y]" +lemma fremoveAll_filter: + "removeAll y xs = [x \ xs. x \ y]" by (induct xs) simp_all lemma fcard_raw_delete: - "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) + "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" + by (auto simp add: fcard_raw_def memb_def) lemma finter_raw_empty: "finter_raw l [] = []" by (induct l) (simp_all add: not_memb_nil) -lemma set_cong: - shows "(x \