<commit_before>(*  Title:      quotient_typ.thy
    Author:     <NAME> and <NAME>

    Definition of a quotient type.

*)

signature QUOTIENT_TYPE =
sig
  val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm
    -> Proof.context -> (thm * thm) * local_theory

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

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

structure Quotient_Type: QUOTIENT_TYPE =
struct

open Quotient_Info;

(* wrappers for define, note, Attrib.internal and theorem_i *)
fun define (name, mx, rhs) lthy =
let
  val ((rhs, (_ , thm)), lthy') =
     Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
in
  ((rhs, thm), lthy')
end

fun note (name, thm, attrs) lthy =
let
  val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
in
  (thm', lthy')
end

fun intern_attr at = Attrib.internal (K at)

fun theorem after_qed goals ctxt =
let
  val goals' = map (rpair []) goals
  fun after_qed' thms = after_qed (the_single thms)
in
  Proof.theorem_i NONE after_qed' [goals'] ctxt
end



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

val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)}
val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)}

(* constructs the term lambda (c::rty => bool). EX (x::rty). c = 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
  lambda c (HOLogic.exists_const rty $
     lambda x (HOLogic.mk_eq (c, (rel $ x))))
end


(* makes the new type definitions and proves non-emptyness *)
fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
let
  val typedef_tac =
    EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
in
  Typedef.add_typedef false NONE (qty_name, 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 = mem_def2 RS #Abs_inverse typedef_info<commit_msg>rollback of local typedef until problem with type-variables can be sorted out; fixed header<commit_after>(*  Title:      HOL/Tools/Quotient/quotient_typ.thy
    Author:     <NAME> and <NAME>

Definition of a quotient type.

*)

signature QUOTIENT_TYPE =
sig
  val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm
    -> Proof.context -> (thm * thm) * local_theory

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

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

structure Quotient_Type: QUOTIENT_TYPE =
struct

open Quotient_Info;

(* wrappers for define, note, Attrib.internal and theorem_i *)
fun define (name, mx, rhs) lthy =
let
  val ((rhs, (_ , thm)), lthy') =
     Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
in
  ((rhs, thm), lthy')
end

fun note (name, thm, attrs) lthy =
let
  val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
in
  (thm', lthy')
end

fun intern_attr at = Attrib.internal (K at)

fun theorem after_qed goals ctxt =
let
  val goals' = map (rpair []) goals
  fun after_qed' thms = after_qed (the_single thms)
in
  Proof.theorem_i NONE after_qed' [goals'] ctxt
end



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

val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)}
val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)}

(* constructs the term lambda (c::rty => bool). EX (x::rty). c = 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
  lambda c (HOLogic.exists_const rty $
     lambda x (HOLogic.mk_eq (c, (rel $ x))))
end


(* makes the new type definitions and proves non-emptyness *)
fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
let
  val typedef_tac =
    EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
in
(* FIXME: purely local typedef causes at the moment 
   problems with type variables
  
  Typedef.add_typedef false NONE (qty_name, vs, mx) 
    (typedef_term rel rty lthy) NONE typedef_tac lthy
*)
   Local_Theory.theory_result
     (Typedef.add_typedef_global false NONE
       (qty_name, 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 = mem_def2 RS #Abs_inverse typedef_info
{'fraction_non_alphanumeric': 0.12875882946518669, 'fraction_numerical': 0.0024217961654894047, 'mean_word_length': 3.6843100189035916, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 29, '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': '3001526', 'n_tokens_mistral': 1886, 'n_tokens_neox': 1830, 'n_words': 596}