theory AbsRepTest+
−
imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List+
−
begin+
−
+
−
ML {* open Quotient_Term *}+
−
+
−
ML {*+
−
fun test_funs flag ctxt (rty, qty) =+
−
  (absrep_fun_chk flag ctxt (rty, qty)+
−
   |> Syntax.string_of_term ctxt+
−
   |> writeln;+
−
   equiv_relation_chk ctxt (rty, qty) +
−
   |> Syntax.string_of_term ctxt+
−
   |> writeln)+
−
*}+
−
+
−
definition+
−
  erel1 (infixl "\<approx>1" 50)+
−
where+
−
  "erel1 \<equiv> \<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"+
−
+
−
quotient_type +
−
  'a fset = "'a list" / erel1+
−
  apply(rule equivpI)+
−
  unfolding erel1_def reflp_def symp_def transp_def+
−
  by auto+
−
+
−
definition+
−
  erel2 (infixl "\<approx>2" 50)+
−
where+
−
  "erel2 \<equiv> \<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"+
−
+
−
quotient_type +
−
  'a foo = "('a * 'a) list" / erel2+
−
  apply(rule equivpI)+
−
  unfolding erel2_def reflp_def symp_def transp_def+
−
  by auto+
−
+
−
definition+
−
  erel3 (infixl "\<approx>3" 50)+
−
where+
−
  "erel3 \<equiv> \<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"+
−
+
−
quotient_type +
−
  'a bar = "('a * int) list" / "erel3"+
−
  apply(rule equivpI)+
−
  unfolding erel3_def reflp_def symp_def transp_def+
−
  by auto+
−
+
−
fun+
−
  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50)+
−
where+
−
  "intrel (x, y) (u, v) = (x + v = u + y)"+
−
+
−
quotient_type myint = "nat \<times> nat" / intrel+
−
  by (auto simp add: equivp_def expand_fun_eq)+
−
+
−
ML {*+
−
test_funs absF @{context} +
−
     (@{typ "nat \<times> nat"}, +
−
      @{typ "myint"})+
−
*}+
−
+
−
ML {*+
−
test_funs absF @{context} +
−
     (@{typ "('a * 'a) list"}, +
−
      @{typ "'a foo"})+
−
*}+
−
+
−
ML {*+
−
test_funs repF @{context} +
−
     (@{typ "(('a * 'a) list * 'b)"}, +
−
      @{typ "('a foo * 'b)"})+
−
*}+
−
+
−
ML {*+
−
test_funs absF @{context} +
−
     (@{typ "(('a list) * int) list"}, +
−
      @{typ "('a fset) bar"})+
−
*}+
−
+
−
ML {*+
−
test_funs absF @{context} +
−
     (@{typ "('a list)"}, +
−
      @{typ "('a fset)"})+
−
*}+
−
+
−
ML {*+
−
test_funs absF @{context} +
−
     (@{typ "('a list) list"}, +
−
      @{typ "('a fset) fset"})+
−
*}+
−
+
−
+
−
ML {*+
−
test_funs absF @{context} +
−
     (@{typ "((nat * nat) list) list"}, +
−
      @{typ "((myint) fset) fset"})+
−
*}+
−
+
−
ML {*+
−
test_funs absF @{context} +
−
     (@{typ "(('a * 'a) list) list"}, +
−
      @{typ "(('a * 'a) fset) fset"})+
−
*}+
−
+
−
ML {*+
−
test_funs absF @{context} +
−
      (@{typ "(nat * nat) list"}, +
−
       @{typ "myint fset"})+
−
*}+
−
+
−
ML {*+
−
test_funs absF @{context} +
−
     (@{typ "('a list) list \<Rightarrow> 'a list"}, +
−
      @{typ "('a fset) fset \<Rightarrow> 'a fset"})+
−
*}+
−
+
−
lemma OO_sym_inv:+
−
  assumes sr: "symp r"+
−
  and     ss: "symp s"+
−
  shows "(r OO s) x y = (s OO r) y x"+
−
  using sr ss+
−
  unfolding symp_def+
−
  apply (metis pred_comp.intros pred_compE ss symp_def)+
−
  done+
−
+
−
lemma abs_o_rep:+
−
  assumes a: "Quotient r absf repf"+
−
  shows "absf o repf = id"+
−
  apply(rule ext)+
−
  apply(simp add: Quotient_abs_rep[OF a])+
−
  done+
−
+
−
lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"+
−
  apply (rule eq_reflection)+
−
  apply auto+
−
  done+
−
+
−
lemma map_rel_cong: "b \<approx>1 ba \<Longrightarrow> map f b \<approx>1 map f ba"+
−
  unfolding erel1_def+
−
  apply(simp only: set_map set_in_eq)+
−
  done+
−
+
−
lemma quotient_compose_list_gen_pre:+
−
  assumes a: "equivp r2"+
−
  and b: "Quotient r2 abs2 rep2"+
−
  shows  "(list_rel r2 OO op \<approx>1 OO list_rel r2) r s =+
−
          ((list_rel r2 OO op \<approx>1 OO list_rel r2) r r \<and>+
−
           (list_rel r2 OO op \<approx>1 OO list_rel r2) s s \<and>+
−
           abs_fset (map abs2 r) = abs_fset (map abs2 s))"+
−
  apply rule+
−
  apply rule+
−
  apply rule+
−
  apply (rule list_rel_refl)+
−
  apply (metis equivp_def a)+
−
  apply rule+
−
  apply (rule equivp_reflp[OF fset_equivp])+
−
  apply (rule list_rel_refl)+
−
  apply (metis equivp_def a)+
−
  apply(rule)+
−
  apply rule+
−
  apply (rule list_rel_refl)+
−
  apply (metis equivp_def a)+
−
  apply rule+
−
  apply (rule equivp_reflp[OF fset_equivp])+
−
  apply (rule list_rel_refl)+
−
  apply (metis equivp_def a)+
−
  apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")+
−
  apply (metis Quotient_rel[OF Quotient_fset])+
−
  apply (auto)[1]+
−
  apply (subgoal_tac "map abs2 r = map abs2 b")+
−
  prefer 2+
−
  apply (metis Quotient_rel[OF list_quotient[OF b]])+
−
  apply (subgoal_tac "map abs2 s = map abs2 ba")+
−
  prefer 2+
−
  apply (metis Quotient_rel[OF list_quotient[OF b]])+
−
  apply (simp add: map_rel_cong)+
−
  apply rule+
−
  apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"])+
−
  apply (rule list_quotient)+
−
  apply (rule b)+
−
  apply (rule list_rel_refl)+
−
  apply (metis equivp_def a)+
−
  apply rule+
−
  prefer 2+
−
  apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"])+
−
  apply (rule list_quotient)+
−
  apply (rule b)+
−
  apply (rule list_rel_refl)+
−
  apply (metis equivp_def a)+
−
  apply (erule conjE)++
−
  apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")+
−
  apply (rule map_rel_cong)+
−
  apply (assumption)+
−
  apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b)+
−
  done+
−
+
−
lemma quotient_compose_list_gen:+
−
  assumes a: "Quotient r2 abs2 rep2"+
−
  and     b: "equivp r2" (* reflp is not enough *)+
−
  shows  "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2))+
−
               (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"+
−
  unfolding Quotient_def comp_def+
−
  apply (rule)++
−
  apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset])+
−
  apply (rule)+
−
  apply (rule)+
−
  apply (rule)+
−
  apply (rule list_rel_refl)+
−
  apply (metis b equivp_def)+
−
  apply (rule)+
−
  apply (rule equivp_reflp[OF fset_equivp])+
−
  apply (rule list_rel_refl)+
−
  apply (metis b equivp_def)+
−
  apply rule+
−
  apply rule+
−
  apply(rule quotient_compose_list_gen_pre[OF b a])+
−
  done+
−
+
−
(* This is the general statement but the types of abs2 and rep2+
−
   are wrong as can be seen in following exanples *)+
−
lemma quotient_compose_general:+
−
  assumes a2: "Quotient r1 abs1 rep1"+
−
  and         "Quotient r2 abs2 rep2"+
−
  shows  "Quotient ((list_rel r2) OO r1 OO (list_rel r2))+
−
               (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)"+
−
sorry+
−
+
−
thm quotient_compose_list_gen[OF Quotient_fset fset_equivp]+
−
thm quotient_compose_general[OF Quotient_fset]+
−
(* Doesn't work: *)+
−
(* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *)+
−
+
−
end+
−