theory FSet3imports "../QuotMain" "../QuotList" ListbeginML {*structure QuotientRules = Named_Thms (val name = "quot_thm" val description = "Quotient theorems.")*}ML {*open QuotientRules*}fun list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)where "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"lemma list_eq_equivp: shows "equivp list_eq"unfolding equivp_reflp_symp_transp reflp_def symp_def transp_defby auto(* FIXME-TODO: because of beta-reduction, one cannot give the *)(* FIXME-TODO: relation as a term or abbreviation *) quotient_type 'a fset = "'a list" / "list_eq"by (rule list_eq_equivp)section {* empty fset, finsert and membership *} quotient_definition "fempty :: 'a fset" ("{||}")as "[]::'a list"quotient_definition "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op #"syntax "@Finset" :: "args => 'a fset" ("{|(_)|}")translations "{|x, xs|}" == "CONST finsert x {|xs|}" "{|x|}" == "CONST finsert x {||}"definition memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"where "memb x xs \<equiv> x \<in> set xs"quotient_definition "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50)as "memb"abbreviation fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)where "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)"lemma memb_rsp[quot_respect]: shows "(op = ===> op \<approx> ===> op =) memb memb"by (auto simp add: memb_def)lemma nil_rsp[quot_respect]: shows "[] \<approx> []"by simplemma cons_rsp[quot_respect]: shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"by simpsection {* Augmenting a set -- @{const finsert} *}text {* raw section *}lemma nil_not_cons: shows "\<not>[] \<approx> x # xs" by autolemma memb_cons_iff: shows "memb x (y # xs) = (x = y \<or> memb x xs)"by (induct xs) (auto simp add: memb_def)lemma memb_consI1: shows "memb x (x # xs)"by (simp add: memb_def)lemma memb_consI2: shows "memb x xs \<Longrightarrow> memb x (y # xs)" by (simp add: memb_def)lemma memb_absorb: shows "memb x xs \<Longrightarrow> (x # xs) \<approx> xs"by (induct xs) (auto simp add: memb_def)text {* lifted section *}lemma fempty_not_finsert[simp]: shows "{||} \<noteq> finsert x S"by (lifting nil_not_cons)lemma fin_finsert_iff[simp]: "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"by (lifting memb_cons_iff) lemma shows finsertI1: "x |\<in>| finsert x S" and finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S" by (lifting memb_consI1, lifting memb_consI2)lemma finsert_absorb [simp]: shows "x |\<in>| S \<Longrightarrow> finsert x S = S"by (lifting memb_absorb)section {* Singletons *}text {* raw section *}lemma singleton_list_eq: shows "[x] \<approx> [y] \<longleftrightarrow> x = y"by autotext {* lifted section *}lemma fsingleton_eq[simp]: shows "{|x|} = {|y|} \<longleftrightarrow> x = y"by (lifting singleton_list_eq)section {* Union *}quotient_definition "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)as "op @"section {* Cardinality of finite sets *}fun fcard_raw :: "'a list \<Rightarrow> 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))"quotient_definition "fcard :: 'a fset \<Rightarrow> nat" as "fcard_raw"text {* raw section *}lemma fcard_raw_ge_0: assumes a: "x \<in> set xs" shows "0 < fcard_raw xs"using aby (induct xs) (auto simp add: memb_def)lemma fcard_raw_delete_one: "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"by (induct xs) (auto dest: fcard_raw_ge_0 simp add: memb_def)lemma fcard_raw_rsp_aux: assumes a: "a \<approx> b" shows "fcard_raw a = fcard_raw b"using aapply(induct a arbitrary: b)apply(auto simp add: memb_def)apply(metis)apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)apply(simp add: fcard_raw_delete_one)apply(metis Suc_pred' fcard_raw_ge_0 fcard_raw_delete_one memb_def)donelemma fcard_raw_rsp[quot_respect]: "(op \<approx> ===> op =) fcard_raw fcard_raw" by (simp add: fcard_raw_rsp_aux)text {* lifted section *}lemma fcard_fempty [simp]: shows "fcard {||} = 0"by (lifting fcard_raw_nil)lemma fcard_finsert_if [simp]: shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"by (lifting fcard_raw_cons)section {* Induction and Cases rules for finite sets *}lemma fset_exhaust[case_names fempty finsert, cases type: fset]: shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"by (lifting list.exhaust)lemma fset_induct[case_names fempty finsert]: shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"by (lifting list.induct)lemma fset_induct2[case_names fempty finsert, induct type: fset]: assumes prem1: "P {||}" and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" shows "P S"proof(induct S rule: fset_induct) case fempty show "P {||}" by (rule prem1)next case (finsert x S) have asm: "P S" by fact show "P (finsert x S)" proof(cases "x |\<in>| S") case True have "x |\<in>| S" by fact then show "P (finsert x S)" using asm by simp next case False have "x |\<notin>| S" by fact then show "P (finsert x S)" using prem2 asm by simp qedqedsection {* fmap and fset comprehension *}quotient_definition "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"as "map"quotient_definition "fconcat :: ('a fset) fset => 'a fset"as "concat"(*lemma fconcat_rsp[quot_respect]: shows "((list_rel op \<approx>) ===> op \<approx>) concat concat"apply(auto)sorry*)(* PROBLEM: these lemmas needs to be restated, since *)(* concat.simps(1) and concat.simps(2) contain the *)(* type variables ?'a1.0 (which are turned into frees *)(* 'a_1 *)lemma concat1: shows "concat [] \<approx> []"by (simp)lemma concat2: shows "concat (x # xs) \<approx> x @ concat xs"by (simp)lemma concat_rsp[quot_respect]: shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat"sorrylemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []"apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)donelemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" apply (rule eq_reflection) apply auto donelemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" unfolding list_eq.simps apply(simp only: set_map set_in_eq) donelemma quotient_compose_list_pre: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r s = ((list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r r \<and> (list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" apply rule apply rule apply rule apply (rule list_rel_refl) apply (metis equivp_def fset_equivp) apply rule apply (rule equivp_reflp[OF fset_equivp]) apply (rule list_rel_refl) apply (metis equivp_def fset_equivp) apply(rule) apply rule apply (rule list_rel_refl) apply (metis equivp_def fset_equivp) apply rule apply (rule equivp_reflp[OF fset_equivp]) apply (rule list_rel_refl) apply (metis equivp_def fset_equivp) apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s") apply (metis Quotient_rel[OF Quotient_fset]) apply (auto simp only:)[1] apply (subgoal_tac "map abs_fset r = map abs_fset b") prefer 2 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) apply (subgoal_tac "map abs_fset s = map abs_fset ba") prefer 2 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) apply (simp only: map_rel_cong) apply rule apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"]) apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) apply (rule list_rel_refl) apply (metis equivp_def fset_equivp) apply rule prefer 2 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"]) apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) apply (rule list_rel_refl) apply (metis equivp_def fset_equivp) apply (erule conjE)+ apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s") prefer 2 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) apply (rule map_rel_cong) apply (assumption) donelemma quotient_compose_list[quot_thm]: shows "Quotient ((list_rel op \<approx>) OO (op \<approx>) OO (list_rel op \<approx>)) (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" unfolding Quotient_def comp_def apply (rule)+ apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) apply (rule) apply (rule) apply (rule) apply (rule list_rel_refl) apply (metis equivp_def fset_equivp) apply (rule) apply (rule equivp_reflp[OF fset_equivp]) apply (rule list_rel_refl) apply (metis equivp_def fset_equivp) apply rule apply rule apply(rule quotient_compose_list_pre) donelemma fconcat_empty: shows "fconcat {||} = {||}"apply(lifting concat1)apply(cleaning)apply(simp add: comp_def)apply(fold fempty_def[simplified id_simps])apply(rule refl)donelemma fconcat_insert: shows "fconcat (finsert x S) = x |\<union>| fconcat S"apply(lifting concat2)apply(injection)(* The Relation is wrong to apply rep_abs_rsp *)thm rep_abs_rsp[of "(op \<approx> ===> op =)"]deferapply (simp only: finsert_def[simplified id_simps])apply (simp only: fconcat_def[simplified id_simps])apply(cleaning)(* finsert_def doesn't get folded, since rep-abs types are incorrect *)apply(simp add: comp_def)apply (simp add: fconcat_def[simplified id_simps])apply cleaning(* The Relation is wrong again. *)sorrytext {* raw section *}lemma map_rsp_aux: assumes a: "a \<approx> b" shows "map f a \<approx> map f b" using aapply(induct a arbitrary: b)apply(auto)apply(metis rev_image_eqI)donelemma map_rsp[quot_respect]: shows "(op = ===> op \<approx> ===> op \<approx>) map map"by (auto simp add: map_rsp_aux)text {* lifted section *}(* TBD *)text {* syntax for fset comprehensions (adapted from lists) *}nonterminals fsc_qual fsc_qualssyntax"_fsetcompr" :: "'a \<Rightarrow> fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> 'a fset" ("{|_ . __")"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ <- _")"_fsc_test" :: "bool \<Rightarrow> fsc_qual" ("_")"_fsc_end" :: "fsc_quals" ("|}")"_fsc_quals" :: "fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> fsc_quals" (", __")"_fsc_abs" :: "'a => 'b fset => 'b fset"syntax (xsymbols)"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")syntax (HTML output)"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")parse_translation (advanced) {*let val femptyC = Syntax.const @{const_name fempty}; val finsertC = Syntax.const @{const_name finsert}; val fmapC = Syntax.const @{const_name fmap}; val fconcatC = Syntax.const @{const_name fconcat}; val IfC = Syntax.const @{const_name If}; fun fsingl x = finsertC $ x $ femptyC; fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *) let val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT); val e = if opti then fsingl e else e; val case1 = Syntax.const "_case1" $ p $ e; val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN $ femptyC; val cs = Syntax.const "_case2" $ case1 $ case2 val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs] in lambda x ft end; fun abs_tr ctxt (p as Free(s,T)) e opti = let val thy = ProofContext.theory_of ctxt; val s' = Sign.intern_const thy s in if Sign.declared_const thy s' then (pat_tr ctxt p e opti, false) else (lambda p e, true) end | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false); fun fsc_tr ctxt [e, Const("_fsc_test",_) $ b, qs] = let val res = case qs of Const("_fsc_end",_) => fsingl e | Const("_fsc_quals",_)$ q $ qs => fsc_tr ctxt [e, q, qs]; in IfC $ b $ res $ femptyC end | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_end",_)] = (case abs_tr ctxt p e true of (f,true) => fmapC $ f $ es | (f, false) => fconcatC $ (fmapC $ f $ es)) | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_quals",_) $ q $ qs] = let val e' = fsc_tr ctxt [e, q, qs]; in fconcatC $ (fmapC $ (fst (abs_tr ctxt p e' false)) $ es) endin [("_fsetcompr", fsc_tr)] end*}(* examles *)term "{|(x,y,z). b|}"term "{|x. x \<leftarrow> xs|}"term "{|(x,y,z). x\<leftarrow>xs|}"term "{|e x y. x\<leftarrow>xs, y\<leftarrow>ys|}"term "{|(x,y,z). x<a, x>b|}"term "{|(x,y,z). x\<leftarrow>xs, x>b|}"term "{|(x,y,z). x<a, x\<leftarrow>xs|}"term "{|(x,y). Cons True x \<leftarrow> xs|}"term "{|(x,y,z). Cons x [] \<leftarrow> xs|}"term "{|(x,y,z). x<a, x>b, x=d|}"term "{|(x,y,z). x<a, x>b, y\<leftarrow>ys|}"term "{|(x,y,z). x<a, x\<leftarrow>xs,y>b|}"term "{|(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys|}"term "{|(x,y,z). x\<leftarrow>xs, x>b, y<a|}"term "{|(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys|}"term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x|}"term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs|}"(* BELOW CONSTRUCTION SITE *)lemma no_mem_nil: "(\<forall>a. a \<notin> set A) = (A = [])"by (induct A) (auto)lemma none_mem_nil: "(\<forall>a. a \<notin> set A) = (A \<approx> [])"by simplemma mem_cons: "a \<in> set A \<Longrightarrow> a # A \<approx> A"by autolemma cons_left_comm: "x #y # A \<approx> y # x # A"by autolemma cons_left_idem: "x # x # A \<approx> x # A"by autolemma finite_set_raw_strong_cases: "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))" apply (induct X) apply (simp) apply (rule disjI2) apply (erule disjE) apply (rule_tac x="a" in exI) apply (rule_tac x="[]" in exI) apply (simp) apply (erule exE)+ apply (case_tac "a = aa") apply (rule_tac x="a" in exI) apply (rule_tac x="Y" in exI) apply (simp) apply (rule_tac x="aa" in exI) apply (rule_tac x="a # Y" in exI) apply (auto) donefun delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"where "delete_raw [] x = []"| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"lemma mem_delete_raw: "x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))" by (induct A arbitrary: x a) (auto)lemma mem_delete_raw_ident: "\<not>(a \<in> set (delete_raw A a))"by (induct A) (auto)lemma not_mem_delete_raw_ident: "b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"by (induct A) (auto)lemma delete_raw_RSP: "A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"apply(induct A arbitrary: B a)apply(auto)sorrylemma cons_delete_raw: "a # (delete_raw A a) \<approx> (if a \<in> set A then A else (a # A))"sorrylemma mem_cons_delete_raw: "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A"sorrylemma finite_set_raw_delete_raw_cases: "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)" by (induct X) (auto)lemma list2set_thm: shows "set [] = {}" and "set (h # t) = insert h (set t)" by (auto)lemma list2set_RSP: "A \<approx> B \<Longrightarrow> set A = set B" by autodefinition rsp_foldwhere "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"primrec fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"where "fold_raw f z [] = z"| "fold_raw f z (a # A) = (if (rsp_fold f) then if a mem A then fold_raw f z A else f a (fold_raw f z A) else z)"lemma mem_lcommuting_fold_raw: "rsp_fold f \<Longrightarrow> h mem B \<Longrightarrow> fold_raw f z B = f h (fold_raw f z (delete_raw B h))"sorrylemma fold_rsp[quot_respect]: "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"apply(auto)sorrylemma append_rsp[quot_respect]: "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"by autoprimrec inter_rawwhere "inter_raw [] B = []"| "inter_raw (a # A) B = (if a mem B then a # inter_raw A B else inter_raw A B)"lemma mem_inter_raw: "x mem (inter_raw A B) = x mem A \<and> x mem B"sorrylemma inter_raw_RSP: "A1 \<approx> A2 \<and> B1 \<approx> B2 \<Longrightarrow> (inter_raw A1 B1) \<approx> (inter_raw A2 B2)"sorry(* LIFTING DEFS *)section {* Constants on the Quotient Type *} quotient_definition "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" as "delete_raw"quotient_definition "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) as "inter_raw"quotient_definition "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" as "fold_raw"quotient_definition "fset_to_set :: 'a fset \<Rightarrow> 'a set" as "set"section {* Lifted Theorems *}thm list.cases (* ??? *)thm cons_left_commlemma "finsert a (finsert b S) = finsert b (finsert a S)"by (lifting cons_left_comm)thm cons_left_idemlemma "finsert a (finsert a S) = finsert a S"by (lifting cons_left_idem)(* thm MEM: MEM x [] = F MEM x (h::t) = (x=h) \/ MEM x t *)thm none_mem_nil(*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*)thm mem_consthm finite_set_raw_strong_cases(*thm card_raw.simps*)(*thm not_mem_card_raw*)(*thm card_raw_suc*)lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"(*by (lifting card_raw_suc)*)sorry(*thm card_raw_cons_gt_0thm mem_card_raw_gt_0thm not_nil_equiv_cons*)thm delete_raw.simps(*thm mem_delete_raw*)(*thm card_raw_delete_raw*)thm cons_delete_rawthm mem_cons_delete_rawthm finite_set_raw_delete_raw_casesthm append.simps(* MEM_APPEND: MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2 *)thm inter_raw.simpsthm mem_inter_rawthm fold_raw.simpsthm list2set_thmthm list_eq_defthm list.inductlemma "\<lbrakk>P fempty; \<And>a x. P x \<Longrightarrow> P (finsert a x)\<rbrakk> \<Longrightarrow> P l"by (lifting list.induct)(* We also have map and some properties of it in FSet *)(* and the following which still lifts ok *)lemma "funion (funion x xa) xb = funion x (funion xa xb)"by (lifting append_assoc)quotient_definition "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"as "list_case"(* NOT SURE IF TRUE *)lemma list_case_rsp[quot_respect]: "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" apply (auto) sorrylemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"apply (lifting list.cases(2))donethm quot_respectend