# HG changeset patch # User Christian Urban # Date 1274417903 -3600 # Node ID d134bd4f6d1b0566dcd42c0a5e2f99c89830e01c # Parent 20ee31bc34d5f8bf5e55b7d2e9a68452d360c91f tuned diff -r 20ee31bc34d5 -r d134bd4f6d1b Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Fri May 21 00:44:39 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Fri May 21 05:58:23 2010 +0100 @@ -5,7 +5,7 @@ atom_decl name ML {* print_depth 50 *} -declare [[STEPS = 19]] +declare [[STEPS = 4]] nominal_datatype trm = Var "name" diff -r 20ee31bc34d5 -r d134bd4f6d1b Nominal/NewParser.thy --- a/Nominal/NewParser.thy Fri May 21 00:44:39 2010 +0100 +++ b/Nominal/NewParser.thy Fri May 21 05:58:23 2010 +0100 @@ -185,7 +185,7 @@ *} ML {* -fun prep_bn lthy dt_names dts eqs = +fun prep_bn_descr lthy dt_names dts eqs = let fun aux eq = let @@ -252,16 +252,16 @@ 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_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds - val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs) + val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs) val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy - val (raw_bn_funs, raw_bn_eqs, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 + val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy 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; + val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr; in - (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, raw_bns, lthy2) + (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr_exp, raw_bn_descr, lthy2) end *} @@ -290,70 +290,6 @@ handle TERM _ => @{thm eqTrueI} OF [t] *} -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 {* (* for testing porposes - to exit the procedure early *) @@ -370,12 +306,17 @@ 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, raw_bns2, lthy1) = + val (raw_dt_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_funs, raw_bn_eqs, raw_bn_descr, raw_bn_descr2, 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 _ = tracing ("raw_bn_descr " ^ @{make_string} raw_bn_descr) + val _ = tracing ("raw_bn_descr2 " ^ @{make_string} raw_bn_descr2) + val _ = tracing ("bclauses " ^ @{make_string} bclauses) + val _ = tracing ("raw_bn_fund " ^ @{make_string} raw_bn_funs) + val _ = tracing ("raw_bn_eqs " ^ @{make_string} raw_bn_eqs) + val _ = tracing ("raw_bn_fund2 " ^ @{make_string} raw_bn_funs2) + val _ = tracing ("raw_bn_eqs2 " ^ cat_lines (map (Syntax.string_of_term lthy o snd) raw_bn_eqs2)) val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo @@ -391,7 +332,7 @@ val exhaust_thms = map #exhaust dtinfos; (* definitions of raw permutations *) - val ((perms, raw_perm_defs, raw_perm_simps), lthy2) = + val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = if get_STEPS lthy1 > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 else raise TEST lthy1 @@ -405,22 +346,22 @@ (* definition of raw fv_functions *) val lthy3 = Theory_Target.init NONE thy; - val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; val (fv, fvbn, fv_def, lthy3a) = if get_STEPS lthy2 > 3 - then define_raw_fvs descr sorts raw_bns raw_bns2 raw_bclauses lthy3 + then define_raw_fvs (map (fn (x, _, _) => Binding.name_of x) bn_funs) (map snd bn_eqs) descr sorts raw_bn_descr raw_bn_descr2 raw_bclauses lthy3 else raise TEST lthy3 + (* definition of raw alphas *) val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = if get_STEPS lthy > 4 - then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a + then define_raw_alpha dtinfo raw_bn_descr raw_bclauses fv lthy3a else raise TEST lthy3a val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts - val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); + val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; 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; @@ -433,8 +374,6 @@ 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);*) - (* proving equivariance lemmas *) val _ = warning "Proving equivariance"; val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 @@ -474,7 +413,7 @@ (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 + val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else @@ -488,7 +427,7 @@ 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 (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) 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 @@ -497,7 +436,7 @@ val _ = warning "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 thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) 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); @@ -717,108 +656,71 @@ (main_parser >> nominal_datatype2_cmd) *} -(* -atom_decl name + +text {* + nominal_datatype2 does the following things in order: -nominal_datatype lam = - Var name -| App lam lam -| Lam x::name t::lam bind_set x in t -| Let p::pt t::lam bind_set "bn p" in t -and pt = - P1 name -| P2 pt pt -binder - bn::"pt \ atom set" -where - "bn (P1 x) = {atom x}" -| "bn (P2 p1 p2) = bn p1 \ bn p2" - -find_theorems Var_raw - - +Parser.thy/raw_nominal_decls + 1) define the raw datatype + 2) define the raw binding functions -thm lam_pt.bn -thm lam_pt.fv[simplified lam_pt.supp(1-2)] -thm lam_pt.eq_iff -thm lam_pt.induct -thm lam_pt.perm - -nominal_datatype exp = - EVar name -| EUnit -| EPair q1::exp q2::exp -| ELetRec l::lrbs e::exp bind "b_lrbs l" in e l +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 -and fnclause = - K x::name p::pat f::exp bind_res "b_pat p" in f - -and fnclauses = - S fnclause -| ORs fnclause fnclauses - -and lrb = - Clause fnclauses - -and lrbs = - Single lrb -| More lrb lrbs +Perm.thy/distinct_rel + 6) prove alpha_distincts (C1 x \ C2 y ...) (Proof by cases; simp) -and pat = - PVar name -| PUnit -| PPair pat pat - -binder - b_lrbs :: "lrbs \ atom list" and - b_pat :: "pat \ atom set" and - b_fnclauses :: "fnclauses \ atom list" and - b_fnclause :: "fnclause \ atom list" and - b_lrb :: "lrb \ atom list" - -where - "b_lrbs (Single l) = b_lrb l" -| "b_lrbs (More l ls) = append (b_lrb l) (b_lrbs ls)" -| "b_pat (PVar x) = {atom x}" -| "b_pat (PUnit) = {}" -| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" -| "b_fnclauses (S fc) = (b_fnclause fc)" -| "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)" -| "b_lrb (Clause fcs) = (b_fnclauses fcs)" -| "b_fnclause (K x pat exp) = [atom x]" - -thm exp_fnclause_fnclauses_lrb_lrbs_pat.bn -thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv -thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff -thm exp_fnclause_fnclauses_lrb_lrbs_pat.induct -thm exp_fnclause_fnclauses_lrb_lrbs_pat.perm - -nominal_datatype ty = - Vr "name" -| Fn "ty" "ty" -and tys = - Al xs::"name fset" t::"ty" bind_res xs in t - -thm ty_tys.fv[simplified ty_tys.supp] -thm ty_tys.eq_iff - -*) - -(* some further tests *) - -(* -nominal_datatype ty2 = - Vr2 "name" -| Fn2 "ty2" "ty2" - -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 -*) +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 +*} diff -r 20ee31bc34d5 -r d134bd4f6d1b Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Fri May 21 00:44:39 2010 +0100 +++ b/Nominal/nominal_dt_rawfuns.ML Fri May 21 05:58:23 2010 +0100 @@ -17,9 +17,13 @@ val setify: Proof.context -> term -> term val listify: Proof.context -> term -> 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 + val define_raw_fvs: + string list -> term list -> + Datatype_Aux.descr -> + (string * sort) list -> + (term * int * (int * term option) list list) list -> + (term * int * (int * term option) list list) list -> + bclause list list list -> Proof.context -> term list * term list * thm list * local_theory end @@ -29,7 +33,7 @@ datatype bmode = Lst | Res | Set datatype bclause = BC of bmode * (term option * int) list * int list -(* atom types *) +(* testing for concrete atom types *) fun is_atom ctxt ty = Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) @@ -43,15 +47,16 @@ | is_atom_list _ _ = false -(* functions for producing sets, fsets and lists *) +(* functions for producing sets, fsets and lists of general atom type + out from concrete atom types *) 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; + Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t +end fun mk_atom_fset t = let @@ -61,20 +66,19 @@ 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; +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; -*) + Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t +end -(* functions that coerces atoms, sets and fsets into atom sets ? *) +(* functions that coerces concrete atoms, sets and fsets into sets + of general atoms *) fun setify ctxt t = let val ty = fastype_of t; @@ -88,7 +92,8 @@ else raise TERM ("setify", [t]) end -(* functions that coerces atoms and lists into atom lists ? *) +(* functions that coerces concrete atoms and lists into lists of + general atoms *) fun listify ctxt t = let val ty = fastype_of t; @@ -109,7 +114,7 @@ (* functions that construct the equations for fv and fv_bn *) -fun make_fv_body fv_map args i = +fun mk_fv_body fv_map args i = let val arg = nth args i val ty = fastype_of arg @@ -119,37 +124,7 @@ | SOME fv => fv $ arg end -fun make_fv_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_fv_body fv_map args) bodies - val (t2, t3) = split_list (map (make_fv_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_fv_bn_body fv_map fv_bn_map bn_args args i = +fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = let val arg = nth args i val ty = fastype_of arg @@ -162,39 +137,70 @@ | 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 = +fun mk_fv_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 mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = +let + val t1 = map (mk_fv_body fv_map args) bodies + val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) +in + fold_union (mk_diff (fold_union t1, fold_union t2)::t3) +end + +fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = case bclause of - BC (_, [], bodies) => fold_union (map (make_fv_bn_body fv_map fv_bn_map bn_args args) bodies) + BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) | BC (_, binders, bodies) => let - val t1 = map (make_fv_body fv_map args) bodies - val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders) + val t1 = map (mk_fv_body fv_map args) bodies + val (t2, t3) = split_list (map (mk_fv_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, _, arg_tys)) bclauses = +fun mk_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 (mk_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 mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, 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_trms = map (mk_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) = +fun mk_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 + map2 (mk_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 = +fun define_raw_fvs t1 t2 dt_descr sorts bn_funs bn_funs2 bclausesss lthy = let + val _ = tracing ("bn-functions to be defined\n " ^ commas t1) + val _ = tracing ("bn-equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) t2)) 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; @@ -212,11 +218,17 @@ val fv_bn_map2 = bns ~~ fv_bn_frees2 val fv_bn_map3 = bns2 ~~ fv_bn_frees2 + val _ = tracing ("fn_bn_map2 " ^ @{make_string} fv_bn_map2) + val _ = tracing ("fn_bn_map3 " ^ @{make_string} fv_bn_map3) + 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 fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss + val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 + val _ = tracing ("functions to be defined\n " ^ @{make_string} (fv_names @ fv_bn_names2)) + val _ = tracing ("equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_eqs2 @ flat fv_bn_eqs2))) + 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) diff -r 20ee31bc34d5 -r d134bd4f6d1b Nominal/nominal_dt_rawperm.ML --- a/Nominal/nominal_dt_rawperm.ML Fri May 21 00:44:39 2010 +0100 +++ b/Nominal/nominal_dt_rawperm.ML Fri May 21 05:58:23 2010 +0100 @@ -103,7 +103,7 @@ (* 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 = +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);