--- a/Quot/Nominal/Fv.thy Thu Feb 18 23:07:28 2010 +0100
+++ b/Quot/Nominal/Fv.thy Thu Feb 18 23:07:52 2010 +0100
@@ -1,5 +1,5 @@
theory Fv
-imports "Nominal2_Atoms"
+imports "Nominal2_Atoms" "Abs"
begin
(* Bindings are given as a list which has a length being equal
@@ -23,6 +23,35 @@
[],
[[], [], [(NONE, 0)]],
[[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
+
+A SOME binding has to have a function returning an atom set,
+and a NONE binding has to be on an argument that is an atom
+or an atom set.
+
+How the procedure works:
+ For each of the defined datatypes,
+ For each of the constructors,
+ It creates a union of free variables for each argument.
+
+ For an argument the free variables are the variables minus
+ bound variables.
+
+ The variables are:
+ For an atom, a singleton set with the atom itself.
+ For an atom set, the atom set itself.
+ For a recursive argument, the appropriate fv function applied to it.
+ (* TODO: This one is not implemented *)
+ For other arguments it should be an appropriate fv function stored
+ in the database.
+ The bound variables are a union of results of all bindings that
+ involve the given argument. For a paricular binding the result is:
+ For a function applied to an argument this function with the argument.
+ For an atom, a singleton set with the atom itself.
+ For an atom set, the atom set itself.
+ For a recursive argument, the appropriate fv function applied to it.
+ (* TODO: This one is not implemented *)
+ For other arguments it should be an appropriate fv function stored
+ in the database.
*)
ML {*
@@ -40,13 +69,32 @@
if b = noatoms then a else
if b = a then noatoms else
HOLogic.mk_binop @{const_name minus} (a, b);
+ fun mk_atoms t =
+ let
+ val ty = fastype_of t;
+ val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
+ val img_ty = atom_ty --> ty --> @{typ "atom set"};
+ in
+ (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+ end;
+ (* Copy from Term *)
+ fun is_funtype (Type ("fun", [_, _])) = true
+ | is_funtype _ = false;
+ (* Similar to one in USyntax *)
+ fun mk_pair (fst, snd) =
+ let val ty1 = fastype_of fst
+ val ty2 = fastype_of snd
+ val c = HOLogic.pair_const ty1 ty2
+ in c $ fst $ snd
+ end;
+
*}
ML {*
(* Currently needs just one full_tname to access Datatype *)
-fun define_raw_fv full_tname bindsall lthy =
+fun define_fv_alpha full_tname bindsall lthy =
let
- val thy = ProofContext.theory_of lthy
+ val thy = ProofContext.theory_of lthy;
val {descr, ...} = Datatype.the_info thy full_tname;
val sorts = []; (* TODO *)
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
@@ -54,46 +102,92 @@
"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);
- fun fv_eq_constr i (cname, dts) bindcs =
+ 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;
+ val alpha_frees = map Free (alpha_names ~~ alpha_types);
+ fun fv_alpha_constr i (cname, dts) bindcs =
let
val Ts = map (typ_of_dtyp descr sorts) dts;
val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
val args = map Free (names ~~ Ts);
+ val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
+ val args2 = map Free (names2 ~~ Ts);
val c = Const (cname, Ts ---> (nth_dtyp i));
- val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"});
- fun fv_bind (NONE, i) =
+ val fv_c = nth fv_frees i;
+ val alpha = nth alpha_frees i;
+ fun fv_bind args (NONE, i) =
if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
(* TODO we assume that all can be 'atomized' *)
+ if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
mk_single_atom (nth args i)
- | fv_bind (SOME f, i) = f $ (nth args i);
+ | fv_bind args (SOME f, i) = f $ (nth args i);
fun fv_arg ((dt, x), bindxs) =
let
val arg =
if is_rec_type dt then nth fv_frees (body_index dt) $ x else
(* TODO: we just assume everything can be 'atomized' *)
- HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]
- val sub = mk_union (map fv_bind bindxs)
+ if (is_funtype o fastype_of) x then mk_atoms x else
+ HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]
+ val sub = mk_union (map (fv_bind args) bindxs)
in
mk_diff arg sub
end;
- val _ = tracing ("d" ^ string_of_int (length dts));
- val _ = tracing (string_of_int (length args));
- val _ = tracing (string_of_int (length bindcs));
+ val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))
+ val alpha_rhs =
+ HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
+ fun alpha_arg ((dt, bindxs), (arg, arg2)) =
+ if bindxs = [] then (
+ if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
+ else (HOLogic.mk_eq (arg, arg2)))
+ else
+ if is_rec_type dt then let
+ (* THE HARD CASE *)
+ val lhs_binds = mk_union (map (fv_bind args) bindxs);
+ val lhs = mk_pair (lhs_binds, arg);
+ val rhs_binds = mk_union (map (fv_bind args2) bindxs);
+ val rhs = mk_pair (rhs_binds, arg2);
+ val alpha = nth alpha_frees (body_index dt);
+ val fv = nth fv_frees (body_index dt);
+ val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs;
+ val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre
+ in
+ HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t)
+ (* TODO Add some test that is makes sense *)
+ end else @{term "True"}
+ val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2))
+ val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs)
in
- (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
- (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))))
+ (fv_eq, alpha_eq)
end;
- fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds;
- val fv_eqs = flat (map2 fv_eq descr bindsall)
+ fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;
+ val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))
+ val add_binds = map (fn x => (Attrib.empty_binding, x))
+ val (fvs, lthy') = (Primrec.add_primrec
+ (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)
+ val (alphas, lthy'') = (Inductive.add_inductive_i
+ {quiet_mode = false, verbose = true, alt_name = Binding.empty,
+ coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
+ (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
+ (add_binds alpha_eqs) [] lthy')
in
- snd (Primrec.add_primrec
- (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy)
+ ((fvs, alphas), lthy'')
end
*}
-(* test
+(* tests
atom_decl name
+datatype ty =
+ Var "name set"
+
+ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}
+
+local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *}
+print_theorems
+
+
datatype rtrm1 =
rVr1 "name"
| rAp1 "rtrm1" "rtrm1"
@@ -113,11 +207,12 @@
| "bv1 (BVr x) = {atom x}"
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-local_setup {* define_raw_fv "Fv.rtrm1"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
+setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *}
+
+local_setup {* define_fv_alpha "Fv.rtrm1"
+ [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
[[], [[]], [[], []]]] *}
print_theorems
-
*)
end