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;

   new_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

  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) = (e \<in> B))) \<equiv> A = B"

apply (rule eq_reflection)

apply auto

done

lemma map_rep_ok: "b \<approx>1 ba \<Longrightarrow> map rep_fset b \<approx>1 map rep_fset ba"

unfolding erel1_def

apply(simp only: set_map set_in_eq)

done

lemma map_abs_ok: "b \<approx>1 ba \<Longrightarrow> map abs_fset b \<approx>1 map abs_fset ba"

unfolding erel1_def

apply(simp only: set_map set_in_eq)

done

lemma quotient_compose_list_pre:

 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =

       ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>

        (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) 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>1 map abs_fset s")

apply (metis Quotient_rel[OF Quotient_fset])

apply (auto)[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 add: map_abs_ok)

apply rule

apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "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>1" "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>1 map abs_fset s")

prefer 2

apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)

apply (rule map_rep_ok)

apply (assumption)

done

lemma quotient_compose_list:

  shows  "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1))

               (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)

done

lemma quotient_compose_list_gen:

  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 (rule)

apply (rule)

apply (rule)

apply (rule list_rel_refl)

apply (rule)

apply (rule equivp_reflp[OF fset_equivp])

apply (rule list_rel_refl)

apply rule

apply rule

done

lemma quotient_compose_general:

  and         "Quotient r2 abs2 rep2"

  shows  "Quotient ((list_rel r2) OO r1 OO (list_rel r2))

sorry

thm quotient_compose_ok     [OF Quotient_fset]

thm quotient_compose_general[OF Quotient_fset]

thm quotient_compose_ok     [OF Quotient_fset Quotient_fset]

(* Doesn't work: *)

(* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *)

end