--- a/Nominal/Fv.thy Wed Mar 10 12:48:38 2010 +0100
+++ b/Nominal/Fv.thy Wed Mar 10 12:48:55 2010 +0100
@@ -193,6 +193,51 @@
end
*}
+ML {*
+fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) =
+let
+ val {descr, sorts, ...} = dt_info;
+ fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+ val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+ val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}
+ val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);
+ fun alpha_bn_constr (cname, dts) args_in_bn =
+ let
+ val Ts = map (typ_of_dtyp descr sorts) dts;
+ val pi = Free("pi", @{typ perm})
+ val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
+ val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
+ val args = map Free (names ~~ Ts);
+ val args2 = map Free (names2 ~~ Ts);
+ val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+ val rhs = HOLogic.mk_Trueprop
+ (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2)));
+ fun lhs_arg ((dt, arg_no), (arg, arg2)) =
+ let
+ val argty = fastype_of arg;
+ val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty);
+ val permarg = if is_rec then permute $ pi $ arg else arg
+ in
+ if is_rec_type dt then
+ if arg_no mem args_in_bn then alpha_bn_free $ pi $ arg $ arg2
+ else (nth alpha_frees (body_index dt)) $ permarg $ arg2
+ else
+ if arg_no mem args_in_bn then @{term True}
+ else HOLogic.mk_eq (permarg, arg2)
+ end
+ val arg_nos = 0 upto (length dts - 1)
+ val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
+ val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs)
+ in
+ eq
+ end
+ val (_, (_, _, constrs)) = nth descr ith_dtyp;
+ val eqs = map2i alpha_bn_constr constrs args_in_bns
+in
+ ((bn, alpha_bn_free), (alpha_bn_name, eqs))
+end
+*}
+
ML {* fn x => split_list(flat x) *}
ML {* fn x => apsnd flat (split_list (map split_list x)) *}
(* TODO: Notice datatypes without bindings and replace alpha with equality *)
@@ -209,12 +254,17 @@
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;
val alpha_frees = map Free (alpha_names ~~ alpha_types);
+ (* We assume that a bn is either recursive or not *)
+ val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
+ val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec))
+ val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs;
+ val alpha_bn_frees = map snd bn_alpha_bns;
+ val alpha_bn_types = map fastype_of alpha_bn_frees;
fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
let
val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -269,14 +319,26 @@
HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
fun alpha_arg ((dt, arg_no), (arg, arg2)) =
let
- val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) bind_pis;
+ val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis;
+ val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis;
+ val rel_has_binds = filter (fn ((SOME _, _, j), _) => j = arg_no | _ => false) bind_pis;
in
- if relevant = [] 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 *)
+ case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of
+ ([], [], []) =>
+ if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
+ else (HOLogic.mk_eq (arg, arg2))
+ (* TODO: if more then check and accept *)
+ | (_, [], []) => @{term True}
+ | ([], [(((SOME (bn, _)), _, _), pi)], []) =>
+ let
+ val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2
+ val ty = fastype_of (bn $ arg)
+ val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
+ in
+ HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))
+ end
+ | ([], [], relevant) =>
+ let
val (rbinds, rpis) = split_list relevant
val lhs_binds = fv_binds args rbinds
val lhs = mk_pair (lhs_binds, arg);
@@ -290,10 +352,10 @@
(* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *)
in
- (*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
+(* if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
alpha_gen
- (* TODO Add some test that is makes sense *)
- end else @{term "True"}
+ end
+ | _ => error "Fv.alpha: not supported binding structure"
end
val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2))
val alpha_lhss = mk_conjl alphas
@@ -307,7 +369,7 @@
val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall)
val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs))
val rel_bns_nos = map (fn (_, i, _) => i) rel_bns;
- fun filter_fun (a, b) = b mem rel_bns_nos;
+ fun filter_fun (_, b) = b mem rel_bns_nos;
val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1))
val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs)))
val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs)))
@@ -325,38 +387,35 @@
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}
- (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
- (add_binds alpha_eqs) [] lthy'')
+ (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names)
+ (alpha_types @ alpha_bn_types)) []
+ (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
+ val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
in
- ((fvs, alphas), lthy''')
+ ((all_fvs, alphas), lthy''')
end
*}
(*
atom_decl name
-
datatype lam =
VAR "name"
| APP "lam" "lam"
| LET "bp" "lam"
and bp =
BP "name" "lam"
-
primrec
bi::"bp \<Rightarrow> atom set"
where
"bi (BP x t) = {atom x}"
-
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}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
+ [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
print_theorems
*)
-(*
+(*atom_decl name
datatype rtrm1 =
rVr1 "name"
| rAp1 "rtrm1" "rtrm1"
@@ -366,24 +425,38 @@
BUnit
| BVr "name"
| BPr "bp" "bp"
-
-(* to be given by the user *)
-
primrec
bv1
where
"bv1 (BUnit) = {}"
| "bv1 (BVr x) = {atom x}"
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-
-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)]]],
- [[], [[]], [[], []]]] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *}
+local_setup {*
+ snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1")
+ [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]],
+ [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
print_theorems
*)
+(*
+atom_decl name
+datatype rtrm5 =
+ rVr5 "name"
+| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
+and rlts =
+ rLnil
+| rLcons "name" "rtrm5" "rlts"
+primrec
+ rbv5
+where
+ "rbv5 rLnil = {}"
+| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *}
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5")
+ [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
+print_theorems
+*)
ML {*
fun alpha_inj_tac dist_inj intrs elims =