# HG changeset patch # User blanchet # Date 1348404773 -7200 # Node ID b39354db8629642f883a381d17cd08c4ab174c1b # Parent 32fb6e4c7f4be9cbf955746f759ed2ff7971c547 renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name diff -r 32fb6e4c7f4b -r b39354db8629 src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -90,11 +90,13 @@ val unfoldsN: string val uniqueN: string + val mk_ctor_setsN: int -> string + val mk_dtor_set_inductN: int -> string + val mk_dtor_setsN: int -> string val mk_exhaustN: string -> string val mk_injectN: string -> string val mk_nchotomyN: string -> string - val mk_set_simpsN: int -> string - val mk_set_minimalN: int -> string + val mk_setsN: int -> string val mk_set_inductN: int -> string val mk_common_name: string list -> string @@ -196,9 +198,11 @@ val LevN = "Lev" val rvN = "recover" val behN = "beh" -fun mk_set_simpsN i = mk_setN i ^ "_" ^ simpsN -fun mk_set_minimalN i = mk_setN i ^ "_minimal" +fun mk_setsN i = mk_setN i ^ "s" +val mk_ctor_setsN = prefix (ctorN ^ "_") o mk_setsN +val mk_dtor_setsN = prefix (dtorN ^ "_") o mk_setsN fun mk_set_inductN i = mk_setN i ^ "_induct" +val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN val str_initN = "str_init" val recN = "rec" diff -r 32fb6e4c7f4b -r b39354db8629 src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML Sun Sep 23 14:52:53 2012 +0200 @@ -70,6 +70,8 @@ unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; +(* TODO: Try "map_pair_simp" instead of "map_pair_def" everywhere. *) + val rec_like_unfold_thms = @{thms comp_def convol_def id_apply map_pair_def prod_case_Pair_iden sum.simps(5,6) sum_map.simps split_conv unit_case_Unity}; @@ -79,7 +81,7 @@ rec_like_unfold_thms) THEN unfold_thms_tac ctxt @{thms id_def} THEN rtac refl 1; val corec_like_ss = ss_only @{thms if_True if_False}; -val corec_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases}; +val corec_like_unfold_thms = @{thms id_apply map_pair_def prod.cases sum_map.simps}; fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt = unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN diff -r 32fb6e4c7f4b -r b39354db8629 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -2302,7 +2302,7 @@ val YTs = mk_Ts passiveYs; val ((((((((((((((((((((fs, fs'), fs_copy), gs), us), - (Jys, Jys')), (Jys_copy, Jys'_copy)), set_induct_phiss), JRs), Jphis), + (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss), JRs), Jphis), B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)), names_lthy) = names_lthy |> mk_Frees' "f" fTs @@ -2677,7 +2677,7 @@ val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs; - val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, hset_induct_thms) = + val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) = let fun tinst_of dtor = map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors); @@ -2713,7 +2713,7 @@ SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y', HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz)))))) phis jsets Jzs Jzs'; - val set_induct_thms = + val dtor_set_induct_thms = map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => ((set_minimal |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y') @@ -2722,9 +2722,9 @@ maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss)) |> singleton (Proof_Context.export names_lthy lthy) |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl))) - set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' set_induct_phiss + set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss in - (set_incl_thmss, set_set_incl_thmsss, set_induct_thms) + (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms) end; fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit); @@ -2833,7 +2833,7 @@ Skip_Proof.prove lthy [] [] goal (mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms) |> Thm.close_derivation) - goals hset_induct_thms + goals dtor_hset_induct_thms |> map split_conj_thm |> transpose |> map (map_filter (try (fn thm => thm RS bspec RS mp))) @@ -2876,7 +2876,7 @@ val set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss; val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss; - val set_induct_thms = map fold_sets hset_induct_thms; + val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms; val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; val Jsrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Jbnfs; @@ -2905,10 +2905,10 @@ val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs; in map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong => - fn dtor_map => fn set_simps => fn dtor_inject => fn dtor_ctor => + fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => fn set_naturals => fn set_incls => fn set_set_inclss => Skip_Proof.prove lthy [] [] goal - (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map set_simps + (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor set_naturals set_incls set_set_inclss)) |> Thm.close_derivation) ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss' @@ -2934,7 +2934,7 @@ val Jbnf_common_notes = [(map_uniqueN, [fold_maps map_unique_thm])] @ - map2 (fn i => fn thm => (mk_set_inductN i, [thm])) ls' set_induct_thms + map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_set_induct_thms |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); @@ -2944,7 +2944,7 @@ (dtor_srelN, map single dtor_Jsrel_thms), (set_inclN, set_incl_thmss), (set_set_inclN, map flat set_set_incl_thmsss)] @ - map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss + map2 (fn i => fn thms => (mk_dtor_setsN i, map single thms)) ls' folded_set_simp_thmss |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) diff -r 32fb6e4c7f4b -r b39354db8629 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 @@ -1494,7 +1494,7 @@ ALLGOALS (TRY o FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) -fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map set_simps dtor_inject dtor_ctor +fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor set_naturals set_incls set_set_inclss = let val m = length set_incls; @@ -1538,7 +1538,7 @@ dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) (rev (active_set_naturals ~~ in_Jsrels))]) - (set_simps ~~ passive_set_naturals), + (dtor_sets ~~ passive_set_naturals), rtac conjI, REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map, rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans, diff -r 32fb6e4c7f4b -r b39354db8629 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -1475,13 +1475,13 @@ FTs_setss ctors xFs sets) ls setss_by_range; - val set_simpss = map3 (fn i => map3 (fn set_nats => fn goal => fn set => + val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set => Skip_Proof.prove lthy [] [] goal (K (mk_set_simp_tac set (nth set_nats (i - 1)) (drop m set_nats))) |> Thm.close_derivation) set_natural'ss) ls simp_goalss setss; in - set_simpss + ctor_setss end; fun mk_set_thms set_simp = (@{thm xt1(3)} OF [set_simp, @{thm Un_upper1}]) :: @@ -1522,9 +1522,9 @@ fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss ctor_map_thms; val thms = - map5 (fn goal => fn csets => fn set_simps => fn induct => fn i => + map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i => singleton (Proof_Context.export names_lthy lthy) - (Skip_Proof.prove lthy [] [] goal (mk_tac induct csets set_simps i)) + (Skip_Proof.prove lthy [] [] goal (mk_tac induct csets ctor_sets i)) |> Thm.close_derivation) goals csetss set_simp_thmss inducts ls; in @@ -1549,9 +1549,9 @@ fun mk_tac induct = mk_set_bd_tac m (rtac induct) bd_Cinfinite set_bd_cpowss; val thms = - map4 (fn goal => fn set_simps => fn induct => fn i => + map4 (fn goal => fn ctor_sets => fn induct => fn i => singleton (Proof_Context.export names_lthy lthy) - (Skip_Proof.prove lthy [] [] goal (mk_tac induct set_simps i)) + (Skip_Proof.prove lthy [] [] goal (mk_tac induct ctor_sets i)) |> Thm.close_derivation) goals set_simp_thmss inducts ls; in @@ -1748,10 +1748,10 @@ val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs; in map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong => - fn ctor_map => fn set_simps => fn ctor_inject => fn ctor_dtor => + fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor => fn set_naturals => fn set_incls => fn set_set_inclss => Skip_Proof.prove lthy [] [] goal - (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map set_simps + (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject ctor_dtor set_naturals set_incls set_set_inclss)) |> Thm.close_derivation) ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss' @@ -1786,7 +1786,7 @@ (ctor_srelN, map single ctor_Isrel_thms), (set_inclN, set_incl_thmss), (set_set_inclN, map flat set_set_incl_thmsss)] @ - map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss + map2 (fn i => fn thms => (mk_ctor_setsN i, map single thms)) ls' folded_set_simp_thmss |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) diff -r 32fb6e4c7f4b -r b39354db8629 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 @@ -607,7 +607,7 @@ end; fun mk_set_nat_tac m induct_tac set_natural'ss - ctor_maps csets set_simps i {context = ctxt, prems = _} = + ctor_maps csets ctor_sets i {context = ctxt, prems = _} = let val n = length ctor_maps; @@ -623,12 +623,12 @@ REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})), EVERY' (map useIH (drop m set_nats))]; in - (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps set_simps set_natural'ss)) 1 + (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_natural'ss)) 1 end; -fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss set_simps i {context = ctxt, prems = _} = +fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i {context = ctxt, prems = _} = let - val n = length set_simps; + val n = length ctor_sets; fun useIH set_bd = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac set_bd, rtac ballI, Goal.assume_rule_tac ctxt, rtac bd_Cinfinite]; @@ -639,7 +639,7 @@ REPEAT_DETERM_N (n - 1) o rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), EVERY' (map useIH (drop m set_bds))]; in - (induct_tac THEN' EVERY' (map2 mk_set_nat set_simps set_bdss)) 1 + (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1 end; fun mk_mcong_tac induct_tac set_setsss map_congs ctor_maps {context = ctxt, prems = _} = @@ -676,7 +676,7 @@ (induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1 end; -fun mk_lfp_map_wpull_tac m induct_tac wpulls ctor_maps set_simpss set_setsss ctor_injects = +fun mk_lfp_map_wpull_tac m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects = let val n = length wpulls; val ks = 1 upto n; @@ -701,7 +701,7 @@ EVERY' [rtac @{thm UN_least}, rtac CollectE, etac set_rev_mp, atac, REPEAT_DETERM o etac conjE, atac]]; - fun mk_wpull wpull ctor_map set_simps set_setss ctor_inject = + fun mk_wpull wpull ctor_map ctor_sets set_setss ctor_inject = EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac rev_mp, rtac wpull, EVERY' (map (fn i => REPEAT_DETERM_N (i - 1) o etac thin_rl THEN' atac) ls), @@ -715,9 +715,9 @@ rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map, rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], hyp_subst_tac, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI, - CONJ_WRAP' mk_subset set_simps]; + CONJ_WRAP' mk_subset ctor_sets]; in - (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps set_simpss set_setsss ctor_injects)) 1 + (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps ctor_setss set_setsss ctor_injects)) 1 end; (* BNF tactics *) @@ -770,7 +770,7 @@ EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp, REPEAT_DETERM_N n o etac UnE]))))] 1); -fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map set_simps ctor_inject +fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject ctor_dtor set_naturals set_incls set_set_inclss = let val m = length set_incls; @@ -819,7 +819,7 @@ dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) (rev (active_set_naturals ~~ in_Isrels))]) - (set_simps ~~ passive_set_naturals), + (ctor_sets ~~ passive_set_naturals), rtac conjI, REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2), rtac trans, rtac map_comp, rtac trans, rtac map_cong,