diff -r 6e37bfb62474 -r 486d4647bb37 Nominal/nominal_dt_supp.ML --- a/Nominal/nominal_dt_supp.ML Sun Sep 05 07:00:19 2010 +0800 +++ b/Nominal/nominal_dt_supp.ML Fri Sep 10 09:17:40 2010 +0800 @@ -12,44 +12,48 @@ val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> local_theory -> local_theory + + val prove_fv_supp: typ list -> term list -> term list -> term list -> thm list -> thm list -> + thm list -> thm list -> thm list -> thm list -> bclause list list -> Proof.context -> thm list end structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = struct +fun lookup xs x = the (AList.lookup (op=) xs x) (* supports lemmas for constructors *) fun mk_supports_goal ctxt qtrm = -let - val vs = fresh_args ctxt qtrm - val rhs = list_comb (qtrm, vs) - val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} - |> mk_supp -in - mk_supports lhs rhs - |> HOLogic.mk_Trueprop -end + let + val vs = fresh_args ctxt qtrm + val rhs = list_comb (qtrm, vs) + val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} + |> mk_supp + in + mk_supports lhs rhs + |> HOLogic.mk_Trueprop + end fun supports_tac ctxt perm_simps = -let - val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} - val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} -in - EVERY' [ simp_tac ss1, - Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], - simp_tac ss2 ] -end + let + val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} + val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} + in + EVERY' [ simp_tac ss1, + Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], + simp_tac ss2 ] + end fun prove_supports_single ctxt perm_simps qtrm = -let - val goal = mk_supports_goal ctxt qtrm - val ctxt' = Variable.auto_fixes goal ctxt -in - Goal.prove ctxt' [] [] goal - (K (HEADGOAL (supports_tac ctxt perm_simps))) - |> singleton (ProofContext.export ctxt' ctxt) -end + let + val goal = mk_supports_goal ctxt qtrm + val ctxt' = Variable.auto_fixes goal ctxt + in + Goal.prove ctxt' [] [] goal + (K (HEADGOAL (supports_tac ctxt perm_simps))) + |> singleton (ProofContext.export ctxt' ctxt) + end fun prove_supports ctxt perm_simps qtrms = map (prove_supports_single ctxt perm_simps) qtrms @@ -58,44 +62,182 @@ (* finite supp lemmas for qtypes *) fun prove_fsupp ctxt qtys qinduct qsupports_thms = -let - val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt - val goals = vs ~~ qtys - |> map Free - |> map (mk_finite o mk_supp) - |> foldr1 (HOLogic.mk_conj) - |> HOLogic.mk_Trueprop + let + val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt + val goals = vs ~~ qtys + |> map Free + |> map (mk_finite o mk_supp) + |> foldr1 (HOLogic.mk_conj) + |> HOLogic.mk_Trueprop - val tac = - EVERY' [ rtac @{thm supports_finite}, - resolve_tac qsupports_thms, - asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] -in - Goal.prove ctxt' [] [] goals - (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) - |> singleton (ProofContext.export ctxt' ctxt) - |> Datatype_Aux.split_conj_thm - |> map zero_var_indexes -end + val tac = + EVERY' [ rtac @{thm supports_finite}, + resolve_tac qsupports_thms, + asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] + in + Goal.prove ctxt' [] [] goals + (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) + |> singleton (ProofContext.export ctxt' ctxt) + |> Datatype_Aux.split_conj_thm + |> map zero_var_indexes + end (* finite supp instances *) fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy = -let - val lthy1 = - lthy - |> Local_Theory.exit_global - |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) + let + val lthy1 = + lthy + |> Local_Theory.exit_global + |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) - fun tac _ = - Class.intro_classes_tac [] THEN - (ALLGOALS (resolve_tac qfsupp_thms)) -in - lthy1 - |> Class.prove_instantiation_exit tac - |> Named_Target.theory_init -end + fun tac _ = + Class.intro_classes_tac [] THEN + (ALLGOALS (resolve_tac qfsupp_thms)) + in + lthy1 + |> Class.prove_instantiation_exit tac + |> Named_Target.theory_init + end + + +(* proves that fv and fv_bn equals supp *) + +fun mk_fvs_goals ty_arg_map fv = + let + val arg = fastype_of fv + |> domain_type + |> lookup ty_arg_map + in + (fv $ arg, mk_supp arg) + |> HOLogic.mk_eq + |> HOLogic.mk_Trueprop + end + +fun mk_fv_bns_goals ty_arg_map fv_bn alpha_bn = + let + val arg = fastype_of fv_bn + |> domain_type + |> lookup ty_arg_map + in + (fv_bn $ arg, mk_supp_rel alpha_bn arg) + |> HOLogic.mk_eq + |> HOLogic.mk_Trueprop + end + +fun add_ss thms = + HOL_basic_ss addsimps thms + +fun symmetric thms = + map (fn thm => thm RS @{thm sym}) thms + +val supp_abs_set = @{thms supp_abs(1)[symmetric]} +val supp_abs_res = @{thms supp_abs(2)[symmetric]} +val supp_abs_lst = @{thms supp_abs(3)[symmetric]} + +fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_set + | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_res + | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_lst + +fun mk_supp_abs_tac ctxt [] = [] + | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs + | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs + +fun mk_bn_supp_abs_tac thm = + (prop_of thm) + |> HOLogic.dest_Trueprop + |> snd o HOLogic.dest_eq + |> fastype_of + |> (fn ty => case ty of + @{typ "atom set"} => simp_tac (add_ss supp_abs_set) + | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst) + | _ => raise TERM ("mk_bn_supp_abs_tac", [prop_of thm])) + + +val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} +val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} +val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def + prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI} + +fun ind_tac ctxt qinducts = + let + fun CASES_TAC_TO_TAC cases_tac st = Seq.map snd (cases_tac st) + in + DETERM o (CASES_TAC_TO_TAC o (Induct.induct_tac ctxt false [] [] [] (SOME qinducts) [])) + end + +fun p_tac msg i = + if false then print_tac ("ptest: " ^ msg) else all_tac + +fun q_tac msg i = + if true then print_tac ("qtest: " ^ msg) else all_tac + +fun prove_fv_supp qtys fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps + fv_bn_eqvts qinducts bclausess ctxt = + let + val (arg_names, ctxt') = + Variable.variant_fixes (replicate (length qtys) "x") ctxt + val args = map2 (curry Free) arg_names qtys + val ty_arg_map = qtys ~~ args + val ind_args = map SOME arg_names + + val goals1 = map (mk_fvs_goals ty_arg_map) fvs + val goals2 = map2 (mk_fv_bns_goals ty_arg_map) fv_bns alpha_bns + + fun fv_tac ctxt bclauses = + SOLVED' (EVERY' [ + (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ " with " ^ (@{make_string} bclauses))), + TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), + p_tac "A", + TRY o EVERY' (mk_supp_abs_tac ctxt bclauses), + p_tac "B", + TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), + p_tac "C", + TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], + p_tac "D", + TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), + p_tac "E", + TRY o asm_full_simp_tac (add_ss thms3), + p_tac "F", + TRY o simp_tac (add_ss thms2), + p_tac "G", + TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), + p_tac "H", + (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i)) + ]) + + fun bn_tac ctxt bn_simp = + SOLVED' (EVERY' [ + (fn i => print_tac ("BN Goal: " ^ string_of_int i)), + TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), + q_tac "A", + TRY o mk_bn_supp_abs_tac bn_simp, + q_tac "B", + TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), + q_tac "C", + TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], + q_tac "D", + TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), + q_tac "E", + TRY o asm_full_simp_tac (add_ss thms3), + q_tac "F", + TRY o simp_tac (add_ss thms2), + q_tac "G", + TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), + (fn i => print_tac ("finished with BN Goal: " ^ string_of_int i)) + ]) + + fun fv_tacs ctxt = map (fv_tac ctxt) bclausess + fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps + + in + Goal.prove_multi ctxt' [] [] (goals1 @ goals2) + (fn {context as ctxt, ...} => HEADGOAL + (ind_tac ctxt qinducts THEN' RANGE (fv_tacs ctxt @ bn_tacs ctxt))) + |> ProofContext.export ctxt' ctxt + end + end (* structure *)