# HG changeset patch # User Christian Urban # Date 1280538325 -3600 # Node ID 920366e646b033eee88ea1e23baf001e11a8e450 # Parent 0f24c961b5f69b0ca7c2267718c442f561413797 further simplification with alpha_prove diff -r 0f24c961b5f6 -r 920366e646b0 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Sat Jul 31 01:24:39 2010 +0100 +++ b/Nominal/nominal_dt_alpha.ML Sat Jul 31 02:05:25 2010 +0100 @@ -381,11 +381,12 @@ (fn {context, ...} => HEADGOAL (DETERM o (rtac alpha_induct_thm) THEN_ALL_NEW (rtac @{thm TrueI} ORELSE' cases_tac context))) |> singleton (ProofContext.export ctxt' ctxt) - |> Datatype_Aux.split_conj_thm + |> Datatype_Aux.split_conj_thm + |> map (fn th => th RS mp) |> map Datatype_Aux.split_conj_thm |> flat |> map zero_var_indexes - |> map (fn th => th RS mp) + |> filter_out (is_true o concl_of) end @@ -549,7 +550,8 @@ (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt end -(* proves the equivp predicate for all alphas *) + +(** proves the equivp predicate for all alphas **) val equivp_intro = @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y. R x y --> (!z. R y z --> R x z)|] ==> equivp R" @@ -587,55 +589,15 @@ resolve_tac alpha_intros ])) end) ctxt -fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt = +fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt = let + val arg_ty = domain_type o fastype_of val alpha_names = map (fst o dest_Const) alpha_trms - - val arg_tys = - alpha_trms - |> map fastype_of - |> map domain_type - val arg_bn_tys = - alpha_bns - |> map fastype_of - |> map domain_type - val (arg_names1, (arg_names2, ctxt')) = - ctxt - |> Variable.variant_fixes (replicate (length arg_tys) "x") - ||> Variable.variant_fixes (replicate (length arg_tys) "y") - val arg_bn_names1 = map (lookup (arg_tys ~~ arg_names1)) arg_bn_tys - val arg_bn_names2 = map (lookup (arg_tys ~~ arg_names2)) arg_bn_tys - val args1 = map Free (arg_names1 ~~ arg_tys) - val args2 = map Free (arg_names2 ~~ arg_tys) - val arg_bns1 = map Free (arg_bn_names1 ~~ arg_bn_tys) - val arg_bns2 = map Free (arg_bn_names2 ~~ arg_bn_tys) - - val alpha_bn_trms = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_bns (arg_bns1 ~~ arg_bns2) - val true_trms = map (K @{term True}) arg_tys - - val goal_rhs = - group ((arg_bn_tys ~~ alpha_bn_trms) @ (arg_tys ~~ true_trms)) - |> map snd - |> map (foldr1 HOLogic.mk_conj) - - val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_trms (args1 ~~ args2) - val goal_rest = map (fn t => HOLogic.mk_imp (t, @{term "True"})) alpha_bn_trms - - val goal = - (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs) @ goal_rest - |> foldr1 HOLogic.mk_conj - |> HOLogic.mk_Trueprop + val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms + val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms in - Goal.prove ctxt' [] [] goal - (fn {context, ...} => - HEADGOAL (DETERM o (rtac alpha_induct) - THEN_ALL_NEW (raw_prove_bn_imp_tac alpha_names alpha_intros context))) - |> singleton (ProofContext.export ctxt' ctxt) - |> Datatype_Aux.split_conj_thm - |> map (fn th => zero_var_indexes (th RS mp)) - |> map Datatype_Aux.split_conj_thm - |> flat - |> filter_out (is_true o concl_of) + alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct + (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt end @@ -643,72 +605,18 @@ fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = let - val arg_tys = - alpha_trms - |> map fastype_of - |> map domain_type - - val fv_bn_tys1 = - (bns @ fvs) - |> map fastype_of - |> map domain_type - - val (arg_names1, (arg_names2, ctxt')) = - ctxt - |> Variable.variant_fixes (replicate (length arg_tys) "x") - ||> Variable.variant_fixes (replicate (length arg_tys) "y") - - val args1 = map Free (arg_names1 ~~ arg_tys) - val args2 = map Free (arg_names2 ~~ arg_tys) - - val fv_bn_args1a = map (lookup (arg_tys ~~ args1)) fv_bn_tys1 - val fv_bn_args1b = map (lookup (arg_tys ~~ args2)) fv_bn_tys1 - val fv_bn_eqs1 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) - (bns @ fvs) (fv_bn_args1a ~~ fv_bn_args1b) - - val arg_bn_tys = - alpha_bn_trms - |> map fastype_of - |> map domain_type + val arg_ty = domain_type o fastype_of + val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms - val fv_bn_tys2 = - fv_bns - |> map fastype_of - |> map domain_type - - val (arg_bn_names1, (arg_bn_names2, ctxt'')) = - ctxt' - |> Variable.variant_fixes (replicate (length arg_bn_tys) "x") - ||> Variable.variant_fixes (replicate (length arg_bn_tys) "y") + val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) fvs + val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) bns + val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => HOLogic.mk_eq (t2 $ x, t2 $ y))) alpha_bn_trms fv_bns - val args_bn1 = map Free (arg_bn_names1 ~~ fv_bn_tys2) - val args_bn2 = map Free (arg_bn_names2 ~~ fv_bn_tys2) - val fv_bn_eqs2 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) - fv_bns (args_bn1 ~~ args_bn2) - - val goal_rhs = - group (fv_bn_tys1 ~~ fv_bn_eqs1) - |> map snd - |> map (foldr1 HOLogic.mk_conj) - - val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) - (alpha_trms @ alpha_bn_trms) ((args1 ~~ args2) @ (args_bn1 ~~ args_bn2)) - - val goal = - map2 (curry HOLogic.mk_imp) goal_lhs (goal_rhs @ fv_bn_eqs2) - |> foldr1 HOLogic.mk_conj - |> HOLogic.mk_Trueprop - 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 - Goal.prove ctxt'' [] [] goal (fn {context, ...} => - HEADGOAL (DETERM o (rtac alpha_induct) THEN_ALL_NEW (asm_full_simp_tac ss))) - |> singleton (ProofContext.export ctxt'' ctxt) - |> Datatype_Aux.split_conj_thm - |> map (fn th => zero_var_indexes (th RS mp)) - |> map Datatype_Aux.split_conj_thm - |> flat + alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct + (K (asm_full_simp_tac ss)) ctxt end end (* structure *)