theory QuotMain
imports QuotScript QuotList Prove
begin

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) \<equiv> a"
  apply  (rule eq_reflection)
  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:
  shows "(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"
by (simp_all add: thm10 thm11)

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

lemma R_trans:
  assumes ab: "R a b"
  and     bc: "R b c"
  shows "R a c"
proof -
  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
  moreover have ab: "R a b" by fact
  moreover have bc: "R b c" by fact
  ultimately show "R a c" unfolding TRANS_def by blast
qed

lemma R_sym:
  assumes ab: "R a b"
  shows "R b a"
proof -
  have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
  then show "R b a" using ab unfolding SYM_def by blast
qed

lemma R_trans2:
  assumes ac: "R a c"
  and     bd: "R b d"
  shows "R a b = R c d"
proof
  assume "R a b"
  then have "R b a" using R_sym by blast
  then have "R b c" using ac R_trans by blast
  then have "R c b" using R_sym by blast
  then show "R c d" using bd R_trans by blast
next
  assume "R c d"
  then have "R a d" using ac R_trans by blast
  then have "R d a" using R_sym by blast
  then have "R b a" using bd R_trans by blast
  then show "R a b" using R_sym by blast
qed

lemma REPS_same:
  shows "R (REP a) (REP b) \<equiv> (a = b)"
  apply (rule eq_reflection)
proof
  assume as: "R (REP a) (REP b)"
  from rep_prop
  obtain x y
    where eqs: "Rep a = R x" "Rep b = R y" by blast
  from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
  then have "R x (Eps (R y))" using lem9 by simp
  then have "R (Eps (R y)) x" using R_sym by blast
  then have "R y x" using lem9 by simp
  then have "R x y" using R_sym by blast
  then have "ABS x = ABS y" using thm11 by simp
  then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
  then show "a = b" using rep_inverse by simp
next
  assume ab: "a = b"
  have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
  then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
qed

end

section {* type definition for the quotient type *}

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 {*
(* makes the new type definitions and proves non-emptyness*)
fun typedef_make (qty_name, rel, ty) lthy =
let
  val typedef_tac =
     EVERY1 [rewrite_goal_tac @{thms mem_def},
             rtac @{thm exI},
             rtac @{thm exI},
             rtac @{thm refl}]
in
  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
end
*}

ML {*
(* proves the QUOT_TYPE theorem for the new type *)
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

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
    (K (typedef_quot_type_tac equiv_thm typedef_info))
end
*}

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

  val typedef_quotient_thm_tac =
    EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
            rtac @{thm QUOT_TYPE.QUOTIENT},
            rtac quot_type_thm]
in
  Goal.prove lthy [] [] goal
    (K typedef_quotient_thm_tac)
end
*}

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

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

ML {*
val no_vars = Thm.rule_attribute (fn context => fn th =>
  let
    val ctxt = Variable.set_body false (Context.proof_of context);
    val ((_, [th']), _) = Variable.import true [th] ctxt;
  in th' end);
*}

ML {*
fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
let
  (* generates typedef *)
  val ((_, typedef_info), lthy1) = 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 lthy1 (ABS_const $ rel $ abs)
  val REP_trm = Syntax.check_term lthy1 (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)), lthy2) =
         lthy1 |> 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) lthy2
  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) lthy2
  val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name

  (* interpretation *)
  val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
  val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2;
  val eqn1i = Thm.prop_of (symmetric eqn1pre)
  val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3;
  val eqn2i = Thm.prop_of (symmetric eqn2pre)

  val exp_morphism = ProofContext.export_morphism lthy4 (ProofContext.init (ProofContext.theory_of lthy4));
  val exp_term = Morphism.term exp_morphism;
  val exp = Morphism.thm exp_morphism;

  val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
    ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
  val mthdt = Method.Basic (fn _ => mthd)
  val bymt = Proof.global_terminal_proof (mthdt, NONE)
  val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
    Expression.Named [
     ("R", rel),
     ("Abs", abs),
     ("Rep", rep)
    ]))]
in
  lthy4
  |> note_thm (quot_thm_name, quot_thm)
  ||>> note_thm (quotient_thm_name, quotient_thm)
  ||> LocalTheory.theory (fn thy =>
      let
        val global_eqns = map exp_term [eqn2i, eqn1i];
        (* Not sure if the following context should not be used *)
        val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4;
        val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
      in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
end
*}

section {* various tests for quotient types*}
datatype trm =
  var  "nat"
| app  "trm" "trm"
| lam  "nat" "trm"

axiomatization
  RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
where
  r_eq: "EQUIV RR"

local_setup {*
  typedef_main (@{binding "qtrm"}, @{term "RR"}, @{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

(* Test interpretation *)
thm QUOT_TYPE_I_qtrm.thm11
thm QUOT_TYPE.thm11

print_theorems

thm Rep_qtrm

text {* another test *}
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
*}

print_theorems

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_bname oconst mx rty qty lthy =
let
  val oconst_ty = fastype_of oconst
  val nconst_ty = exchange_ty rty qty oconst_ty
  val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
  val def_trm = get_const_def nconst oconst rty qty lthy
in
  make_def (nconst_bname, mx, def_trm) lthy
end
*}

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

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

local_setup {*
  make_const_def @{binding 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
*}

print_theorems

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

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

local_setup {*
  make_const_def @{binding 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 *}
print_syntax
inductive
  list_eq (infix "\<approx>" 50)
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
*}

print_theorems

typ "'a fset"
thm "Rep_fset"

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

term Nil
term EMPTY
thm EMPTY_def


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

term Cons
term INSERT
thm INSERT_def

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

term append
term UNION
thm UNION_def


thm QUOTIENT_fset

thm QUOT_TYPE_I_fset.thm11


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

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


fun
  card1 :: "'a list \<Rightarrow> nat"
where
  card1_nil: "(card1 []) = 0"
| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"

local_setup {*
  make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}

term card1
term card
thm card_def

(* text {*
 Maybe make_const_def should require a theorem that says that the particular lifted function
 respects the relation. With it such a definition would be impossible:
 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*} *)

lemma card1_rsp:
  fixes a b :: "'a list"
  assumes e: "a \<approx> b"
  shows "card1 a = card1 b"
  using e apply induct
  apply (simp_all add:mem_respects)
  done

lemma card1_0:
  fixes a :: "'a list"
  shows "(card1 a = 0) = (a = [])"
  apply (induct a)
   apply (simp)
  apply (simp_all)
   apply meson
  apply (simp_all)
  done

lemma not_mem_card1:
  fixes x :: "'a"
  fixes xs :: "'a list"
  shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"
  by simp


lemma mem_cons:
  fixes x :: "'a"
  fixes xs :: "'a list"
  assumes a : "x memb xs"
  shows "x # xs \<approx> xs"
  using a apply (induct xs)
  apply (simp_all)
  apply (meson)
  apply (simp_all add: list_eq.intros(4))
  proof -
    fix a :: "'a"
    fix xs :: "'a list"
    assume a1 : "x # xs \<approx> xs"
    assume a2 : "x memb xs"
    have a3 : "x # a # xs \<approx> a # x # xs" using list_eq.intros(1)[of "x"] by blast
    have a4 : "a # x # xs \<approx> a # xs" using a1 list_eq.intros(5)[of "x # xs" "xs"] by simp
    then show "x # a # xs \<approx> a # xs" using a3 list_eq.intros(6) by blast
  qed

lemma card1_suc:
  fixes xs :: "'a list"
  fixes n :: "nat"
  assumes c: "card1 xs = Suc n"
  shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
  using c apply (induct xs)
   apply (simp)
(*  apply (rule allI)*)
  proof -
    fix a :: "'a"
    fix xs :: "'a list"
    fix n :: "nat"
    assume a1: "card1 xs = Suc n \<Longrightarrow> \<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys"
    assume a2: "card1 (a # xs) = Suc n"
    from a1 a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
    apply -
    apply (rule True_or_False [of "a memb xs", THEN disjE])
    apply (simp_all add: card1_cons if_True simp_thms)
  proof -
    assume a1: "\<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys"
    assume a2: "card1 xs = Suc n"
    assume a3: "a memb xs"
    from a1 obtain b ys where a5: "\<not> b memb ys \<and> xs \<approx> b # ys" by blast
    from a2 a3 a5 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
    apply -
    apply (rule_tac x = "b" in exI)
    apply (rule_tac x = "ys" in exI)
    apply (simp_all)
  proof -
    assume a1: "a memb xs"
    assume a2: "\<not> b memb ys \<and> xs \<approx> b # ys"
    then have a3: "xs \<approx> b # ys" by simp
    have "a # xs \<approx> xs" using a1 mem_cons[of "a" "xs"] by simp
    then show "a # xs \<approx> b # ys" using a3 list_eq.intros(6) by blast
  qed
next
  assume a2: "\<not> a memb xs"
  from a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
    apply -
    apply (rule_tac x = "a" in exI)
    apply (rule_tac x = "xs" in exI)
    apply (simp)
    apply (rule list_eq_sym)
    done
  qed
qed

lemma cons_preserves:
  fixes z
  assumes a: "xs \<approx> ys"
  shows "(z # xs) \<approx> (z # ys)"
  using a by (rule QuotMain.list_eq.intros(5))


text {*
  unlam_def converts a definition theorem given as 'a = \lambda x. \lambda y. f (x y)'
  to a theorem 'a x y = f (x, y)'. These are needed to rewrite right-to-left.
*}

ML {*
fun unlam_def_aux orig_ctxt ctxt t =
  let val rhs = Thm.rhs_of t in
  (case try (Thm.dest_abs NONE) rhs of
    SOME (v, vt) =>
      let
        val (vname, vt) = Term.dest_Free (Thm.term_of v)
        val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt
        val nv = Free(vnname, vt)
        val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv)
        val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2
      in unlam_def_aux orig_ctxt ctxt tnorm end
  | NONE => singleton (ProofContext.export ctxt orig_ctxt) t)
  end;

fun unlam_def ctxt t = unlam_def_aux ctxt ctxt t
*}

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

term membship
term IN
thm IN_def
ML {* unlam_def @{context} @{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_I_fset.REP_ABS_rsp)
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 append_respects_fst:
  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_I_fset.thm11[symmetric])
  apply(rule append_respects_fst)
  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
  apply(rule list_eq_sym)
  apply(simp)
  apply(rule_tac f="(op =)" in arg_cong2)
  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
  apply(rule append_respects_fst)
  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
  apply(rule list_eq_sym)
  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
  apply(rule list_eq.intros(5))
  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
  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 (simp add: QUOT_TYPE_I_fset.thm10)
  done

ML {*
  fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
  val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}]
*}

ML lambda

ML {*
fun build_goal thm constructors lifted_type mk_rep_abs =
  let
    fun is_const (Const (x, t)) = x mem constructors
      | is_const _ = false
    fun maybe_mk_rep_abs t =
      let
        val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t)
      in
        if type_of t = lifted_type then mk_rep_abs t else t
      end
(*      handle TYPE _ => t*)
    fun build_aux (Abs (s, t, tr)) =
        let
          val [(fresh_s, _)] = Variable.variant_frees @{context} [] [(s, ())];
          val newv = Free (fresh_s, t);
          val str = subst_bound (newv, tr);
          val rec_term = build_aux str;
          val bound_term = lambda newv rec_term
        in
          bound_term
        end
      | build_aux (f $ a) =
          let
            val (f, args) = strip_comb (f $ a)
            val _ = writeln (Syntax.string_of_term @{context} f)
           in
            (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args))))
            else list_comb ((build_aux f), (map build_aux args)))
          end
      | build_aux x =
          if is_const x then maybe_mk_rep_abs x else x
    val concl2 = term_of (#prop (crep_thm thm))
  in
  Logic.mk_equals ((build_aux concl2), concl2)
end *}

ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *}

ML {*
  fun dest_cbinop t =
    let
      val (t2, rhs) = Thm.dest_comb t;
      val (bop, lhs) = Thm.dest_comb t2;
    in
      (bop, (lhs, rhs))
    end
*}
ML {*
  fun dest_ceq t =
    let
      val (bop, pair) = dest_cbinop t;
      val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
    in
      if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
    end
*}
ML Thm.instantiate
ML {*@{thm arg_cong2}*}
ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
ML {*
  Toplevel.program (fn () =>
    Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2}
  )
*}

ML {*
  fun split_binop_conv t =
    let
      val _ = tracing (Syntax.string_of_term @{context} (term_of t))
      val (lhs, rhs) = dest_ceq t;
      val (bop, _) = dest_cbinop lhs;
      val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
      val [cmT, crT] = Thm.dest_ctyp cr2;
    in
      Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
    end
*}

ML {*
  fun split_arg_conv t =
    let
      val (lhs, rhs) = dest_ceq t;
      val (lop, larg) = Thm.dest_comb lhs;
      val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
    in
      Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
    end
*}

ML {*
  fun split_binop_tac n thm =
    let
      val concl = Thm.cprem_of thm n;
      val (_, cconcl) = Thm.dest_comb concl;
      val rewr = split_binop_conv cconcl;
    in
      rtac rewr n thm
    end
      handle CTERM _ => Seq.empty
*}

ML {*
  fun split_arg_tac n thm =
    let
      val concl = Thm.cprem_of thm n;
      val (_, cconcl) = Thm.dest_comb concl;
      val rewr = split_arg_conv cconcl;
    in
      rtac rewr n thm
    end
      handle CTERM _ => Seq.empty
*}

(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)

lemma trueprop_cong:
  shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
  by auto

ML {*
  fun foo_tac' ctxt =
    REPEAT_ALL_NEW (FIRST' [
      rtac @{thm trueprop_cong},
      rtac @{thm list_eq_sym},
      rtac @{thm cons_preserves},
      rtac @{thm mem_respects},
      rtac @{thm card1_rsp},
      rtac @{thm QUOT_TYPE_I_fset.R_trans2},
      CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
      DatatypeAux.cong_tac,
      rtac @{thm ext},
(*      rtac @{thm eq_reflection}*)
      CHANGED o (ObjectLogic.full_atomize_tac)
    ])
*}

ML {*
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
  val cgoal = cterm_of @{theory} goal
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}

(*notation ( output) "prop" ("#_" [1000] 1000) *)
notation ( output) "Trueprop" ("#_" [1000] 1000)

prove {* (Thm.term_of cgoal2) *}
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
  apply (tactic {* foo_tac' @{context} 1 *})
  done

thm length_append (* Not true but worth checking that the goal is correct *)
ML {*
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
  val cgoal = cterm_of @{theory} goal
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
prove {* Thm.term_of cgoal2 *}
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
  apply (tactic {* foo_tac' @{context} 1 *})
  sorry

thm m2
ML {*
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
  val cgoal = cterm_of @{theory} goal
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
prove {* Thm.term_of cgoal2 *}
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
  apply (tactic {* foo_tac' @{context} 1 *})
  done

thm list_eq.intros(4)
ML {*
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
  val cgoal = cterm_of @{theory} goal
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
  val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
*}

(* It is the same, but we need a name for it. *)
prove {* Thm.term_of cgoal3 *}
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
  apply (tactic {* foo_tac' @{context} 1 *})
  done
lemma zzz :
  "Trueprop (REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))
    \<equiv> Trueprop (a # a # xs \<approx> a # xs)"
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
  apply (tactic {* foo_tac' @{context} 1 *})
  done

lemma zzz' :
  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
  using list_eq.intros(4) by (simp only: zzz)

thm QUOT_TYPE_I_fset.REPS_same
ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}

ML Drule.instantiate'
ML {* zzz'' *}
text {*
  A variable export will still be necessary in the end, but this is already the final theorem.
*}
ML {*
  Toplevel.program (fn () =>
    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
      Drule.instantiate' [] [NONE, SOME (@{cpat "REP_fset x"})] zzz''
    )
  )
*}


thm list_eq.intros(5)
ML {*
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
*}
ML {*
  val cgoal =
    Toplevel.program (fn () =>
      cterm_of @{theory} goal
    )
*}
ML {*
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
*}
prove {* Thm.term_of cgoal2 *}
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
  apply (tactic {* foo_tac' @{context} 1 *})
  done

thm list.induct

ML {*
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
*}
ML {*
  val goal =
    Toplevel.program (fn () =>
      build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
    )
*}
ML {*
  val cgoal = cterm_of @{theory} goal
*}
ML {*
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
*}

prove {* (Thm.term_of cgoal2) *}
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
  apply (tactic {* foo_tac' @{context} 1 *})
  sorry

thm card1_suc

ML {*
  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc}))
*}
ML {*
  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
*}
ML {*
  val cgoal = cterm_of @{theory} goal
  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
*}
ML {* @{term "\<exists>x. P x"} *}
prove {* (Thm.term_of cgoal2) *}
  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
  apply (tactic {* foo_tac' @{context} 1 *})
  done


(*
datatype obj1 =
  OVAR1 "string"
| OBJ1 "(string * (string \<Rightarrow> obj1)) list"
| INVOKE1 "obj1 \<Rightarrow> string"
| UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
*)