--- a/Nominal/Ex/Ex1.thy Wed Dec 22 23:12:51 2010 +0000
+++ b/Nominal/Ex/Ex1.thy Thu Dec 23 00:22:41 2010 +0000
@@ -40,8 +40,8 @@
thm foo_bar.supp
lemma
- "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"
-apply(simp only: foo_bar.fv_defs)
+ "supp (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"
+apply(simp only: foo_bar.supp)
apply(simp only: foo_bar.bn_defs)
apply(simp only: supp_at_base)
apply(simp)
--- 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
--- a/Nominal/nominal_library.ML Wed Dec 22 23:12:51 2010 +0000
+++ b/Nominal/nominal_library.ML Thu Dec 23 00:22:41 2010 +0000
@@ -11,8 +11,8 @@
val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
+ val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a
-
val is_true: term -> bool
val dest_listT: typ -> typ
@@ -94,9 +94,18 @@
val mk_conj: term * term -> term
val fold_conj: term list -> term
+ (* functions for de-Bruijn open terms *)
+ val mk_binop_env: typ list -> string -> term * term -> term
+ val mk_union_env: typ list -> term * term -> term
+ val fold_union_env: typ list -> term list -> term
+
(* fresh arguments for a term *)
val fresh_args: Proof.context -> term -> term list
+ (* some logic operations *)
+ val strip_full_horn: term -> (string * typ) list * term list * term
+ val mk_full_horn: (string * typ) list -> term list -> term -> term
+
(* datatype operations *)
type cns_info = (term * typ * typ list * bool list) list
@@ -117,6 +126,8 @@
(* transformation into the object logic *)
val atomize: thm -> thm
+ (* applies a tactic to a formula composed of conjunctions *)
+ val conj_tac: (int -> tactic) -> int -> tactic
end
@@ -152,6 +163,12 @@
else (r, x :: l)
end
+(* to be used with left-infix binop-operations *)
+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 is_true @{term "Trueprop True"} = true
| is_true _ = false
@@ -343,6 +360,24 @@
fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
+(* functions for de-Bruijn open terms *)
+
+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_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"}
+
+
(* produces fresh arguments for a term *)
fun fresh_args ctxt f =
@@ -353,6 +388,24 @@
|> map Free
+(** some logic operations **)
+
+(* decompses a formula into params, premises and a conclusion *)
+fun strip_full_horn trm =
+ let
+ fun strip_outer_params (Const ("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
+ | strip_outer_params B = ([], B)
+
+ val (params, body) = strip_outer_params trm
+ val (prems, concl) = Logic.strip_horn body
+ in
+ (params, prems, concl)
+ end
+
+(* composes a formula out of params, premises and a conclusion *)
+fun mk_full_horn params prems concl =
+ Logic.list_implies (prems, concl)
+ |> fold_rev mk_all params
(** datatypes **)
@@ -532,6 +585,19 @@
(* transformes a theorem into one of the object logic *)
val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
+(* applies a tactic to a formula composed of conjunctions *)
+fun conj_tac tac i =
+ let
+ fun select (trm, i) =
+ case trm of
+ @{term "Trueprop"} $ t' => select (t', i)
+ | @{term "op &"} $ _ $ _ => EVERY' [rtac @{thm conjI}, RANGE [conj_tac tac, conj_tac tac]] i
+ | _ => tac i
+ in
+ SUBGOAL select i
+ end
+
+
end (* structure *)
open Nominal_Library;
\ No newline at end of file