# HG changeset patch # User Christian Urban # Date 1274387033 -3600 # Node ID 3b83960f95446a1389b3bbb34514d4eeebdf1642 # Parent a5dc3558cdecbbc8312309e5c7b2a34f3b27b2f8 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files diff -r a5dc3558cdec -r 3b83960f9544 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Wed May 19 12:44:03 2010 +0100 +++ b/Nominal-General/nominal_library.ML Thu May 20 21:23:53 2010 +0100 @@ -6,6 +6,8 @@ signature NOMINAL_LIBRARY = sig + val dest_listT: typ -> typ + val mk_minus: term -> term val mk_plus: term -> term -> term @@ -25,12 +27,25 @@ val mk_equiv: thm -> thm val safe_mk_equiv: thm -> thm + + (* datatype operations *) + val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ + val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> + (term * typ * typ list) list list + val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> + (term * typ * typ list) list + val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list + end structure Nominal_Library: NOMINAL_LIBRARY = struct +(* this function should be in hologic.ML *) +fun dest_listT (Type (@{type_name list}, [T])) = T + | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) + fun mk_minus p = @{term "uminus::perm => perm"} $ p; fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q; @@ -59,6 +74,49 @@ fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; +(** datatypes **) + + +(* returns the type of the nth datatype *) +fun nth_dtyp descr sorts n = + Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); + +(* returns info about constructors in a datatype *) +fun all_dtyp_constrs_info descr = + map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr + +(* returns the constants of the constructors plus the + corresponding type and types of arguments *) +fun all_dtyp_constrs_types descr sorts = +let + fun aux ((ty_name, vs), (cname, args)) = + let + val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs + val ty = Type (ty_name, vs_tys) + val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args + in + (Const (cname, arg_tys ---> ty), ty, arg_tys) + end +in + map (map aux) (all_dtyp_constrs_info descr) +end + +fun nth_dtyp_constrs_types descr sorts n = + nth (all_dtyp_constrs_types descr sorts) n + + +(* generates for every datatype a name str ^ dt_name + plus and index for multiple occurences of a string *) +fun prefix_dt_names descr sorts str = +let + fun get_nth_name (i, _) = + Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) +in + Datatype_Prop.indexify_names + (map (prefix str o get_nth_name) descr) +end + + end (* structure *) open Nominal_Library; \ No newline at end of file diff -r a5dc3558cdec -r 3b83960f9544 Nominal/Equivp.thy --- a/Nominal/Equivp.thy Wed May 19 12:44:03 2010 +0100 +++ b/Nominal/Equivp.thy Thu May 20 21:23:53 2010 +0100 @@ -194,7 +194,7 @@ else mk_supp ty x val lhss = map mk_supp_arg (frees ~~ tys) val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) - val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) + val eq = HOLogic.mk_Trueprop (supports $ fold_union lhss $ rhs) in (names, eq) end @@ -203,7 +203,7 @@ ML {* fun prove_supports ctxt perms cnst = let - val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst + val (names, eq) = mk_supports_eq ctxt cnst in Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) end diff -r a5dc3558cdec -r 3b83960f9544 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Wed May 19 12:44:03 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Thu May 20 21:23:53 2010 +0100 @@ -4,6 +4,9 @@ atom_decl name +ML {* print_depth 50 *} +declare [[STEPS = 19]] + nominal_datatype trm = Var "name" | App "trm" "trm" @@ -16,6 +19,8 @@ where "bn (As x t) = {atom x}" +thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] + ML {* Inductive.the_inductive *} thm trm_assg.fv thm trm_assg.supp @@ -26,8 +31,10 @@ thm trm_assg.inducts thm trm_assg.distinct ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} + +(* TEMPORARY thm trm_assg.fv[simplified trm_assg.supp(1-2)] - +*) diff -r a5dc3558cdec -r 3b83960f9544 Nominal/Ex/Test.thy --- a/Nominal/Ex/Test.thy Wed May 19 12:44:03 2010 +0100 +++ b/Nominal/Ex/Test.thy Thu May 20 21:23:53 2010 +0100 @@ -13,6 +13,7 @@ thm fv_trm_raw.simps[no_vars] *) + (* This file contains only the examples that are not supposed to work yet. *) @@ -29,7 +30,6 @@ | Ap "trm" "trm list" | Lm x::"name" t::"trm" bind x in t - (* thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] diff -r a5dc3558cdec -r 3b83960f9544 Nominal/NewAlpha.thy --- a/Nominal/NewAlpha.thy Wed May 19 12:44:03 2010 +0100 +++ b/Nominal/NewAlpha.thy Thu May 20 21:23:53 2010 +0100 @@ -1,7 +1,18 @@ theory NewAlpha -imports "NewFv" +imports "Abs" "Perm" "Nominal2_FSet" +uses ("nominal_dt_rawperm.ML") + ("nominal_dt_rawfuns.ML") begin +use "nominal_dt_rawperm.ML" +use "nominal_dt_rawfuns.ML" + +ML {* +open Nominal_Dt_RawPerm +open Nominal_Dt_RawFuns +*} + + ML {* fun mk_binop2 ctxt s (l, r) = Syntax.check_term ctxt (Const (s, dummyT) $ l $ r) @@ -16,17 +27,16 @@ fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn alpha_const binds bodys = let - val thy = ProofContext.theory_of lthy; - fun bind_set args (NONE, no) = setify thy (nth args no) + fun bind_set args (NONE, no) = setify lthy (nth args no) | bind_set args (SOME f, no) = f $ (nth args no) - fun bind_lst args (NONE, no) = listify thy (nth args no) + fun bind_lst args (NONE, no) = listify lthy (nth args no) | bind_lst args (SOME f, no) = f $ (nth args no) fun append (t1, t2) = Const(@{const_name append}, @{typ "atom list \ atom list \ atom list"}) $ t1 $ t2; fun binds_fn args nos = if alpha_const = @{const_name alpha_lst} then foldr1 append (map (bind_lst args) nos) - else mk_union (map (bind_set args) nos); + else fold_union (map (bind_set args) nos); val lhs_binds = binds_fn args binds; val rhs_binds = binds_fn args2 binds; val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys); @@ -64,7 +74,7 @@ ML {* fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm = case bm of - BEmy i => + BC (_, [], [i]) => let val arg = nth args i; val arg2 = nth args2 i; @@ -77,11 +87,11 @@ | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2] | SOME NONE => [] end -| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees +| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn @{const_name alpha_lst} x y -| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees +| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn @{const_name alpha_gen} x y -| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees +| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn @{const_name alpha_res} x y *} @@ -137,7 +147,7 @@ ML {* fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm = case bm of - BEmy i => + BC (_, [], [i]) => let val arg = nth args i; val arg2 = nth args2 i; @@ -147,11 +157,11 @@ then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2] else [HOLogic.mk_eq (arg, arg2)] end -| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees +| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn @{const_name alpha_lst} x y -| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees +| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn @{const_name alpha_gen} x y -| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees +| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn @{const_name alpha_res} x y *} diff -r a5dc3558cdec -r 3b83960f9544 Nominal/NewFv.thy --- a/Nominal/NewFv.thy Wed May 19 12:44:03 2010 +0100 +++ b/Nominal/NewFv.thy Thu May 20 21:23:53 2010 +0100 @@ -4,38 +4,42 @@ begin ML {* -(* binding modes *) +(* binding modes and binding clauses *) -datatype bmodes = - BEmy of int -| BLst of ((term option * int) list) * (int list) -| BSet of ((term option * int) list) * (int list) -| BRes of ((term option * int) list) * (int list) +datatype bmode = Lst | Res | Set + +datatype bclause = + BC of bmode * (term option * int) list * int list *} ML {* -fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x]; - -val noatoms = @{term "{} :: atom set"}; +fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} + | mk_diff (t1, @{term "{}::atom set"}) = t1 + | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) -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; +fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} + | mk_union (t1 , @{term "{}::atom set"}) = t1 + | mk_union (@{term "{}::atom set"}, t2) = t2 + | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2) + +fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} *} ML {* -fun is_atom thy ty = - Sign.of_sort thy (ty, @{sort at_base}) +fun is_atom ctxt ty = + Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) -fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t +fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t | is_atom_set _ _ = false; -fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t +fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t | is_atom_fset _ _ = false; +fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t + | is_atom_list _ _ = false +*} + +ML {* fun mk_atom_set t = let val ty = fastype_of t; @@ -55,23 +59,6 @@ fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) end; -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); -*} - -ML {* -fun is_atom_list (Type (@{type_name list}, [T])) = true - | is_atom_list _ = false -*} - -ML {* -fun dest_listT (Type (@{type_name list}, [T])) = T - | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) -*} - -ML {* fun mk_atom_list t = let val ty = fastype_of t; @@ -83,191 +70,170 @@ *} ML {* -fun setify thy t = +fun setify ctxt t = let val ty = fastype_of t; in - if is_atom thy ty - then mk_singleton_atom t - else if is_atom_set thy ty + if is_atom ctxt ty + then HOLogic.mk_set @{typ atom} [mk_atom t] + else if is_atom_set ctxt ty then mk_atom_set t - else if is_atom_fset thy ty + else if is_atom_fset ctxt ty then mk_atom_fset t else error ("setify" ^ (PolyML.makestring (t, ty))) end *} ML {* -fun listify thy t = +fun listify ctxt t = let val ty = fastype_of t; in - if is_atom thy ty + if is_atom ctxt ty then HOLogic.mk_list @{typ atom} [mk_atom t] - else if is_atom_list ty + else if is_atom_list ctxt ty then mk_atom_set t else error "listify" end *} ML {* -fun set x = +fun to_set x = if fastype_of x = @{typ "atom list"} then @{term "set::atom list \ atom set"} $ x else x *} ML {* -fun fv_body thy dts args fv_frees supp i = +fun make_body fv_map args i = let - val x = nth args i; - val dt = nth dts i; + val arg = nth args i + val ty = fastype_of arg in - if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) $ x - else (if supp then mk_supp x else setify thy x) -end + case (AList.lookup (op=) fv_map ty) of + NONE => mk_supp arg + | SOME fv => fv $ arg +end *} ML {* -fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = +fun make_binder lthy fv_bn_map args (bn_option, i) = let - val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys) - fun bound_var (SOME bn, i) = set (bn $ nth args i) - | bound_var (NONE, i) = fv_body thy dts args fv_frees false i - val bound_vars = mk_union (map bound_var binds); - fun non_rec_var (SOME bn, i) = - if member (op =) bodys i - then noatoms - else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i) - | non_rec_var (NONE, _) = noatoms + val arg = nth args i in - mk_union ((mk_diff fv_bodys bound_vars) :: (map non_rec_var binds)) + case bn_option of + NONE => (setify lthy arg, @{term "{}::atom set"}) + | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) +end +*} + +ML {* +fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = +let + val t1 = map (make_body fv_map args) bodies + val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders) +in + fold_union (mk_diff (fold_union t1, fold_union t2)::t3) end *} ML {* -fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm = -case bm of - BEmy i => - let - val x = nth args i; - val dt = nth dts i; - in - case AList.lookup (op=) args_in_bn i of - NONE => if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) $ x - else mk_supp x - | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x - | SOME NONE => noatoms - end -| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -*} - -ML {* -fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bclausess (fvbn, (_, ith_dtyp, args_in_bns)) = +fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = let - fun fv_bn_constr (cname, dts) (args_in_bn, bclauses) = - let - val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; - val names = Datatype_Prop.make_tnames Ts; - val args = map Free (names ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp)); - val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn - in - HOLogic.mk_Trueprop (HOLogic.mk_eq - (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bclauses))) - end; - val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv = the (AList.lookup (op=) fv_map ty) + val lhs = fv $ list_comb (constr, args) + val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses + val rhs = fold_union rhs_trms in - map2 fv_bn_constr constrs (args_in_bns ~~ bclausess) + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end *} ML {* -fun fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss = +fun make_bn_body fv_map fv_bn_map bn_args args i = 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 arg = nth args i + val ty = fastype_of arg +in + case AList.lookup (op=) bn_args i of + NONE => (case (AList.lookup (op=) fv_map ty) of + NONE => mk_supp arg + | SOME fv => fv $ arg) + | SOME (NONE) => @{term "{}::atom set"} + | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg +end +*} - val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs); - val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees - val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs; - val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs); +ML {* +fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = + case bclause of + BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies) + | BC (_, binders, bodies) => + let + val t1 = map (make_body fv_map args) bodies + val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders) + in + fold_union (mk_diff (fold_union t1, fold_union t2)::t3) + end +*} + +ML {* +fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, ty, arg_tys)) bclauses = +let + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) + val lhs = fv_bn $ list_comb (constr, args) + val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses + val rhs = fold_union rhs_trms in - (bn_fvbn, fvbn_names, eqs) + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end *} ML {* -fun fv_bm thy dts args fv_frees bn_fvbn bm = -case bm of - BEmy i => - let - val x = nth args i; - val dt = nth dts i; - in - if Datatype_Aux.is_rec_type dt - then nth fv_frees (Datatype_Aux.body_index dt) $ x - else mk_supp x - end -| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y -*} - -ML {* -fun fv thy dt_descr sorts fv_frees bn_fvbn bclausess (fv_free, ith_dtyp) = +fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let - fun fv_constr (cname, dts) bclauses = - let - val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; - val names = Datatype_Prop.make_tnames Ts; - val args = map Free (names ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp)); - val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn - in - HOLogic.mk_Trueprop (HOLogic.mk_eq - (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bclauses))) - end; - val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; + val nth_constrs_info = nth constrs_info bn_n + val nth_bclausess = nth bclausesss bn_n in - map2 fv_constr constrs bclausess + map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end *} ML {* -fun define_raw_fvs dt_descr sorts bn_funs bclausesss lthy = +fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy = let - val thy = ProofContext.theory_of lthy; val fv_names = prefix_dt_names dt_descr sorts "fv_" - val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr; - val fv_frees = map Free (fv_names ~~ fv_types); + val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr; + val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; + val fv_frees = map Free (fv_names ~~ fv_tys); + val fv_map = fv_arg_tys ~~ fv_frees - (* free variables for the bn-functions *) - val (bn_fvbn_map, fv_bn_names, fv_bn_eqs) = - fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; + val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs) + val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2) + val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2 + val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2 + val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2 + val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2 + val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2) + val fv_bn_map2 = bns ~~ fv_bn_frees2 + val fv_bn_map3 = bns2 ~~ fv_bn_frees2 + + val constrs_info = all_dtyp_constrs_types dt_descr sorts - val _ = tracing ("bn_fvbn_map" ^ commas (map @{make_string} bn_fvbn_map)) + val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss + val fv_bn_eqs2 = map (make_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 - val fv_bns = map snd bn_fvbn_map; - val fv_nums = 0 upto (length fv_frees - 1) - - val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn_map) bclausesss (fv_frees ~~ fv_nums); + val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2) + val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2) - val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) - val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) - - fun pat_completeness_auto ctxt = - Pat_Completeness.pat_completeness_tac ctxt 1 - THEN auto_tac (clasimpset_of ctxt) + fun pat_completeness_auto lthy = + Pat_Completeness.pat_completeness_tac lthy 1 + THEN auto_tac (clasimpset_of lthy) fun prove_termination lthy = Function.prove_termination NONE @@ -290,21 +256,8 @@ end *} -(**************************************************) -datatype foo = - C1 nat -| C2 foo int -(* -ML {* -fun mk_body descr sorts fv_ty_map dtyp = -let - val nth_dtyp_constr_tys descr sorts -in - true -end -*} -*) + end diff -r a5dc3558cdec -r 3b83960f9544 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Wed May 19 12:44:03 2010 +0100 +++ b/Nominal/NewParser.thy Thu May 20 21:23:53 2010 +0100 @@ -2,9 +2,10 @@ imports "../Nominal-General/Nominal2_Base" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp" "Lift" + "Perm" "NewAlpha" "Tacs" "Equivp" "Lift" begin + section{* Interface for nominal_datatype *} @@ -154,10 +155,7 @@ fun rawify_bnds bnds = map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds - fun rawify_bclause (BEmy n) = BEmy n - | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys) - | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys) - | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys) + fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys) in map (map (map rawify_bclause)) bclauses end @@ -219,9 +217,9 @@ val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) - val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) + (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*) (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*) - val _ = tracing ("ordered'\n" ^ @{make_string} ordered') + (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*) in ordered' end @@ -263,7 +261,7 @@ fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; in - (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, lthy2) + (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, raw_bns, lthy2) end *} @@ -372,10 +370,13 @@ fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = let (* definition of the raw datatypes and raw bn-functions *) - val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) = + val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, raw_bns2, lthy1) = if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy else raise TEST lthy + (*val _ = tracing ("exported: " ^ commas (map @{make_string} raw_bns))*) + (*val _ = tracing ("plain: " ^ commas (map @{make_string} raw_bns2))*) + val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr @@ -408,7 +409,7 @@ val (fv, fvbn, fv_def, lthy3a) = if get_STEPS lthy2 > 3 - then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3 + then define_raw_fvs descr sorts raw_bns raw_bns2 raw_bclauses lthy3 else raise TEST lthy3 (* definition of raw alphas *) @@ -431,7 +432,8 @@ (* definition of raw_alpha_eq_iff lemmas *) val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; - val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp); + + (*val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);*) (* proving equivariance lemmas *) val _ = warning "Proving equivariance"; @@ -639,16 +641,16 @@ fun prep_body env bn_str = index_lookup env bn_str - fun prep_mode "bind" = BLst - | prep_mode "bind_set" = BSet - | prep_mode "bind_res" = BRes + fun prep_mode "bind" = Lst + | prep_mode "bind_set" = Set + | prep_mode "bind_res" = Res fun prep_bclause env (mode, binders, bodies) = let val binders' = map (prep_binder env) binders val bodies' = map (prep_body env) bodies in - prep_mode mode (binders', bodies') + BC (prep_mode mode, binders', bodies') end fun prep_bclauses (annos, bclause_strs) = @@ -670,10 +672,7 @@ ML {* fun included i bcs = let - fun incl (BEmy j) = i = j - | incl (BLst (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) - | incl (BSet (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) - | incl (BRes (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) + fun incl (BC (_, bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) in exists incl bcs end @@ -688,7 +687,7 @@ fun complt n bcs = let - fun add bcs i = (if included i bcs then [] else [BEmy i]) + fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) in bcs @ (flat (map_range (add bcs) n)) end diff -r a5dc3558cdec -r 3b83960f9544 Nominal/Perm.thy --- a/Nominal/Perm.thy Wed May 19 12:44:03 2010 +0100 +++ b/Nominal/Perm.thy Thu May 20 21:23:53 2010 +0100 @@ -1,180 +1,9 @@ theory Perm -imports "../Nominal-General/Nominal2_Atoms" +imports + "../Nominal-General/Nominal2_Base" + "../Nominal-General/Nominal2_Atoms" begin -(* definitions of the permute function for raw nominal datatypes *) - - -ML {* -(* returns the type of the nth datatype *) -fun nth_dtyp descr sorts n = - Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); - -(* returns the constructors of the nth datatype *) -fun nth_dtyp_constrs descr n = -let - val (_, (_, _, constrs)) = nth descr n -in - constrs -end - -(* returns the types of the constructors of the nth datatype *) -fun nth_dtyp_constr_typs descr sorts n = - map (map (Datatype_Aux.typ_of_dtyp descr sorts) o snd) (nth_dtyp_constrs descr n) -*} - -ML {* -(* generates for every datatype a name str ^ dt_name - plus and index for multiple occurences of a string *) -fun prefix_dt_names descr sorts str = -let - fun get_nth_name (i, _) = - Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) -in - Datatype_Prop.indexify_names - (map (prefix str o get_nth_name) descr) -end -*} - - -ML {* -(* permutation function for one argument - - - in case the argument is recursive it returns - - permute_fn p arg - - - in case the argument is non-recursive it will return - - p o arg - -*) -fun perm_arg permute_fn_frees p (arg_dty, arg) = - if Datatype_Aux.is_rec_type arg_dty - then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg - else mk_perm p arg -*} - -ML {* -(* generates the equation for the permutation function for one constructor; - i is the index of the corresponding datatype *) -fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) = -let - val p = Free ("p", @{typ perm}) - val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts - val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) - val args = map Free (arg_names ~~ arg_tys) - val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) - val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args) - val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args)) - val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) -in - (Attrib.empty_binding, eq) -end -*} - -ML {* -(* proves the two pt-type class properties *) -fun prove_permute_zero lthy induct perm_defs perm_fns = -let - val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = Datatype_Prop.make_tnames perm_types - - fun single_goal ((perm_fn, T), x) = - HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) - - val goals = - HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) - - val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) - - val tac = (Datatype_Aux.indtac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 -in - Goal.prove lthy perm_indnames [] goals (K tac) - |> Datatype_Aux.split_conj_thm -end -*} - -ML {* -fun prove_permute_plus lthy induct perm_defs perm_fns = -let - val p = Free ("p", @{typ perm}) - val q = Free ("q", @{typ perm}) - val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = Datatype_Prop.make_tnames perm_types - - fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq - (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) - - val goals = - HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) - - val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) - - val tac = (Datatype_Aux.indtac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 -in - Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) - |> Datatype_Aux.split_conj_thm -end -*} - -ML {* -(* defines the permutation functions for raw datatypes and - proves that they are instances of pt - - user_dt_nos refers to the number of "un-unfolded" datatypes - given by the user -*) -fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy = -let - val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; - val user_full_tnames = List.take (all_full_tnames, user_dt_nos); - - val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" - val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr - val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) - - fun perm_eq (i, (_, _, constrs)) = - map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; - - val perm_eqs = maps perm_eq dt_descr; - - val lthy = - Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; - - val ((perm_funs, perm_eq_thms), lthy') = - Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; - - val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs - val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs - val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); - val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) - val perms_name = space_implode "_" perm_fn_names - val perms_zero_bind = Binding.name (perms_name ^ "_zero") - val perms_plus_bind = Binding.name (perms_name ^ "_plus") - - fun tac _ (_, _, simps) = - Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) - - fun morphism phi (fvs, dfs, simps) = - (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); -in - lthy' - |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) - |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) - |> Class_Target.prove_instantiation_exit_result morphism tac - (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') -end -*} - - - - (* permutations for quotient types *) diff -r a5dc3558cdec -r 3b83960f9544 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Wed May 19 12:44:03 2010 +0100 +++ b/Nominal/ROOT.ML Thu May 20 21:23:53 2010 +0100 @@ -14,6 +14,6 @@ "Ex/ExPS3", "Ex/ExPS7", "Ex/CoreHaskell", - "Ex/Test", - "Manual/Term4" + "Ex/Test"(*, + "Manual/Term4"*) ]; diff -r a5dc3558cdec -r 3b83960f9544 Nominal/nominal_dt_rawfuns.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Thu May 20 21:23:53 2010 +0100 @@ -0,0 +1,262 @@ +(* Title: nominal_dt_rawperm.ML + Author: Cezary Kaliszyk + Author: Christian Urban + + Definitions of the raw bn, fv and fv_bn + functions +*) + +signature NOMINAL_DT_RAWFUNS = +sig + (* binding modes and binding clauses *) + + datatype bmode = Lst | Res | Set + + datatype bclause = BC of bmode * (term option * int) list * int list + + val setify: Proof.context -> term -> term + val listify: Proof.context -> term -> term + val fold_union: term list -> term + + val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> + (term * 'a * 'b) list -> (term * int * (int * term option) list list) list -> + bclause list list list -> Proof.context -> term list * term list * thm list * local_theory +end + + +structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = +struct + +datatype bmode = Lst | Res | Set +datatype bclause = BC of bmode * (term option * int) list * int list + +(* functions that construct differences and unions + but avoid producing empty atom sets *) + +fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} + | mk_diff (t1, @{term "{}::atom set"}) = t1 + | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) + +fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} + | mk_union (t1 , @{term "{}::atom set"}) = t1 + | mk_union (@{term "{}::atom set"}, t2) = t2 + | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2) + +fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} + + +(* atom types *) +fun is_atom ctxt ty = + Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) + +fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t + | is_atom_set _ _ = false; + +fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t + | is_atom_fset _ _ = false; + +fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t + | is_atom_list _ _ = false + + +(* functions for producing sets, fsets and lists *) +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) $ mk_atom_ty 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; + +fun mk_atom_list t = +let + val ty = fastype_of t; + val atom_ty = dest_listT ty --> @{typ atom}; + val map_ty = atom_ty --> ty --> @{typ "atom list"}; +in + (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t) +end; + + +(* functions that coerces atoms, sets and fsets into atom sets ? *) +fun setify ctxt t = +let + val ty = fastype_of t; +in + if is_atom ctxt ty + then HOLogic.mk_set @{typ atom} [mk_atom t] + else if is_atom_set ctxt ty + then mk_atom_set t + else if is_atom_fset ctxt ty + then mk_atom_fset t + else raise TERM ("setify", [t]) +end + +(* functions that coerces atoms and lists into atom lists ? *) +fun listify ctxt t = +let + val ty = fastype_of t; +in + if is_atom ctxt ty + then HOLogic.mk_list @{typ atom} [mk_atom t] + else if is_atom_list ctxt ty + then mk_atom_set t + else raise TERM ("listify", [t]) +end + +(* coerces a list into a set *) +fun to_set x = + if fastype_of x = @{typ "atom list"} + then @{term "set::atom list => atom set"} $ x + else x + + + +fun make_body fv_map args i = +let + val arg = nth args i + val ty = fastype_of arg +in + case (AList.lookup (op=) fv_map ty) of + NONE => mk_supp arg + | SOME fv => fv $ arg +end + +fun make_binder lthy fv_bn_map args (bn_option, i) = +let + val arg = nth args i +in + case bn_option of + NONE => (setify lthy arg, @{term "{}::atom set"}) + | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) +end + +fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = +let + val t1 = map (make_body fv_map args) bodies + val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders) +in + fold_union (mk_diff (fold_union t1, fold_union t2)::t3) +end + +fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = +let + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv = the (AList.lookup (op=) fv_map ty) + val lhs = fv $ list_comb (constr, args) + val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses + val rhs = fold_union rhs_trms +in + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) +end + + +fun make_bn_body fv_map fv_bn_map bn_args args i = +let + val arg = nth args i + val ty = fastype_of arg +in + case AList.lookup (op=) bn_args i of + NONE => (case (AList.lookup (op=) fv_map ty) of + NONE => mk_supp arg + | SOME fv => fv $ arg) + | SOME (NONE) => @{term "{}::atom set"} + | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg +end + +fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = + case bclause of + BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies) + | BC (_, binders, bodies) => + let + val t1 = map (make_body fv_map args) bodies + val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders) + in + fold_union (mk_diff (fold_union t1, fold_union t2)::t3) + end + +fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, ty, arg_tys)) bclauses = +let + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) + val lhs = fv_bn $ list_comb (constr, args) + val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses + val rhs = fold_union rhs_trms +in + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) +end + +fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = +let + val nth_constrs_info = nth constrs_info bn_n + val nth_bclausess = nth bclausesss bn_n +in + map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess +end + +fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy = +let + + val fv_names = prefix_dt_names dt_descr sorts "fv_" + val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr; + val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; + val fv_frees = map Free (fv_names ~~ fv_tys); + val fv_map = fv_arg_tys ~~ fv_frees + + val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs) + val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2) + val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2 + val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2 + val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2 + val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2 + val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2) + val fv_bn_map2 = bns ~~ fv_bn_frees2 + val fv_bn_map3 = bns2 ~~ fv_bn_frees2 + + val constrs_info = all_dtyp_constrs_types dt_descr sorts + + val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss + val fv_bn_eqs2 = map (make_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 + + val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2) + val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2) + + fun pat_completeness_auto lthy = + Pat_Completeness.pat_completeness_tac lthy 1 + THEN auto_tac (clasimpset_of lthy) + + fun prove_termination lthy = + Function.prove_termination NONE + (Lexicographic_Order.lexicographic_order_tac true lthy) lthy + + val (_, lthy') = Function.add_function all_fv_names all_fv_eqs + Function_Common.default_config pat_completeness_auto lthy + + val (info, lthy'') = prove_termination (Local_Theory.restore lthy') + + val {fs, simps, ...} = info; + + val morphism = ProofContext.export_morphism lthy'' lthy + val fs_exp = map (Morphism.term morphism) fs + + val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp + val simps_exp = Morphism.fact morphism (the simps) +in + (fv_frees_exp, fv_bns_exp, simps_exp, lthy'') +end + +end (* structure *) + diff -r a5dc3558cdec -r 3b83960f9544 Nominal/nominal_dt_rawperm.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_rawperm.ML Thu May 20 21:23:53 2010 +0100 @@ -0,0 +1,150 @@ +(* Title: nominal_dt_rawperm.ML + Author: Cezary Kaliszyk + Author: Christian Urban + + Definitions of the raw permutations and + proof that the raw datatypes are in the + pt-class. +*) + +signature NOMINAL_DT_RAWPERM = +sig + val define_raw_perms: Datatype.descr -> (string * sort) list -> thm -> int -> theory -> + (term list * thm list * thm list) * theory +end + + +structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM = +struct + + +(* permutation function for one argument + + - in case the argument is recursive it returns + + permute_fn p arg + + - in case the argument is non-recursive it will return + + p o arg + +*) +fun perm_arg permute_fn_frees p (arg_dty, arg) = + if Datatype_Aux.is_rec_type arg_dty + then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg + else mk_perm p arg + + +(* generates the equation for the permutation function for one constructor; + i is the index of the corresponding datatype *) +fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) = +let + val p = Free ("p", @{typ perm}) + val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts + val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) + val args = map Free (arg_names ~~ arg_tys) + val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) + val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args) + val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args)) + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) +in + (Attrib.empty_binding, eq) +end + + +(** proves the two pt-type class properties **) + +fun prove_permute_zero lthy induct perm_defs perm_fns = +let + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = Datatype_Prop.make_tnames perm_types + + fun single_goal ((perm_fn, T), x) = + HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) + + val goals = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) + + val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) + + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 +in + Goal.prove lthy perm_indnames [] goals (K tac) + |> Datatype_Aux.split_conj_thm +end + + +fun prove_permute_plus lthy induct perm_defs perm_fns = +let + val p = Free ("p", @{typ perm}) + val q = Free ("q", @{typ perm}) + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = Datatype_Prop.make_tnames perm_types + + fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq + (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) + + val goals = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) + + val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) + + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 +in + Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) + |> Datatype_Aux.split_conj_thm +end + + +(* user_dt_nos refers to the number of "un-unfolded" datatypes + given by the user +*) +fun define_raw_perms (dt_descr:Datatype.descr) sorts induct_thm user_dt_nos thy = +let + val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; + val user_full_tnames = List.take (all_full_tnames, user_dt_nos); + + val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" + val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr + val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) + + fun perm_eq (i, (_, _, constrs)) = + map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; + + val perm_eqs = maps perm_eq dt_descr; + + val lthy = + Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; + + val ((perm_funs, perm_eq_thms), lthy') = + Primrec.add_primrec + (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; + + val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs + val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs + val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); + val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) + val perms_name = space_implode "_" perm_fn_names + val perms_zero_bind = Binding.name (perms_name ^ "_zero") + val perms_plus_bind = Binding.name (perms_name ^ "_plus") + + fun tac _ (_, _, simps) = + Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) + + fun morphism phi (fvs, dfs, simps) = + (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); +in + lthy' + |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) + |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) + |> Class_Target.prove_instantiation_exit_result morphism tac + (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') +end + + +end (* structure *) +