theory FSetimports "../QuotMain" "../QuotList" "../QuotProd" Listbegininductive list_eq (infix "\<approx>" 50)where "a#b#xs \<approx> b#a#xs"| "[] \<approx> []"| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"| "a#a#xs \<approx> a#xs"| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"lemma list_eq_refl: shows "xs \<approx> xs" by (induct xs) (auto intro: list_eq.intros)lemma equivp_list_eq: shows "equivp list_eq" unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def apply(auto intro: list_eq.intros list_eq_refl) donequotient_type 'a fset = "'a list" / "list_eq" by (rule equivp_list_eq)quotient_definition "EMPTY :: 'a fset"as "[]::'a list"quotient_definition "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"as "op #"quotient_definition "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"as "op @"fun card1 :: "'a list \<Rightarrow> nat"where card1_nil: "(card1 []) = 0"| card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"quotient_definition "CARD :: 'a fset \<Rightarrow> nat"as "card1"quotient_definition "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"as "concat"term concatterm fconcattext {* Maybe make_const_def should require a theorem that says that the particular lifted function respects the relation. With it such a definition would be impossible: make_const_def CARD @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd*}lemma card1_0: fixes a :: "'a list" shows "(card1 a = 0) = (a = [])" by (induct a) autolemma not_mem_card1: fixes x :: "'a" fixes xs :: "'a list" shows "(~(x mem xs)) = (card1 (x # xs) = Suc (card1 xs))" by autolemma mem_cons: fixes x :: "'a" fixes xs :: "'a list" assumes a : "x mem xs" shows "x # xs \<approx> xs" using a by (induct xs) (auto intro: list_eq.intros )lemma card1_suc: fixes xs :: "'a list" fixes n :: "nat" assumes c: "card1 xs = Suc n" shows "\<exists>a ys. ~(a mem ys) \<and> xs \<approx> (a # ys)" using capply(induct xs)apply (metis Suc_neq_Zero card1_0)apply (metis FSet.card1_cons list_eq.intros(6) list_eq_refl mem_cons)donedefinition rsp_foldwhere "rsp_fold f = ((!u v. (f u v = f v u)) \<and> (!u v w. ((f u (f v w) = f (f u v) w))))"primrec fold1where "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"| "fold1 f g z (a # A) = (if rsp_fold f then ( if (a mem A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) ) else z)"lemma fs1_strong_cases: fixes X :: "'a list" shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))" apply (induct X) apply (simp) apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons) donequotient_definition "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"as "op mem"quotient_definition "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"as "fold1"quotient_definition "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"as "map"lemma mem_rsp: fixes z assumes a: "x \<approx> y" shows "(z mem x) = (z mem y)" using a by induct autolemma ho_memb_rsp[quot_respect]: "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)" by (simp add: mem_rsp)lemma card1_rsp: fixes a b :: "'a list" assumes e: "a \<approx> b" shows "card1 a = card1 b" using e by induct (simp_all add: mem_rsp)lemma ho_card1_rsp[quot_respect]: "(op \<approx> ===> op =) card1 card1" by (simp add: card1_rsp)lemma cons_rsp: fixes z assumes a: "xs \<approx> ys" shows "(z # xs) \<approx> (z # ys)" using a by (rule list_eq.intros(5))lemma ho_cons_rsp[quot_respect]: "(op = ===> op \<approx> ===> op \<approx>) op # op #" by (simp add: cons_rsp)lemma append_rsp_aux1: assumes a : "l2 \<approx> r2 " shows "(h @ l2) \<approx> (h @ r2)"using aapply(induct h)apply(auto intro: list_eq.intros(5))donelemma append_rsp_aux2: assumes a : "l1 \<approx> r1" "l2 \<approx> r2 " shows "(l1 @ l2) \<approx> (r1 @ r2)"using aapply(induct arbitrary: l2 r2)apply(simp_all)apply(blast intro: list_eq.intros append_rsp_aux1)+donelemma append_rsp[quot_respect]: "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" by (auto simp add: append_rsp_aux2)lemma map_rsp: assumes a: "a \<approx> b" shows "map f a \<approx> map f b" using a apply (induct) apply(auto intro: list_eq.intros) donelemma ho_map_rsp[quot_respect]: "(op = ===> op \<approx> ===> op \<approx>) map map" by (simp add: map_rsp)lemma map_append: "(map f (a @ b)) \<approx> (map f a) @ (map f b)" by simp (rule list_eq_refl)lemma ho_fold_rsp[quot_respect]: "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1" apply (auto) apply (case_tac "rsp_fold x") prefer 2 apply (erule_tac list_eq.induct) apply (simp_all) apply (erule_tac list_eq.induct) apply (simp_all) apply (auto simp add: mem_rsp rsp_fold_def)donelemma list_equiv_rsp[quot_respect]: shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"by (auto intro: list_eq.intros)lemma "IN x EMPTY = False"apply(lifting member.simps(1))donelemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"apply (lifting member.simps(2))donelemma "INSERT a (INSERT a x) = INSERT a x"apply (lifting list_eq.intros(4))donelemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"apply (lifting list_eq.intros(5))donelemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"apply (lifting card1_suc)donelemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"apply (lifting not_mem_card1)donelemma "FOLD f g (z::'b) (INSERT a x) = (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"apply(lifting fold1.simps(2))donelemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"apply (lifting map_append)donelemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"apply (lifting append_assoc)donelemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"apply(lifting list.induct)donelemma list_induct_part: assumes a: "P (x :: 'a list) ([] :: 'c list)" assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" shows "P x l" apply (rule_tac P="P x" in list.induct) apply (rule a) apply (rule b) apply (assumption) donelemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"apply (lifting list_induct_part)donelemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"apply (lifting list_induct_part)donelemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l"apply (lifting list_induct_part)donequotient_type 'a fset2 = "'a list" / "list_eq" by (rule equivp_list_eq)quotient_definition "EMPTY2 :: 'a fset2"as "[]::'a list"quotient_definition "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"as "op #"lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"apply (lifting list_induct_part)donelemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l"apply (lifting list_induct_part)donequotient_definition "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"as "list_rec"quotient_definition "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"as "list_case"(* Probably not true without additional assumptions about the function *)lemma list_rec_rsp[quot_respect]: "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" apply (auto) apply (erule_tac list_eq.induct) apply (simp_all) sorrylemma list_case_rsp[quot_respect]: "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" apply (auto) sorrylemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"apply (lifting list.recs(2))donelemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"apply (lifting list.cases(2))donelemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))"sorrylemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))"apply (lifting ttt)donelemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"sorrylemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"apply(lifting ttt2)apply(regularize)apply(rule impI)apply(simp)apply(rule allI)apply(rule list_eq_refl)donelemma ttt3: "(\<lambda>x. ((op @) x (e # []))) = (op #) e"sorrylemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = INSERT e"apply(lifting ttt3)apply(regularize)apply(auto simp add: cons_rsp)donelemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"sorrylemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"apply(lifting hard)apply(regularize)apply(rule fun_rel_id_asm)apply(subst babs_simp)apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})apply(rule fun_rel_id_asm)apply(rule impI)apply(rule mp[OF eq_imp_rel[OF fset_equivp]])apply(drule fun_cong)apply(drule fun_cong)apply(assumption)donelemma test: "All (\<lambda>(x::'a list, y). x = y)"sorrylemma "All (\<lambda>(x::'a fset, y). x = y)"apply(lifting test)donelemma test2: "Ex (\<lambda>(x::'a list, y). x = y)"sorrylemma "Ex (\<lambda>(x::'a fset, y). x = y)"apply(lifting test2)donelemma test3: "All (\<lambda> (x :: 'a list, y, z). x = y \<and> y = z)"sorrylemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)"apply(lifting test3)doneend