--- 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 \<Rightarrow> perm \<Rightarrow> 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 \<Rightarrow> 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"