theory AbsRepTest
imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
begin


(*
ML_command "ProofContext.debug := false"
ML_command "ProofContext.verbose := false"
*)

ML {*
val ctxt0 = @{context}
val ty = Syntax.read_typ ctxt0 "bool"  
val ctxt1 = Variable.declare_typ ty ctxt0 
val trm = Syntax.parse_term ctxt1 "A \<and> B"
val trm' = Syntax.type_constraint ty trm
val trm'' = Syntax.check_term ctxt1 trm'
val ctxt2 = Variable.declare_term trm'' ctxt1 
*}

term "split"

term "Ex1 (\<lambda>(x, y). P x y)" 

lemma "(Ex1 (\<lambda>(x, y). P x y)) \<Longrightarrow> (\<exists>! x. \<exists>! y. P x y)"
apply(erule ex1E)
apply(case_tac x)
apply(clarify)
apply(rule_tac a="aa" in ex1I)
apply(rule ex1I)
apply(assumption)
apply(blast)
apply(blast)
done

(*
lemma "(\<exists>! x. \<exists>! y. P x y) \<Longrightarrow> (Ex1 (\<lambda>(x, y). P x y))"
apply(erule ex1E)
apply(erule ex1E)
apply(rule_tac a="(x, y)" in ex1I)
apply(clarify)
apply(case_tac xa)
apply(clarify)

apply(rule ex1I)
apply(assumption)
apply(blast)
apply(blast)
done

apply(metis)
*)

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 OOO op \<approx>1) r s =
          ((list_rel r2 OOO op \<approx>1) r r \<and> (list_rel r2 OOO op \<approx>1) 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) OOO (op \<approx>1))
               (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) OOO r1)
               (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