*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Instantiating type variables within a modified definition declaration.*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Thu, 10 Nov 2016 12:38:48 +0200*In-reply-to*: <78fc2283-03d4-355e-dc91-01d6b01f3ff5@aalto.fi>*References*: <CAK0o7cbmHp4Mt-tC_Os0r7GNVrDPv1EkhzLXtG9J_k-sYCX1kw@mail.gmail.com> <69c41820-2071-8792-6ad4-6468578cb92e@inf.ethz.ch> <78fc2283-03d4-355e-dc91-01d6b01f3ff5@aalto.fi>*User-agent*: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

I think that I sent an empty theory file. Here I send it again. 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 begin definition "TestDefB a = (a = a)" ML{* 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; *} ML{* fun gen_def prep (raw_var, raw_spec) int lthy = let 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)] => let val y = Variable.check_name b; val _ = x = y orelse error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ Position.here (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)" end

**Follow-Ups**:**Re: [isabelle] Instantiating type variables within a modified definition declaration.***From:*Viorel Preoteasa

**References**:**[isabelle] Turning on tracing for mode inference?***From:*Mark Wassell

**Re: [isabelle] Turning on tracing for mode inference?***From:*Andreas Lochbihler

**[isabelle] Instantiating type variables within a modified definition declaration.***From:*Viorel Preoteasa

- Previous by Date: [isabelle] Instantiating type variables within a modified definition declaration.
- Next by Date: Re: [isabelle] Isabelle2016-1-RC1 processing theories twice
- Previous by Thread: [isabelle] Instantiating type variables within a modified definition declaration.
- Next by Thread: Re: [isabelle] Instantiating type variables within a modified definition declaration.
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list