# HG changeset patch # User Cezary Kaliszyk # Date 1268148279 -3600 # Node ID aa787c9b6955ae54e224b344e324ea0e07d450f2 # Parent d39ca37e526af0d02c341f728268dfc7091eac23 A version of Fv that takes into account recursive and non-recursive bindings. diff -r d39ca37e526a -r aa787c9b6955 Nominal/Fv.thy --- a/Nominal/Fv.thy Tue Mar 09 11:36:40 2010 +0100 +++ b/Nominal/Fv.thy Tue Mar 09 16:24:39 2010 +0100 @@ -77,7 +77,8 @@ *} (* Finds bindings with the same function and binding, and gathers all - bodys for such pairs *) + bodys for such pairs + *) ML {* fun gather_binds binds = let @@ -143,9 +144,58 @@ ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \ perm \ perm"}) $ p1 $ p2 *} +ML {* +fun non_rec_binds l = +let + fun is_non_rec (SOME (f, false), _, _) = SOME f + | is_non_rec _ = NONE +in + distinct (op =) (map_filter is_non_rec (flat (flat l))) +end +*} + +(* We assume no bindings in the type on which bn is defined *) +ML {* +fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bn) = +let + val {descr, sorts, ...} = dt_info; + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); + val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp)); + fun fv_bn_constr (cname, dts) = + let + val Ts = map (typ_of_dtyp descr sorts) dts; + val names = Datatype_Prop.make_tnames Ts; + val args = map Free (names ~~ Ts); + val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); + fun fv_arg ((dt, x), arg_no) = + let + val ty = fastype_of x + in + if arg_no mem args_in_bn then + (if is_rec_type dt then + (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: not good") + else @{term "{} :: atom set"}) else + if is_atom thy ty then mk_single_atom x else + if is_atom_set thy ty then mk_atoms x else + if is_rec_type dt then nth fv_frees (body_index dt) $ x else + @{term "{} :: atom set"} + end; + val arg_nos = 0 upto (length dts - 1) + in + HOLogic.mk_Trueprop (HOLogic.mk_eq + (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) + end; + val (_, (_, _, constrs)) = nth descr ith_dtyp; + val eqs = map fv_bn_constr constrs +in + ((bn, fvbn), (fvbn_name, eqs)) +end +*} + (* TODO: Notice datatypes without bindings and replace alpha with equality *) ML {* -fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = +fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = let val thy = ProofContext.theory_of lthy; val {descr, sorts, ...} = dt_info; @@ -154,6 +204,11 @@ "fv_" ^ name_of_typ (nth_dtyp i)) descr); val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; val fv_frees = map Free (fv_names ~~ fv_types); + val nr_bns = non_rec_binds bindsall; + val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; + val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); + val fv_bns = map snd bn_fv_bns; + val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => "alpha_" ^ name_of_typ (nth_dtyp i)) descr); val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; @@ -182,22 +237,30 @@ if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else (* TODO we do not know what to do with non-atomizable things *) @{term "{} :: atom set"} - | fv_bind args (SOME f, i, _) = f $ (nth args i); + | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) + fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE + | find_nonrec_binder _ _ = NONE fun fv_arg ((dt, x), arg_no) = - let - val arg = - if is_rec_type dt then nth fv_frees (body_index dt) $ x else - if ((is_atom thy) o fastype_of) x then mk_single_atom x else - if ((is_atom_set thy) o fastype_of) x then mk_atoms x else - (* TODO we do not know what to do with non-atomizable things *) - @{term "{} :: atom set"} - (* If i = j then we generate it only once *) - val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; - val sub = fv_binds args relevant - in - mk_diff arg sub - end; + case get_first (find_nonrec_binder arg_no) bindcs of + SOME f => + (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of + SOME fv_bn => fv_bn $ x + | NONE => error "bn specified in a non-rec binding but not in bn list") + | NONE => + let + val arg = + if is_rec_type dt then nth fv_frees (body_index dt) $ x else + if ((is_atom thy) o fastype_of) x then mk_single_atom x else + if ((is_atom_set thy) o fastype_of) x then mk_atoms x else + (* TODO we do not know what to do with non-atomizable things *) + @{term "{} :: atom set"} + (* If i = j then we generate it only once *) + val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; + val sub = fv_binds args relevant + in + mk_diff arg sub + end; val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) val alpha_rhs = @@ -240,9 +303,12 @@ end; fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr (gather_binds bindsall))) + val fv_eqs_all = fv_eqs @ (flat fv_bn_eqs); + val fv_names_all = fv_names @ fv_bn_names; val add_binds = map (fn x => (Attrib.empty_binding, x)) +(* Function_Fun.add_fun Function_Common.default_config ... true *) val (fvs, lthy') = (Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) + (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) val (alphas, lthy'') = (Inductive.add_inductive_i {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} @@ -253,18 +319,31 @@ end *} -(* tests +(* atom_decl name -datatype ty = - Var "name set" +datatype lam = + VAR "name" +| APP "lam" "lam" +| LET "bp" "lam" +and bp = + BP "name" "lam" -ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} +primrec + bi::"bp \ atom set" +where + "bi (BP x t) = {atom x}" -local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *} -print_theorems +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} +local_setup {* + snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") + [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [0])] *} +print_theorems +*) + +(* datatype rtrm1 = rVr1 "name" | rAp1 "rtrm1" "rtrm1" diff -r d39ca37e526a -r aa787c9b6955 Nominal/Parser.thy --- a/Nominal/Parser.thy Tue Mar 09 11:36:40 2010 +0100 +++ b/Nominal/Parser.thy Tue Mar 09 16:24:39 2010 +0100 @@ -146,7 +146,7 @@ ML {* fun rawify_binds dts_env cnstrs_env bn_fun_env binds = map (map (map (map (fn (opt_trm, i, j) => - (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env) opt_trm, i, j))))) binds + (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds *} ML {* @@ -232,6 +232,8 @@ val thy_name = Context.theory_name thy val (((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), lthy2) = raw_nominal_decls dts bn_funs bn_eqs binds lthy + val bn_funs_decls = []; + val morphism_2_1 = ProofContext.export_morphism lthy2 lthy val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc @@ -250,7 +252,12 @@ val ((raw_perm_def, raw_perm_simps, perms), lthy3) = Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; val raw_binds_flat = map (map flat) raw_binds; - val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3; + val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; +in +if !restricted_nominal = 0 then + ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) +else +let val alpha_ts_loc = #preds alpha val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; @@ -268,11 +275,6 @@ val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc -in -if !restricted_nominal = 0 then - ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) -else -let val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; @@ -436,7 +438,7 @@ fun prep_bn env bn_str = case (Syntax.read_term lthy bn_str) of Free (x, _) => (NONE, env_lookup env x) - | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), env_lookup env x) + | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x) | _ => error (bn_str ^ " not allowed as binding specification."); fun prep_typ env (i, opt_name) =