Proper definition of CARD and some properties of it.
Translation should now support Pure assumptions and Trueprops anywhere,
but a problem needs to be fixed with the tactic.
theory Quotientsimports Mainbegindefinition "REFL E \<equiv> \<forall>x. E x x"definition "SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"definition "TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"definition "NONEMPTY E \<equiv> \<exists>x. E x x"definition "EQUIV E \<equiv> REFL E \<and> SYM E \<and> TRANS E" definition "EQUIV_PROP E \<equiv> (\<forall>x y. E x y = (E x = E y))"lemma EQUIV_PROP_EQUALITY: shows "EQUIV_PROP (op =)"unfolding EQUIV_PROP_def expand_fun_eqby (blast)lemma EQUIV_implies_EQUIV_PROP: assumes a: "REFL E" and b: "SYM E" and c: "TRANS E" shows "EQUIV_PROP E"using a b cunfolding EQUIV_PROP_def REFL_def SYM_def TRANS_def expand_fun_eqby (metis)lemma EQUIV_PROP_implies_REFL: assumes a: "EQUIV_PROP E" shows "REFL E"using aunfolding EQUIV_PROP_def REFL_def expand_fun_eqby (metis)lemma EQUIV_PROP_implies_SYM: assumes a: "EQUIV_PROP E" shows "SYM E"using aunfolding EQUIV_PROP_def SYM_def expand_fun_eqby (metis)lemma EQUIV_PROP_implies_TRANS: assumes a: "EQUIV_PROP E" shows "TRANS E"using aunfolding EQUIV_PROP_def TRANS_def expand_fun_eqby (blast)ML {* fun equiv_refl thm = thm RS @{thm EQUIV_PROP_implies_REFL} fun equiv_sym thm = thm RS @{thm EQUIV_PROP_implies_SYM} fun equiv_trans thm = thm RS @{thm EQUIV_PROP_implies_TRANS} fun refl_sym_trans_equiv thm1 thm2 thm3 = [thm1,thm2,thm3] MRS @{thm EQUIV_implies_EQUIV_PROP} *}fun LIST_RELwhere "LIST_REL R [] [] = True"| "LIST_REL R (x#xs) [] = False"| "LIST_REL R [] (x#xs) = False"| "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"fun OPTION_REL where "OPTION_REL R None None = True"| "OPTION_REL R (Some x) None = False"| "OPTION_REL R None (Some x) = False"| "OPTION_REL R (Some x) (Some y) = R x y"fun option_mapwhere "option_map f None = None"| "option_map f (Some x) = Some (f x)"fun PROD_RELwhere "PROD_REL R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"fun prod_mapwhere "prod_map f1 f2 (a,b) = (f1 a, f2 b)"fun SUM_REL where "SUM_REL R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"| "SUM_REL R1 R2 (Inl a1) (Inr b2) = False"| "SUM_REL R1 R2 (Inr a2) (Inl b1) = False"| "SUM_REL R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"fun sum_mapwhere "sum_map f1 f2 (Inl a) = Inl (f1 a)"| "sum_map f1 f2 (Inr a) = Inr (f2 a)"fun FUN_REL where "FUN_REL R1 R2 f g = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"fun fun_mapwhere "fun_map f g h x = g (h (f x))" definition "QUOTIENT_ABS_REP Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a)"definition "QUOTIENT R Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and> (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))"lemma QUOTIENT_ID: shows "QUOTIENT (op =) id id"unfolding QUOTIENT_def id_defby (blast)lemma QUOTIENT_PROD: assumes a: "QUOTIENT E1 Abs1 Rep1" and b: "QUOTIENT E2 Abs2 Rep2" shows "QUOTIENT (PROD_REL E1 E2) (prod_map Abs1 Abs2) (prod_map Rep1 Rep2)"using a b unfolding QUOTIENT_defoopslemma QUOTIENT_ABS_REP_LIST: assumes a: "QUOTIENT_ABS_REP Abs Rep" shows "QUOTIENT_ABS_REP (map Abs) (map Rep)"using aunfolding QUOTIENT_ABS_REP_defapply(rule_tac allI)apply(induct_tac a rule: list.induct)apply(auto)donedefinition eqclass ("[_]_")where "[x]E \<equiv> E x"definition QUOTIENT_SET :: "'a set \<Rightarrow> ('a \<Rightarrow>'a\<Rightarrow>bool) \<Rightarrow> ('a set) set" ("_'/#'/_")where "S/#/E = {[x]E | x. x\<in>S}"definition QUOTIENT_UNIVwhere "QUOTIENT_UNIV TYPE('a) E \<equiv> (UNIV::'a set)/#/E"consts MY::"'a\<Rightarrow>'a\<Rightarrow>bool"axioms my1: "REFL MY"axioms my2: "SYM MY"axioms my3: "TRANS MY"term "QUOTIENT_UNIV TYPE('a) MY"term "\<lambda>f. \<exists>x. f = [x]MY"typedef 'a quot = "\<lambda>f::'a\<Rightarrow>bool. \<exists>x. f = [x]MY"by (auto simp add: mem_def)thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quotthm Abs_quot_cases Rep_quot_cases Abs_quot_induct Rep_quot_inductlemma lem2: shows "([x]MY = [y]MY) = MY x y"apply(rule iffI)apply(simp add: eqclass_def)using my1apply(auto simp add: REFL_def)[1]apply(simp add: eqclass_def expand_fun_eq)apply(rule allI)apply(rule iffI)apply(subgoal_tac "MY y x")using my3apply(simp add: TRANS_def)[1]apply(drule_tac x="y" in spec)apply(drule_tac x="x" in spec)apply(drule_tac x="xa" in spec)apply(simp)using my2apply(simp add: SYM_def)[1]oopslemma lem6: "\<forall>a. \<exists>r. Rep_quot a = [r]MY"apply(rule allI)apply(subgoal_tac "Rep_quot a \<in> quot")apply(simp add: quot_def mem_def)apply(rule Rep_quot)donelemma lem7: "\<forall>x y. (Abs_quot ([x]MY) = Abs_quot ([y]MY)) = ([x]MY = [y]MY)"apply(subst Abs_quot_inject)apply(unfold quot_def mem_def)apply(auto)donedefinition "Abs x = Abs_quot ([x]MY)"definition "Rep a = Eps (Rep_quot a)"lemma lem9: "\<forall>r. [(Eps [r]MY)]MY = [r]MY"apply(rule allI)apply(subgoal_tac "MY r r \<Longrightarrow> MY r (Eps (MY r))")apply(drule meta_mp)apply(rule eq1[THEN spec])apply(rule_tac x="MY r" in someI)lemma "(f \<in> UNIV/#/MY) = (Rep_quot (Abs_quot f) = f)"apply(simp add: QUOTIENT_SET_def)apply(auto)apply(subgoal_tac "[x]MY \<in> quot")apply(simp add: Abs_quot_inverse)apply(simp add: quot_def)apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)apply(auto)[1]apply(subgoal_tac "[x]MY \<in> quot")apply(simp add: Abs_quot_inverse)apply(simp add: quot_def)apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)apply(auto)[1]apply(subst expand_set_eq)thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quotlemma "\<forall>a. \<exists>r. Rep_quot a = [r]MY"apply(rule allI)apply(subst Abs_quot_inject[symmetric])apply(rule Rep_quot)apply(simp add: quot_def)apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)apply(auto)[1]apply(simp add: Rep_quot_inverse)thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quotapply(subst Abs_quot_inject[symmetric])proof - have "[r]MY \<in> quot" apply(simp add: quot_def) apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def) apply(auto)thm Abs_quot_inversethm Abs_quot_inverseapply(simp add: Rep_quot_inverse)thm Rep_quot_inverseterm ""lemma assumes a: "EQUIV2 E" shows "([x]E = [y]E) = E x y"using aby (simp add: eqclass_def EQUIV2_def)lemma shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)"apply(unfold QUOTIENT_def)apply(blast)donedefinition fun_app ("_ ---> _")where "f ---> g \<equiv> \<lambda>h x. g (h (f x))"lemma helper: assumes q: "QUOTIENT R ab re" and a: "R z z" shows "R (re (ab z)) z"using q aapply(unfold QUOTIENT_def)[1]apply(blast)donelemma assumes q1: "QUOTIENT R1 abs1 rep1" and q2: "QUOTIENT R2 abs2 rep2" shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"proof - have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" apply(simp add: expand_fun_eq) apply(simp add: fun_app_def) using q1 q2 apply(simp add: QUOTIENT_def) done moreover have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" apply(simp add: FUN_REL_def) apply(auto) apply(simp add: fun_app_def) using q1 q2 apply(unfold QUOTIENT_def) apply(metis) done moreover have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> (rep1 ---> abs2) r = (rep1 ---> abs2) s)" apply(simp add: expand_fun_eq) apply(rule allI)+ apply(rule iffI) using q1 q2 apply(unfold QUOTIENT_def)[1] apply(unfold fun_app_def)[1] apply(unfold FUN_REL_def)[1] apply(rule conjI) apply(metis) apply(rule conjI) apply(metis) apply(metis) apply(erule conjE) apply(simp (no_asm) add: FUN_REL_def) apply(rule allI impI)+ apply(subgoal_tac "R1 x x \<and> R1 y y \<and> abs1 x = abs1 y")(*A*) using q2 apply(unfold QUOTIENT_def)[1] apply(unfold fun_app_def)[1] apply(unfold FUN_REL_def)[1] apply(subgoal_tac "R2 (r x) (r x)")(*B*) apply(subgoal_tac "R2 (s y) (s y)")(*C*) apply(subgoal_tac "abs2 (r x) = abs2 (s y)")(*D*) apply(blast) (*D*) apply(metis helper q1) (*C*) apply(blast) (*B*) apply(blast) (*A*) using q1 apply(unfold QUOTIENT_def)[1] apply(unfold fun_app_def)[1] apply(unfold FUN_REL_def)[1] apply(metis) done ultimately show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" apply(unfold QUOTIENT_def)[1] apply(blast) doneqeddefinition "USER R \<equiv> NONEMPTY R \<and> typedecl tauconsts R::"tau \<Rightarrow> tau \<Rightarrow> bool"definition FACTOR :: "'a set \<Rightarrow> ('a \<times>'a \<Rightarrow> bool) \<Rightarrow> ('a set) set" ("_ '/'/'/ _")where "A /// r \<equiv> \<Union>x\<in>A. {r``{x}}"typedef qtau = "\<lambda>c::tau\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"apply(rule exI)apply(rule_tac x="R x" in exI)apply(auto)definition "QUOT TYPE('a) R \<equiv> \<lambda>c::'a\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"