--- a/Quot/Nominal/Fv.thy Thu Feb 18 15:03:09 2010 +0100
+++ b/Quot/Nominal/Fv.thy Thu Feb 18 18:33:53 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
@@ -80,12 +80,19 @@
(* 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 {descr, ...} = Datatype.the_info thy full_tname;
@@ -95,19 +102,26 @@
"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 = nth fv_frees i;
- fun fv_bind (NONE, 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 =
@@ -115,70 +129,64 @@
(* TODO: we just assume everything can be 'atomized' *)
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 bindxs)
+ 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
- (* The snd will be removed later *)
- snd (Primrec.add_primrec
- (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy)
+ ((fvs, alphas), lthy'')
end
*}
-ML {*
-fun define_alpha full_tname bindsall lthy =
-let
- 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);
- 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 alpha_eq_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 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 i));
- val alpha = nth alpha_frees i;
- in
- (Attrib.empty_binding, HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))))
- end;
- fun alpha_eq (i, (_, _, constrs)) binds = map2 (alpha_eq_constr i) constrs binds;
- val alpha_eqs = flat (map2 alpha_eq descr bindsall)
-in
- (* The snd will be removed later *)
- snd (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) [] (alpha_eqs) [] lthy)
-end
-*}
-
+(* tests
atom_decl name
-(*datatype ty =
+datatype ty =
Var "name set"
ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}
-local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *}
+local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *}
print_theorems
-*)
+
datatype rtrm1 =
rVr1 "name"
@@ -199,15 +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
-
-local_setup {* define_alpha "Fv.rtrm1"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
- [[], [[]], [[], []]]] *}
-print_theorems
-
+*)
end