diff -r 07f775729e90 -r 9fa37acdb2ce Nominal/nominal_dt_supp.ML --- a/Nominal/nominal_dt_supp.ML Mon Dec 06 17:11:34 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,218 +0,0 @@ -(* Title: nominal_dt_alpha.ML - Author: Christian Urban - Author: Cezary Kaliszyk - - Deriving support propoerties for the quotient types. -*) - -signature NOMINAL_DT_SUPP = -sig - -end - -structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = -struct - -(* 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 - -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 - -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 - -fun prove_supports ctxt perm_simps qtrms = - map (prove_supports_single ctxt perm_simps) qtrms - - -(* 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 - - 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}) - - 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 gen_mk_goals fv supp = - let - val arg_ty = - fastype_of fv - |> domain_type - in - (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x)) - end - -fun mk_fvs_goals fv = gen_mk_goals fv mk_supp -fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn) - -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 trm = - trm - |> fastype_of - |> body_type - |> (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", [trm])) - - -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_def permute_prod_def - prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} - -fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps - fv_bn_eqvts qinduct bclausess ctxt = - let - val goals1 = map mk_fvs_goals fvs - val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns - - fun tac ctxt = - SUBGOAL (fn (goal, i) => - let - val (fv_fun, arg) = - goal |> Envir.eta_contract - |> Logic.strip_assums_concl - |> HOLogic.dest_Trueprop - |> fst o HOLogic.dest_eq - |> dest_comb - val supp_abs_tac = - case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of - SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) - | NONE => mk_bn_supp_abs_tac fv_fun - in - EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), - TRY o supp_abs_tac, - TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), - TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], - TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), - TRY o asm_full_simp_tac (add_ss thms3), - TRY o simp_tac (add_ss thms2), - TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i - end) - in - induct_prove qtys (goals1 @ goals2) qinduct tac ctxt - |> map atomize - |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]})) - end - - -fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt = - let - fun mk_goal qbn = - let - val arg_ty = domain_type (fastype_of qbn) - val finite = @{term "finite :: atom set => bool"} - in - (arg_ty, fn x => finite $ (to_set (qbn $ x))) - end - - val props = map mk_goal qbns - val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ - @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) - in - induct_prove qtys props qinduct (K ss_tac) ctxt - end - -fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt = - let - val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt - val p = Free (p, @{typ perm}) - - fun mk_goal qperm_bn alpha_bn = - let - val arg_ty = domain_type (fastype_of alpha_bn) - in - (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) - end - - val props = map2 mk_goal qperm_bns alpha_bns - val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls - val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss) - in - induct_prove qtys props qinduct (K ss_tac) ctxt' - |> ProofContext.export ctxt' ctxt - |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) - end - - -end (* structure *)