--- a/Nominal/Nominal2.thy Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/Nominal2.thy Thu Dec 23 00:46:06 2010 +0000
@@ -16,250 +16,6 @@
use "nominal_dt_quot.ML"
ML {* open Nominal_Dt_Quot *}
-text {* TEST *}
-
-
-ML {*
-(* 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
-*}
-
-
-ML {*
-(* derives the freshness theorem that there exists a p, such that
- (p o as) #* (c, t1,\<dots>, 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
-*}
-
-ML {*
-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
-*}
-
-
-
-ML {*
-(* 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
-*}
-
-
-
-lemma setify:
- shows "xs = ys \<Longrightarrow> set xs = set ys"
- by simp
-
-ML {*
-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 @{thm 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
-*}
-
-ML {*
-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
-*}
-
-
ML {*
val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)