--- 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 *)