theory Perm

imports "../Nominal-General/Nominal2_Atoms"

begin

ML {*

fun quotient_lift_consts_export qtys spec ctxt =

let

  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;

  val (ts_loc, defs_loc) = split_list result;

  val morphism = ProofContext.export_morphism ctxt' ctxt;

  val ts = map (Morphism.term morphism) ts_loc

  val defs = Morphism.fact morphism defs_loc

in

  (ts, defs, ctxt')

end

*}

ML {*

fun prove_perm_empty lthy induct perm_def perm_frees =

let

  val perm_types = map fastype_of perm_frees;

  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);

  fun glc ((perm, T), x) =

  val gl =

    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)));

  fun tac _ =

    EVERY [

      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def)))

    ];

in

end;

*}

ML {*

fun prove_perm_append lthy induct perm_def perm_frees =

let

  val pi1 = Free ("pi1", @{typ perm});

  val pi2 = Free ("pi2", @{typ perm});

  val perm_types = map fastype_of perm_frees

  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);

  fun glc ((perm, T), x) =

    HOLogic.mk_eq (

      perm $ pi1 $ (perm $ pi2 $ Free (x, T)))

    (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))

  fun tac _ =

    EVERY [

      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))

    ]

in

end;

*}

ML {*

let

  val {descr, induct, sorts, ...} = dt_info;

  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;

  val full_tnames = List.take (all_full_tnames, number);

  val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>

  val perm_types = map (fn (i, _) =>

    let val T = nth_dtyp i

    in @{typ perm} --> T --> T end) descr;

  val perm_names_types' = perm_names' ~~ perm_types;

  val pi = Free ("pi", @{typ perm});

  fun perm_eq_constr i (cname, dts) =

    let

      val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);

      val args = map Free (names ~~ Ts);

      val c = Const (cname, Ts ---> (nth_dtyp i));

      fun perm_arg (dt, x) =

        let val T = type_of x

        in

            let val (Us, _) = strip_type T

            in list_abs (map (pair "x") Us,

                list_comb (x, map (fn (i, U) =>

                  (mk_perm_ty U (mk_minus pi) (Bound i)))

                  ((length Us - 1 downto 0) ~~ Us)))

            end

          else (mk_perm_ty T pi x)

        end;

    in

      (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq

        (Free (nth perm_names_types' i) $

           Free ("pi", @{typ perm}) $ list_comb (c, args),

         list_comb (c, map perm_arg (dts ~~ args)))))

    end;

    fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;

    val perm_eqs = maps perm_eq descr;

    val lthy =

      Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;

    val ((perm_frees, perm_ldef), lthy') =

      Primrec.add_primrec

        (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;

    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number);

    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number)

    val perms_name = space_implode "_" perm_names'

    val perms_zero_bind = Binding.name (perms_name ^ "_zero")

    val perms_append_bind = Binding.name (perms_name ^ "_append")

    fun tac _ (_, simps, _) =

      (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps));

    fun morphism phi (dfs, simps, fvs) =

      (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);

  in

  lthy'

  |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))

  |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))

  |> Class_Target.prove_instantiation_exit_result morphism tac 

      (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)

  end

*}

ML {*

fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =

let

  val lthy =

    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;

  val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;

  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;

  fun tac _ =

    Class.intro_classes_tac [] THEN

    (ALLGOALS (resolve_tac lifted_thms))

  val lthy'' = Class.prove_instantiation_instance tac lthy'

in

  Local_Theory.exit_global lthy''

end

*}

ML {*

fun neq_to_rel r neq =

let

  val neq = HOLogic.dest_Trueprop (prop_of neq)

  val eq = HOLogic.dest_not neq

  val (lhs, rhs) = HOLogic.dest_eq eq

  val rel = r $ lhs $ rhs

  val nrel = HOLogic.mk_not rel

in

  HOLogic.mk_Trueprop nrel

end

*}

ML {*

fun neq_to_rel_tac cases distinct =

  rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)

*}

ML {*

fun distinct_rel ctxt cases (dists, rel) =

let

  val ((_, thms), ctxt') = Variable.import false dists ctxt

  val terms = map (neq_to_rel rel) thms

  val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms

in

  Variable.export ctxt' ctxt nrels

end

*}

(* Test

atom_decl name

and bp =

  BUnit

print_theorems

*)

end