theory LFex
imports Nominal QuotMain
begin

atom_decl name id

nominal_datatype kind = 
    Type
  | KPi "ty" "name" "kind"
and ty =  
    TConst "id"
  | TApp "ty" "trm"
  | TPi "ty" "name" "ty"
and trm = 
    Const "id"
  | Var "name"
  | App "trm" "trm"
  | Lam "ty" "name" "trm" 

function
    fv_kind :: "kind \<Rightarrow> name set"
and fv_ty   :: "ty \<Rightarrow> name set"
and fv_trm  :: "trm \<Rightarrow> name set"
where
  "fv_kind (Type) = {}"
| "fv_kind (KPi A x K) = (fv_ty A) \<union> ((fv_kind K) - {x})"
| "fv_ty (TConst i) = {}"
| "fv_ty (TApp A M) = (fv_ty A) \<union> (fv_trm M)"
| "fv_ty (TPi A x B) = (fv_ty A) \<union> ((fv_ty B) - {x})"
| "fv_trm (Const i) = {}"
| "fv_trm (Var x) = {x}"
| "fv_trm (App M N) = (fv_trm M) \<union> (fv_trm N)"
| "fv_trm (Lam A x M) = (fv_ty A) \<union> ((fv_trm M) - {x})"
sorry

termination fv_kind sorry

inductive
    akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
where
  a1:  "(Type) \<approx>ki (Type)"
| a21: "\<lbrakk>A \<approx>ty A'; K \<approx>ki K'\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x K')"
| a22: "\<lbrakk>A \<approx>ty A'; K \<approx>ki ([(x,x')]\<bullet>K'); x \<notin> (fv_ty A'); x \<notin> ((fv_kind K') - {x'})\<rbrakk> 
        \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
| a3:  "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
| a4:  "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
| a51: "\<lbrakk>A \<approx>ty A'; B \<approx>ty B'\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x B')"
| a52: "\<lbrakk>A \<approx>ty A'; B \<approx>ty ([(x,x')]\<bullet>B'); x \<notin> (fv_ty B'); x \<notin> ((fv_ty B') - {x'})\<rbrakk> 
        \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
| a6:  "i = j \<Longrightarrow> (Const i) \<approx>trm (Const j)"
| a7:  "x = y \<Longrightarrow> (Var x) \<approx>trm (Var y)"
| a8:  "\<lbrakk>M \<approx>trm M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
| a91: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x M')"
| a92: "\<lbrakk>A \<approx>ty A'; M \<approx>tr ([(x,x')]\<bullet>M'); x \<notin> (fv_ty B'); x \<notin> ((fv_trm M') - {x'})\<rbrakk> 
        \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"

lemma al_refl:
  fixes K::"kind" 
  and   A::"ty"
  and   M::"trm"
  shows "K \<approx>ki K"
  and   "A \<approx>ty A"
  and   "M \<approx>tr M"
  apply(induct K and A and M rule: kind_ty_trm.inducts)
  apply(auto intro: akind_aty_atrm.intros)
  done

lemma alpha_EQUIVs:
  shows "EQUIV akind"
  and   "EQUIV aty"
  and   "EQUIV atrm"
sorry

quotient KIND = kind / akind
  by (rule alpha_EQUIVs)

quotient TY = ty / aty
   and   TRM = trm / atrm
  by (auto intro: alpha_EQUIVs)

print_quotients

quotient_def 
  TYP :: "KIND"
where
  "TYP \<equiv> Type"

quotient_def 
  KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
where
  "KPI \<equiv> KPi"

quotient_def 
  TCONST :: "id \<Rightarrow> TY"
where
  "TCONST \<equiv> TConst"

quotient_def 
  TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY"
where
  "TAPP \<equiv> TApp"

quotient_def 
  TPI :: "TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
where
  "TPI \<equiv> TPi"

(* FIXME: does not work with CONST *)
quotient_def 
  CONS :: "id \<Rightarrow> TRM"
where
  "CONS \<equiv> Const"

quotient_def 
  VAR :: "name \<Rightarrow> TRM"
where
  "VAR \<equiv> Var"

quotient_def 
  APP :: "TRM \<Rightarrow> TRM \<Rightarrow> TRM"
where
  "APP \<equiv> App"

quotient_def 
  LAM :: "TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
where
  "LAM \<equiv> Lam"

thm TYP_def
thm KPI_def
thm TCONST_def
thm TAPP_def
thm TPI_def
thm VAR_def
thm CONS_def
thm APP_def
thm LAM_def

(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
quotient_def 
  FV_kind :: "KIND \<Rightarrow> name set"
where
  "FV_kind \<equiv> fv_kind"

quotient_def 
  FV_ty :: "TY \<Rightarrow> name set"
where
  "FV_ty \<equiv> fv_ty"

quotient_def 
  FV_trm :: "TRM \<Rightarrow> name set"
where
  "FV_trm \<equiv> fv_trm"

thm FV_kind_def
thm FV_ty_def
thm FV_trm_def

(* FIXME: does not work yet *)
overloading
    perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"   (unchecked)
    perm_ty   \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"       (unchecked)
    perm_trm  \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"     (unchecked) 
begin

quotient_def 
  perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
where
  "perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"

quotient_def 
  perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY"
where
  "perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"

quotient_def 
  perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
where
  "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"

thm akind_aty_atrm.induct

lemma left_ball_regular:
  assumes a: "EQUIV R"
  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
apply (rule LEFT_RES_FORALL_REGULAR)
using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
apply (simp)
done

lemma right_bex_regular:
  assumes a: "EQUIV R"
  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
apply (rule RIGHT_RES_EXISTS_REGULAR)
using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
apply (simp)
done

lemma ball_respects_refl:
  fixes P::"'a \<Rightarrow> bool"
  and x::"'a"
  assumes a: "EQUIV R2"
  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
apply(rule iffI)
apply(rule allI)
apply(drule_tac x="\<lambda>y. f x" in bspec)
apply(simp add: Respects_def IN_RESPECTS)
apply(rule impI)
using a EQUIV_REFL_SYM_TRANS[of "R2"]
apply(simp add: REFL_def)
apply(simp)
apply(simp)
done

ML {*
fun ball_simproc rel_eqvs ss redex =
  let
    val ctxt = Simplifier.the_context ss
    val thy = ProofContext.theory_of ctxt
  in
  case redex of
      (ogl as ((Const (@{const_name "Ball"}, _)) $
        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ P1)) =>
      (let
        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
        val _ = tracing (Syntax.string_of_term ctxt glc);
        val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
        val thm = (@{thm eq_reflection} OF [@{thm ball_respects_refl} OF [eqv]]);
        val R1c = cterm_of @{theory} R1;
        val thmi = Drule.instantiate' [] [SOME R1c] thm;
        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));
        val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
        val _ = tracing "AAA";
        val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
      in
        SOME thm2
      end
      handle _ => NONE

      )
  | _ => NONE
  end
*}

ML {*
fun regularize_tac ctxt rel_eqvs =
  let
    val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs;
    val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs;
    val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2);
    val pat = [@{term "Ball (Respects (R1 ===> R2)) P"}];
    val thy = ProofContext.theory_of ctxt
    val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs))
  in
  (ObjectLogic.full_atomize_tac) THEN'
  (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) THEN'
  REPEAT_ALL_NEW (FIRST' [
    (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
    (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
    (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
    (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
    (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
    (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
    (resolve_tac (Inductive.get_monos ctxt)),
    rtac @{thm move_forall},
    rtac @{thm move_exists},
    (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc]))
  ])
  end
*}

ML {* val defs =
  @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
    FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
*}

lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K');
 \<And>A A' K x x' K'.
    \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk>
    \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K');
 \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
 \<And>A A' M M'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
 \<And>A A' B B' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x B');
 \<And>A A' B x x' B'.
    \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \<bullet> B'); P2 B ([(x, x')] \<bullet> B'); x \<notin> FV_ty B'; x \<notin> FV_ty B' - {x'}\<rbrakk>
    \<Longrightarrow> P2 (TPI A x B) (TPI A' x' B');
 \<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j)); \<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y));
 \<And>M m M' N N'. \<lbrakk>(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\<rbrakk> \<Longrightarrow> P3 (APP M N) (APP M' N');
 \<And>A A' M M' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x M');
 \<And>A A' M x x' M' B'.
    \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk>
    \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk>
\<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>
   ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *}
apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
prefer 2
ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *}
apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
apply (tactic {* lambda_prs_tac @{context} quot 1 *})
ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}
apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *})
ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *}
apply (tactic {* simp_tac (HOL_ss addsimps reps_same) 1 *})
apply (tactic {* lambda_prs_tac @{context} quot 1 *})
ML_prf {*
val rrr1 = ref @{cterm "0"}
val rrr2 = ref @{cterm "0"}
val rrrt = ref @{thm refl}
*}

ML_prf {*
fun lambda_prs_conv1 ctxt quot_thms ctrm =
  case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
  let
    val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
    val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
    val thy = ProofContext.theory_of ctxt;
    val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
    val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
    val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
    val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
    val tac =
      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
      (quotient_tac quot_thms);
    val gc = Drule.strip_imp_concl (cprop_of lpi);
    val t = Goal.prove_internal [] gc (fn _ => tac 1)
    val te = @{thm eq_reflection} OF [t]
    val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
    val tl = Thm.lhs_of ts;
    val _ = rrrt := ts;
    val _ = rrr1 := ctrm;
    val _ = rrr2 := tl;
(*    val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
    val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
    val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
  in
    Conv.all_conv ctrm
(*    Conv.rewr_conv ti ctrm *)
  end
(* TODO: We can add a proper error message... *)
  handle Bind => Conv.all_conv ctrm

*}

(* quot stands for the QUOTIENT theorems: *) 
(* could be potentially all of them       *)
ML_prf {*
fun lambda_prs_conv ctxt quot ctrm =
  case (term_of ctrm) of
    (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>
      (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
      then_conv (lambda_prs_conv1 ctxt quot)) ctrm
  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
  | _ => Conv.all_conv ctrm
*}

ML_prf {*
fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
  CONVERSION
    (Conv.params_conv ~1 (fn ctxt =>
       (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
          Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
*}
apply (tactic {* lambda_prs_tac @{context} quot 1 *})
ML_prf {* !rrr1 *}
ML_prf {* val rrr1' = @{cterm "((ABS_KIND ---> ABS_KIND ---> Fun.id) ---> Fun.id)
     (\<lambda>P1\<Colon>kind \<Rightarrow> kind \<Rightarrow> bool.
         All (((ABS_TY ---> ABS_TY ---> Fun.id) ---> Fun.id)
               (\<lambda>P2\<Colon>ty \<Rightarrow> ty \<Rightarrow> bool.
                   \<forall>(a\<Colon>TRM \<Rightarrow> TRM \<Rightarrow> bool) (b\<Colon>KIND) (c\<Colon>KIND) (d\<Colon>TY) (e\<Colon>TY) (f\<Colon>TRM) g\<Colon>TRM.
                      (REP_KIND ---> REP_KIND ---> Fun.id) P1 TYP TYP \<longrightarrow>
                      (\<forall>a\<Colon>TY. (REP_TY ---> REP_TY ---> Fun.id) P2 a a \<longrightarrow>
                              (\<forall>x\<Colon>KIND.
                                  (REP_KIND ---> REP_KIND ---> Fun.id) P1 x x \<longrightarrow>
                                  (\<forall>xa\<Colon>name. (REP_KIND ---> REP_KIND ---> Fun.id) P1 (KPI a xa x) (KPI a xa x)))) \<longrightarrow>
                      (\<forall>a\<Colon>TY. (REP_TY ---> REP_TY ---> Fun.id) P2 a a \<longrightarrow>
                              (\<forall>(x\<Colon>name) (x'\<Colon>name) xa\<Colon>KIND.
                                  (REP_KIND ---> REP_KIND ---> Fun.id) P1 ([(x, x')] \<bullet> xa) ([(x, x')] \<bullet> xa) \<longrightarrow>
                                  x \<notin> FV_ty a \<longrightarrow>
                                  x \<notin> FV_kind xa - {x'} \<longrightarrow>
                                  (REP_KIND ---> REP_KIND ---> Fun.id) P1 (KPI a x ([(x, x')] \<bullet> xa)) (KPI a x' xa))) \<longrightarrow>
                      (b = c \<longrightarrow> (REP_KIND ---> REP_KIND ---> Fun.id) P1 c c) \<and>
                      (d = e \<longrightarrow> (REP_TY ---> REP_TY ---> Fun.id) P2 e e) \<and> (f = g \<longrightarrow> a g g))))"} *}
ML_prf {* (!rrrt); rrr1'; (!rrr1) *}

ML_prf {*
fun make_inst lhs t =
  let
    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
    val _ $ (Abs (_, _, g)) = t;
    fun mk_abs i t =
      if incr_boundvars i u aconv t then Bound i
      else (case t of
        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
      | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t')
      | Bound j => if i = j then error "make_inst" else t
      | _ => t);
  in (f, Abs ("x", T, mk_abs 0 g)) end;
*}

ML_prf {* cterm_of @{theory} (snd (make_inst (term_of (!rrr2)) (term_of (!rrr1)))) *}
ML_prf {* val betaeta = Conv.fconv_rule Drule.beta_eta_conversion *}
ML_prf {* val rr = betaeta (Drule.instantiate' [] [SOME it] (!rrrt)) *}
ML_prf {* (term_of (Thm.lhs_of rr)) aconv (term_of (!rrr1)) *}
ML_prf {* matching_prs @{theory} (term_of (!rrr2)) (term_of (rrr1')) *}
ML_prf {* matching_prs @{theory} (term_of (!rrr2)) (term_of (!rrr1)) *}

apply (tactic {* clean_tac @{context}  defs aps 1 *})
ML_prf {*  *}
print_quotients
apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl [trans2] [] 1*})


ML {* val consts = lookup_quot_consts defs *}

ML {*
val rty_qty_rel =
  [(@{typ kind}, (@{typ KIND}, @{term akind})),
   (@{typ ty}, (@{typ TY}, @{term aty})),
   (@{typ trm}, (@{typ TRM}, @{term atrm}))]
*}

print_quotients

ML {* val rty = [@{typ }] *}
ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *}
prove {* build_regularize_goal t_a rty rel @{context}

end