# HG changeset patch # User Cezary Kaliszyk # Date 1269673905 -3600 # Node ID 6a114f8d45e68a7a19dff8abb0343b1b2fe50f07 # Parent ed89a26b70748d27e3fe461707f159d4cc82713f# Parent 3c51fccbe98965434adda3246ecb7a3778c3a5b6 merge diff -r 3c51fccbe989 -r 6a114f8d45e6 Nominal/ExTySch.thy --- a/Nominal/ExTySch.thy Sat Mar 27 06:44:47 2010 +0100 +++ b/Nominal/ExTySch.thy Sat Mar 27 08:11:45 2010 +0100 @@ -5,6 +5,7 @@ (* Type Schemes *) atom_decl name +(*ML {* val _ = alpha_type := AlphaRes *}*) nominal_datatype t = Var "name" | Fun "t" "t" diff -r 3c51fccbe989 -r 6a114f8d45e6 Nominal/Fv.thy --- 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 diff -r 3c51fccbe989 -r 6a114f8d45e6 Nominal/Nominal2_Supp.thy --- a/Nominal/Nominal2_Supp.thy Sat Mar 27 06:44:47 2010 +0100 +++ b/Nominal/Nominal2_Supp.thy Sat Mar 27 08:11:45 2010 +0100 @@ -415,7 +415,7 @@ apply(rule conjI) prefer 2 apply(auto)[1] -apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2)) +apply (metis permute_atom_def_raw permute_minus_cancel(2)) defer apply(rule psubset_card_mono) apply(simp add: finite_supp) diff -r 3c51fccbe989 -r 6a114f8d45e6 Nominal/Parser.thy --- 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 *}