Re: [isabelle] Instantiating type variables within a modified definition declaration.

I think that I sent an empty theory file. Here I send it

Best regards,

Viorel Preoteasa

onstruct, that in addition to creating the definition,
would also insatiate all type variables to a given type
(bool for simplicity)

For example the declaration:

  mydef "TestDefA a = (a = a)"

will create the theorem TestDefA_def:

  "TestDefA (a::bool) = (a = a)"

I am trying to do this in the following way:

 - generalize the type variables using Thm.generalize
 - Drule.instantiate_normalize to instantiate the schematic type to bool

This works on a theorem that has been generated with
Simplifier.rewrite, but it does not work when I try to
apply it to the theorem within the code for creating the
definition, just before  Local_Theory.notes.
When I try to generalize the type variables I get the error:

exception THM 0 raised (line 1127 of "thm.ML"):
  generalize: variable free in assumptions
  TestDefA ?a = (?a = ?a)  [TestDefA â ??.TestDef.TestDefA]

While writing this I realized, that it is not enough
just to change the theorem of the definition to work
on bool, but I also need to change the constant to
work on bool only.

Attached is the theory where I try to define this
new type of definition.

Any help would be appreciated.

Best regards,

Viorel Preoteasa
theory TestDef imports Main
keywords "mydef" :: thy_decl

definition "TestDefB a = (a = a)"

  val th_A = Simplifier.rewrite (@{context} addsimps [ at {thm TestDefB_def}]) @{cterm "TestDef u"}
  val tfrees = Term.add_tfrees (Thm.prop_of th_A)  [];
  val th_A_gen = Thm.generalize (map fst tfrees, [])  ((Thm.maxidx_of th_A) + 1) th_A;
  val tvars = Term.add_tvars (Thm.prop_of th_A_gen) [];
  val th_A_inst = Drule.instantiate_normalize (map (fn x => (x, @{ctyp bool})) tvars,[]) th_A_gen;

fun gen_def prep (raw_var, raw_spec) int lthy =
    val ((vars, [((raw_name, atts), prop)]), get_pos) =
      fst (prep (the_list raw_var) [raw_spec] lthy);
    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
    val _ = Name.reject_internal (x, []);
    val var as (b, _) =
      (case vars of
        [] => (Binding.make (x, get_pos x), NoSyn)
      | [((b, _), mx)] =>
            val y = Variable.check_name b;
            val _ = x = y orelse
              error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
       (Binding.pos_of b));
          in (b, mx) end);
    val name = Binding.reset_pos (Thm.def_binding_optional b raw_name);
    val ((lhs, (_, raw_th)), lthy2) = lthy
      |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));

    val th = prove lthy2 raw_th;
    val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);

        val th_a =  th;
        val tfrees = Term.add_tfrees (Thm.prop_of th_a)  [];
        val th_gen = Thm.generalize (map fst tfrees, []) ((Thm.maxidx_of th_a) + 1) th_a;

    val ([(def_name, [th'])], lthy4) = lthy3
      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];

    val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;

    val _ =
      Proof_Display.print_consts int (Position.thread_data ()) lthy4
        (member (op =) (Term.add_frees lhs' [])) [(x, T)];
  in ((lhs, (def_name, th')), lthy4) end;

val definition_cmd = gen_def  Specification.read_free_spec;

val _ =
  Outer_Syntax.local_theory' @{command_keyword mydef} "constant mydef"
    (Parse_Spec.constdef >> (fn args => #2 oo definition_cmd args));


mydef "TestDefA a = (a = a)"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.