# HG changeset patch # User blanchet # Date 1383558761 -3600 # Node ID 7cc6e286fe28b64fbd17d9e2571f2e4ef837d5b1 # Parent e000095237279f75af3da934148b1add59d98ac7 made sugared 'coinduct' theorem construction n2m-proof diff -r e00009523727 -r 7cc6e286fe28 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Mon Nov 04 10:52:41 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_def.ML Mon Nov 04 10:52:41 2013 +0100 @@ -79,8 +79,8 @@ val mk_map: int -> typ list -> typ list -> term -> term val mk_rel: int -> typ list -> typ list -> term -> term - val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term - val build_rel: local_theory -> (typ * typ -> term) -> typ * typ -> term + val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term + val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term val mk_witness: int list * term -> thm list -> nonemptiness_witness val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list @@ -501,7 +501,7 @@ Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t end; -fun build_map_or_rel mk const of_bnf dest lthy build_simple = +fun build_map_or_rel mk const of_bnf dest ctxt build_simple = let fun build (TU as (T, U)) = if T = U then @@ -511,7 +511,7 @@ (Type (s, Ts), Type (s', Us)) => if s = s' then let - val bnf = the (bnf_of lthy s); + val bnf = the (bnf_of ctxt s); val live = live_of_bnf bnf; val mapx = mk live Ts Us (of_bnf bnf); val TUs' = map dest (fst (strip_typeN live (fastype_of mapx))); diff -r e00009523727 -r 7cc6e286fe28 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Nov 04 10:52:41 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Nov 04 10:52:41 2013 +0100 @@ -40,7 +40,6 @@ val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list val dest_map: Proof.context -> string -> term -> term * term list - val dest_ctr: Proof.context -> string -> term -> term * term list type lfp_sugar_thms = (thm list * thm * Args.src list) @@ -348,7 +347,7 @@ fun nesty_bnfs ctxt ctr_Tsss Us = map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []); -fun indexify proj xs f p = f (find_index (curry op = (proj p)) xs) p; +fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p; type lfp_sugar_thms = (thm list * thm * Args.src list) @@ -390,7 +389,7 @@ ns mss ctr_Tsss ctor_iter_fun_Tss; val z_Tsss' = map (map flat_rec_arg_args) z_Tssss; - val h_Tss = map2 (map2 (curry op --->)) z_Tsss' Css; + val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css; val hss = map2 (map2 retype_free) h_Tss gss; val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss; @@ -412,7 +411,7 @@ val f_sum_prod_Ts = map range_type fun_Ts; val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts; val f_Tsss = map2 (map2 (dest_tupleT o length)) ctr_Tsss' f_prod_Tss; - val f_Tssss = map3 (fn C => map2 (map2 (map (curry op --> C) oo unzip_corecT))) + val f_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT))) Cs ctr_Tsss' f_Tsss; val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss; in @@ -537,7 +536,7 @@ fun generate_iter suf (f_Tss, _, fss, xssss) ctor_iter = let - val res_T = fold_rev (curry op --->) f_Tss fpT_to_C; + val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C; val b = mk_binding suf; val spec = mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)), @@ -556,7 +555,7 @@ fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter = let - val res_T = fold_rev (curry op --->) pf_Tss C_to_fpT; + val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT; val b = mk_binding suf; val spec = mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)), @@ -605,7 +604,7 @@ val lives = lives_of_bnf bnf; val sets = sets_of_bnf bnf; fun mk_set U = - (case find_index (curry op = U) lives of + (case find_index (curry (op =) U) lives of ~1 => Term.dummy | i => nth sets i); in @@ -622,7 +621,7 @@ end; fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) = - [([], (find_index (curry op = X) Xs + 1, x))] + [([], (find_index (curry (op =) X) Xs + 1, x))] | mk_raw_prem_prems names_lthy (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) = (case AList.lookup (op =) setss_nested T_name of NONE => [] @@ -662,7 +661,7 @@ val goal = Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry op $) ps us))); + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us))); val kksss = map (map (map (fst o snd) o #2)) raw_premss; @@ -781,39 +780,29 @@ map4 (fn u => fn v => fn uvr => fn uv_eq => fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; - fun build_rel rs' T = - (case find_index (curry op = T) fpTs of - ~1 => - if exists_subtype_in fpTs T then - let - val Type (s, Ts) = T - val bnf = the (bnf_of lthy s); - val live = live_of_bnf bnf; - val rel = mk_rel live Ts Ts (rel_of_bnf bnf); - val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel))); - in Term.list_comb (rel, map (build_rel rs') Ts') end - else - HOLogic.eq_const T - | kk => nth rs' kk); + fun build_the_rel rs' T Xs_T = + build_rel lthy (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) + |> Term.subst_atomic_types (Xs ~~ fpTs); - fun build_rel_app rs' usel vsel = fold rapp [usel, vsel] (build_rel rs' (fastype_of usel)); + fun build_rel_app rs' usel vsel Xs_T = + fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T); - fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels = + fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts = (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ (if null usels then [] else [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], - Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app rs') usels vsels))]); + Library.foldr1 HOLogic.mk_conj (map3 (build_rel_app rs') usels vsels ctrXs_Ts))]); - fun mk_prem_concl rs' n udiscs uselss vdiscs vselss = - Library.foldr1 HOLogic.mk_conj - (flat (map5 (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss)) + fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = + Library.foldr1 HOLogic.mk_conj (flat (map6 (mk_prem_ctr_concls rs' n) + (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss)) handle List.Empty => @{term True}; - fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss = + fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, - HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss))); + HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss))); val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -821,8 +810,8 @@ uvrs us vs)); fun mk_goal rs' = - Logic.list_implies (map8 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss, - concl); + Logic.list_implies (map9 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss + ctrXs_Tsss, concl); val goals = map mk_goal [rs, strong_rs];