# HG changeset patch # User Christian Urban # Date 1273668228 -3600 # Node ID 409ecb7284dd44b8a82783fdd05a8e0e7b18749e # Parent e25b0fff0dd2767138f8f051dce3e284163b0e6d properly exported defined bn-functions diff -r e25b0fff0dd2 -r 409ecb7284dd Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue May 11 18:20:25 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Wed May 12 13:43:48 2010 +0100 @@ -16,6 +16,7 @@ where "bn (As x t) = {atom x}" + thm trm_assg.fv thm trm_assg.supp thm trm_assg.eq_iff diff -r e25b0fff0dd2 -r 409ecb7284dd Nominal/NewParser.thy --- a/Nominal/NewParser.thy Tue May 11 18:20:25 2010 +0200 +++ b/Nominal/NewParser.thy Wed May 12 13:43:48 2010 +0100 @@ -65,6 +65,7 @@ map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs *} + ML {* fun add_primrec_wrapper funs eqs lthy = if null funs then (([], []), lthy) @@ -72,8 +73,10 @@ let val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs + val ((funs'', eqs''), lthy') = Primrec.add_primrec funs' eqs' lthy + val phi = ProofContext.export_morphism lthy' lthy in - Primrec.add_primrec funs' eqs' lthy + ((map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs''), lthy') end *} @@ -218,7 +221,6 @@ end *} - ML {* fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = let @@ -361,10 +363,15 @@ fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = let (* definition of the raw datatype and raw bn-functions *) - val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = + val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) = if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy else raise TEST lthy + val _ = tracing ("raw_bn_eqs\n" ^ cat_lines (map (@{make_string} o prop_of) raw_bn_eqs)) + + val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) + val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) + val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); val {descr, sorts, ...} = dtinfo; val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; @@ -373,11 +380,6 @@ val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; - (* what is the difference between raw_dt_names and all_full_tnames ? *) - (* what is the purpose of dtinfo and dtinfos ? *) - val _ = tracing ("raw_dt_names " ^ commas raw_dt_names) - val _ = tracing ("all_full_tnames " ^ commas all_full_tnames) - val inject_thms = flat (map #inject dtinfos); val distinct_thms = flat (map #distinct dtinfos); val rel_dtinfos = List.take (dtinfos, (length dts)); @@ -390,11 +392,11 @@ if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 else raise TEST lthy1 + (* definition of raw fv_functions *) val morphism_2_0 = ProofContext.export_morphism lthy2 lthy fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); - val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc val (_, lthy2a) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; @@ -404,9 +406,12 @@ val lthy3 = Theory_Target.init NONE thy; val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; - (* definition of raw fv_functions *) + (* + val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) + val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns_exp) + val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) - val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls) + *) val ((fv, fvbn), fv_def, lthy3a) = if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 else raise TEST lthy3 diff -r e25b0fff0dd2 -r 409ecb7284dd Nominal/Perm.thy --- a/Nominal/Perm.thy Tue May 11 18:20:25 2010 +0200 +++ b/Nominal/Perm.thy Wed May 12 13:43:48 2010 +0100 @@ -62,6 +62,7 @@ *} ML {* +(* proves the two pt-type class properties *) fun prove_permute_zero lthy induct perm_defs perm_fns = let val perm_types = map (body_type o fastype_of) perm_fns diff -r e25b0fff0dd2 -r 409ecb7284dd Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Tue May 11 18:20:25 2010 +0200 +++ b/Pearl-jv/Paper.thy Wed May 12 13:43:48 2010 +0100 @@ -55,10 +55,16 @@ there are bound term variables and bound type variables; each kind needs to be represented by a different sort of atoms. - Unfortunately, the type system of Isabelle/HOL is not a good fit for the way - atoms and sorts are used in the original formulation of the nominal logic work. - The reason is that one has to ensure that permutations are sort-respecting. - This was done implicitly in the original nominal logic work \cite{Pitts03}. + In our formalisation of the nominal logic work, we have to make a design decision + about how to represent sorted atoms and sort-respecting permutations. One possibility + is to + + + +% Unfortunately, the type system of Isabelle/HOL is not a good fit for the way +% atoms and sorts are used in the original formulation of the nominal logic work. +% The reason is that one has to ensure that permutations are sort-respecting. +% This was done implicitly in the original nominal logic work \cite{Pitts03}. Isabelle used the two-place permutation operation with the generic type