# HG changeset patch # User Christian Urban # Date 1309396799 -3600 # Node ID c537d43c09f18a697cdc6ec5a355ad4235dcd8a4 # Parent 116f9ba4f59f83c3bbe97aa3f7030e58bf1775a3 more code refactoring diff -r 116f9ba4f59f -r c537d43c09f1 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Wed Jun 29 23:08:44 2011 +0100 +++ b/Nominal/Nominal2.thy Thu Jun 30 02:19:59 2011 +0100 @@ -232,14 +232,9 @@ (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b val _ = trace_msg (K "Defining alpha relations...") - val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, alpha_result, lthy4) = + val (alpha_result, lthy4) = define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c - val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct)) - val _ = tracing ("alpha_intros\n" ^ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_intros)) - - val alpha_tys = map (domain_type o fastype_of) alpha_trms - val _ = trace_msg (K "Proving distinct theorems...") val alpha_distincts = raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names @@ -267,7 +262,11 @@ val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) val alpha_eqvt = - Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 + let + val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, alpha_intros, ...} = alpha_result + in + Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros lthy5 + end val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt @@ -281,35 +280,27 @@ raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms val _ = trace_msg (K "Proving alpha implies bn...") - val alpha_bn_imp_thms = - raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 - - val _ = tracing ("alpha_bn_imp_thms:\n" ^ cat_lines (map (Syntax.string_of_term lthy5 o prop_of) alpha_bn_imp_thms)) + val alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result val _ = trace_msg (K "Proving respectfulness...") val raw_funs_rsp_aux = - raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs - raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5 + raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux val raw_size_rsp = - raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct - (raw_size_thms @ raw_size_eqvt) lthy5 + raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |> map mk_funs_rsp val raw_constrs_rsp = - raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros - (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy5 + raw_constrs_rsp lthy5 alpha_result (flat raw_constrs) (alpha_bn_imp_thms @ raw_funs_rsp_aux) val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt val alpha_bn_rsp = - raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms + raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms - val raw_perm_bn_rsp = - raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct - alpha_intros raw_perm_bn_simps lthy5 + val raw_perm_bn_rsp =raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps (* noting the quot_respects lemmas *) val (_, lthy6) = @@ -321,7 +312,11 @@ val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts val (qty_infos, lthy7) = - define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 + let + val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result + in + define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 + end val qtys = map #qtyp qty_infos val qty_full_names = map (fst o dest_Type) qtys @@ -341,7 +336,11 @@ map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns val qalpha_bns_descr = - map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs alpha_bn_trms + let + val AlphaResult {alpha_bn_trms, ...} = alpha_result + in + map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs alpha_bn_trms + end val qperm_descr = map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs @@ -484,7 +483,6 @@ ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) - ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) diff -r 116f9ba4f59f -r c537d43c09f1 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Wed Jun 29 23:08:44 2011 +0100 +++ b/Nominal/nominal_dt_alpha.ML Thu Jun 30 02:19:59 2011 +0100 @@ -10,8 +10,7 @@ val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> - bclause list list list -> term list -> Proof.context -> - term list * term list * thm list * thm list * thm * alpha_result * local_theory + bclause list list list -> term list -> Proof.context -> alpha_result * local_theory val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list @@ -26,14 +25,13 @@ val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> thm list * thm list - val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list - val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> - term list -> thm -> thm list -> Proof.context -> thm list - val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list - val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list - val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list - val raw_perm_bn_rsp: term list -> term list -> thm -> thm list -> thm list -> - Proof.context -> thm list + val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list + val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> + thm list -> thm list + val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list + val raw_constrs_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list + val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list + val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list val mk_funs_rsp: thm -> thm val mk_alpha_permute_rsp: thm -> thm @@ -267,20 +265,14 @@ val alpha_cases = map (Morphism.thm phi) alpha_cases_loc val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms - val alpha_tys = - alpha_trms - |> map fastype_of - |> map domain_type - - val alpha_bn_tys = - alpha_bn_trms - |> map fastype_of - |> map domain_type + + val alpha_tys = map (domain_type o fastype_of) alpha_trms + val alpha_bn_tys = map (domain_type o fastype_of) alpha_bn_trms val alpha_names = map (fst o dest_Const) alpha_trms val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms - - val alpha_result = AlphaResult + in + (AlphaResult {alpha_names = alpha_names, alpha_trms = alpha_trms, alpha_tys = alpha_tys, @@ -289,9 +281,7 @@ alpha_bn_tys = alpha_bn_tys, alpha_intros = alpha_intros, alpha_cases = alpha_cases, - alpha_raw_induct = alpha_raw_induct} - in - (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_raw_induct, alpha_result, lthy') + alpha_raw_induct = alpha_raw_induct}, lthy') end @@ -645,11 +635,13 @@ (* proves that alpha_raw implies alpha_bn *) -fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = +fun raw_prove_bn_imp_tac alpha_result ctxt = SUBPROOF (fn {prems, context, ...} => let + val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result + val prems' = flat (map Datatype_Aux.split_conj_thm prems) - val prems'' = map (transform_prem1 context pred_names) prems' + val prems'' = map (transform_prem1 context alpha_names) prems' in HEADGOAL (REPEAT_ALL_NEW @@ -660,24 +652,28 @@ resolve_tac alpha_intros ])) end) ctxt -fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt = + +fun raw_prove_bn_imp ctxt alpha_result = let + val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result + val arg_ty = domain_type o fastype_of - val alpha_names = map (fst o dest_Const) alpha_trms - val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms + val ty_assoc = alpha_tys ~~ alpha_trms val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms in - alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct - (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt + alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct + (raw_prove_bn_imp_tac alpha_result) ctxt end (* respectfulness for fv_raw / bn_raw *) -fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = +fun raw_fv_bn_rsp_aux ctxt alpha_result fvs bns fv_bns simps = let - val arg_ty = fst o dest_Type o domain_type o fastype_of - val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms + val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result + + val arg_ty = domain_type o fastype_of + val ty_assoc = alpha_tys ~~ alpha_trms fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y) val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs @@ -687,28 +683,29 @@ val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) in - alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct + alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct (K (asm_full_simp_tac ss)) ctxt end (* respectfulness for size *) -fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt = +fun raw_size_rsp_aux ctxt alpha_result simps = let - val arg_tys = map (domain_type o fastype_of) all_alpha_trms - + val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = + alpha_result + fun mk_prop ty (x, y) = HOLogic.mk_eq (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) - val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys + val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def permute_prod_def prod.cases prod.recs}) val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss in - alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt + alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt end @@ -726,12 +723,12 @@ THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss) end -fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt = +fun raw_constrs_rsp ctxt alpha_result constrs simps = let - val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms - + val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result + fun lookup ty = - case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of + case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of NONE => HOLogic.eq_const ty | SOME alpha => alpha @@ -763,8 +760,10 @@ (* we have to reorder the alpha_bn_imps theorems in order to be in order with alpha_bn_trms *) -fun raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp alpha_bn_imps = +fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps = let + val AlphaResult {alpha_bn_trms, ...} = alpha_result + fun mk_map thm = thm |> `prop_of |>> List.last o snd o strip_comb @@ -787,11 +786,12 @@ val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f" by (simp add: fun_rel_def)} -fun raw_prove_perm_bn_tac pred_names alpha_intros simps ctxt = +fun raw_prove_perm_bn_tac alpha_result simps ctxt = SUBPROOF (fn {prems, context, ...} => let + val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result val prems' = flat (map Datatype_Aux.split_conj_thm prems) - val prems'' = map (transform_prem1 context pred_names) prems' + val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems' in HEADGOAL (simp_tac (HOL_basic_ss addsimps (simps @ prems')) @@ -804,11 +804,13 @@ resolve_tac alpha_intros ])) end) ctxt -fun raw_perm_bn_rsp alpha_trms perm_bns alpha_induct alpha_intros simps ctxt = +fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps = let - val arg_ty = domain_type o fastype_of + val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = + alpha_result + val perm_bn_ty = range_type o range_type o fastype_of - val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms + val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms) val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) @@ -820,12 +822,10 @@ (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y)) end - val goals = map mk_prop perm_bns - val alpha_names = map (fst o dest_Const) alpha_trms - + val goals = map mk_prop perm_bns in - alpha_prove alpha_trms goals alpha_induct - (raw_prove_perm_bn_tac alpha_names alpha_intros simps) ctxt + alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct + (raw_prove_perm_bn_tac alpha_result simps) ctxt |> ProofContext.export ctxt' ctxt |> map atomize |> map single