# HG changeset patch # User Christian Urban # Date 1293063761 0 # Node ID 478c5648e73fa7826bde1855b3302f79d5ffc4c7 # Parent bfa48c000aa7def28ed01aa0b83e9f97d2bbde92 moved generic functions into nominal_library diff -r bfa48c000aa7 -r 478c5648e73f Nominal/Ex/Ex1.thy --- 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) diff -r bfa48c000aa7 -r 478c5648e73f Nominal/Nominal2.thy --- 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 \"} $ _ $ _ => (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 \ 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 diff -r bfa48c000aa7 -r 478c5648e73f Nominal/nominal_library.ML --- 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