# HG changeset patch # User Andreas Lochbihler # Date 1375978815 -7200 # Node ID 2b68f4109075b55a432be2c90e96e269cfc3a92d # Parent 5f3faf72b62a43e7ac94789a2dbfa921aaf576c0# Parent c10bd1f49ff5b4dc5b72a1aeadd116dad8a8597d merged diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/BNF_FP_Basic.thy --- a/src/HOL/BNF/BNF_FP_Basic.thy Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/BNF_FP_Basic.thy Thu Aug 08 18:20:15 2013 +0200 @@ -113,6 +113,36 @@ lemma spec2: "\x y. P x y \ P x y" by blast +lemma rewriteR_comp_comp: "\g o h = r\ \ f o g o h = f o r" + unfolding o_def fun_eq_iff by auto + +lemma rewriteR_comp_comp2: "\g o h = r1 o r2; f o r1 = l\ \ f o g o h = l o r2" + unfolding o_def fun_eq_iff by auto + +lemma rewriteL_comp_comp: "\f o g = l\ \ f o (g o h) = l o h" + unfolding o_def fun_eq_iff by auto + +lemma rewriteL_comp_comp2: "\f o g = l1 o l2; l2 o h = r\ \ f o (g o h) = l1 o r" + unfolding o_def fun_eq_iff by auto + +lemma convol_o: " o h = " + unfolding convol_def by auto + +lemma map_pair_o_convol: "map_pair h1 h2 o =

" + unfolding convol_def by auto + +lemma map_pair_o_convol_id: "(map_pair f id \ ) x = f , g> x" + unfolding map_pair_o_convol id_o o_id .. + +lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" + unfolding o_def by (auto split: sum.splits) + +lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)" + unfolding o_def by (auto split: sum.splits) + +lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x" + unfolding sum_case_o_sum_map id_o o_id .. + lemma fun_rel_def_butlast: "(fun_rel R (fun_rel S T)) f g = (\x y. R x y \ (fun_rel S T) (f x) (g y))" unfolding fun_rel_def .. diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Thu Aug 08 18:20:15 2013 +0200 @@ -13,9 +13,6 @@ "codatatype" :: thy_decl begin -lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" -unfolding o_def by (auto split: sum.splits) - lemma sum_case_expand_Inr: "f o Inl = g \ f x = sum_case g (f o Inr) x" by (auto split: sum.splits) diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Thu Aug 08 18:20:15 2013 +0200 @@ -44,9 +44,6 @@ lemma snd_convol': "snd ( x) = g x" using snd_convol unfolding convol_def by simp -lemma convol_o: " o h = " - unfolding convol_def by auto - lemma convol_expand_snd: "fst o f = g \ = f" unfolding convol_def by auto diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Aug 08 18:20:15 2013 +0200 @@ -9,6 +9,7 @@ signature BNF_FP_UTIL = sig datatype fp_kind = Least_FP | Greatest_FP + val fp_case: fp_kind -> 'a -> 'a -> 'a type fp_result = {Ts: typ list, @@ -54,11 +55,13 @@ val ctor_inductN: string val ctor_injectN: string val ctor_foldN: string + val ctor_fold_o_mapN: string + val ctor_fold_transferN: string val ctor_fold_uniqueN: string - val ctor_fold_transferN: string val ctor_mapN: string val ctor_map_uniqueN: string val ctor_recN: string + val ctor_rec_o_mapN: string val ctor_rec_uniqueN: string val ctor_relN: string val ctor_set_inclN: string @@ -70,6 +73,7 @@ val dtorN: string val dtor_coinductN: string val dtor_corecN: string + val dtor_corec_o_mapN: string val dtor_corec_uniqueN: string val dtor_ctorN: string val dtor_exhaustN: string @@ -83,8 +87,9 @@ val dtor_set_set_inclN: string val dtor_strong_coinductN: string val dtor_unfoldN: string + val dtor_unfold_o_mapN: string + val dtor_unfold_transferN: string val dtor_unfold_uniqueN: string - val dtor_unfold_transferN: string val exhaustN: string val foldN: string val hsetN: string @@ -175,6 +180,8 @@ val mk_un_fold_transfer_thms: fp_kind -> term list -> term list -> term list -> term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list + val mk_xtor_un_fold_o_map_thms: fp_kind -> bool -> int -> thm -> thm list -> thm list -> + thm list -> thm list -> thm list val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) -> @@ -190,6 +197,8 @@ open BNF_Util datatype fp_kind = Least_FP | Greatest_FP; +fun fp_case Least_FP f1 _ = f1 + | fp_case Greatest_FP _ f2 = f2; type fp_result = {Ts: typ list, @@ -256,7 +265,9 @@ val ctor_foldN = ctorN ^ "_" ^ foldN val dtor_unfoldN = dtorN ^ "_" ^ unfoldN val ctor_fold_uniqueN = ctor_foldN ^ uniqueN +val ctor_fold_o_mapN = ctor_foldN ^ "_o_" ^ mapN val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN +val dtor_unfold_o_mapN = dtor_unfoldN ^ "_o_" ^ mapN val ctor_fold_transferN = ctor_foldN ^ transferN val dtor_unfold_transferN = dtor_unfoldN ^ transferN val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN @@ -287,8 +298,10 @@ val recN = "rec" val corecN = coN ^ recN val ctor_recN = ctorN ^ "_" ^ recN +val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN val ctor_rec_uniqueN = ctor_recN ^ uniqueN val dtor_corecN = dtorN ^ "_" ^ corecN +val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN val dtor_corec_uniqueN = dtor_corecN ^ uniqueN val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN @@ -516,6 +529,37 @@ |> split_conj_thm end; +fun mk_xtor_un_fold_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps + map_cong0s = + let + val n = length sym_map_comps; + val rewrite_comp_comp2 = fp_case fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2}; + val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp}; + val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_o} @{thm o_id} RS fun_cong); + val map_cong_active_args1 = replicate n (if is_rec + then fp_case fp @{thm convol_o} @{thm o_sum_case} RS fun_cong + else refl); + val map_cong_passive_args2 = replicate m (fp_case fp @{thm o_id} @{thm id_o} RS fun_cong); + val map_cong_active_args2 = replicate n (if is_rec + then fp_case fp @{thm map_pair_o_convol_id} @{thm sum_case_o_sum_map_id} + else fp_case fp @{thm id_o} @{thm o_id} RS fun_cong); + fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s; + val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1; + val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2; + + fun mk_rewrites map_congs = map2 (fn sym_map_comp => fn map_cong => + mk_trans sym_map_comp map_cong RS rewrite_comp_comp) sym_map_comps map_congs; + val rewrite1s = mk_rewrites map_cong1s; + val rewrite2s = mk_rewrites map_cong2s; + val unique_prems = + map4 (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 => + mk_trans (rewrite_comp_comp2 OF [xtor_map, un_fold]) + (mk_trans rewrite1 (mk_sym rewrite2))) + xtor_maps xtor_un_folds rewrite1s rewrite2s; + in + split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems) + end; + fun fp_bnf construct_fp bs resBs eqs lthy = let val timer = time (Timer.startRealTimer ()); diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 18:20:15 2013 +0200 @@ -210,7 +210,7 @@ val bd_Cinfinite = hd bd_Cinfinites; val in_monos = map in_mono_of_bnf bnfs; val map_comps = map map_comp_of_bnf bnfs; - val sym_map_comps = map (fn thm => thm RS sym) map_comps; + val sym_map_comps = map mk_sym map_comps; val map_comp's = map map_comp'_of_bnf bnfs; val map_cong0s = map map_cong0_of_bnf bnfs; val map_ids = map map_id_of_bnf bnfs; @@ -2003,8 +2003,8 @@ |> Thm.close_derivation end; - val dtor_corec_unique_thms = - split_conj_thm (split_conj_prems n + val (dtor_corec_unique_thms, dtor_corec_unique_thm) = + `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @ map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); @@ -2131,10 +2131,11 @@ val in_rels = map in_rel_of_bnf bnfs; (*register new codatatypes as BNFs*) - val (timer, Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_set_induct_thms, - dtor_Jrel_thms, lthy) = + val (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss', + dtor_set_induct_thms, dtor_Jrel_thms, lthy) = if m = 0 then - (timer, replicate n DEADID_bnf, map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's, + (timer, replicate n DEADID_bnf, + map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's), replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; @@ -2254,7 +2255,7 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) - (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps) + (mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps) |> Thm.close_derivation end; @@ -2725,6 +2726,7 @@ val in_Jrels = map in_rel_of_bnf Jbnfs; val folded_dtor_map_thms = map fold_maps dtor_map_thms; + val folded_dtor_map_o_thms = map fold_maps map_thms; val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss; val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss; @@ -2767,10 +2769,18 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - (timer, Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_set_induct_thms, - dtor_Jrel_thms, lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd) + (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss', + dtor_set_induct_thms, dtor_Jrel_thms, + lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd) end; + val dtor_unfold_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m + dtor_unfold_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) + sym_map_comps map_cong0s; + val dtor_corec_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m + dtor_corec_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_corec_thms) + sym_map_comps map_cong0s; + val passiveABs = map2 (curry HOLogic.mk_prodT) passiveAs passiveBs; val zip_ranTs = passiveABs @ prodTsTs'; val allJphis = Jphis @ activeJphis; @@ -2906,7 +2916,9 @@ (dtor_injectN, dtor_inject_thms), (dtor_unfoldN, dtor_unfold_thms), (dtor_unfold_uniqueN, dtor_unfold_unique_thms), - (dtor_corec_uniqueN, dtor_corec_unique_thms)] + (dtor_corec_uniqueN, dtor_corec_unique_thms), + (dtor_unfold_o_mapN, dtor_unfold_o_map_thms), + (dtor_corec_o_mapN, dtor_corec_o_map_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 18:20:15 2013 +0200 @@ -1061,7 +1061,7 @@ EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1; fun mk_map_id_tac maps unfold_unique unfold_dtor = - EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps), + EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps), rtac unfold_dtor] 1; fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique = @@ -1114,9 +1114,9 @@ rtac conjI, rtac refl, rtac refl]) ks]) 1 end -fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} = +fun mk_dtor_map_unique_tac unfold_unique sym_map_comps {context = ctxt, prems = _} = rtac unfold_unique 1 THEN - unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN + unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN ALLGOALS (etac sym); fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 18:20:15 2013 +0200 @@ -1133,8 +1133,8 @@ `split_conj_thm unique_mor end; - val ctor_fold_unique_thms = - split_conj_thm (mk_conjIN n RS + val (ctor_fold_unique_thms, ctor_fold_unique_thm) = + `split_conj_thm (mk_conjIN n RS (mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm)) val fold_ctor_thms = @@ -1294,8 +1294,8 @@ |> Thm.close_derivation end; - val ctor_rec_unique_thms = - split_conj_thm (split_conj_prems n + val (ctor_rec_unique_thms, ctor_rec_unique_thm) = + `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm) |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @ map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); @@ -1396,9 +1396,11 @@ val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; (*register new datatypes as BNFs*) - val (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) = + val (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss', + ctor_Irel_thms, lthy) = if m = 0 then - (timer, replicate n DEADID_bnf, map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's, + (timer, replicate n DEADID_bnf, + map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's), replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; @@ -1446,7 +1448,7 @@ val p1s_maps = map (mk_map XTs p1s Ts ctors (mk_passive_maps passiveXs passiveAs)) ks; val p2s_maps = map (mk_map XTs p2s Ts' ctor's (mk_passive_maps passiveXs passiveBs)) ks; - val ctor_map_thms = + val (ctor_map_thms, ctor_map_o_thms) = let fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor), @@ -1458,7 +1460,7 @@ |> Thm.close_derivation) goals ctor_fold_thms map_comp_id_thms map_cong0s; in - map (fn thm => thm RS @{thm comp_eq_dest}) maps + `(map (fn thm => thm RS @{thm comp_eq_dest})) maps end; val (ctor_map_unique_thms, ctor_map_unique_thm) = @@ -1472,7 +1474,7 @@ (map2 (curry HOLogic.mk_eq) us fs_maps)); val unique = Goal.prove_sorry lthy [] [] (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) - (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_cong0s)) + (mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps) |> Thm.close_derivation; in `split_conj_thm unique @@ -1756,6 +1758,7 @@ val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss; val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss; val folded_ctor_map_thms = map fold_maps ctor_map_thms; + val folded_ctor_map_o_thms = map fold_maps ctor_map_o_thms; val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss; val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss; @@ -1797,10 +1800,15 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, - lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd) + (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss', + ctor_Irel_thms, lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd) end; + val ctor_fold_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm + folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; + val ctor_rec_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm + folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s; + val Irels = if m = 0 then map HOLogic.eq_const Ts else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; val Irel_induct_thm = @@ -1831,6 +1839,8 @@ (ctor_foldN, ctor_fold_thms), (ctor_fold_uniqueN, ctor_fold_unique_thms), (ctor_rec_uniqueN, ctor_rec_unique_thms), + (ctor_fold_o_mapN, ctor_fold_o_map_thms), + (ctor_rec_o_mapN, ctor_rec_o_map_thms), (ctor_injectN, ctor_inject_thms), (ctor_recN, ctor_rec_thms), (dtor_ctorN, dtor_ctor_thms), diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 08 18:20:15 2013 +0200 @@ -42,7 +42,7 @@ val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic val mk_map_id_tac: thm list -> thm -> tactic val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic - val mk_ctor_map_unique_tac: int -> thm -> thm -> thm list -> thm list -> tactic + val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm -> @@ -584,19 +584,10 @@ REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])), rtac sym, rtac o_apply] 1; -fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s = - let - val n = length map_cong0s; - fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm comp_eq_dest}, - rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong), - rtac (cong RS arg_cong), - REPEAT_DETERM_N m o rtac refl, - REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))]; - in - EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI, - CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_cong0s, - CONJ_WRAP' mk_mor (map_comp_ids ~~ map_cong0s)] 1 - end; +fun mk_ctor_map_unique_tac fold_unique sym_map_comps {context = ctxt, prems = _} = + rtac fold_unique 1 THEN + unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN + ALLGOALS atac; fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac sym, rtac o_apply] 1; diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/Tools/bnf_tactics.ML --- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 08 18:20:15 2013 +0200 @@ -19,6 +19,8 @@ val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> int -> tactic + val mk_pointfree: Proof.context -> thm -> thm + val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm val mk_Abs_inj_thm: thm -> thm @@ -53,6 +55,16 @@ fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x; +(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) +fun mk_pointfree ctxt thm = thm + |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq + |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp) + |> mk_Trueprop_eq + |> (fn goal => Goal.prove_sorry ctxt [] [] goal + (fn {context=ctxt, prems = _} => + unfold_thms_tac ctxt [@{thm o_def}, mk_sym thm] THEN rtac refl 1)) + |> Thm.close_derivation; + (* Theorems for open typedefs with UNIV as representing set *) diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Thu Aug 08 18:20:15 2013 +0200 @@ -604,7 +604,7 @@ (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys); fun mk_trans thm1 thm2 = trans OF [thm1, thm2]; -fun mk_sym thm = sym OF [thm]; +fun mk_sym thm = thm RS sym; (*TODO: antiquote heavily used theorems once*) val Pair_eqD = @{thm iffD1[OF Pair_eq]}; diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/IMP/Compiler.thy --- a/src/HOL/IMP/Compiler.thy Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/IMP/Compiler.thy Thu Aug 08 18:20:15 2013 +0200 @@ -2,7 +2,7 @@ header "Compiler for IMP" -theory Compiler imports Big_Step +theory Compiler imports Big_Step Star begin subsection "List setup" @@ -63,24 +63,25 @@ "P \ c \ c' = (\i s stk. c = (i,s,stk) \ c' = iexec(P!!i) (i,s,stk) \ 0 \ i \ i < size P)" +(* declare exec1_def [simp] +*) lemma exec1I [intro, code_pred_intro]: "c' = iexec (P!!i) (i,s,stk) \ 0 \ i \ i < size P \ P \ (i,s,stk) \ c'" -by simp +by (simp add: exec1_def) -inductive exec :: "instr list \ config \ config \ bool" - ("(_/ \ (_ \*/ _))" 50) +abbreviation + exec :: "instr list \ config \ config \ bool" ("(_/ \ (_ \*/ _))" 50) where -refl: "P \ c \* c" | -step: "P \ c \ c' \ P \ c' \* c'' \ P \ c \* c''" + "exec P \ star (exec1 P)" + +declare star.step[intro] -declare refl[intro] step[intro] +lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)] -lemmas exec_induct = exec.induct[split_format(complete)] - -code_pred exec by fastforce +code_pred exec1 by (metis exec1_def) values "{(i,map t [''x'',''y''],stk) | i t stk. @@ -90,9 +91,6 @@ subsection{* Verification infrastructure *} -lemma exec_trans: "P \ c \* c' \ P \ c' \* c'' \ P \ c \* c''" -by (induction rule: exec.induct) fastforce+ - text{* Below we need to argue about the execution of code that is embedded in larger programs. For this purpose we show that execution is preserved by appending code to the left or right of a program. *} @@ -102,16 +100,17 @@ by(auto split:instr.split) lemma exec1_appendR: "P \ c \ c' \ P@P' \ c \ c'" -by auto +by (auto simp: exec1_def) lemma exec_appendR: "P \ c \* c' \ P@P' \ c \* c'" -by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+ +by (induction rule: star.induct) (fastforce intro: exec1_appendR)+ lemma exec1_appendL: fixes i i' :: int shows "P \ (i,s,stk) \ (i',s',stk') \ P' @ P \ (size(P')+i,s,stk) \ (size(P')+i',s',stk')" + unfolding exec1_def by (auto split: instr.split) lemma exec_appendL: @@ -154,7 +153,7 @@ j'' = size P + i'' \ P @ P' \ (0,s,stk) \* (j'',s'',stk'')" -by(metis exec_trans[OF exec_appendR exec_appendL_if]) +by(metis star_trans[OF exec_appendR exec_appendL_if]) declare Let_def[simp] @@ -237,7 +236,7 @@ moreover have "?cc1 @ ?cc2 \ (size ?cc1,s2,stk) \* (size(?cc1 @ ?cc2),s3,stk)" using Seq.IH(2) by fastforce - ultimately show ?case by simp (blast intro: exec_trans) + ultimately show ?case by simp (blast intro: star_trans) next case (WhileTrue b s1 c s2 s3) let ?cc = "ccomp c" @@ -253,7 +252,7 @@ by fastforce moreover have "?cw \ (0,s2,stk) \* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2)) - ultimately show ?case by(blast intro: exec_trans) + ultimately show ?case by(blast intro: star_trans) qed fastforce+ end diff -r 5f3faf72b62a -r 2b68f4109075 src/HOL/IMP/Compiler2.thy --- a/src/HOL/IMP/Compiler2.thy Thu Aug 08 18:15:12 2013 +0200 +++ b/src/HOL/IMP/Compiler2.thy Thu Aug 08 18:20:15 2013 +0200 @@ -50,7 +50,7 @@ lemma exec_exec_n: "P \ c \* c' \ \n. P \ c \^n c'" - by (induct rule: exec.induct) (auto simp del: exec1_def intro: exec_Suc) + by (induct rule: star.induct) (auto intro: exec_Suc) lemma exec_eq_exec_n: "(P \ c \* c') = (\n. P \ c \^n c')" @@ -58,7 +58,7 @@ lemma exec_n_Nil [simp]: "[] \ c \^k c' = (c' = c \ k = 0)" - by (induct k) auto + by (induct k) (auto simp: exec1_def) lemma exec1_exec_n [intro!]: "P \ c \ c' \ P \ c \^1 c'" @@ -75,7 +75,7 @@ lemma exec1_end: "size P <= fst c \ \ P \ c \ c'" - by auto + by (auto simp: exec1_def) lemma exec_n_end: "size P <= (n::int) \ @@ -262,7 +262,7 @@ shows "P @ c @ P' \ (size P + i, s) \ (j,s') \ 0 \ i \ i < size c \ c \ (i,s) \ (j - size P, s')" - by (auto split: instr.splits) + by (auto split: instr.splits simp: exec1_def) lemma exec_n_split: fixes i j :: int @@ -304,7 +304,7 @@ assume "j0 \ {0 ..< size c}" moreover from c j0 have "j0 \ succs c 0" - by (auto dest: succs_iexec1 simp del: iexec.simps) + by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps) ultimately have "j0 \ exits c" by (simp add: exits_def) with c j0 rest @@ -343,7 +343,8 @@ have "n = size P1 + (n - size P1)" by simp then obtain n' :: int where "n = size P1 + n'" .. ultimately - show ?thesis using assms by (clarsimp simp del: iexec.simps) + show ?thesis using assms + by (clarsimp simp: exec1_def simp del: iexec.simps) qed lemma exec_n_drop_left: @@ -365,7 +366,7 @@ by (rule exec1_drop_left) moreover then have "i' - size P \ succs P' 0" - by (fastforce dest!: succs_iexec1 simp del: iexec.simps) + by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps) with `exits P' \ {0..}` have "size P \ i'" by (auto simp: exits_def) from rest this `exits P' \ {0..}` @@ -438,8 +439,8 @@ "[ADD] \ (0,s2,stk2) \^n3 (1, s', stk')" by (auto dest!: exec_n_split_full) - thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps) -qed (auto simp: exec_n_simps) + thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps exec1_def) +qed (auto simp: exec_n_simps exec1_def) lemma bcomp_split: fixes i j :: int @@ -460,7 +461,7 @@ s' = s \ stk' = stk" using assms proof (induction b arbitrary: c j i n s' stk') case Bc thus ?case - by (simp split: split_if_asm add: exec_n_simps) + by (simp split: split_if_asm add: exec_n_simps exec1_def) next case (Not b) from Not.prems show ?case @@ -488,7 +489,7 @@ by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm) next case Less - thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *) + thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps exec1_def) (* takes time *) qed lemma ccomp_empty [elim!]: @@ -506,7 +507,7 @@ next case (Assign x a) thus ?case - by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps) + by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps exec1_def) next case (Seq c1 c2) thus ?case by (fastforce dest!: exec_n_split_full) @@ -542,7 +543,8 @@ show ?thesis by simp (fastforce dest: exec_n_drop_right - split: split_if_asm simp: exec_n_simps) + split: split_if_asm + simp: exec_n_simps exec1_def) next case False with cs' show ?thesis @@ -583,7 +585,7 @@ obtain m where "?cs \ (0,s,stk) \^m (size (ccomp ?c0), t, stk')" "m < n" - by (auto simp: exec_n_step [where k=k]) + by (auto simp: exec_n_step [where k=k] exec1_def) with "1.IH" show ?case by blast next @@ -603,7 +605,7 @@ obtain k' where "?cs \ (0, s'', stk) \^k' (size ?cs, t, stk')" "k' < n" - by (auto simp: exec_n_step [where k=m]) + by (auto simp: exec_n_step [where k=m] exec1_def) with "1.IH" have "(?c0, s'') \ t \ stk' = stk" by blast ultimately