--- a/Nominal/Fv.thy Sat Mar 27 06:44:47 2010 +0100
+++ b/Nominal/Fv.thy Sat Mar 27 08:11:45 2010 +0100
@@ -136,14 +136,31 @@
*)
ML {*
+datatype alpha_type = AlphaGen | AlphaRes | AlphaLst;
+*}
+
+ML {*
+fun atyp_const AlphaGen = @{const_name alpha_gen}
+ | atyp_const AlphaRes = @{const_name alpha_res}
+ | atyp_const AlphaLst = @{const_name alpha_lst}
+*}
+
+(* TODO: make sure that parser checks that bindings are compatible *)
+ML {*
+fun alpha_const_for_binds [] = atyp_const AlphaGen
+ | alpha_const_for_binds ((NONE, _, _, at) :: t) = atyp_const at
+ | alpha_const_for_binds ((SOME (_, _), _, _, at) :: _) = atyp_const at
+*}
+
+ML {*
fun is_atom thy typ =
Sign.of_sort thy (typ, @{sort at})
fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
- | is_atom_set thy _ = false;
+ | is_atom_set _ _ = false;
fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
- | is_atom_fset thy _ = false;
+ | is_atom_fset _ _ = false;
*}
@@ -163,11 +180,11 @@
let
fun gather_binds_cons binds =
let
- val common = map (fn (f, bi, _) => (f, bi)) binds
+ val common = map (fn (f, bi, _, aty) => (f, bi, aty)) binds
val nodups = distinct (op =) common
- fun find_bodys (sf, sbi) =
- filter (fn (f, bi, _) => f = sf andalso bi = sbi) binds
- val bodys = map ((map (fn (_, _, bo) => bo)) o find_bodys) nodups
+ fun find_bodys (sf, sbi, sty) =
+ filter (fn (f, bi, _, aty) => f = sf andalso bi = sbi andalso aty = sty) binds
+ val bodys = map ((map (fn (_, _, bo, _) => bo)) o find_bodys) nodups
in
nodups ~~ bodys
end
@@ -178,11 +195,13 @@
ML {*
fun un_gather_binds_cons binds =
- flat (map (fn (((f, bi), bos), pi) => map (fn bo => ((f, bi, bo), pi)) bos) binds)
+ flat (map (fn (((f, bi, aty), bos), pi) => map (fn bo => ((f, bi, bo, aty), pi)) bos) binds)
*}
ML {*
open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
+*}
+ML {*
(* TODO: It is the same as one in 'nominal_atoms' *)
fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
val noatoms = @{term "{} :: atom set"};
@@ -259,7 +278,7 @@
ML {*
fun non_rec_binds l =
let
- fun is_non_rec (SOME (f, false), _, _) = SOME f
+ fun is_non_rec (SOME (f, false), _, _, _) = SOME f
| is_non_rec _ = NONE
in
distinct (op =) (map_filter is_non_rec (flat (flat l)))
@@ -307,6 +326,7 @@
end
*}
+ML {* print_depth 100 *}
ML {*
fun fv_bns thy dt_info fv_frees rel_bns =
let
@@ -326,11 +346,10 @@
ML {*
-fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees bn_alphabn ((bn, ith_dtyp, args_in_bns), (alpha_bn_free, is_rec)) =
+fun alpha_bn (dt_info : Datatype_Aux.info) alpha_frees bn_alphabn ((bn, ith_dtyp, args_in_bns), (alpha_bn_free, _ (*is_rec*) )) =
let
val {descr, sorts, ...} = dt_info;
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
- val pi = Free("pi", @{typ perm})
fun alpha_bn_constr (cname, dts) args_in_bn =
let
val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -342,17 +361,12 @@
val rhs = HOLogic.mk_Trueprop
(alpha_bn_free $ (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);
- in
- case AList.lookup (op=) args_in_bn arg_no of
- SOME NONE => @{term True}
- | SOME (SOME f) => (the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2
- | NONE =>
- if is_rec_type dt then (nth alpha_frees (body_index dt)) $ arg $ arg2
- else HOLogic.mk_eq (arg, arg2)
- end
+ case AList.lookup (op=) args_in_bn arg_no of
+ SOME NONE => @{term True}
+ | SOME (SOME f) => (the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2
+ | NONE =>
+ if is_rec_type dt then (nth alpha_frees (body_index dt)) $ arg $ arg2
+ else HOLogic.mk_eq (arg, arg2)
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)
@@ -367,7 +381,7 @@
*}
ML {*
-fun alpha_bns thy dt_info alpha_frees rel_bns bns_rec =
+fun alpha_bns dt_info alpha_frees rel_bns bns_rec =
let
val {descr, sorts, ...} = dt_info;
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
@@ -381,7 +395,7 @@
end;
val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free rel_bns);
val bn_alphabn = (map (fn (bn, _, _) => bn) rel_bns) ~~ alphabn_frees;
- val pair = split_list (map (alpha_bn thy dt_info alpha_frees bn_alphabn)
+ val pair = split_list (map (alpha_bn dt_info alpha_frees bn_alphabn)
(rel_bns ~~ (alphabn_frees ~~ bns_rec)))
in
(alphabn_names, pair)
@@ -392,7 +406,7 @@
(* Checks that a list of bindings contains only compatible ones *)
ML {*
fun bns_same l =
- length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1
+ length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1
*}
(* TODO: Notice datatypes without bindings and replace alpha with equality *)
@@ -422,7 +436,7 @@
(* We assume that a bn is either recursive or not *)
val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) =
- alpha_bns thy dt_info alpha_frees bns bns_rec
+ alpha_bns dt_info alpha_frees bns bns_rec
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 =
@@ -443,16 +457,16 @@
val fv_c = nth fv_frees ith_dtyp;
val alpha = nth alpha_frees ith_dtyp;
val arg_nos = 0 upto (length dts - 1)
- fun fv_bind args (NONE, 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
if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else
if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else
if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (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
+ 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) =
case get_first (find_nonrec_binder arg_no) bindcs of
@@ -470,7 +484,7 @@
(* 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 relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs;
val sub = fv_binds args relevant
in
mk_diff arg sub
@@ -481,13 +495,13 @@
HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
fun alpha_arg ((dt, arg_no), (arg, arg2)) =
let
- 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 ((NONE, _, j), _) => j = arg_no
- | ((SOME (_, false), _, j), _) => j = arg_no
+ 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 ((NONE, _, j, _), _) => j = arg_no
+ | ((SOME (_, false), _, j, _), _) => j = arg_no
| _ => false) bind_pis;
- val rel_has_rec_binds = filter
- (fn ((SOME (_, true), _, j), _) => j = arg_no | _ => false) bind_pis;
+ val rel_has_rec_binds = filter
+ (fn ((SOME (_, true), _, j, _), _) => j = arg_no | _ => false) bind_pis;
in
case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds, rel_has_rec_binds) of
([], [], [], []) =>
@@ -495,16 +509,15 @@
else (HOLogic.mk_eq (arg, arg2))
| (_, [], [], []) => @{term True}
| ([], [], [], _) => @{term True}
- | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), [], []) =>
+ | ([], ((((SOME (bn, is_rec)), _, _, atyp), _) :: _), [], []) =>
if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else
if is_rec then
let
val (rbinds, rpis) = split_list rel_in_comp_binds
- val bound_in_nos = map (fn (_, _, i) => i) rbinds
+ val bound_in_nos = map (fn (_, _, i, _) => i) rbinds
val bound_in_ty_nos = map (fn i => body_index (nth dts i)) bound_in_nos;
val bound_args = arg :: map (nth args) bound_in_nos;
val bound_args2 = arg2 :: map (nth args2) bound_in_nos;
- fun bound_in args (_, _, i) = nth args i;
val lhs_binds = fv_binds args rbinds
val lhs_arg = foldr1 HOLogic.mk_prod bound_args
val lhs = mk_pair (lhs_binds, lhs_arg);
@@ -516,7 +529,7 @@
val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos);
val alpha = mk_compound_alpha alphas;
val pi = foldr1 add_perm (distinct (op =) rpis);
- val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+ val alpha_gen_pre = Const (atyp_const atyp, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
val alpha_gen = Syntax.check_term lthy alpha_gen_pre
in
alpha_gen
@@ -538,7 +551,8 @@
val alpha = nth alpha_frees (body_index dt);
val fv = nth fv_frees (body_index dt);
val pi = foldr1 add_perm (distinct (op =) rpis);
- val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+ val alpha_const = alpha_const_for_binds rbinds;
+ val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
val alpha_gen = Syntax.check_term lthy alpha_gen_pre
in
alpha_gen
@@ -578,7 +592,6 @@
(alpha_types @ alpha_bn_types)) []
(add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
val ordered_fvs = fv_frees @ fvbns;
- val exported_fvs = map (Morphism.term (ProofContext.export_morphism lthy''' lthy)) ordered_fvs;
val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
in
(((all_fvs, ordered_fvs), alphas), lthy''')
@@ -621,7 +634,6 @@
val args = map Free (names ~~ tys);
fun find_alphas ty x =
domain_type (fastype_of x) = ty;
- fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg;
fun refl_eq_arg (ty, arg) =
let
val rel_alphas = filter (find_alphas ty) alphas;
@@ -636,7 +648,7 @@
*}
ML {*
-fun reflp_tac induct eq_iff ctxt =
+fun reflp_tac induct eq_iff =
rtac induct THEN_ALL_NEW
simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
@@ -649,7 +661,7 @@
fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
let
val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
- val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1);
+ val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
in
HOLogic.conj_elims refl_conj
end
--- a/Nominal/Parser.thy Sat Mar 27 06:44:47 2010 +0100
+++ b/Nominal/Parser.thy Sat Mar 27 08:11:45 2010 +0100
@@ -141,10 +141,14 @@
end
*}
+ML {*
+fun apfst3 f (a, b, c) = (f a, b, c)
+*}
+
ML {*
fun rawify_binds dts_env cnstrs_env bn_fun_env binds =
- map (map (map (map (fn (opt_trm, i, j) =>
- (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds
+ map (map (map (map (fn (opt_trm, i, j, aty) =>
+ (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j, aty))))) binds
*}
ML {*
@@ -152,8 +156,6 @@
| find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
*}
-ML {* @{term "{x, y}"} *}
-ML range_type
ML {*
fun strip_union t =
case t of
@@ -291,9 +293,6 @@
ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
ML {* val cheat_const_rsp = Unsynchronized.ref false *}
-ML {* fun map_option _ NONE = NONE
- | map_option f (SOME x) = SOME (f x) *}
-
(* nominal_datatype2 does the following things in order:
1) define the raw datatype
2) define the raw binding functions
@@ -340,7 +339,7 @@
val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
raw_nominal_decls dts bn_funs bn_eqs binds lthy
val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
- fun export_fun f (t, l) = (f t, map (map (apsnd (map_option f))) l);
+ fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_1)))) raw_bns;
val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
@@ -572,6 +571,7 @@
ML {*
val recursive = Unsynchronized.ref false
+val alpha_type = Unsynchronized.ref AlphaGen
*}
ML {*
@@ -602,7 +602,8 @@
end
in
- map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))
+ map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type)))))
+ (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
end
*}