--- a/Nominal/Nominal2.thy Wed Dec 22 23:12:51 2010 +0000
+++ b/Nominal/Nominal2.thy Thu Dec 23 00:22:41 2010 +0000
@@ -18,41 +18,6 @@
text {* TEST *}
-ML {*
-fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
- | strip_outer_params B = ([], B)
-
-fun strip_params_prems_concl trm =
- let
- val (params, body) = strip_outer_params trm
- val (prems, concl) = Logic.strip_horn body
- in
- (params, prems, concl)
- end
-
-fun list_params_prems_concl params prems concl =
- Logic.list_implies (prems, concl)
- |> fold_rev mk_all params
-
-fun mk_binop_env tys c (t, u) =
- let val ty = fastype_of1 (tys, t) in
- Const (c, [ty, ty] ---> ty) $ t $ u
- end
-
-fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1
- | mk_union_env tys (@{term "{}::atom set"}, t2) = t2
- | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1
- | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2
- | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2)
-
-fun fold_left f [] z = z
- | fold_left f [x] z = x
- | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z
-
-fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"}
-*}
-
-
ML {*
(* adds a freshness condition to the assumptions *)
@@ -79,7 +44,7 @@
|> (fn t => mk_fresh_star t c)
|> (fn t => HOLogic.mk_Trueprop t :: prems)
in
- list_params_prems_concl params prems' concl
+ mk_full_horn params prems' concl
end
*}
@@ -119,77 +84,20 @@
*}
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 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 body_ty = fastype_of body_trm
-
- fun mk_abs cnst_name ty1 ty2 =
- Const (cnst_name, [ty1, body_ty] ---> Type (ty2, [body_ty]))
-
- val abs_const =
- case bmode of
- Lst => mk_abs @{const_name "Abs_lst"} @{typ "atom list"} @{type_name abs_lst}
- | Set => mk_abs @{const_name "Abs_set"} @{typ "atom set"} @{type_name abs_set}
- | Res => mk_abs @{const_name "Abs_res"} @{typ "atom set"} @{type_name abs_res}
-
- val abs_lhs = abs_const $ binder_trm $ body_trm
- val abs_rhs =
- if flag
- then abs_const $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm
- else abs_const $ mk_perm (Bound 0) 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)
+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
- 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 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 flag
- then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
- else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns [])
- ]
- end
-*}
+fun mk_abs bmode trm1 trm2 =
+ abs_const bmode (fastype_of trm2) $ trm1 $ trm2
-ML {*
-fun conj_tac tac i =
- let
- fun select (t, i) =
- case t of
- @{term "Trueprop"} $ t' => select (t', i)
- | @{term "op \<and>"} $ _ $ _ => (rtac @{thm conjI} THEN' RANGE [conj_tac tac, conj_tac tac]) i
- | _ => tac i
- in
- SUBGOAL select i
- end
-*}
-
-ML {*
fun is_abs_eq thm =
let
fun is_abs trm =
@@ -207,6 +115,57 @@
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
@@ -241,43 +200,27 @@
val (abs_eqs, peqs) = split_filter is_abs_eq eqs
- val fprops' = map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
- val fprops'' = map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
+ val fprops' =
+ map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
+ @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
- val _ = tracing ("prem:\n" ^ (Syntax.string_of_term ctxt'' o prop_of) prem)
- val _ = tracing ("prems:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) prems))
- val _ = tracing ("fprop':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops'))
- val _ = tracing ("fprop'':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops''))
- val _ = tracing ("abseq:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) abs_eqs))
- val _ = tracing ("peqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) peqs))
-
-
- val tac1 = EVERY'
+ (* for freshness conditions *)
+ val tac1 = SOLVED' (EVERY'
[ simp_tac (HOL_basic_ss addsimps peqs),
rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
- K (print_tac "before solving freshness"),
- conj_tac (TRY o DETERM o resolve_tac (fprops' @ fprops'')) ]
+ conj_tac (DETERM o resolve_tac fprops') ])
- val tac2 = EVERY'
+ (* for equalities between constructors *)
+ val tac2 = SOLVED' (EVERY'
[ rtac (@{thm ssubst} OF prems),
rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
- K (print_tac "before substituting"),
rewrite_goal_tac (map safe_mk_equiv abs_eqs),
- K (print_tac "after substituting"),
- conj_tac (TRY o DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)),
- K (print_tac "end")
- ]
+ conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ])
+ (* proves goal "P" *)
val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
- (fn _ => (* Skip_Proof.cheat_tac (ProofContext.theory_of ctxt'') *)
- EVERY
- [ rtac prem 1,
- print_tac "after applying prem",
- RANGE [SOLVED' tac1, SOLVED' tac2] 1,
- print_tac "final" ] )
+ (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
|> singleton (ProofContext.export ctxt'' ctxt)
-
- val _ = tracing ("side_thm:\n" ^ (Syntax.string_of_term ctxt o prop_of) side_thm)
in
rtac side_thm 1
end) ctxt
@@ -295,13 +238,14 @@
val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
val c = Free (c, TFree (a, @{sort fs}))
- val (ecases, main_concls) = exhausts' (* ecases or of the form (params, prems, concl) *)
+ val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
|> map prop_of
|> map Logic.strip_horn
|> split_list
- |>> (map o map) strip_params_prems_concl
- val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases bclausesss
+ 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