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