1 (*notation ( output) "prop" ("#_" [1000] 1000) *)

     2 notation ( output) "Trueprop" ("#_" [1000] 1000)

     3 

     4 syntax

     5   "Bex1_rel" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)

     6 translations

     7   "\<exists>!!x\<in>A. P"  == "Bex1_rel A (%x. P)"

     8 

     9 (*interpretation code *)

    10 (*val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))

    11   val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;

    12   val eqn1i = Thm.prop_of (symmetric eqn1pre)

    13   val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;

    14   val eqn2i = Thm.prop_of (symmetric eqn2pre)

    15 

    16   val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));

    17   val exp_term = Morphism.term exp_morphism;

    18   val exp = Morphism.thm exp_morphism;

    19 

    20   val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN

    21     ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))

    22   val mthdt = Method.Basic (fn _ => mthd)

    23   val bymt = Proof.global_terminal_proof (mthdt, NONE)

    24   val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),

    25     Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]*)

    26 

    27 (*||> Local_Theory.theory (fn thy =>

    28       let

    29         val global_eqns = map exp_term [eqn2i, eqn1i];

    30         (* Not sure if the following context should not be used *)

    31         val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;

    32         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;

    33       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*)