# HG changeset patch # User Christian Urban # Date 1272805586 -3600 # Node ID 1bddffddc03fdb700e02d40e57ceb74cc78805a5 # Parent 7ee9a2fefc77435c640fabbdd735506c88a108e5 attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing) diff -r 7ee9a2fefc77 -r 1bddffddc03f Nominal/Attic/Fv.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Attic/Fv.thy Sun May 02 14:06:26 2010 +0100 @@ -0,0 +1,653 @@ +theory Fv +imports "../Nominal-General/Nominal2_Atoms" + "Abs" "Perm" "Rsp" "Nominal2_FSet" +begin + +(* The bindings data structure: + + Bindings are a list of lists of lists of triples. + + The first list represents the datatypes defined. + The second list represents the constructors. + The internal list is a list of all the bndings that + concern the constructor. + + Every triple consists of a function, the binding and + the body. + + Eg: +nominal_datatype + + C1 + | C2 x y z bind x in z + | C3 x y z bind f x in z bind g y in z + +yields: +[ + [], + [(NONE, 0, 2)], + [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]] + +A SOME binding has to have a function which takes an appropriate +argument and returns an atom set. A NONE binding has to be on an +argument that is an atom or an atom set. +*) + +(* +An overview of the generation of free variables: + +1) fv_bn functions are generated only for the non-recursive binds. + + An fv_bn for a constructor is a union of values for the arguments: + + For an argument x that is in the bn function + - if it is a recursive argument bn' we return: fv_bn' x + - otherwise empty + + For an argument x that is not in the bn function + - for atom we return: {atom x} + - for atom set we return: atom ` x + - for a recursive call to type ty' we return: fv_ty' x + with fv of the appropriate type + - otherwise empty + +2) fv_ty functions generated for all types being defined: + + fv_ty for a constructor is a union of values for the arguments. + + For an argument that is bound in a shallow binding we return empty. + + For an argument x that bound in a non-recursive deep binding + we return: fv_bn x. + + Otherwise we return the free variables of the argument minus the + bound variables of the argument. + + The free variables for an argument x are: + - for an atom: {atom x} + - for atom set: atom ` x + - for recursive call to type ty' return: fv_ty' x + - for nominal datatype ty' return: fv_ty' x + + The bound variables are a union of results of all bindings that + involve the given argument. For a paricular binding: + + - for a binding function bn: bn x + - for a recursive argument of type ty': fv_fy' x + - for nominal datatype ty' return: fv_ty' x +*) + +(* +An overview of the generation of alpha-equivalence: + +1) alpha_bn relations are generated for binding functions. + + An alpha_bn for a constructor is true if a conjunction of + propositions for each argument holds. + + For an argument a proposition is build as follows from + th: + + - for a recursive argument in the bn function, we return: alpha_bn argl argr + - for a recursive argument for type ty not in bn, we return: alpha_ty argl argr + - for other arguments in the bn function we return: True + - for other arguments not in the bn function we return: argl = argr + +2) alpha_ty relations are generated for all the types being defined: + + For each constructor we gather all the arguments that are bound, + and for each of those we add a permutation. We associate those + permutations with the bindings. Note that two bindings can have + the same permutation if the arguments being bound are the same. + + An alpha_ty for a constructor is true if there exist permutations + as above such that a conjunction of propositions for all arguments holds. + + For an argument we allow bindings where only one of the following + holds: + + - Argument is bound in some shallow bindings: We return true + - Argument of type ty is bound recursively in some other + arguments [i1, .. in] with one binding function bn. + We return: + + (bn argl, (argl, argl_i1, ..., argl_in)) \gen + \(argl,argl1,..,argln) (argr,argr1,..,argrn). + (alpha_ty argl argr) \ (alpha_i1 argl1 argr1) \ .. \ (alpha_in argln argrn) + \(arg,arg1,..,argn). (fv_ty arg) \ (fv_i1 arg1) \ .. \ (fv_in argn) + pi + (bn argr, (argr, argr_i1, ..., argr_in)) + + - Argument is bound in some deep non-recursive bindings. + We return: alpha_bn argl argr + - Argument of type ty has some shallow bindings [b1..bn] and/or + non-recursive bindings [f1 a1, .., fm am], where the bindings + have the permutations p1..pl. We return: + + (b1l \..\ bnl \ f1 a1l \..\ fn anl, argl) \gen + alpha_ty fv_ty (p1 +..+ pl) + (b1r \..\ bnr \ f1 a1r \..\ fn anr, argr) + + - Argument has some recursive bindings. The bindings were + already treated in 2nd case so we return: True + - Argument has no bindings and is not bound. + If it is recursive for type ty, we return: alpha_ty argl argr + Otherwise we return: argl = argr + +*) + + +ML {* +datatype alpha_mode = 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 _ _ = false; + +fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t + | is_atom_fset _ _ = false; +*} + + +(* Like map2, only if the second list is empty passes empty lists insted of error *) +ML {* +fun map2i _ [] [] = [] + | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys + | map2i f (x :: xs) [] = f x [] :: map2i f xs [] + | map2i _ _ _ = raise UnequalLengths; +*} + +(* Finds bindings with the same function and binding, and gathers all + bodys for such pairs + *) +ML {* +fun gather_binds binds = +let + fun gather_binds_cons binds = + let + val common = map (fn (f, bi, _, aty) => (f, bi, aty)) binds + val nodups = distinct (op =) common + 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 +in + map (map gather_binds_cons) binds +end +*} + +ML {* +fun un_gather_binds_cons 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"}; + fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]; + fun mk_union sets = + fold (fn a => fn b => + if a = noatoms then b else + if b = noatoms then a else + if a = b then a else + HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; + val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf}) + fun mk_diff a b = + if b = noatoms then a else + if b = a then noatoms else + HOLogic.mk_binop @{const_name minus} (a, b); + fun mk_atom_set 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; + fun mk_atom_fset t = + let + val ty = fastype_of t; + val atom_ty = dest_fsetT ty --> @{typ atom}; + val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; + val fset_to_set = @{term "fset_to_set :: atom fset \ atom set"} + in + fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)) + end; + (* 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; +*} + +(* Given [fv1, fv2, fv3] creates %(x, y, z). fv1 x u fv2 y u fv3 z *) +ML {* +fun mk_compound_fv fvs = +let + val nos = (length fvs - 1) downto 0; + val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos); + val fvs_union = mk_union fvs_applied; + val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs); + fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t)) +in + fold fold_fun tys (Abs ("", tyh, fvs_union)) +end; +*} + +(* Given [R1, R2, R3] creates %(x,x'). %(y,y'). %(z,z'). R x x' \ R y y' \ R z z' *) +ML {* +fun mk_compound_alpha Rs = +let + val nos = (length Rs - 1) downto 0; + val nos2 = (2 * length Rs - 1) downto length Rs; + val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no) (Rs ~~ (nos2 ~~ nos)); + val Rs_conj = mk_conjl Rs_applied; + val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs); + fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t)) + val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj)) +in + fold fold_fun tys (Abs ("", tyh, abs_rhs)) +end; +*} + + +ML {* +fun non_rec_binds l = +let + fun is_non_rec (SOME (f, false), _, _, _) = SOME f + | is_non_rec _ = NONE +in + distinct (op =) (map_filter is_non_rec (flat (flat l))) +end +*} + +(* We assume no bindings in the type on which bn is defined *) +ML {* +fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) = +let + val {descr, sorts, ...} = dt_info; + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + fun fv_bn_constr (cname, dts) args_in_bn = + let + val Ts = map (typ_of_dtyp descr sorts) dts; + val names = Datatype_Prop.make_tnames Ts; + val args = map Free (names ~~ Ts); + val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); + fun fv_arg ((dt, x), arg_no) = + let + val ty = fastype_of x +(* val _ = tracing ("B 1" ^ PolyML.makestring args_in_bn);*) +(* val _ = tracing ("B 2" ^ PolyML.makestring bn_fvbn);*) + in + case AList.lookup (op=) args_in_bn arg_no of + SOME NONE => @{term "{} :: atom set"} + | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x + | NONE => + if is_atom thy ty then mk_single_atom x else + if is_atom_set thy ty then mk_atom_set x else + if is_atom_fset thy ty then mk_atom_fset x else + if is_rec_type dt then nth fv_frees (body_index dt) $ x else + @{term "{} :: atom set"} + end; + val arg_nos = 0 upto (length dts - 1) + in + HOLogic.mk_Trueprop (HOLogic.mk_eq + (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) + end; + val (_, (_, _, constrs)) = nth descr ith_dtyp; + val eqs = map2i fv_bn_constr constrs args_in_bns +in + ((bn, fvbn), eqs) +end +*} + +ML {* print_depth 100 *} +ML {* +fun fv_bns thy dt_info fv_frees rel_bns = +let + fun mk_fvbn_free (bn, ith, _) = + let + val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); + in + (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) + end; + val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free rel_bns); + val bn_fvbn = (map (fn (bn, _, _) => bn) rel_bns) ~~ fvbn_frees + val (l1, l2) = split_list (map (fv_bn thy dt_info fv_frees bn_fvbn) (fvbn_frees ~~ rel_bns)); +in + (l1, (fvbn_names ~~ l2)) +end +*} + + +ML {* +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); + fun alpha_bn_constr (cname, dts) args_in_bn = + 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 ith_dtyp)); + val rhs = HOLogic.mk_Trueprop + (alpha_bn_free $ (list_comb (c, args)) $ (list_comb (c, args2))); + fun lhs_arg ((dt, arg_no), (arg, arg2)) = + 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) + in + eq + end + val (_, (_, _, constrs)) = nth descr ith_dtyp; + val eqs = map2i alpha_bn_constr constrs args_in_bns +in + ((bn, alpha_bn_free), eqs) +end +*} + +ML {* +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); + fun mk_alphabn_free (bn, ith, _) = + let + val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); + val alphabn_type = nth_dtyp ith --> nth_dtyp ith --> @{typ bool}; + val alphabn_free = Free(alphabn_name, alphabn_type); + in + (alphabn_name, alphabn_free) + 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 dt_info alpha_frees bn_alphabn) + (rel_bns ~~ (alphabn_frees ~~ bns_rec))) +in + (alphabn_names, pair) +end +*} + + +(* Checks that a list of bindings contains only compatible ones *) +ML {* +fun bns_same l = + length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1 +*} + +ML {* +fun setify x = + if fastype_of x = @{typ "atom list"} then + Const (@{const_name set}, @{typ "atom list \ atom set"}) $ x else x +*} + +ML {* +fun define_fv (dt_info : Datatype_Aux.info) bindsall bns lthy = +let + val thy = ProofContext.theory_of lthy; + val {descr, sorts, ...} = dt_info; + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => + "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); +(* TODO: We need a transitive closure, but instead we do this hack considering + all binding functions as recursive or not *) + val nr_bns = + if (non_rec_binds bindsall) = [] then [] + else map (fn (bn, _, _) => bn) bns; + val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; + val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns; + val fvbns = map snd bn_fv_bns; + val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; + + fun fv_constr ith_dtyp (cname, dts) bindcs = + let + val Ts = map (typ_of_dtyp descr sorts) dts; + val bindslen = length bindcs + val pi_strs_same = replicate bindslen "pi" + val pi_strs = Name.variant_list [] pi_strs_same; + val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; + val bind_pis_gath = bindcs ~~ pis; + val bind_pis = un_gather_binds_cons bind_pis_gath; + val bindcs = map fst bind_pis; + val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); + val args = map Free (names ~~ Ts); + val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); + val fv_c = nth fv_frees ith_dtyp; + val arg_nos = 0 upto (length dts - 1) + 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 goes the code for preiously defined nominal datatypes *) + @{term "{} :: atom set"} + | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) + fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant) + 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 + SOME f => + (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of + SOME fv_bn => fv_bn $ x + | NONE => error "bn specified in a non-rec binding but not in bn list") + | NONE => + let + val arg = + if is_rec_type dt then nth fv_frees (body_index dt) $ x else + if ((is_atom thy) o fastype_of) x then mk_single_atom x else + if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else + if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else + (* TODO goes the code for preiously defined nominal datatypes *) + @{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 sub = fv_binds_as_set args relevant + in + mk_diff arg sub + end; + val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq + (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) + in + fv_eq + end; + fun fv_eq (i, (_, _, constrs)) binds = map2i (fv_constr i) constrs binds; + val fveqs = map2i fv_eq descr (gather_binds bindsall) + val fv_eqs_perfv = fveqs + val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; + 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))) + val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); + val fv_names_all = fv_names_fst @ fv_bn_names; + val add_binds = map (fn x => (Attrib.empty_binding, x)) +(* Function_Fun.add_fun Function_Common.default_config ... true *) + val (fvs, lthy') = (Primrec.add_primrec + (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) + val (fvs2, lthy'') = + if fv_eqs_snd = [] then (([], []), lthy') else + (Primrec.add_primrec + (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') + val ordered_fvs = fv_frees @ fvbns; + val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) +in + ((all_fvs, ordered_fvs), lthy'') +end +*} + +ML {* +fun define_alpha (dt_info : Datatype_Aux.info) bindsall bns fv_frees lthy = +let + val thy = ProofContext.theory_of lthy; + val {descr, sorts, ...} = dt_info; + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); +(* TODO: We need a transitive closure, but instead we do this hack considering + all binding functions as recursive or not *) + val nr_bns = + if (non_rec_binds bindsall) = [] then [] + else map (fn (bn, _, _) => bn) bns; + 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 (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) = + 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 alpha_constr ith_dtyp (cname, dts) bindcs = + let + val Ts = map (typ_of_dtyp descr sorts) dts; + val bindslen = length bindcs + val pi_strs_same = replicate bindslen "pi" + val pi_strs = Name.variant_list [] pi_strs_same; + val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; + val bind_pis_gath = bindcs ~~ pis; + val bind_pis = un_gather_binds_cons bind_pis_gath; + val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); + val args = map Free (names ~~ Ts); + val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); + val args2 = map Free (names2 ~~ Ts); + val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); + val alpha = nth alpha_frees ith_dtyp; + val arg_nos = 0 upto (length dts - 1) + 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 goes the code for preiously defined nominal datatypes *) + @{term "{} :: atom set"} + | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) + fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) + val alpha_rhs = + 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 + | _ => 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 + ([], [], [], []) => + if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) + else (HOLogic.mk_eq (arg, arg2)) + | (_, [], [], []) => @{term True} + | ([], [], [], _) => @{term True} + | ([], ((((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_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; + val lhs_binds = fv_binds args rbinds + val lhs_arg = foldr1 HOLogic.mk_prod bound_args + val lhs = mk_pair (lhs_binds, lhs_arg); + val rhs_binds = fv_binds args2 rbinds; + val rhs_arg = foldr1 HOLogic.mk_prod bound_args2; + val rhs = mk_pair (rhs_binds, rhs_arg); + val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos); + val fv = mk_compound_fv fvs; + val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); + val alpha = mk_compound_alpha alphas; + val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis); + 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 + end + else + let + val alpha_bn_const = + nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) + in + alpha_bn_const $ arg $ arg2 + end + | ([], [], relevant, []) => + let + val (rbinds, rpis) = split_list relevant + val lhs_binds = fv_binds args rbinds + val lhs = mk_pair (lhs_binds, arg); + val rhs_binds = fv_binds args2 rbinds; + val rhs = mk_pair (rhs_binds, arg2); + val alpha = nth alpha_frees (body_index dt); + val fv = nth fv_frees (body_index dt); + val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis); + 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 + 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 + val alpha_lhss_ex = + fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss + val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) + in + alpha_eq + end; + fun alpha_eq (i, (_, _, constrs)) binds = map2i (alpha_constr i) constrs binds; + val alphaeqs = map2i alpha_eq descr (gather_binds bindsall) + val alpha_eqs = flat alphaeqs + val add_binds = map (fn x => (Attrib.empty_binding, x)) + 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_bn_names) + (alpha_types @ alpha_bn_types)) [] + (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy) +in + (alphas, lthy') +end +*} + +end diff -r 7ee9a2fefc77 -r 1bddffddc03f Nominal/Attic/Parser.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Attic/Parser.thy Sun May 02 14:06:26 2010 +0100 @@ -0,0 +1,670 @@ +theory Parser +imports "../Nominal-General/Nominal2_Atoms" + "../Nominal-General/Nominal2_Eqvt" + "../Nominal-General/Nominal2_Supp" + "Perm" "Equivp" "Rsp" "Lift" +begin + +section{* Interface for nominal_datatype *} + +text {* + +Nominal-Datatype-part: + + +1nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + type(s) to be defined constructors list + (ty args, name, syn) (name, typs, syn) + +Binder-Function-part: + +2rd Arg: (binding * typ option * mixfix) list + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + binding function(s) + to be defined + (name, type, syn) + +3th Arg: term list + ^^^^^^^^^ + the equations of the binding functions + (Trueprop equations) +*} + +ML {* + +*} + +text {*****************************************************} +ML {* +(* nominal datatype parser *) +local + structure P = OuterParse + + fun tuple ((x, y, z), u) = (x, y, z, u) + fun tswap (((x, y), z), u) = (x, y, u, z) +in + +val _ = OuterKeyword.keyword "bind" +val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ + +(* binding specification *) +(* maybe use and_list *) +val bind_parser = + P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name) >> swap) + +val constr_parser = + P.binding -- Scan.repeat anno_typ + +(* datatype parser *) +val dt_parser = + (P.type_args -- P.binding -- P.opt_mixfix >> P.triple1) -- + (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> tswap)) >> tuple + +(* function equation parser *) +val fun_parser = + Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) + +(* main parser *) +val main_parser = + (P.and_list1 dt_parser) -- fun_parser >> P.triple2 + +end +*} + +(* adds "_raw" to the end of constants and types *) +ML {* +fun add_raw s = s ^ "_raw" +fun add_raws ss = map add_raw ss +fun raw_bind bn = Binding.suffix_name "_raw" bn + +fun replace_str ss s = + case (AList.lookup (op=) ss s) of + SOME s' => s' + | NONE => s + +fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) + | replace_typ ty_ss T = T + +fun raw_dts ty_ss dts = +let + + fun raw_dts_aux1 (bind, tys, mx) = + (raw_bind bind, map (replace_typ ty_ss) tys, mx) + + fun raw_dts_aux2 (ty_args, bind, mx, constrs) = + (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) +in + map raw_dts_aux2 dts +end + +fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) + | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T) + | replace_aterm trm_ss trm = trm + +fun replace_term trm_ss ty_ss trm = + trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) +*} + +ML {* +fun get_cnstrs dts = + map (fn (_, _, _, constrs) => constrs) dts + +fun get_typed_cnstrs dts = + flat (map (fn (_, bn, _, constrs) => + (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) + +fun get_cnstr_strs dts = + map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) + +fun get_bn_fun_strs bn_funs = + map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs +*} + +ML {* +fun rawify_dts dt_names dts dts_env = +let + val raw_dts = raw_dts dts_env dts + val raw_dt_names = add_raws dt_names +in + (raw_dt_names, raw_dts) +end +*} + +ML {* +fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = +let + val bn_funs' = map (fn (bn, ty, mx) => + (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs + + val bn_eqs' = map (fn (attr, trm) => + (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs +in + (bn_funs', bn_eqs') +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, aty) => + (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j, aty))))) binds +*} + +ML {* +fun find [] _ = error ("cannot find element") + | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y +*} + +ML {* +fun strip_bn_fun t = + case t of + Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r + | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r + | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => + (i, NONE) :: strip_bn_fun y + | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => + (i, NONE) :: strip_bn_fun y + | Const (@{const_name bot}, _) => [] + | Const (@{const_name Nil}, _) => [] + | (f as Free _) $ Bound i => [(i, SOME f)] + | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t)) +*} + +ML {* +fun prep_bn dt_names dts eqs = +let + fun aux eq = + let + val (lhs, rhs) = eq + |> strip_qnt_body "all" + |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq + val (bn_fun, [cnstr]) = strip_comb lhs + val (_, ty) = dest_Free bn_fun + val (ty_name, _) = dest_Type (domain_type ty) + val dt_index = find_index (fn x => x = ty_name) dt_names + val (cnstr_head, cnstr_args) = strip_comb cnstr + val rhs_elements = strip_bn_fun rhs + val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements + in + (dt_index, (bn_fun, (cnstr_head, included))) + end + fun order dts i ts = + let + val dt = nth dts i + val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) + val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts + in + map (find ts') cts + end + + val unordered = AList.group (op=) (map aux eqs) + val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered + val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' +in + ordered +end +*} + +ML {* +fun add_primrec_wrapper funs eqs lthy = + if null funs then (([], []), lthy) + else + let + val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs + val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs + in + Primrec.add_primrec funs' eqs' lthy + end +*} + +ML {* +fun add_datatype_wrapper dt_names dts = +let + val conf = Datatype.default_config +in + Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts) +end +*} + +ML {* +fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = +let + val thy = ProofContext.theory_of lthy + val thy_name = Context.theory_name thy + + val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts + val dt_full_names = map (Long_Name.qualify thy_name) dt_names + val dt_full_names' = add_raws dt_full_names + val dts_env = dt_full_names ~~ dt_full_names' + + val cnstrs = get_cnstr_strs dts + val cnstrs_ty = get_typed_cnstrs dts + val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs + val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name + (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty + val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' + + val bn_fun_strs = get_bn_fun_strs bn_funs + val bn_fun_strs' = add_raws bn_fun_strs + val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' + val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) + (bn_fun_strs ~~ bn_fun_strs') + + val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env + + val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs + + val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds + + val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) + +(*val _ = tracing (cat_lines (map PolyML.makestring raw_bns))*) +in + lthy + |> add_datatype_wrapper raw_dt_names raw_dts + ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs + ||>> pair raw_binds + ||>> pair raw_bns +end +*} + +lemma equivp_hack: "equivp x" +sorry +ML {* +fun equivp_hack ctxt rel = +let + val thy = ProofContext.theory_of ctxt + val ty = domain_type (fastype_of rel) + val cty = ctyp_of thy ty + val ct = cterm_of thy rel +in + Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} +end +*} + +ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} +ML {* val cheat_equivp = Unsynchronized.ref false *} +ML {* val cheat_fv_rsp = Unsynchronized.ref false *} +ML {* val cheat_const_rsp = Unsynchronized.ref false *} + +(* nominal_datatype2 does the following things in order: + +Parser.thy/raw_nominal_decls + 1) define the raw datatype + 2) define the raw binding functions + +Perm.thy/define_raw_perms + 3) define permutations of the raw datatype and show that the raw type is + in the pt typeclass + +Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha + 4) define fv and fv_bn + 5) define alpha and alpha_bn + +Perm.thy/distinct_rel + 6) prove alpha_distincts (C1 x \ C2 y ...) (Proof by cases; simp) + +Tacs.thy/build_rel_inj + 6) prove alpha_eq_iff (C1 x = C2 y \ P x y ...) + (left-to-right by intro rule, right-to-left by cases; simp) +Equivp.thy/prove_eqvt + 7) prove bn_eqvt (common induction on the raw datatype) + 8) prove fv_eqvt (common induction on the raw datatype with help of above) +Rsp.thy/build_alpha_eqvts + 9) prove alpha_eqvt and alpha_bn_eqvt + (common alpha-induction, unfolding alpha_gen, permute of #* and =) +Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps + 10) prove that alpha and alpha_bn are equivalence relations + (common induction and application of 'compose' lemmas) +Lift.thy/define_quotient_types + 11) define quotient types +Rsp.thy/build_fvbv_rsps + 12) prove bn respects (common induction and simp with alpha_gen) +Rsp.thy/prove_const_rsp + 13) prove fv respects (common induction and simp with alpha_gen) + 14) prove permute respects (unfolds to alpha_eqvt) +Rsp.thy/prove_alpha_bn_rsp + 15) prove alpha_bn respects + (alpha_induct then cases then sym and trans of the relations) +Rsp.thy/prove_alpha_alphabn + 16) show that alpha implies alpha_bn (by unduction, needed in following step) +Rsp.thy/prove_const_rsp + 17) prove respects for all datatype constructors + (unfold eq_iff and alpha_gen; introduce zero permutations; simp) +Perm.thy/quotient_lift_consts_export + 18) define lifted constructors, fv, bn, alpha_bn, permutations +Perm.thy/define_lifted_perms + 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass +Lift.thy/lift_thm + 20) lift permutation simplifications + 21) lift induction + 22) lift fv + 23) lift bn + 24) lift eq_iff + 25) lift alpha_distincts + 26) lift fv and bn eqvts +Equivp.thy/prove_supports + 27) prove that union of arguments supports constructors +Equivp.thy/prove_fs + 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) +Equivp.thy/supp_eq + 29) prove supp = fv +*) +ML {* +fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = +let + val _ = tracing "Raw declarations"; + val thy = ProofContext.theory_of lthy + val thy_name = Context.theory_name thy + 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 (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 + val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc + + val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); + val {descr, sorts, ...} = dtinfo; + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + val raw_tys = map (fn (i, _) => nth_dtyp i) descr; + val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) + val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; + val rel_dtinfos = List.take (dtinfos, (length dts)); + val inject = flat (map #inject dtinfos); + val distincts = flat (map #distinct dtinfos); + val rel_distinct = map #distinct rel_dtinfos; + val induct = #induct dtinfo; + val exhausts = map #exhaust dtinfos; + val _ = tracing "Defining permutations, fv and alpha"; + val ((raw_perm_def, raw_perm_simps, perms), lthy3) = + Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; + val raw_binds_flat = map (map flat) raw_binds; + val ((((_, fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = + define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; + val (fv, fvbn) = chop (length perms) fv_ts; + + val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts + val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); + val bn_tys = map (domain_type o fastype_of) raw_bn_funs; + val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; + val bns = raw_bn_funs ~~ bn_nos; + val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) + (rel_distinct ~~ alpha_ts_nobn)); + val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) + ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) + val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 + val _ = tracing "Proving equivariance"; + val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 + val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 + fun alpha_eqvt_tac' _ = + if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy + else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1 + val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; + val _ = tracing "Proving equivalence"; + val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; + val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; + val alpha_equivp = + if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn + else build_equivps alpha_ts reflps alpha_induct + inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; + val qty_binds = map (fn (_, b, _, _) => b) dts; + val qty_names = map Name.of_binding qty_binds; + val qty_full_names = map (Long_Name.qualify thy_name) qty_names + val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; + val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); + val raw_consts = + flat (map (fn (i, (_, _, l)) => + map (fn (cname, dts) => + Const (cname, map (typ_of_dtyp descr sorts) dts ---> + typ_of_dtyp descr sorts (DtRec i))) l) descr); + val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; + val _ = tracing "Proving respects"; + val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; + val (bns_rsp_pre, lthy9) = fold_map ( + fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => + resolve_tac bns_rsp_pre' 1)) bns lthy8; + val bns_rsp = flat (map snd bns_rsp_pre); + fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy + else fvbv_rsp_tac alpha_induct fv_def lthy8 1; + val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; + val (fv_rsp_pre, lthy10) = fold_map + (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] + (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; + val fv_rsp = flat (map snd fv_rsp_pre); + val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms + (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; + val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11; + val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] + (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11 +(* val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*) + fun const_rsp_tac _ = + if !cheat_const_rsp then Skip_Proof.cheat_tac thy + else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a + in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end + val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] + const_rsp_tac) raw_consts lthy11a + val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) + val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; + val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; + val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs + val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; + val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn + val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; + val _ = tracing "Lifting permutations"; + val thy = Local_Theory.exit_global lthy12c; + val perm_names = map (fn x => "permute_" ^ x) qty_names + val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy; + val lthy13 = Theory_Target.init NONE thy'; + val q_name = space_implode "_" qty_names; + fun suffix_bind s = Binding.qualify true q_name (Binding.name s); + val _ = tracing "Lifting induction"; + val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; + val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct); + fun note_suffix s th ctxt = + snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); + fun note_simp_suffix s th ctxt = + snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); + val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", + [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; + val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct + val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; + val q_perm = map (lift_thm qtys lthy14) raw_perm_def; + val lthy15 = note_simp_suffix "perm" q_perm lthy14a; + val q_fv = map (lift_thm qtys lthy15) fv_def; + val lthy16 = note_simp_suffix "fv" q_fv lthy15; + val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; + val lthy17 = note_simp_suffix "bn" q_bn lthy16; + val _ = tracing "Lifting eq-iff"; + val _ = map tracing (map PolyML.makestring alpha_eq_iff); + val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff + val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 + val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 + val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; + val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 + val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 + val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 + val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; + val q_dis = map (lift_thm qtys lthy18) rel_dists; + val lthy19 = note_simp_suffix "distinct" q_dis lthy18; + val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); + val (_, lthy20) = Local_Theory.note ((Binding.empty, + [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; + val _ = tracing "Finite Support"; + val supports = map (prove_supports lthy20 q_perm) consts; + val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); + val thy3 = Local_Theory.exit_global lthy20; + val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; + fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) + val lthy22 = Class.prove_instantiation_instance tac lthy21 + val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; + val (names, supp_eq_t) = supp_eq fv_alpha_all; + val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => []; + val lthy23 = note_suffix "supp" q_supp lthy22; +in + ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy23) +end +*} + + +ML {* +(* parsing the datatypes and declaring *) +(* constructors in the local theory *) +fun prepare_dts dt_strs lthy = +let + val thy = ProofContext.theory_of lthy + + fun mk_type full_tname tvrs = + Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs) + + fun prep_cnstr lthy full_tname tvs (cname, anno_tys, mx, _) = + let + val tys = map (Syntax.read_typ lthy o snd) anno_tys + val ty = mk_type full_tname tvs + in + ((cname, tys ---> ty, mx), (cname, tys, mx)) + end + + fun prep_dt lthy (tvs, tname, mx, cnstrs) = + let + val full_tname = Sign.full_name thy tname + val (cnstrs', cnstrs'') = + split_list (map (prep_cnstr lthy full_tname tvs) cnstrs) + in + (cnstrs', (tvs, tname, mx, cnstrs'')) + end + + val (cnstrs, dts) = + split_list (map (prep_dt lthy) dt_strs) +in + lthy + |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs)) + |> pair dts +end +*} + +ML {* +(* parsing the binding function specification and *) +(* declaring the functions in the local theory *) +fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy = +let + val ((bn_funs, bn_eqs), _) = + Specification.read_spec bn_fun_strs bn_eq_strs lthy + + fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) + val bn_funs' = map prep_bn_fun bn_funs +in + lthy + |> Local_Theory.theory (Sign.add_consts_i bn_funs') + |> pair (bn_funs', bn_eqs) +end +*} + +ML {* +fun find_all eq xs (k',i) = + maps (fn (k, (v1, v2)) => if eq (k, k') then [(v1, v2, i)] else []) xs +*} + +ML {* +(* associates every SOME with the index in the list; drops NONEs *) +fun mk_env xs = + let + fun mapp (_: int) [] = [] + | mapp i (a :: xs) = + case a of + NONE => mapp (i + 1) xs + | SOME x => (x, i) :: mapp (i + 1) xs + in mapp 0 xs end +*} + +ML {* +fun env_lookup xs x = + case AList.lookup (op =) xs x of + SOME x => x + | NONE => error ("cannot find " ^ x ^ " in the binding specification."); +*} + +ML {* +val recursive = Unsynchronized.ref false +val alpha_type = Unsynchronized.ref AlphaGen +*} + +ML {* +fun prepare_binds dt_strs lthy = +let + fun extract_annos_binds dt_strs = + map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs + + fun prep_bn env bn_str = + case (Syntax.read_term lthy bn_str) of + Free (x, _) => (NONE, env_lookup env x) + | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), !recursive), env_lookup env x) + | _ => error (bn_str ^ " not allowed as binding specification."); + + fun prep_typ env (i, opt_name) = + case opt_name of + NONE => [] + | SOME x => find_all (op=) env (x,i); + + (* annos - list of annotation for each type (either NONE or SOME fo a type *) + + fun prep_binds (annos, bind_strs) = + let + val env = mk_env annos (* for every label the index *) + val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs + in + map_index (prep_typ binds) annos + end + + val result = map (map (map (map (fn (a, b, c) => + (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) + (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) + + val _ = warning (@{make_string} result) + +in + result +end +*} + +ML {* +fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = +let + fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) + + val lthy0 = + Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy + val (dts, lthy1) = + prepare_dts dt_strs lthy0 + val ((bn_funs, bn_eqs), lthy2) = + prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 + val binds = prepare_binds dt_strs lthy2 +in + nominal_datatype2 dts bn_funs bn_eqs binds lthy |> snd +end +*} + + +(* Command Keyword *) + +ML {* +let + val kind = OuterKeyword.thy_decl +in + OuterSyntax.local_theory "nominal_datatype" "test" kind + (main_parser >> nominal_datatype2_cmd) +end +*} + + +end + + + diff -r 7ee9a2fefc77 -r 1bddffddc03f Nominal/Equivp.thy --- a/Nominal/Equivp.thy Sat May 01 09:15:46 2010 +0100 +++ b/Nominal/Equivp.thy Sun May 02 14:06:26 2010 +0100 @@ -1,5 +1,5 @@ theory Equivp -imports "Fv" +imports "NewFv" "Tacs" "Rsp" "NewFv" begin ML {* @@ -188,7 +188,7 @@ val rhs = list_comb (cnstr, frees) fun mk_supp_arg (x, ty) = - if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else + if is_atom thy ty then mk_supp @{typ atom} (mk_atom_ty ty x) else if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) else mk_supp ty x diff -r 7ee9a2fefc77 -r 1bddffddc03f Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Sat May 01 09:15:46 2010 +0100 +++ b/Nominal/Ex/Classical.thy Sun May 02 14:06:26 2010 +0100 @@ -1,5 +1,5 @@ theory Classical -imports "../Parser" +imports "../NewParser" begin (* example from my Urban's PhD *) @@ -8,7 +8,6 @@ alpha_trm_raw is incorrectly defined, therefore the equivalence proof does not go through; below the correct definition is given *) -ML {* val _ = cheat_equivp := true *} atom_decl name atom_decl coname @@ -20,7 +19,7 @@ | AndL1 n::"name" t::"trm" "name" bind n in t | AndL2 n::"name" t::"trm" "name" bind n in t | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 -| ImpR c::"coname" n::"name" t::"trm" "coname" bind n in t, bind c in t +| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t thm trm.fv diff -r 7ee9a2fefc77 -r 1bddffddc03f Nominal/Fv.thy --- a/Nominal/Fv.thy Sat May 01 09:15:46 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,652 +0,0 @@ -theory Fv -imports "../Nominal-General/Nominal2_Atoms" - "Abs" "Perm" "Rsp" "Nominal2_FSet" -begin - -(* The bindings data structure: - - Bindings are a list of lists of lists of triples. - - The first list represents the datatypes defined. - The second list represents the constructors. - The internal list is a list of all the bndings that - concern the constructor. - - Every triple consists of a function, the binding and - the body. - - Eg: -nominal_datatype - - C1 - | C2 x y z bind x in z - | C3 x y z bind f x in z bind g y in z - -yields: -[ - [], - [(NONE, 0, 2)], - [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]] - -A SOME binding has to have a function which takes an appropriate -argument and returns an atom set. A NONE binding has to be on an -argument that is an atom or an atom set. -*) - -(* -An overview of the generation of free variables: - -1) fv_bn functions are generated only for the non-recursive binds. - - An fv_bn for a constructor is a union of values for the arguments: - - For an argument x that is in the bn function - - if it is a recursive argument bn' we return: fv_bn' x - - otherwise empty - - For an argument x that is not in the bn function - - for atom we return: {atom x} - - for atom set we return: atom ` x - - for a recursive call to type ty' we return: fv_ty' x - with fv of the appropriate type - - otherwise empty - -2) fv_ty functions generated for all types being defined: - - fv_ty for a constructor is a union of values for the arguments. - - For an argument that is bound in a shallow binding we return empty. - - For an argument x that bound in a non-recursive deep binding - we return: fv_bn x. - - Otherwise we return the free variables of the argument minus the - bound variables of the argument. - - The free variables for an argument x are: - - for an atom: {atom x} - - for atom set: atom ` x - - for recursive call to type ty' return: fv_ty' x - - for nominal datatype ty' return: fv_ty' x - - The bound variables are a union of results of all bindings that - involve the given argument. For a paricular binding: - - - for a binding function bn: bn x - - for a recursive argument of type ty': fv_fy' x - - for nominal datatype ty' return: fv_ty' x -*) - -(* -An overview of the generation of alpha-equivalence: - -1) alpha_bn relations are generated for binding functions. - - An alpha_bn for a constructor is true if a conjunction of - propositions for each argument holds. - - For an argument a proposition is build as follows from - th: - - - for a recursive argument in the bn function, we return: alpha_bn argl argr - - for a recursive argument for type ty not in bn, we return: alpha_ty argl argr - - for other arguments in the bn function we return: True - - for other arguments not in the bn function we return: argl = argr - -2) alpha_ty relations are generated for all the types being defined: - - For each constructor we gather all the arguments that are bound, - and for each of those we add a permutation. We associate those - permutations with the bindings. Note that two bindings can have - the same permutation if the arguments being bound are the same. - - An alpha_ty for a constructor is true if there exist permutations - as above such that a conjunction of propositions for all arguments holds. - - For an argument we allow bindings where only one of the following - holds: - - - Argument is bound in some shallow bindings: We return true - - Argument of type ty is bound recursively in some other - arguments [i1, .. in] with one binding function bn. - We return: - - (bn argl, (argl, argl_i1, ..., argl_in)) \gen - \(argl,argl1,..,argln) (argr,argr1,..,argrn). - (alpha_ty argl argr) \ (alpha_i1 argl1 argr1) \ .. \ (alpha_in argln argrn) - \(arg,arg1,..,argn). (fv_ty arg) \ (fv_i1 arg1) \ .. \ (fv_in argn) - pi - (bn argr, (argr, argr_i1, ..., argr_in)) - - - Argument is bound in some deep non-recursive bindings. - We return: alpha_bn argl argr - - Argument of type ty has some shallow bindings [b1..bn] and/or - non-recursive bindings [f1 a1, .., fm am], where the bindings - have the permutations p1..pl. We return: - - (b1l \..\ bnl \ f1 a1l \..\ fn anl, argl) \gen - alpha_ty fv_ty (p1 +..+ pl) - (b1r \..\ bnr \ f1 a1r \..\ fn anr, argr) - - - Argument has some recursive bindings. The bindings were - already treated in 2nd case so we return: True - - Argument has no bindings and is not bound. - If it is recursive for type ty, we return: alpha_ty argl argr - Otherwise we return: argl = argr - -*) - -ML {* -datatype alpha_mode = 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 _ _ = false; - -fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t - | is_atom_fset _ _ = false; -*} - - -(* Like map2, only if the second list is empty passes empty lists insted of error *) -ML {* -fun map2i _ [] [] = [] - | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys - | map2i f (x :: xs) [] = f x [] :: map2i f xs [] - | map2i _ _ _ = raise UnequalLengths; -*} - -(* Finds bindings with the same function and binding, and gathers all - bodys for such pairs - *) -ML {* -fun gather_binds binds = -let - fun gather_binds_cons binds = - let - val common = map (fn (f, bi, _, aty) => (f, bi, aty)) binds - val nodups = distinct (op =) common - 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 -in - map (map gather_binds_cons) binds -end -*} - -ML {* -fun un_gather_binds_cons 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"}; - fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]; - fun mk_union sets = - fold (fn a => fn b => - if a = noatoms then b else - if b = noatoms then a else - if a = b then a else - HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; - val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf}) - fun mk_diff a b = - if b = noatoms then a else - if b = a then noatoms else - HOLogic.mk_binop @{const_name minus} (a, b); - fun mk_atom_set 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; - fun mk_atom_fset t = - let - val ty = fastype_of t; - val atom_ty = dest_fsetT ty --> @{typ atom}; - val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; - val fset_to_set = @{term "fset_to_set :: atom fset \ atom set"} - in - fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)) - end; - (* 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; -*} - -(* Given [fv1, fv2, fv3] creates %(x, y, z). fv1 x u fv2 y u fv3 z *) -ML {* -fun mk_compound_fv fvs = -let - val nos = (length fvs - 1) downto 0; - val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos); - val fvs_union = mk_union fvs_applied; - val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs); - fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t)) -in - fold fold_fun tys (Abs ("", tyh, fvs_union)) -end; -*} - -(* Given [R1, R2, R3] creates %(x,x'). %(y,y'). %(z,z'). R x x' \ R y y' \ R z z' *) -ML {* -fun mk_compound_alpha Rs = -let - val nos = (length Rs - 1) downto 0; - val nos2 = (2 * length Rs - 1) downto length Rs; - val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no) (Rs ~~ (nos2 ~~ nos)); - val Rs_conj = mk_conjl Rs_applied; - val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs); - fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t)) - val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj)) -in - fold fold_fun tys (Abs ("", tyh, abs_rhs)) -end; -*} - - -ML {* -fun non_rec_binds l = -let - fun is_non_rec (SOME (f, false), _, _, _) = SOME f - | is_non_rec _ = NONE -in - distinct (op =) (map_filter is_non_rec (flat (flat l))) -end -*} - -(* We assume no bindings in the type on which bn is defined *) -ML {* -fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) = -let - val {descr, sorts, ...} = dt_info; - fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); - fun fv_bn_constr (cname, dts) args_in_bn = - let - val Ts = map (typ_of_dtyp descr sorts) dts; - val names = Datatype_Prop.make_tnames Ts; - val args = map Free (names ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); - fun fv_arg ((dt, x), arg_no) = - let - val ty = fastype_of x -(* val _ = tracing ("B 1" ^ PolyML.makestring args_in_bn);*) -(* val _ = tracing ("B 2" ^ PolyML.makestring bn_fvbn);*) - in - case AList.lookup (op=) args_in_bn arg_no of - SOME NONE => @{term "{} :: atom set"} - | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x - | NONE => - if is_atom thy ty then mk_single_atom x else - if is_atom_set thy ty then mk_atom_set x else - if is_atom_fset thy ty then mk_atom_fset x else - if is_rec_type dt then nth fv_frees (body_index dt) $ x else - @{term "{} :: atom set"} - end; - val arg_nos = 0 upto (length dts - 1) - in - HOLogic.mk_Trueprop (HOLogic.mk_eq - (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) - end; - val (_, (_, _, constrs)) = nth descr ith_dtyp; - val eqs = map2i fv_bn_constr constrs args_in_bns -in - ((bn, fvbn), eqs) -end -*} - -ML {* print_depth 100 *} -ML {* -fun fv_bns thy dt_info fv_frees rel_bns = -let - fun mk_fvbn_free (bn, ith, _) = - let - val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); - in - (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) - end; - val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free rel_bns); - val bn_fvbn = (map (fn (bn, _, _) => bn) rel_bns) ~~ fvbn_frees - val (l1, l2) = split_list (map (fv_bn thy dt_info fv_frees bn_fvbn) (fvbn_frees ~~ rel_bns)); -in - (l1, (fvbn_names ~~ l2)) -end -*} - - -ML {* -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); - fun alpha_bn_constr (cname, dts) args_in_bn = - 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 ith_dtyp)); - val rhs = HOLogic.mk_Trueprop - (alpha_bn_free $ (list_comb (c, args)) $ (list_comb (c, args2))); - fun lhs_arg ((dt, arg_no), (arg, arg2)) = - 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) - in - eq - end - val (_, (_, _, constrs)) = nth descr ith_dtyp; - val eqs = map2i alpha_bn_constr constrs args_in_bns -in - ((bn, alpha_bn_free), eqs) -end -*} - -ML {* -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); - fun mk_alphabn_free (bn, ith, _) = - let - val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); - val alphabn_type = nth_dtyp ith --> nth_dtyp ith --> @{typ bool}; - val alphabn_free = Free(alphabn_name, alphabn_type); - in - (alphabn_name, alphabn_free) - 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 dt_info alpha_frees bn_alphabn) - (rel_bns ~~ (alphabn_frees ~~ bns_rec))) -in - (alphabn_names, pair) -end -*} - - -(* Checks that a list of bindings contains only compatible ones *) -ML {* -fun bns_same l = - length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1 -*} - -ML {* -fun setify x = - if fastype_of x = @{typ "atom list"} then - Const (@{const_name set}, @{typ "atom list \ atom set"}) $ x else x -*} - -ML {* -fun define_fv (dt_info : Datatype_Aux.info) bindsall bns lthy = -let - val thy = ProofContext.theory_of lthy; - val {descr, sorts, ...} = dt_info; - fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); - val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => - "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); -(* TODO: We need a transitive closure, but instead we do this hack considering - all binding functions as recursive or not *) - val nr_bns = - if (non_rec_binds bindsall) = [] then [] - else map (fn (bn, _, _) => bn) bns; - val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; - val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns; - val fvbns = map snd bn_fv_bns; - val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; - - fun fv_constr ith_dtyp (cname, dts) bindcs = - let - val Ts = map (typ_of_dtyp descr sorts) dts; - val bindslen = length bindcs - val pi_strs_same = replicate bindslen "pi" - val pi_strs = Name.variant_list [] pi_strs_same; - val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; - val bind_pis_gath = bindcs ~~ pis; - val bind_pis = un_gather_binds_cons bind_pis_gath; - val bindcs = map fst bind_pis; - val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); - val args = map Free (names ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); - val fv_c = nth fv_frees ith_dtyp; - val arg_nos = 0 upto (length dts - 1) - 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 goes the code for preiously defined nominal datatypes *) - @{term "{} :: atom set"} - | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) - fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant) - 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 - SOME f => - (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of - SOME fv_bn => fv_bn $ x - | NONE => error "bn specified in a non-rec binding but not in bn list") - | NONE => - let - val arg = - if is_rec_type dt then nth fv_frees (body_index dt) $ x else - if ((is_atom thy) o fastype_of) x then mk_single_atom x else - if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else - if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else - (* TODO goes the code for preiously defined nominal datatypes *) - @{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 sub = fv_binds_as_set args relevant - in - mk_diff arg sub - end; - val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq - (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) - in - fv_eq - end; - fun fv_eq (i, (_, _, constrs)) binds = map2i (fv_constr i) constrs binds; - val fveqs = map2i fv_eq descr (gather_binds bindsall) - val fv_eqs_perfv = fveqs - val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; - 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))) - val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); - val fv_names_all = fv_names_fst @ fv_bn_names; - val add_binds = map (fn x => (Attrib.empty_binding, x)) -(* Function_Fun.add_fun Function_Common.default_config ... true *) - val (fvs, lthy') = (Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) - val (fvs2, lthy'') = - if fv_eqs_snd = [] then (([], []), lthy') else - (Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') - val ordered_fvs = fv_frees @ fvbns; - val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) -in - ((all_fvs, ordered_fvs), lthy'') -end -*} - -ML {* -fun define_alpha (dt_info : Datatype_Aux.info) bindsall bns fv_frees lthy = -let - val thy = ProofContext.theory_of lthy; - val {descr, sorts, ...} = dt_info; - fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); -(* TODO: We need a transitive closure, but instead we do this hack considering - all binding functions as recursive or not *) - val nr_bns = - if (non_rec_binds bindsall) = [] then [] - else map (fn (bn, _, _) => bn) bns; - 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 (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) = - 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 alpha_constr ith_dtyp (cname, dts) bindcs = - let - val Ts = map (typ_of_dtyp descr sorts) dts; - val bindslen = length bindcs - val pi_strs_same = replicate bindslen "pi" - val pi_strs = Name.variant_list [] pi_strs_same; - val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; - val bind_pis_gath = bindcs ~~ pis; - val bind_pis = un_gather_binds_cons bind_pis_gath; - val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); - val args = map Free (names ~~ Ts); - val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); - val args2 = map Free (names2 ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); - val alpha = nth alpha_frees ith_dtyp; - val arg_nos = 0 upto (length dts - 1) - 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 goes the code for preiously defined nominal datatypes *) - @{term "{} :: atom set"} - | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) - fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) - val alpha_rhs = - 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 - | _ => 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 - ([], [], [], []) => - if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) - else (HOLogic.mk_eq (arg, arg2)) - | (_, [], [], []) => @{term True} - | ([], [], [], _) => @{term True} - | ([], ((((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_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; - val lhs_binds = fv_binds args rbinds - val lhs_arg = foldr1 HOLogic.mk_prod bound_args - val lhs = mk_pair (lhs_binds, lhs_arg); - val rhs_binds = fv_binds args2 rbinds; - val rhs_arg = foldr1 HOLogic.mk_prod bound_args2; - val rhs = mk_pair (rhs_binds, rhs_arg); - val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos); - val fv = mk_compound_fv fvs; - val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); - val alpha = mk_compound_alpha alphas; - val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis); - 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 - end - else - let - val alpha_bn_const = - nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) - in - alpha_bn_const $ arg $ arg2 - end - | ([], [], relevant, []) => - let - val (rbinds, rpis) = split_list relevant - val lhs_binds = fv_binds args rbinds - val lhs = mk_pair (lhs_binds, arg); - val rhs_binds = fv_binds args2 rbinds; - val rhs = mk_pair (rhs_binds, arg2); - val alpha = nth alpha_frees (body_index dt); - val fv = nth fv_frees (body_index dt); - val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis); - 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 - 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 - val alpha_lhss_ex = - fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss - val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) - in - alpha_eq - end; - fun alpha_eq (i, (_, _, constrs)) binds = map2i (alpha_constr i) constrs binds; - val alphaeqs = map2i alpha_eq descr (gather_binds bindsall) - val alpha_eqs = flat alphaeqs - val add_binds = map (fn x => (Attrib.empty_binding, x)) - 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_bn_names) - (alpha_types @ alpha_bn_types)) [] - (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy) -in - (alphas, lthy') -end -*} - -end diff -r 7ee9a2fefc77 -r 1bddffddc03f Nominal/Lift.thy --- a/Nominal/Lift.thy Sat May 01 09:15:46 2010 +0100 +++ b/Nominal/Lift.thy Sun May 02 14:06:26 2010 +0100 @@ -2,7 +2,7 @@ imports "../Nominal-General/Nominal2_Atoms" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Abs" "Perm" "Equivp" "Rsp" + "Abs" "Perm" "Equivp" "Rsp" "Attic/Fv" begin @@ -66,6 +66,9 @@ end *} + + + ML {* fun define_fv_alpha_export dt binds bns ctxt = let diff -r 7ee9a2fefc77 -r 1bddffddc03f Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sat May 01 09:15:46 2010 +0100 +++ b/Nominal/NewParser.thy Sun May 02 14:06:26 2010 +0100 @@ -258,9 +258,78 @@ end *} + +text {* + nominal_datatype2 does the following things in order: + +Parser.thy/raw_nominal_decls + 1) define the raw datatype + 2) define the raw binding functions + +Perm.thy/define_raw_perms + 3) define permutations of the raw datatype and show that the raw type is + in the pt typeclass + +Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha + 4) define fv and fv_bn + 5) define alpha and alpha_bn + +Perm.thy/distinct_rel + 6) prove alpha_distincts (C1 x \ C2 y ...) (Proof by cases; simp) + +Tacs.thy/build_rel_inj + 6) prove alpha_eq_iff (C1 x = C2 y \ P x y ...) + (left-to-right by intro rule, right-to-left by cases; simp) +Equivp.thy/prove_eqvt + 7) prove bn_eqvt (common induction on the raw datatype) + 8) prove fv_eqvt (common induction on the raw datatype with help of above) +Rsp.thy/build_alpha_eqvts + 9) prove alpha_eqvt and alpha_bn_eqvt + (common alpha-induction, unfolding alpha_gen, permute of #* and =) +Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps + 10) prove that alpha and alpha_bn are equivalence relations + (common induction and application of 'compose' lemmas) +Lift.thy/define_quotient_types + 11) define quotient types +Rsp.thy/build_fvbv_rsps + 12) prove bn respects (common induction and simp with alpha_gen) +Rsp.thy/prove_const_rsp + 13) prove fv respects (common induction and simp with alpha_gen) + 14) prove permute respects (unfolds to alpha_eqvt) +Rsp.thy/prove_alpha_bn_rsp + 15) prove alpha_bn respects + (alpha_induct then cases then sym and trans of the relations) +Rsp.thy/prove_alpha_alphabn + 16) show that alpha implies alpha_bn (by unduction, needed in following step) +Rsp.thy/prove_const_rsp + 17) prove respects for all datatype constructors + (unfold eq_iff and alpha_gen; introduce zero permutations; simp) +Perm.thy/quotient_lift_consts_export + 18) define lifted constructors, fv, bn, alpha_bn, permutations +Perm.thy/define_lifted_perms + 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass +Lift.thy/lift_thm + 20) lift permutation simplifications + 21) lift induction + 22) lift fv + 23) lift bn + 24) lift eq_iff + 25) lift alpha_distincts + 26) lift fv and bn eqvts +Equivp.thy/prove_supports + 27) prove that union of arguments supports constructors +Equivp.thy/prove_fs + 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) +Equivp.thy/supp_eq + 29) prove supp = fv +*} + + ML {* fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = let + + (* definition of the raw datatype and raw bn-functions *) val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = raw_nominal_decls dts bn_funs bn_eqs bclauses lthy @@ -279,6 +348,7 @@ val induct = #induct dtinfo; val exhausts = map #exhaust dtinfos; + (* definitions of raw permutations *) val ((raw_perm_def, raw_perm_simps, perms), lthy2) = Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; @@ -579,6 +649,8 @@ (main_parser >> nominal_datatype2_cmd) *} + +(* atom_decl name nominal_datatype lam = @@ -658,21 +730,24 @@ thm ty_tys.fv[simplified ty_tys.supp] thm ty_tys.eq_iff +*) + (* some further tests *) -nominal_datatype ty = - Vr "name" -| Fn "ty" "ty" +(* +nominal_datatype ty2 = + Vr2 "name" +| Fn2 "ty2" "ty2" -nominal_datatype tys = - All xs::"name fset" ty::"ty_raw" bind_res xs in ty +nominal_datatype tys2 = + All2 xs::"name fset" ty::"ty2" bind_res xs in ty nominal_datatype lam2 = Var2 "name" | App2 "lam2" "lam2 list" | Lam2 x::"name" t::"lam2" bind x in t - +*) diff -r 7ee9a2fefc77 -r 1bddffddc03f Nominal/Parser.thy --- a/Nominal/Parser.thy Sat May 01 09:15:46 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,670 +0,0 @@ -theory Parser -imports "../Nominal-General/Nominal2_Atoms" - "../Nominal-General/Nominal2_Eqvt" - "../Nominal-General/Nominal2_Supp" - "Perm" "Equivp" "Rsp" "Lift" -begin - -section{* Interface for nominal_datatype *} - -text {* - -Nominal-Datatype-part: - - -1nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - type(s) to be defined constructors list - (ty args, name, syn) (name, typs, syn) - -Binder-Function-part: - -2rd Arg: (binding * typ option * mixfix) list - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - binding function(s) - to be defined - (name, type, syn) - -3th Arg: term list - ^^^^^^^^^ - the equations of the binding functions - (Trueprop equations) -*} - -ML {* - -*} - -text {*****************************************************} -ML {* -(* nominal datatype parser *) -local - structure P = OuterParse - - fun tuple ((x, y, z), u) = (x, y, z, u) - fun tswap (((x, y), z), u) = (x, y, u, z) -in - -val _ = OuterKeyword.keyword "bind" -val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ - -(* binding specification *) -(* maybe use and_list *) -val bind_parser = - P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name) >> swap) - -val constr_parser = - P.binding -- Scan.repeat anno_typ - -(* datatype parser *) -val dt_parser = - (P.type_args -- P.binding -- P.opt_mixfix >> P.triple1) -- - (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> tswap)) >> tuple - -(* function equation parser *) -val fun_parser = - Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) - -(* main parser *) -val main_parser = - (P.and_list1 dt_parser) -- fun_parser >> P.triple2 - -end -*} - -(* adds "_raw" to the end of constants and types *) -ML {* -fun add_raw s = s ^ "_raw" -fun add_raws ss = map add_raw ss -fun raw_bind bn = Binding.suffix_name "_raw" bn - -fun replace_str ss s = - case (AList.lookup (op=) ss s) of - SOME s' => s' - | NONE => s - -fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) - | replace_typ ty_ss T = T - -fun raw_dts ty_ss dts = -let - - fun raw_dts_aux1 (bind, tys, mx) = - (raw_bind bind, map (replace_typ ty_ss) tys, mx) - - fun raw_dts_aux2 (ty_args, bind, mx, constrs) = - (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) -in - map raw_dts_aux2 dts -end - -fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) - | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T) - | replace_aterm trm_ss trm = trm - -fun replace_term trm_ss ty_ss trm = - trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) -*} - -ML {* -fun get_cnstrs dts = - map (fn (_, _, _, constrs) => constrs) dts - -fun get_typed_cnstrs dts = - flat (map (fn (_, bn, _, constrs) => - (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) - -fun get_cnstr_strs dts = - map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) - -fun get_bn_fun_strs bn_funs = - map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs -*} - -ML {* -fun rawify_dts dt_names dts dts_env = -let - val raw_dts = raw_dts dts_env dts - val raw_dt_names = add_raws dt_names -in - (raw_dt_names, raw_dts) -end -*} - -ML {* -fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = -let - val bn_funs' = map (fn (bn, ty, mx) => - (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs - - val bn_eqs' = map (fn (attr, trm) => - (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs -in - (bn_funs', bn_eqs') -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, aty) => - (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j, aty))))) binds -*} - -ML {* -fun find [] _ = error ("cannot find element") - | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y -*} - -ML {* -fun strip_bn_fun t = - case t of - Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r - | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r - | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => - (i, NONE) :: strip_bn_fun y - | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => - (i, NONE) :: strip_bn_fun y - | Const (@{const_name bot}, _) => [] - | Const (@{const_name Nil}, _) => [] - | (f as Free _) $ Bound i => [(i, SOME f)] - | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t)) -*} - -ML {* -fun prep_bn dt_names dts eqs = -let - fun aux eq = - let - val (lhs, rhs) = eq - |> strip_qnt_body "all" - |> HOLogic.dest_Trueprop - |> HOLogic.dest_eq - val (bn_fun, [cnstr]) = strip_comb lhs - val (_, ty) = dest_Free bn_fun - val (ty_name, _) = dest_Type (domain_type ty) - val dt_index = find_index (fn x => x = ty_name) dt_names - val (cnstr_head, cnstr_args) = strip_comb cnstr - val rhs_elements = strip_bn_fun rhs - val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements - in - (dt_index, (bn_fun, (cnstr_head, included))) - end - fun order dts i ts = - let - val dt = nth dts i - val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) - val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts - in - map (find ts') cts - end - - val unordered = AList.group (op=) (map aux eqs) - val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered - val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' -in - ordered -end -*} - -ML {* -fun add_primrec_wrapper funs eqs lthy = - if null funs then (([], []), lthy) - else - let - val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs - val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs - in - Primrec.add_primrec funs' eqs' lthy - end -*} - -ML {* -fun add_datatype_wrapper dt_names dts = -let - val conf = Datatype.default_config -in - Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts) -end -*} - -ML {* -fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = -let - val thy = ProofContext.theory_of lthy - val thy_name = Context.theory_name thy - - val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts - val dt_full_names = map (Long_Name.qualify thy_name) dt_names - val dt_full_names' = add_raws dt_full_names - val dts_env = dt_full_names ~~ dt_full_names' - - val cnstrs = get_cnstr_strs dts - val cnstrs_ty = get_typed_cnstrs dts - val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs - val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name - (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty - val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' - - val bn_fun_strs = get_bn_fun_strs bn_funs - val bn_fun_strs' = add_raws bn_fun_strs - val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' - val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) - (bn_fun_strs ~~ bn_fun_strs') - - val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env - - val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs - - val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds - - val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) - -(*val _ = tracing (cat_lines (map PolyML.makestring raw_bns))*) -in - lthy - |> add_datatype_wrapper raw_dt_names raw_dts - ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs - ||>> pair raw_binds - ||>> pair raw_bns -end -*} - -lemma equivp_hack: "equivp x" -sorry -ML {* -fun equivp_hack ctxt rel = -let - val thy = ProofContext.theory_of ctxt - val ty = domain_type (fastype_of rel) - val cty = ctyp_of thy ty - val ct = cterm_of thy rel -in - Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} -end -*} - -ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} -ML {* val cheat_equivp = Unsynchronized.ref false *} -ML {* val cheat_fv_rsp = Unsynchronized.ref false *} -ML {* val cheat_const_rsp = Unsynchronized.ref false *} - -(* nominal_datatype2 does the following things in order: - -Parser.thy/raw_nominal_decls - 1) define the raw datatype - 2) define the raw binding functions - -Perm.thy/define_raw_perms - 3) define permutations of the raw datatype and show that the raw type is - in the pt typeclass - -Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha - 4) define fv and fv_bn - 5) define alpha and alpha_bn - -Perm.thy/distinct_rel - 6) prove alpha_distincts (C1 x \ C2 y ...) (Proof by cases; simp) - -Tacs.thy/build_rel_inj - 6) prove alpha_eq_iff (C1 x = C2 y \ P x y ...) - (left-to-right by intro rule, right-to-left by cases; simp) -Equivp.thy/prove_eqvt - 7) prove bn_eqvt (common induction on the raw datatype) - 8) prove fv_eqvt (common induction on the raw datatype with help of above) -Rsp.thy/build_alpha_eqvts - 9) prove alpha_eqvt and alpha_bn_eqvt - (common alpha-induction, unfolding alpha_gen, permute of #* and =) -Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps - 10) prove that alpha and alpha_bn are equivalence relations - (common induction and application of 'compose' lemmas) -Lift.thy/define_quotient_types - 11) define quotient types -Rsp.thy/build_fvbv_rsps - 12) prove bn respects (common induction and simp with alpha_gen) -Rsp.thy/prove_const_rsp - 13) prove fv respects (common induction and simp with alpha_gen) - 14) prove permute respects (unfolds to alpha_eqvt) -Rsp.thy/prove_alpha_bn_rsp - 15) prove alpha_bn respects - (alpha_induct then cases then sym and trans of the relations) -Rsp.thy/prove_alpha_alphabn - 16) show that alpha implies alpha_bn (by unduction, needed in following step) -Rsp.thy/prove_const_rsp - 17) prove respects for all datatype constructors - (unfold eq_iff and alpha_gen; introduce zero permutations; simp) -Perm.thy/quotient_lift_consts_export - 18) define lifted constructors, fv, bn, alpha_bn, permutations -Perm.thy/define_lifted_perms - 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass -Lift.thy/lift_thm - 20) lift permutation simplifications - 21) lift induction - 22) lift fv - 23) lift bn - 24) lift eq_iff - 25) lift alpha_distincts - 26) lift fv and bn eqvts -Equivp.thy/prove_supports - 27) prove that union of arguments supports constructors -Equivp.thy/prove_fs - 28) show that the lifted type is in fs typeclass (* by q_induct, supports *) -Equivp.thy/supp_eq - 29) prove supp = fv -*) -ML {* -fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = -let - val _ = tracing "Raw declarations"; - val thy = ProofContext.theory_of lthy - val thy_name = Context.theory_name thy - 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 (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 - val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc - - val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); - val {descr, sorts, ...} = dtinfo; - fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); - val raw_tys = map (fn (i, _) => nth_dtyp i) descr; - val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) - val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; - val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; - val rel_dtinfos = List.take (dtinfos, (length dts)); - val inject = flat (map #inject dtinfos); - val distincts = flat (map #distinct dtinfos); - val rel_distinct = map #distinct rel_dtinfos; - val induct = #induct dtinfo; - val exhausts = map #exhaust dtinfos; - val _ = tracing "Defining permutations, fv and alpha"; - val ((raw_perm_def, raw_perm_simps, perms), lthy3) = - Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; - val raw_binds_flat = map (map flat) raw_binds; - val ((((_, fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = - define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; - val (fv, fvbn) = chop (length perms) fv_ts; - - val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts - val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); - val bn_tys = map (domain_type o fastype_of) raw_bn_funs; - val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; - val bns = raw_bn_funs ~~ bn_nos; - val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) - (rel_distinct ~~ alpha_ts_nobn)); - val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) - ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) - val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 - val _ = tracing "Proving equivariance"; - val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 - val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 - fun alpha_eqvt_tac' _ = - if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy - else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1 - val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; - val _ = tracing "Proving equivalence"; - val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; - val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; - val alpha_equivp = - if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn - else build_equivps alpha_ts reflps alpha_induct - inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; - val qty_binds = map (fn (_, b, _, _) => b) dts; - val qty_names = map Name.of_binding qty_binds; - val qty_full_names = map (Long_Name.qualify thy_name) qty_names - val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; - val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); - val raw_consts = - flat (map (fn (i, (_, _, l)) => - map (fn (cname, dts) => - Const (cname, map (typ_of_dtyp descr sorts) dts ---> - typ_of_dtyp descr sorts (DtRec i))) l) descr); - val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; - val _ = tracing "Proving respects"; - val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; - val (bns_rsp_pre, lthy9) = fold_map ( - fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => - resolve_tac bns_rsp_pre' 1)) bns lthy8; - val bns_rsp = flat (map snd bns_rsp_pre); - fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy - else fvbv_rsp_tac alpha_induct fv_def lthy8 1; - val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; - val (fv_rsp_pre, lthy10) = fold_map - (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] - (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; - val fv_rsp = flat (map snd fv_rsp_pre); - val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms - (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; - val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11; - val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] - (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11 -(* val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*) - fun const_rsp_tac _ = - if !cheat_const_rsp then Skip_Proof.cheat_tac thy - else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a - in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end - val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] - const_rsp_tac) raw_consts lthy11a - val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) - val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; - val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; - val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs - val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; - val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn - val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; - val _ = tracing "Lifting permutations"; - val thy = Local_Theory.exit_global lthy12c; - val perm_names = map (fn x => "permute_" ^ x) qty_names - val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy; - val lthy13 = Theory_Target.init NONE thy'; - val q_name = space_implode "_" qty_names; - fun suffix_bind s = Binding.qualify true q_name (Binding.name s); - val _ = tracing "Lifting induction"; - val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; - val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct); - fun note_suffix s th ctxt = - snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); - fun note_simp_suffix s th ctxt = - snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); - val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", - [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; - val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct - val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; - val q_perm = map (lift_thm qtys lthy14) raw_perm_def; - val lthy15 = note_simp_suffix "perm" q_perm lthy14a; - val q_fv = map (lift_thm qtys lthy15) fv_def; - val lthy16 = note_simp_suffix "fv" q_fv lthy15; - val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; - val lthy17 = note_simp_suffix "bn" q_bn lthy16; - val _ = tracing "Lifting eq-iff"; - val _ = map tracing (map PolyML.makestring alpha_eq_iff); - val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff - val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 - val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 - val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; - val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 - val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 - val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 - val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; - val q_dis = map (lift_thm qtys lthy18) rel_dists; - val lthy19 = note_simp_suffix "distinct" q_dis lthy18; - val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); - val (_, lthy20) = Local_Theory.note ((Binding.empty, - [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; - val _ = tracing "Finite Support"; - val supports = map (prove_supports lthy20 q_perm) consts; - val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); - val thy3 = Local_Theory.exit_global lthy20; - val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; - fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) - val lthy22 = Class.prove_instantiation_instance tac lthy21 - val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; - val (names, supp_eq_t) = supp_eq fv_alpha_all; - val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => []; - val lthy23 = note_suffix "supp" q_supp lthy22; -in - ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy23) -end -*} - - -ML {* -(* parsing the datatypes and declaring *) -(* constructors in the local theory *) -fun prepare_dts dt_strs lthy = -let - val thy = ProofContext.theory_of lthy - - fun mk_type full_tname tvrs = - Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs) - - fun prep_cnstr lthy full_tname tvs (cname, anno_tys, mx, _) = - let - val tys = map (Syntax.read_typ lthy o snd) anno_tys - val ty = mk_type full_tname tvs - in - ((cname, tys ---> ty, mx), (cname, tys, mx)) - end - - fun prep_dt lthy (tvs, tname, mx, cnstrs) = - let - val full_tname = Sign.full_name thy tname - val (cnstrs', cnstrs'') = - split_list (map (prep_cnstr lthy full_tname tvs) cnstrs) - in - (cnstrs', (tvs, tname, mx, cnstrs'')) - end - - val (cnstrs, dts) = - split_list (map (prep_dt lthy) dt_strs) -in - lthy - |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs)) - |> pair dts -end -*} - -ML {* -(* parsing the binding function specification and *) -(* declaring the functions in the local theory *) -fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy = -let - val ((bn_funs, bn_eqs), _) = - Specification.read_spec bn_fun_strs bn_eq_strs lthy - - fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) - val bn_funs' = map prep_bn_fun bn_funs -in - lthy - |> Local_Theory.theory (Sign.add_consts_i bn_funs') - |> pair (bn_funs', bn_eqs) -end -*} - -ML {* -fun find_all eq xs (k',i) = - maps (fn (k, (v1, v2)) => if eq (k, k') then [(v1, v2, i)] else []) xs -*} - -ML {* -(* associates every SOME with the index in the list; drops NONEs *) -fun mk_env xs = - let - fun mapp (_: int) [] = [] - | mapp i (a :: xs) = - case a of - NONE => mapp (i + 1) xs - | SOME x => (x, i) :: mapp (i + 1) xs - in mapp 0 xs end -*} - -ML {* -fun env_lookup xs x = - case AList.lookup (op =) xs x of - SOME x => x - | NONE => error ("cannot find " ^ x ^ " in the binding specification."); -*} - -ML {* -val recursive = Unsynchronized.ref false -val alpha_type = Unsynchronized.ref AlphaGen -*} - -ML {* -fun prepare_binds dt_strs lthy = -let - fun extract_annos_binds dt_strs = - map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs - - fun prep_bn env bn_str = - case (Syntax.read_term lthy bn_str) of - Free (x, _) => (NONE, env_lookup env x) - | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), !recursive), env_lookup env x) - | _ => error (bn_str ^ " not allowed as binding specification."); - - fun prep_typ env (i, opt_name) = - case opt_name of - NONE => [] - | SOME x => find_all (op=) env (x,i); - - (* annos - list of annotation for each type (either NONE or SOME fo a type *) - - fun prep_binds (annos, bind_strs) = - let - val env = mk_env annos (* for every label the index *) - val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs - in - map_index (prep_typ binds) annos - end - - val result = map (map (map (map (fn (a, b, c) => - (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) - (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) - - val _ = warning (@{make_string} result) - -in - result -end -*} - -ML {* -fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = -let - fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) - - val lthy0 = - Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy - val (dts, lthy1) = - prepare_dts dt_strs lthy0 - val ((bn_funs, bn_eqs), lthy2) = - prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 - val binds = prepare_binds dt_strs lthy2 -in - nominal_datatype2 dts bn_funs bn_eqs binds lthy |> snd -end -*} - - -(* Command Keyword *) - -ML {* -let - val kind = OuterKeyword.thy_decl -in - OuterSyntax.local_theory "nominal_datatype" "test" kind - (main_parser >> nominal_datatype2_cmd) -end -*} - - -end - - -