<commit_before>(*  Title:      HOL/Tools/Quotient/quotient_type.ML
    Author:     <NAME> and <NAME>

Definition of a quotient type.
*)

signature QUOTIENT_TYPE =
sig
  val can_generate_code_cert: thm -> bool
  
  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
    ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory

  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
    ((binding * binding) option)) list -> Proof.context -> Proof.state

  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
    (binding * binding) option) list -> Proof.context -> Proof.state
end;

structure Quotient_Type: QUOTIENT_TYPE =
struct


(*** definition of quotient types ***)

val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}

(* constructs the term {c. EX (x::rty). rel x x \<and> c = Collect (rel x)} *)
fun typedef_term rel rty lthy =
  let
    val [x, c] =
      [("x", rty), ("c", HOLogic.mk_setT rty)]
      |> Variable.variant_frees lthy [rel]
      |> map Free
  in
    HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $
        lambda x (HOLogic.mk_conj (rel $ x $ x,
        HOLogic.mk_eq (c, HOLogic.Collect_const rty $ (rel $ x))))))
  end


(* makes the new type definitions and proves non-emptyness *)
fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
  let
    val typedef_tac =
      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
  in
    Typedef.add_typedef false NONE (qty_name, map (rpair dummyS) vs, mx)
      (typedef_term rel rty lthy) NONE typedef_tac lthy
  end


(* tactic to prove 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 RS mem_def1
    val rep_inv = #Rep_inverse typedef_info
    val abs_inv = #Abs_inverse typedef_info
    val rep_inj = #Rep_inject typedef_info
  in
    (rtac @{thm quot_type.intro} THEN' RANGE [
      rtac equiv_thm,
      rtac rep_thm,
      rtac rep_inv,
      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
      rtac rep_inj]) 1
  end

(* proves the quot_type theorem for the new type *)
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
  let
    val quot_type_const = Const (@{const_name "quot_type"},
      fastype_of rel --> fastype_of abs --> fastype_of rep --> @{typ bool})
    val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
  in
    Goal.prove lthy [] [] goal
      (K (typedef_quot_type_tac equiv_thm typedef_info))
  end
   
fun can_generate_code_cert quot_thm  =
   case Quotient_Term.get_rel_from_quot_thm quot_thm of
      Const (@{const_name HOL.eq}, _) => true
      | Const (@{const_name Lifting.invariant}, _) $ _  => true
      | _ => false

fun define_abs_type quot_thm lthy =
  if can_generate_code_cert quot_thm then
    let
      val abs_type_thm = quot_thm RS @{thm Quotient3_abs_rep}
      val add_abstype_attribute = 
          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
    in
      lthy
        |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
    end
  else
    lthy

infix 0 MRSL

fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm

fun define_cr_rel equiv_thm abs_fun lthy =
  let
    fun force_type_of_rel rel forced_ty =
      let
        val thy = Proof_Context.theory_of lthy
        val rel_ty = (domain_type o fastype_of) rel
        val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
      in
        Envir.subst_term_types ty_inst rel
      end
  
    val (rty, qty) = (dest_funT o fastype_of) abs_fun
    val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
    val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
      Const (@{const_name equivp}, _) $ _ => abs_fun_graph
      | Const (@{const_name part_equivp}, _) $ rel => 
        HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
      | _ => error "unsupported equivalence theorem"
      )
    val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
    val qty_name = (fst o dest_Type) qty
    val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)  
    val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
    val ((_, (_ , def_thm)), lthy'') =
      Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
  in
    (def_thm, lthy'')
  end;

fun setup_lifting_package quot3_thm equiv_thm lthy =
  let
    val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
    val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
    val quot_thm = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
      Const (@{const_name equivp}, _) $ _ => 
        [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}
      | Const (@{const_name part_equivp}, _) $ _ => 
        [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient}
      | _ => error "unsupported equivalence theorem"
      )
  in
    Lifting_Setup.setup_lifting_infr quot_thm equiv_thm lthy'
  end

fun init_quotient_infr quot_thm equiv_thm lthy =
  let
    val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
    val (qtyp, rtyp) = (dest_funT o fastype_of) rep
    val qty_full_name = (fst o dest_Type) qtyp
    val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm, 
      quot_thm = quot_thm }
    fun quot_info phi = Quotient_Info.transform_quotients phi quotients<commit_msg>note the Quotient theorem in quotient_type<commit_after>(*  Title:      HOL/Tools/Quotient/quotient_type.ML
    Author:     <NAME> and <NAME>

Definition of a quotient type.
*)

signature QUOTIENT_TYPE =
sig
  val can_generate_code_cert: thm -> bool
  
  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
    ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory

  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
    ((binding * binding) option)) list -> Proof.context -> Proof.state

  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
    (binding * binding) option) list -> Proof.context -> Proof.state
end;

structure Quotient_Type: QUOTIENT_TYPE =
struct


(*** definition of quotient types ***)

val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}

(* constructs the term {c. EX (x::rty). rel x x \<and> c = Collect (rel x)} *)
fun typedef_term rel rty lthy =
  let
    val [x, c] =
      [("x", rty), ("c", HOLogic.mk_setT rty)]
      |> Variable.variant_frees lthy [rel]
      |> map Free
  in
    HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $
        lambda x (HOLogic.mk_conj (rel $ x $ x,
        HOLogic.mk_eq (c, HOLogic.Collect_const rty $ (rel $ x))))))
  end


(* makes the new type definitions and proves non-emptyness *)
fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
  let
    val typedef_tac =
      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
  in
    Typedef.add_typedef false NONE (qty_name, map (rpair dummyS) vs, mx)
      (typedef_term rel rty lthy) NONE typedef_tac lthy
  end


(* tactic to prove 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 RS mem_def1
    val rep_inv = #Rep_inverse typedef_info
    val abs_inv = #Abs_inverse typedef_info
    val rep_inj = #Rep_inject typedef_info
  in
    (rtac @{thm quot_type.intro} THEN' RANGE [
      rtac equiv_thm,
      rtac rep_thm,
      rtac rep_inv,
      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
      rtac rep_inj]) 1
  end

(* proves the quot_type theorem for the new type *)
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
  let
    val quot_type_const = Const (@{const_name "quot_type"},
      fastype_of rel --> fastype_of abs --> fastype_of rep --> @{typ bool})
    val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
  in
    Goal.prove lthy [] [] goal
      (K (typedef_quot_type_tac equiv_thm typedef_info))
  end
   
fun can_generate_code_cert quot_thm  =
   case Quotient_Term.get_rel_from_quot_thm quot_thm of
      Const (@{const_name HOL.eq}, _) => true
      | Const (@{const_name Lifting.invariant}, _) $ _  => true
      | _ => false

fun define_abs_type quot_thm lthy =
  if can_generate_code_cert quot_thm then
    let
      val abs_type_thm = quot_thm RS @{thm Quotient3_abs_rep}
      val add_abstype_attribute = 
          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
    in
      lthy
        |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
    end
  else
    lthy

infix 0 MRSL

fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm

fun define_cr_rel equiv_thm abs_fun lthy =
  let
    fun force_type_of_rel rel forced_ty =
      let
        val thy = Proof_Context.theory_of lthy
        val rel_ty = (domain_type o fastype_of) rel
        val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
      in
        Envir.subst_term_types ty_inst rel
      end
  
    val (rty, qty) = (dest_funT o fastype_of) abs_fun
    val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
    val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
      Const (@{const_name equivp}, _) $ _ => abs_fun_graph
      | Const (@{const_name part_equivp}, _) $ rel => 
        HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
      | _ => error "unsupported equivalence theorem"
      )
    val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
    val qty_name = (fst o dest_Type) qty
    val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)  
    val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
    val ((_, (_ , def_thm)), lthy'') =
      Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
  in
    (def_thm, lthy'')
  end;

fun setup_lifting_package quot3_thm equiv_thm lthy =
  let
    val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
    val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
    val (rty, qty) = (dest_funT o fastype_of) abs_fun
    val qty_name = (fst o dest_Type) qty
    val quotient_thm_name = Binding.prefix_name "Quotient_" (Binding.qualified_name qty_name) 
    val quot_thm = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
      Const (@{const_name equivp}, _) $ _ => 
        [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}
      | Const (@{const_name part_equivp}, _) $ _ => 
        [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient}
      | _ => error "unsupported equivalence theorem"
      )
  in
    lthy'
      |> Lifting_Setup.setup_lifting_infr quot_thm equiv_thm
      |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
  end

fun init_quotient_infr quot_thm equiv_thm lthy =
  let
    val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
    val (qtyp, rtyp) = (dest_funT o fastype_of) rep
    val qty_full_name = (fst o dest_Type) qtyp
    val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm, 
      quot_thm = quot_thm }
    fun quot_info phi = Quotient_Info.transform_quotients phi quotients
{'fraction_non_alphanumeric': 0.10436607892527287, 'fraction_numerical': 0.003022670025188917, 'mean_word_length': 3.2630637079455975, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 65, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1444671', 'n_tokens_mistral': 4551, 'n_tokens_neox': 4394, 'n_words': 1198}