theory QuotMain
imports QuotScript QuotList Prove
begin

(*
prove {* @{prop "True"} *}
apply(rule TrueI)
done
*)

locale QUOT_TYPE =
  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
  assumes equiv: "EQUIV R"
  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
  and     rep_inverse: "\<And>x. Abs (Rep x) = x"
  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
begin 

definition
  "ABS x \<equiv> Abs (R x)"

definition
  "REP a = Eps (Rep a)"

lemma lem9: 
  shows "R (Eps (R x)) = R x"
proof -
  have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
  then have "R x (Eps (R x))" by (rule someI)
  then show "R (Eps (R x)) = R x" 
    using equiv unfolding EQUIV_def by simp
qed

theorem thm10:
  shows "ABS (REP a) = a"
unfolding ABS_def REP_def
proof -
  from rep_prop 
  obtain x where eq: "Rep a = R x" by auto
  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
  also have "\<dots> = Abs (R x)" using lem9 by simp
  also have "\<dots> = Abs (Rep a)" using eq by simp
  also have "\<dots> = a" using rep_inverse by simp
  finally
  show "Abs (R (Eps (Rep a))) = a" by simp
qed

lemma REP_refl: 
  shows "R (REP a) (REP a)"
unfolding REP_def
by (simp add: equiv[simplified EQUIV_def])

lemma lem7:
  "(R x = R y) = (Abs (R x) = Abs (R y))"
apply(rule iffI)
apply(simp)
apply(drule rep_inject[THEN iffD2])
apply(simp add: abs_inverse)
done
  
theorem thm11:
  shows "R r r' = (ABS r = ABS r')"
unfolding ABS_def
by (simp only: equiv[simplified EQUIV_def] lem7)


lemma REP_ABS_rsp:
  shows "R f (REP (ABS g)) = R f g"
  and   "R (REP (ABS g)) f = R g f"
apply(subst thm11)
apply(simp add: thm10 thm11)
apply(subst thm11)
apply(simp add: thm10 thm11)
done

lemma QUOTIENT:
  "QUOTIENT R ABS REP"
apply(unfold QUOTIENT_def)
apply(simp add: thm10)
apply(simp add: REP_refl)
apply(subst thm11[symmetric])
apply(simp add: equiv[simplified EQUIV_def])
done

end

section {* type definition for the quotient type *}

ML {*
Variable.variant_frees
*}


ML {*
(* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)
fun typedef_term rel ty lthy =
let 
  val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] 
               |> Variable.variant_frees lthy [rel]
               |> map Free
in
  lambda c 
    (HOLogic.mk_exists 
       ("x", ty, HOLogic.mk_eq (c, (rel $ x))))
end
*}

ML {*
 typedef_term @{term R} @{typ "nat"} @{context} 
  |> Syntax.string_of_term @{context}
  |> writeln
*}

ML {*
val typedef_tac =  
  EVERY1 [rewrite_goal_tac @{thms mem_def},
          rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
*}

ML {*
(* makes the new type definitions *)
fun typedef_make (qty_name, rel, ty) lthy =
  LocalTheory.theory_result
  (Typedef.add_typedef false NONE 
     (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
       (typedef_term rel ty lthy)
         NONE typedef_tac) lthy
*}

text {* proves the QUOT_TYPE theorem for the new type *}
ML {*
fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = 
let
  val rep_thm = #Rep typedef_info
  val rep_inv = #Rep_inverse typedef_info
  val abs_inv = #Abs_inverse typedef_info
  val rep_inj = #Rep_inject typedef_info

  val ss = HOL_basic_ss addsimps @{thms mem_def}
  val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm
  val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv
in
  EVERY1 [rtac @{thm QUOT_TYPE.intro},
          rtac equiv_thm, 
          rtac rep_thm_simpd, 
          rtac rep_inv, 
          rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
          rtac rep_inj]
end
*}

term QUOT_TYPE
ML {* HOLogic.mk_Trueprop *}
ML {* Goal.prove *}
ML {* Syntax.check_term *}

ML {* 
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
let
  val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
  val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
             |> Syntax.check_term lthy
in
  Goal.prove lthy [] [] goal
    (fn _ => typedef_quot_type_tac equiv_thm typedef_info)
end
*}

ML {*
fun typedef_quotient_thm_tac defs quot_type_thm =
  EVERY1 [K (rewrite_goals_tac defs), 
          rtac @{thm QUOT_TYPE.QUOTIENT}, 
          rtac quot_type_thm]
*}

ML {* 
fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
let
  val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)
  val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
             |> Syntax.check_term lthy
in
  Goal.prove lthy [] [] goal
    (fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)
end
*}

text {* two wrappers for define and note *}
ML {* 
fun make_def (name, mx, trm) lthy =
let   
  val ((trm, (_ , thm)), lthy') = 
     LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy
in
  ((trm, thm), lthy')
end
*}

ML {*
fun reg_thm (name, thm) lthy = 
let
  val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy 
in
  (thm',lthy')
end
*}

ML {* 
fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
let 
  (* generates typedef *)
  val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy

  (* abs and rep functions *)
  val abs_ty = #abs_type typedef_info
  val rep_ty = #rep_type typedef_info
  val abs_name = #Abs_name typedef_info
  val rep_name = #Rep_name typedef_info
  val abs = Const (abs_name, rep_ty --> abs_ty)
  val rep = Const (rep_name, abs_ty --> rep_ty)

  (* ABS and REP definitions *)
  val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
  val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
  val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs) 
  val REP_trm = Syntax.check_term lthy' (REP_const $ rep) 
  val ABS_name = Binding.prefix_name "ABS_" qty_name
  val REP_name = Binding.prefix_name "REP_" qty_name  
  val (((ABS, ABS_def), (REP, REP_def)), lthy'') = 
         lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
               ||>> make_def (REP_name, NoSyn, REP_trm)

  (* quot_type theorem *)
  val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
  val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name

  (* quotient theorem *)
  val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
  val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name

in
  lthy'' 
  |> reg_thm (quot_thm_name, quot_thm)  
  ||>> reg_thm (quotient_thm_name, quotient_thm)
end
*}

section {* various tests for quotient types*}
datatype trm =
  var  "nat" 
| app  "trm" "trm"
| lam  "nat" "trm"
  
consts R :: "trm \<Rightarrow> trm \<Rightarrow> bool"
axioms r_eq: "EQUIV R"

ML {*
  typedef_main 
*}

local_setup {*
  typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd
*}

term Rep_qtrm
term REP_qtrm
term Abs_qtrm
term ABS_qtrm
thm QUOT_TYPE_qtrm
thm QUOTIENT_qtrm

thm Rep_qtrm

text {* another test *}
datatype 'a my = foo
consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"
axioms rmy_eq: "EQUIV Rmy"

term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"

datatype 'a trm' =
  var'  "'a" 
| app'  "'a trm'" "'a trm'"
| lam'  "'a" "'a trm'"
  
consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
axioms r_eq': "EQUIV R'"

local_setup {*
  typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
*}

term ABS_qtrm'
term REP_qtrm'
thm QUOT_TYPE_qtrm'
thm QUOTIENT_qtrm'
thm Rep_qtrm'

text {* a test with lists of terms *}
datatype t =
  vr "string"
| ap "t list"
| lm "string" "t"

consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
axioms t_eq: "EQUIV Rt"

local_setup {*
  typedef_main (@{binding "qt"}, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
*}

section {* lifting of constants *}

text {* information about map-functions for type-constructor *}
ML {*
type typ_info = {mapfun: string}

local
  structure Data = GenericDataFun
  (type T = typ_info Symtab.table
   val empty = Symtab.empty
   val extend = I
   fun merge _ = Symtab.merge (K true))
in
 val lookup = Symtab.lookup o Data.get
 fun update k v = Data.map (Symtab.update (k, v)) 
end
*}

(* mapfuns for some standard types *)
setup {*
    Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}})
 #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}})
 #> Context.theory_map (update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}})
*}


ML {* lookup (Context.Proof @{context}) @{type_name list} *}

ML {*
datatype abs_or_rep = abs | rep

fun get_fun abs_or_rep rty qty lthy ty = 
let
  val qty_name = Long_Name.base_name (fst (dest_Type qty))
  
  fun get_fun_aux s fs_tys =
  let
    val (fs, tys) = split_list fs_tys
    val (otys, ntys) = split_list tys 
    val oty = Type (s, otys)
    val nty = Type (s, ntys)
    val ftys = map (op -->) tys
  in
   (case (lookup (Context.Proof lthy) s) of 
      SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))
    | NONE => raise ERROR ("no map association for type " ^ s))
  end

  fun get_const abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
    | get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
in
  if ty = qty
  then (get_const abs_or_rep)
  else (case ty of
          TFree _ => (Abs ("x", ty, Bound 0), (ty, ty))
        | Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty))
        | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys)  
        | _ => raise ERROR ("no variables")
       )
end
*}

ML {*
  get_fun rep @{typ t} @{typ qt} @{context} @{typ "t * nat"}
  |> fst
  |> Syntax.string_of_term @{context}
  |> writeln
*}


ML {*
fun get_const_def nconst oconst rty qty lthy =
let
  val ty = fastype_of nconst
  val (arg_tys, res_ty) = strip_type ty
 
  val fresh_args = arg_tys |> map (pair "x")
                           |> Variable.variant_frees lthy [nconst, oconst] 
                           |> map Free

  val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys
  val abs_fn  = (fst o get_fun abs rty qty lthy) res_ty

in
  map (op $) (rep_fns ~~ fresh_args)
  |> curry list_comb oconst
  |> curry (op $) abs_fn
  |> fold_rev lambda fresh_args
end
*}

ML {*
fun exchange_ty rty qty ty = 
  if ty = rty then qty
  else 
    (case ty of
       Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
      | _ => ty)
*}

ML {*
fun make_const_def nconst_name oconst mx rty qty lthy = 
let
  val oconst_ty = fastype_of oconst
  val nconst_ty = exchange_ty rty qty oconst_ty
  val nconst = Const (nconst_name, nconst_ty)
  val def_trm = get_const_def nconst oconst rty qty lthy
in
  make_def (Binding.name nconst_name, mx, def_trm) lthy
end  
*}

local_setup {*
  make_const_def "VR" @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd
*}

local_setup {*
  make_const_def "AP" @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd
*}

local_setup {*
  make_const_def "LM" @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
*}

thm VR_def
thm AP_def
thm LM_def
term LM 
term VR
term AP


text {* a test with functions *}
datatype 'a t' =
  vr' "string"
| ap' "('a t') * ('a t')"
| lm' "'a" "string \<Rightarrow> ('a t')"

consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
axioms t_eq': "EQUIV Rt'"

local_setup {*
  typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
*}


local_setup {*
  make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
*}

local_setup {*
  make_const_def "AP'" @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
*}

local_setup {*
  make_const_def "LM'" @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
*}

thm VR'_def
thm AP'_def
thm LM'_def
term LM' 
term VR'
term AP'

text {* finite set example *}

inductive 
  list_eq ("_ \<approx> _")
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_sym:
  shows "xs \<approx> xs"
apply(induct xs)
apply(auto intro: list_eq.intros)
done

lemma equiv_list_eq:
  shows "EQUIV list_eq"
unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
apply(auto intro: list_eq.intros list_eq_sym)
done

local_setup {*
  typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
*}

typ "'a fset"
thm "Rep_fset"

local_setup {*
  make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}

term Nil 
term EMPTY
thm EMPTY_def


local_setup {*
  make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}

term Cons 
term INSERT
thm INSERT_def

local_setup {*
  make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}

term append 
term UNION
thm UNION_def

thm QUOTIENT_fset

fun 
  membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _")
where
  m1: "(x memb []) = False"
| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"

lemma mem_respects:
  fixes z::"nat"
  assumes a: "list_eq x y"
  shows "z memb x = z memb y"
using a
apply(induct)
apply(auto)
done


local_setup {*
  make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}

term membship
term IN
thm IN_def

lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]

lemma yy:
  shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
unfolding IN_def EMPTY_def
apply(rule_tac f="(op =) False" in arg_cong)
apply(rule mem_respects)
apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
        simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
apply(rule list_eq.intros)
done

lemma
  shows "IN (x::nat) EMPTY = False"
using m1
apply -
apply(rule yy[THEN iffD1, symmetric])
apply(simp)
done

lemma
  shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
         ((x = y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
unfolding IN_def INSERT_def
apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
apply(rule mem_respects)
apply(rule list_eq.intros(3))
apply(unfold REP_fset_def ABS_fset_def)
apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
apply(rule list_eq_sym)
done

lemma helper:
  assumes a : "list_eq l1 l2"  
  shows "list_eq (l1 @ s) (l2 @ s)"
  using a
  apply(induct)
  apply(auto intro: list_eq.intros)
  apply(simp add: list_eq_sym)
done

lemma yyy :
  shows "
    (
     (UNION EMPTY s = s) &
     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
    ) = (
     ((ABS_fset ([] @ REP_fset s)) = s) &
     ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
    )"
  unfolding UNION_def EMPTY_def INSERT_def
  apply(rule_tac f="(op &)" in arg_cong2)
  apply(rule_tac f="(op =)" in arg_cong2)
  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,
                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
  apply(rule helper)
  apply(rule list_eq.intros(3))
  apply(simp only:QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
  apply(rule list_eq_sym)
  apply(simp)
  apply(rule_tac f="(op =)" in arg_cong2)
  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
                  simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
  apply(rule helper)
  apply(rule list_eq.intros(3))
  apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset,
                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
  apply(rule list_eq_sym)
  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
                     simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
  apply(rule list_eq.intros(5))
  apply(rule list_eq.intros(3))
  apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
                 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
  apply(rule list_eq_sym)
done

lemma
  shows "
    (
     (UNION EMPTY s = s) &
     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
    )"
  apply(simp add:yyy)
  apply (unfold REP_fset_def ABS_fset_def)
  apply (rule QUOT_TYPE.thm10[OF QUOT_TYPE_fset])
done