src/HOL/Tools/Quotient/quotient_type.ML
author kuncar
Mon, 16 Jan 2012 12:33:26 +0100
changeset 47100 f8f788c8b7f3
parent 47096 3ea48c19673e
child 47308 9caab698dbe4
permissions -rw-r--r--
updated comment
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45680
a61510361b89 more conventional file name;
wenzelm
parents: 45676
diff changeset
     1
(*  Title:      HOL/Tools/Quotient/quotient_type.ML
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
    Author:     Cezary Kaliszyk and Christian Urban
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
35806
a814cccce0b8 rollback of local typedef until problem with type-variables can be sorted out; fixed header
Christian Urban <urbanc@in.tum.de>
parents: 35790
diff changeset
     4
Definition of a quotient type.
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
signature QUOTIENT_TYPE =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
sig
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
     9
  val can_generate_code_cert: thm -> bool
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    10
  
45676
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
    11
  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
    12
    ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
35415
1810b1ade437 export add_quotient_type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35351
diff changeset
    13
45676
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
    14
  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
    15
    ((binding * binding) option)) list -> Proof.context -> Proof.state
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
45676
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
    17
  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
    18
    (binding * binding) option) list -> Proof.context -> Proof.state
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
end;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
structure Quotient_Type: QUOTIENT_TYPE =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    22
struct
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    25
(*** definition of quotient types ***)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 43547
diff changeset
    27
val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 43547
diff changeset
    28
val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
47100
f8f788c8b7f3 updated comment
kuncar
parents: 47096
diff changeset
    30
(* constructs the term {c. EX (x::rty). rel x x \<and> c = Collect (rel x)} *)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
fun typedef_term rel rty lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    32
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    33
    val [x, c] =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    34
      [("x", rty), ("c", HOLogic.mk_setT rty)]
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    35
      |> Variable.variant_frees lthy [rel]
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    36
      |> map Free
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    37
  in
45312
bulwahn
parents: 45291
diff changeset
    38
    HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 43547
diff changeset
    39
        lambda x (HOLogic.mk_conj (rel $ x $ x,
45312
bulwahn
parents: 45291
diff changeset
    40
        HOLogic.mk_eq (c, HOLogic.Collect_const rty $ (rel $ x))))))
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    41
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    44
(* makes the new type definitions and proves non-emptyness *)
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
    45
fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    46
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    47
    val typedef_tac =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    48
      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    49
  in
46727
0162a0d284ac Finish localizing the quotient package.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 45835
diff changeset
    50
    Typedef.add_typedef false NONE (qty_name, map (rpair dummyS) vs, mx)
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    51
      (typedef_term rel rty lthy) NONE typedef_tac lthy
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    52
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    53
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    54
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    55
(* tactic to prove the quot_type theorem for the new type *)
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35842
diff changeset
    56
fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    57
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    58
    val rep_thm = #Rep typedef_info RS mem_def1
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    59
    val rep_inv = #Rep_inverse typedef_info
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    60
    val abs_inv = #Abs_inverse typedef_info
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    61
    val rep_inj = #Rep_inject typedef_info
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    62
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    63
    (rtac @{thm quot_type.intro} THEN' RANGE [
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    64
      rtac equiv_thm,
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    65
      rtac rep_thm,
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    66
      rtac rep_inv,
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    67
      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    68
      rtac rep_inj]) 1
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    69
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
(* proves the quot_type theorem for the new type *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    73
  let
45317
bf8b9ac6000c more robust, declarative and unsurprising computation of types in the quotient type definition
bulwahn
parents: 45314
diff changeset
    74
    val quot_type_const = Const (@{const_name "quot_type"},
bf8b9ac6000c more robust, declarative and unsurprising computation of types in the quotient type definition
bulwahn
parents: 45314
diff changeset
    75
      fastype_of rel --> fastype_of abs --> fastype_of rep --> @{typ bool})
bf8b9ac6000c more robust, declarative and unsurprising computation of types in the quotient type definition
bulwahn
parents: 45314
diff changeset
    76
    val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    77
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    78
    Goal.prove lthy [] [] goal
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    79
      (K (typedef_quot_type_tac equiv_thm typedef_info))
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    80
  end
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    81
   
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    82
fun can_generate_code_cert quot_thm  =
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    83
   case Quotient_Term.get_rel_from_quot_thm quot_thm of
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    84
      Const (@{const_name HOL.eq}, _) => true
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    85
      | Const (@{const_name invariant}, _) $ _  => true
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    86
      | _ => false
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    87
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    88
fun define_abs_type quot_thm lthy =
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    89
  if can_generate_code_cert quot_thm then
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    90
    let
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    91
      val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    92
      val add_abstype_attribute = 
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    93
          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    94
        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    95
    in
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    96
      lthy
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    97
        |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    98
    end
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
    99
  else
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   100
    lthy
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   101
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   102
fun init_quotient_infr quot_thm equiv_thm lthy =
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   103
  let
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   104
    val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   105
    val (qtyp, rtyp) = (dest_funT o fastype_of) rep
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   106
    val qty_full_name = (fst o dest_Type) qtyp
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   107
    val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm, 
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   108
      quot_thm = quot_thm }
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   109
    fun quot_info phi = Quotient_Info.transform_quotients phi quotients
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   110
    val abs_rep = {abs = abs, rep = rep}
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   111
    fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   112
  in
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   113
    lthy
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   114
      |> Local_Theory.declaration {syntax = false, pervasive = true}
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   115
        (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   116
          #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   117
      |> define_abs_type quot_thm
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   118
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   119
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   120
(* main function for constructing a quotient type *)
45676
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
   121
fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   122
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   123
    val part_equiv =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   124
      if partial
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   125
      then equiv_thm
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   126
      else equiv_thm RS @{thm equivp_implies_part_equivp}
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   127
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   128
    (* generates the typedef *)
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   129
    val ((_, typedef_info), lthy1) =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   130
      typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   131
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   132
    (* abs and rep functions from the typedef *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   133
    val Abs_ty = #abs_type (#1 typedef_info)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   134
    val Rep_ty = #rep_type (#1 typedef_info)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   135
    val Abs_name = #Abs_name (#1 typedef_info)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   136
    val Rep_name = #Rep_name (#1 typedef_info)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   137
    val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   138
    val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   139
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   140
    (* more useful abs and rep definitions *)
45317
bf8b9ac6000c more robust, declarative and unsurprising computation of types in the quotient type definition
bulwahn
parents: 45314
diff changeset
   141
    val abs_const = Const (@{const_name quot_type.abs},
bf8b9ac6000c more robust, declarative and unsurprising computation of types in the quotient type definition
bulwahn
parents: 45314
diff changeset
   142
      (rty --> rty --> @{typ bool}) --> (Rep_ty --> Abs_ty) --> rty --> Abs_ty)
bf8b9ac6000c more robust, declarative and unsurprising computation of types in the quotient type definition
bulwahn
parents: 45314
diff changeset
   143
    val rep_const = Const (@{const_name quot_type.rep}, (Abs_ty --> Rep_ty) --> Abs_ty --> rty)
bf8b9ac6000c more robust, declarative and unsurprising computation of types in the quotient type definition
bulwahn
parents: 45314
diff changeset
   144
    val abs_trm = abs_const $ rel $ Abs_const
bf8b9ac6000c more robust, declarative and unsurprising computation of types in the quotient type definition
bulwahn
parents: 45314
diff changeset
   145
    val rep_trm = rep_const $ Rep_const
45676
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
   146
    val (rep_name, abs_name) =
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
   147
      (case opt_morphs of
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
   148
        NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
   149
      | SOME morphs => morphs)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   150
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   151
    val ((_, (_, abs_def)), lthy2) = lthy1
46909
3c73a121a387 more explicit indication of def names;
wenzelm
parents: 46727
diff changeset
   152
      |> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm))
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   153
    val ((_, (_, rep_def)), lthy3) = lthy2
46909
3c73a121a387 more explicit indication of def names;
wenzelm
parents: 46727
diff changeset
   154
      |> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm))
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   155
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   156
    (* quot_type theorem *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   157
    val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   158
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   159
    (* quotient theorem *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   160
    val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   161
    val quotient_thm =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   162
      (quot_thm RS @{thm quot_type.Quotient})
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   163
      |> fold_rule [abs_def, rep_def]
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   164
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   165
    (* name equivalence theorem *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   166
    val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   167
45279
89a17197cb98 simplified/standardized signatures;
wenzelm
parents: 45278
diff changeset
   168
    (* storing the quotients *)
47093
0516a6c1ea59 store the quotient theorem for every quotient
kuncar
parents: 47091
diff changeset
   169
    val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm, 
0516a6c1ea59 store the quotient theorem for every quotient
kuncar
parents: 47091
diff changeset
   170
      quot_thm = quotient_thm}
37530
70d03844b2f9 export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37493
diff changeset
   171
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   172
    val lthy4 = lthy3
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   173
      |> init_quotient_infr quotient_thm equiv_thm
45282
eaec1651709a eliminated aliases of standard functions;
wenzelm
parents: 45280
diff changeset
   174
      |> (snd oo Local_Theory.note)
eaec1651709a eliminated aliases of standard functions;
wenzelm
parents: 45280
diff changeset
   175
        ((equiv_thm_name,
eaec1651709a eliminated aliases of standard functions;
wenzelm
parents: 45280
diff changeset
   176
          if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
eaec1651709a eliminated aliases of standard functions;
wenzelm
parents: 45280
diff changeset
   177
          [equiv_thm])
eaec1651709a eliminated aliases of standard functions;
wenzelm
parents: 45280
diff changeset
   178
      |> (snd oo Local_Theory.note)
eaec1651709a eliminated aliases of standard functions;
wenzelm
parents: 45280
diff changeset
   179
        ((quotient_thm_name, [Attrib.internal (K Quotient_Info.quotient_rules_add)]),
eaec1651709a eliminated aliases of standard functions;
wenzelm
parents: 45280
diff changeset
   180
          [quotient_thm])
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   181
  in
45279
89a17197cb98 simplified/standardized signatures;
wenzelm
parents: 45278
diff changeset
   182
    (quotients, lthy4)
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   183
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   184
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   185
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   186
(* sanity checks for the quotient type specifications *)
45676
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
   187
fun sanity_check ((vs, qty_name, _), (rty, rel, _), _) =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   188
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   189
    val rty_tfreesT = map fst (Term.add_tfreesT rty [])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   190
    val rel_tfrees = map fst (Term.add_tfrees rel [])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   191
    val rel_frees = map fst (Term.add_frees rel [])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   192
    val rel_vars = Term.add_vars rel []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   193
    val rel_tvars = Term.add_tvars rel []
43547
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 42361
diff changeset
   194
    val qty_str = Binding.print qty_name ^ ": "
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   195
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   196
    val illegal_rel_vars =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   197
      if null rel_vars andalso null rel_tvars then []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   198
      else [qty_str ^ "illegal schematic variable(s) in the relation."]
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   199
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   200
    val dup_vs =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   201
      (case duplicates (op =) vs of
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   202
        [] => []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   203
      | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   204
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   205
    val extra_rty_tfrees =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   206
      (case subtract (op =) vs rty_tfreesT of
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   207
        [] => []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   208
      | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   209
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   210
    val extra_rel_tfrees =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   211
      (case subtract (op =) vs rel_tfrees of
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   212
        [] => []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   213
      | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   214
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   215
    val illegal_rel_frees =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   216
      (case rel_frees of
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   217
        [] => []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   218
      | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   219
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   220
    val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   221
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   222
    if null errs then () else error (cat_lines errs)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   223
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   224
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   225
(* check for existence of map functions *)
45795
2d8949268303 maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents: 45698
diff changeset
   226
fun map_check ctxt (_, (rty, _, _), _) =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   227
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   228
    fun map_check_aux rty warns =
45280
9fd6fce8a230 localized quotient data;
wenzelm
parents: 45279
diff changeset
   229
      (case rty of
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   230
        Type (_, []) => warns
45340
98ec8b51af9c prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents: 45317
diff changeset
   231
      | Type (s, _) =>
45795
2d8949268303 maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents: 45698
diff changeset
   232
          if Symtab.defined (Enriched_Type.entries ctxt) s then warns else s :: warns
45280
9fd6fce8a230 localized quotient data;
wenzelm
parents: 45279
diff changeset
   233
      | _ => warns)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   234
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   235
    val warns = map_check_aux rty []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   236
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   237
    if null warns then ()
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   238
    else warning ("No map function defined for " ^ commas warns ^
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   239
      ". This will cause problems later on.")
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   240
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   241
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   242
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   243
(*** interface and syntax setup ***)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   244
45698
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   245
(* the ML-interface takes a list of tuples consisting of:
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   246
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   247
 - the name of the quotient type
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   248
 - its free type variables (first argument)
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   249
 - its mixfix annotation
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   250
 - the type to be quotient
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   251
 - the partial flag (a boolean)
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   252
 - the relation according to which the type is quotient
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   253
 - optional names of morphisms (rep/abs)
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   254
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   255
 it opens a proof-state in which one has to show that the
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   256
 relations are equivalence relations
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   257
*)
fd8e140ae879 removed outdated comment moved back and updated (at the direct request of Christian Urban)
kuncar
parents: 45690
diff changeset
   258
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   259
fun quotient_type quot_list lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   260
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   261
    (* sanity check *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   262
    val _ = List.app sanity_check quot_list
45795
2d8949268303 maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents: 45698
diff changeset
   263
    val _ = List.app (map_check lthy) quot_list
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   264
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   265
    fun mk_goal (rty, rel, partial) =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   266
      let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   267
        val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   268
        val const =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   269
          if partial then @{const_name part_equivp} else @{const_name equivp}
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   270
      in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   271
        HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   272
      end
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   273
45676
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
   274
    val goals = map (mk_goal o #2) quot_list
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   275
45282
eaec1651709a eliminated aliases of standard functions;
wenzelm
parents: 45280
diff changeset
   276
    fun after_qed [thms] = fold (snd oo add_quotient_type) (quot_list ~~ thms)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   277
  in
45282
eaec1651709a eliminated aliases of standard functions;
wenzelm
parents: 45280
diff changeset
   278
    Proof.theorem NONE after_qed [map (rpair []) goals] lthy
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   279
  end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   280
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   281
fun quotient_type_cmd specs lthy =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   282
  let
45676
fa46fef06590 alternative names of morphisms in the definition of a quotient type can be specified
kuncar
parents: 45534
diff changeset
   283
    fun parse_spec (((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   284
      let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   285
        val rty = Syntax.read_typ lthy rty_str
46727
0162a0d284ac Finish localizing the quotient package.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 45835
diff changeset
   286
        val tmp_lthy1 = Variable.declare_typ rty lthy
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   287
        val rel =
46727
0162a0d284ac Finish localizing the quotient package.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 45835
diff changeset
   288
          Syntax.parse_term tmp_lthy1 rel_str
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   289
          |> Type.constraint (rty --> rty --> @{typ bool})
46727
0162a0d284ac Finish localizing the quotient package.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 45835
diff changeset
   290
          |> Syntax.check_term tmp_lthy1
0162a0d284ac Finish localizing the quotient package.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 45835
diff changeset
   291
        val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   292
      in
46727
0162a0d284ac Finish localizing the quotient package.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 45835
diff changeset
   293
        (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), tmp_lthy2)
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   294
      end
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   295
46727
0162a0d284ac Finish localizing the quotient package.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 45835
diff changeset
   296
    val (spec', _) = fold_map parse_spec specs lthy
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   297
  in
46727
0162a0d284ac Finish localizing the quotient package.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 45835
diff changeset
   298
    quotient_type spec' lthy
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   299
  end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   300
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46947
diff changeset
   301
val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   302
47091
d5cd13aca90b respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents: 46961
diff changeset
   303
val quotspec_parser =
d5cd13aca90b respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents: 46961
diff changeset
   304
  Parse.and_list1
d5cd13aca90b respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents: 46961
diff changeset
   305
    ((Parse.type_args -- Parse.binding) --
d5cd13aca90b respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents: 46961
diff changeset
   306
      (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
d5cd13aca90b respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents: 46961
diff changeset
   307
      Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
d5cd13aca90b respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents: 46961
diff changeset
   308
        (@{keyword "/"} |-- (partial -- Parse.term))  --
d5cd13aca90b respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents: 46961
diff changeset
   309
        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
d5cd13aca90b respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents: 46961
diff changeset
   310
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   311
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   312
  Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   313
    "quotient type definitions (require equivalence proofs)"
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   314
      (quotspec_parser >> quotient_type_cmd)
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   315
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   316
(* Setup lifting using type_def_thm *)
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   317
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   318
exception SETUP_LIFT_TYPE of string
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   319
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   320
fun setup_lift_type typedef_thm =
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   321
  let
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   322
    val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   323
    val (quot_thm, equivp_thm) = (case typedef_set of
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   324
      Const ("Orderings.top_class.top", _) => 
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   325
        (typedef_thm RS @{thm copy_type_to_Quotient}, 
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   326
         typedef_thm RS @{thm copy_type_to_equivp})
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   327
      | Const (@{const_name "Collect"}, _) $ Abs (_, _, _ $ Bound 0) => 
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   328
        (typedef_thm RS @{thm invariant_type_to_Quotient}, 
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   329
         typedef_thm RS @{thm invariant_type_to_part_equivp})
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   330
      | _ => raise SETUP_LIFT_TYPE "unsupported typedef theorem")
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   331
  in
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   332
    init_quotient_infr quot_thm equivp_thm
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   333
  end
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   334
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   335
fun setup_lift_type_aux xthm lthy = setup_lift_type (singleton (Attrib.eval_thms lthy) xthm) lthy
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   336
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   337
val _ = 
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   338
  Outer_Syntax.local_theory @{command_spec "setup_lifting"}
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   339
    "Setup lifting infrastracture" 
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47093
diff changeset
   340
      (Parse_Spec.xthm >> (fn xthm => setup_lift_type_aux xthm))
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   341
45280
9fd6fce8a230 localized quotient data;
wenzelm
parents: 45279
diff changeset
   342
end;