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