# HG changeset patch # User Christian Urban # Date 1274577324 -3600 # Node ID 8aff3f3ce47fb12a85cadf9d448e93c715fbf240 # Parent 72ad4e766acfa818fa19a926dac605eb89fd4083 started to work on alpha diff -r 72ad4e766acf -r 8aff3f3ce47f Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sat May 22 13:51:47 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Sun May 23 02:15:24 2010 +0100 @@ -5,7 +5,7 @@ atom_decl name ML {* print_depth 50 *} -declare [[STEPS = 4]] +declare [[STEPS = 5]] nominal_datatype trm = @@ -21,6 +21,8 @@ "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] bn_raw.simps[no_vars] +thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] + ML {* Inductive.the_inductive *} thm trm_assg.fv diff -r 72ad4e766acf -r 8aff3f3ce47f Nominal/NewAlpha.thy --- a/Nominal/NewAlpha.thy Sat May 22 13:51:47 2010 +0100 +++ b/Nominal/NewAlpha.thy Sun May 23 02:15:24 2010 +0100 @@ -127,7 +127,7 @@ let fun mk_alphabn_free (bn, ith, _) = let - val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Free bn))); + val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); val ty = nth_dtyp dt_descr sorts ith; val alphabn_type = ty --> ty --> @{typ bool}; val alphabn_free = Free(alphabn_name, alphabn_type); @@ -190,10 +190,8 @@ *} ML {* -fun define_raw_alpha (dt_info : Datatype_Aux.info) bn_funs bclausesss fv_frees lthy = +fun define_raw_alpha dt_descr sorts bn_funs bclausesss fv_frees lthy = let - val {descr as dt_descr, sorts, ...} = dt_info; - val alpha_names = prefix_dt_names dt_descr sorts "alpha_"; val alpha_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr; @@ -230,8 +228,9 @@ val alpha_intros = Morphism.fact morphism alpha_intros_loc val alpha_cases = Morphism.fact morphism alpha_cases_loc in - (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy') + (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy') end +handle UnequalLengths => error "Main" *} end diff -r 72ad4e766acf -r 8aff3f3ce47f Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sat May 22 13:51:47 2010 +0100 +++ b/Nominal/NewParser.thy Sun May 23 02:15:24 2010 +0100 @@ -190,7 +190,7 @@ *} ML {* -fun prep_bn_descr lthy dt_names dts eqs = +fun prep_bn_info lthy dt_names dts eqs = let fun aux eq = let @@ -257,15 +257,14 @@ val raw_dt_names' = map (Long_Name.qualify thy_name) raw_dt_names 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_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs)*) val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy - val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 + val (raw_bn_funs', raw_bn_eqs', lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 - val raw_bn_descr = - prep_bn_descr lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs2) + val raw_bn_info = + prep_bn_info lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs') in - (raw_dt_full_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr, lthy2) + (raw_dt_full_names, raw_bclauses, raw_bn_funs', raw_bn_eqs', raw_bn_info, lthy2) end *} @@ -310,8 +309,9 @@ fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = let (* definition of the raw datatypes *) - val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_descr, lthy1) = - if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy + val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_info, lthy1) = + if get_STEPS lthy > 1 + then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy else raise TEST lthy val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) @@ -343,42 +343,46 @@ (* definition of raw fv_functions *) val lthy3 = Theory_Target.init NONE thy; - val (fv, fvbn, fv_def, lthy3a) = + val (fv, fv_bn, fv_def, lthy3a) = if get_STEPS lthy2 > 3 - then define_raw_fvs descr sorts raw_bn_funs raw_bn_descr raw_bclauses lthy3 + then define_raw_fvs descr sorts raw_bn_info raw_bclauses lthy3 else raise TEST lthy3 (* definition of raw alphas *) - val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = + val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = if get_STEPS lthy > 4 - then define_raw_alpha dtinfo raw_bn_descr raw_bclauses fv lthy3a + then define_raw_alpha descr sorts raw_bn_info 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; - val bn_tys = map (domain_type o fastype_of) [] (*raw_bn_funs;*) + 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 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)) (* 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 = + if get_STEPS lthy > 5 + then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 + else raise TEST lthy4 + val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; (* 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 - val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5 + val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fv_bn) lthy5 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; (* proving alpha equivalence *) val _ = warning "Proving equivalence"; - val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; + val fv_alpha_all = combine_fv_alpha_bns (fv, fv_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; val alpha_equivp = if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts @@ -407,7 +411,7 @@ 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; + (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fv_bn) lthy9; val fv_rsp = flat (map snd fv_rsp_pre); val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; @@ -421,8 +425,8 @@ in constr_rsp_tac alpha_eq_iff_simp (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_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fv_bn) + val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fv_bn)) lthy12; 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; diff -r 72ad4e766acf -r 8aff3f3ce47f Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Sat May 22 13:51:47 2010 +0100 +++ b/Nominal/nominal_dt_rawfuns.ML Sun May 23 02:15:24 2010 +0100 @@ -8,27 +8,26 @@ signature NOMINAL_DT_RAWFUNS = sig - (* binding modes and binding clauses *) + (* info of binding functions *) + type bn_info = (term * int * (int * term option) list list) list + (* 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 define_raw_fvs: - Datatype_Aux.descr -> - (string * sort) list -> - term 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: Datatype_Aux.descr -> (string * sort) list -> bn_info -> + bclause list list list -> Proof.context -> term list * term list * thm list * local_theory end structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = struct +type bn_info = (term * int * (int * term option) list list) list + datatype bmode = Lst | Res | Set datatype bclause = BC of bmode * (term option * int) list * int list @@ -76,8 +75,8 @@ Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t end -(* functions that coerces concrete atoms, sets and fsets into sets - of general atoms *) +(* functions that coerces singletons, sets and fsets of concrete atoms + into sets of general atoms *) fun setify ctxt t = let val ty = fastype_of t; @@ -91,8 +90,8 @@ else raise TERM ("setify", [t]) end -(* functions that coerces concrete atoms and lists into lists of - general atoms *) +(* functions that coerces singletons and lists of concrete atoms + into lists of general atoms *) fun listify ctxt t = let val ty = fastype_of t; @@ -111,42 +110,29 @@ else t -(* functions that construct the equations for fv and fv_bn *) - -fun mk_fv_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 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_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 +(** functions that construct the equations for fv and fv_bn **) fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = let + fun mk_fv_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 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 + 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 @@ -156,10 +142,24 @@ (* in case of fv_bn we have to treat the case special, where an "empty" binding clause is given *) fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = +let + 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 + 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 +in case bclause of BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause - +end fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = let @@ -193,28 +193,29 @@ 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_trms bn_funs2 bclausesss lthy = +fun define_raw_fvs descr sorts bn_info 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_names = prefix_dt_names descr sorts "fv_" + val fv_arg_tys = map (fn (i, _) => nth_dtyp descr sorts i) 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 bn_tys2 = map (fn (_, i, _) => i) bn_funs2 - val fv_bn_names2 = map (fn bn => "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bn_trms - 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_map = bn_trms ~~ fv_bn_frees2 + val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) + val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns + val fv_bn_names = map (prefix "fv_") bn_names + val fv_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys + val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys + val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) + val fv_bn_map = bns ~~ fv_bn_frees - val constrs_info = all_dtyp_constrs_types dt_descr sorts + val constrs_info = all_dtyp_constrs_types descr sorts - val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss - val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_funs2 + val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss + val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info - 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_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) + val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) fun pat_completeness_auto lthy = Pat_Completeness.pat_completeness_tac lthy 1 @@ -224,7 +225,7 @@ Function.prove_termination NONE (Lexicographic_Order.lexicographic_order_tac true lthy) lthy - val (_, lthy') = Function.add_function all_fv_names all_fv_eqs + val (_, lthy') = Function.add_function all_fun_names all_fun_eqs Function_Common.default_config pat_completeness_auto lthy val (info, lthy'') = prove_termination (Local_Theory.restore lthy') diff -r 72ad4e766acf -r 8aff3f3ce47f Nominal/nominal_dt_rawperm.ML --- a/Nominal/nominal_dt_rawperm.ML Sat May 22 13:51:47 2010 +0100 +++ b/Nominal/nominal_dt_rawperm.ML Sun May 23 02:15:24 2010 +0100 @@ -27,7 +27,6 @@ - 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