--- a/Nominal/nominal_dt_quot.ML Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML Thu Dec 23 00:46:06 2010 +0000
@@ -3,7 +3,7 @@
Author: Cezary Kaliszyk
Performing quotient constructions, lifting theorems and
- deriving support propoerties for the quotient types.
+ deriving support properties for the quotient types.
*)
signature NOMINAL_DT_QUOT =
@@ -38,6 +38,10 @@
val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
thm list -> Proof.context -> thm list
+
+ val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list ->
+ thm list -> thm list -> thm list -> thm list -> thm list
+
end
structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -373,5 +377,236 @@
|> map (simplify (HOL_basic_ss addsimps @{thms id_def}))
end
+
+(** proves strong exhauts theorems **)
+
+
+(* fixme: move into nominal_library *)
+fun abs_const bmode ty =
+ let
+ val (const_name, binder_ty, abs_ty) =
+ case bmode of
+ Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})
+ | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set})
+ | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res})
+ in
+ Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty]))
+ end
+
+fun mk_abs bmode trm1 trm2 =
+ abs_const bmode (fastype_of trm2) $ trm1 $ trm2
+
+fun is_abs_eq thm =
+ let
+ fun is_abs trm =
+ case (head_of trm) of
+ Const (@{const_name "Abs_set"}, _) => true
+ | Const (@{const_name "Abs_lst"}, _) => true
+ | Const (@{const_name "Abs_res"}, _) => true
+ | _ => false
+ in
+ thm |> prop_of
+ |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_eq
+ |> fst
+ |> is_abs
+ end
+
+
+(* adds a freshness condition to the assumptions *)
+fun mk_ecase_prems lthy c (params, prems, concl) bclauses =
+ let
+ val tys = map snd params
+ val binders = get_all_binders bclauses
+
+ fun prep_binder (opt, i) =
+ let
+ val t = Bound (length tys - i - 1)
+ in
+ case opt of
+ NONE => setify_ty lthy (nth tys i) t
+ | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)
+ end
+
+ val prems' =
+ case binders of
+ [] => prems (* case: no binders *)
+ | _ => binders (* case: binders *)
+ |> map prep_binder
+ |> fold_union_env tys
+ |> (fn t => mk_fresh_star t c)
+ |> (fn t => HOLogic.mk_Trueprop t :: prems)
+ in
+ mk_full_horn params prems' concl
+ end
+
+
+(* derives the freshness theorem that there exists a p, such that
+ (p o as) #* (c, t1,..., tn) *)
+fun fresh_thm ctxt c parms binders bn_finite_thms =
+ let
+ fun prep_binder (opt, i) =
+ case opt of
+ NONE => setify ctxt (nth parms i)
+ | SOME bn => to_set (bn $ (nth parms i))
+
+ fun prep_binder2 (opt, i) =
+ case opt of
+ NONE => atomify ctxt (nth parms i)
+ | SOME bn => bn $ (nth parms i)
+
+ val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))
+ val lhs = binders
+ |> map prep_binder
+ |> fold_union
+ |> mk_perm (Bound 0)
+
+ val goal = mk_fresh_star lhs rhs
+ |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))
+ |> HOLogic.mk_Trueprop
+
+ val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp}
+ @ @{thms finite.intros finite_Un finite_set finite_fset}
+ in
+ Goal.prove ctxt [] [] goal
+ (K (HEADGOAL (rtac @{thm at_set_avoiding1}
+ THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
+ end
+
+
+(* derives an abs_eq theorem of the form
+
+ Exists q. [as].x = [p o as].(q o x) for non-recursive binders
+ Exists q. [as].x = [q o as].(q o x) for recursive binders
+*)
+fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
+ (bclause as (BC (bmode, binders, bodies))) =
+ case binders of
+ [] => []
+ | _ =>
+ let
+ val rec_flag = is_recursive_binder bclause
+ val binder_trm = comb_binders ctxt bmode parms binders
+ val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
+
+ val abs_lhs = mk_abs bmode binder_trm body_trm
+ val abs_rhs =
+ if rec_flag
+ then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm)
+ else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm)
+
+ val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
+ val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm)
+
+ val goal = HOLogic.mk_conj (abs_eq, peq)
+ |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
+ |> HOLogic.mk_Trueprop
+
+ val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
+ @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
+ fresh_star_set} @ @{thms finite.intros finite_fset}
+
+ val tac1 =
+ if rec_flag
+ then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
+ else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
+
+ val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss]
+ in
+ [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
+ |> (if rec_flag
+ then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
+ else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ]
+ end
+
+
+val setify = @{lemma "xs = ys ==> set xs = set ys" by simp}
+
+fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas
+ prems bclausess qexhaust_thm =
+ let
+ fun aux_tac prem bclauses =
+ case (get_all_binders bclauses) of
+ [] => EVERY' [rtac prem, atac]
+ | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>
+ let
+ val parms = map (term_of o snd) params
+ val fthm = fresh_thm ctxt c parms binders bn_finite_thms
+
+ val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
+ val (([(_, fperm)], fprops), ctxt') = Obtain.result
+ (K (EVERY1 [etac exE,
+ full_simp_tac (HOL_basic_ss addsimps ss),
+ REPEAT o (etac @{thm conjE})])) [fthm] ctxt
+
+ val abs_eq_thms = flat
+ (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses)
+
+ val ((_, eqs), ctxt'') = Obtain.result
+ (K (EVERY1
+ [ REPEAT o (etac @{thm exE}),
+ REPEAT o (etac @{thm conjE}),
+ REPEAT o (dtac setify),
+ full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt'
+
+ val (abs_eqs, peqs) = split_filter is_abs_eq eqs
+
+ val fprops' =
+ map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
+ @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
+
+ (* for freshness conditions *)
+ val tac1 = SOLVED' (EVERY'
+ [ simp_tac (HOL_basic_ss addsimps peqs),
+ rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
+ conj_tac (DETERM o resolve_tac fprops') ])
+
+ (* for equalities between constructors *)
+ val tac2 = SOLVED' (EVERY'
+ [ rtac (@{thm ssubst} OF prems),
+ rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
+ rewrite_goal_tac (map safe_mk_equiv abs_eqs),
+ conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ])
+
+ (* proves goal "P" *)
+ val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
+ (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
+ |> singleton (ProofContext.export ctxt'' ctxt)
+ in
+ rtac side_thm 1
+ end) ctxt
+ in
+ EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
+ end
+
+
+fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns
+ perm_bn_alphas =
+ let
+ val ((_, exhausts'), lthy') = Variable.import true exhausts lthy
+
+ val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
+ val c = Free (c, TFree (a, @{sort fs}))
+
+ val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
+ |> map prop_of
+ |> map Logic.strip_horn
+ |> split_list
+
+ val ecases' = (map o map) strip_full_horn ecases
+
+ val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss
+
+ fun tac bclausess exhaust {prems, context} =
+ case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas
+ prems bclausess exhaust
+
+ fun prove prems bclausess exhaust concl =
+ Goal.prove lthy'' [] prems concl (tac bclausess exhaust)
+ in
+ map4 prove premss bclausesss exhausts' main_concls
+ |> ProofContext.export lthy'' lthy
+ end
+
end (* structure *)