# HG changeset patch # User blanchet # Date 1348646459 -7200 # Node ID 4e5bd3883429f32d05254558418aff0c2ef19d76 # Parent 040cfb087b3a9320bcca4a0f0bf0ee80b73d9919 renamed "dtor_coinduct" etc. to "dtor_map_coinduct" diff -r 040cfb087b3a -r 4e5bd3883429 src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:00:59 2012 +0200 @@ -44,13 +44,14 @@ val disc_corec_iffN: string val disc_corecsN: string val dtorN: string - val dtor_coinductN: string val dtor_corecN: string val dtor_corecsN: string val dtor_ctorN: string val dtor_exhaustN: string val dtor_injectN: string val dtor_mapN: string + val dtor_map_coinductN: string + val dtor_map_strong_coinductN: string val dtor_map_uniqueN: string val dtor_relN: string val dtor_rel_coinductN: string @@ -60,7 +61,6 @@ val dtor_srelN: string val dtor_srel_coinductN: string val dtor_srel_strong_coinductN: string - val dtor_strong_coinductN: string val dtor_unfoldN: string val dtor_unfold_uniqueN: string val dtor_unfoldsN: string @@ -243,11 +243,11 @@ val coinductN = coN ^ inductN val ctor_inductN = ctorN ^ "_" ^ inductN val ctor_induct2N = ctor_inductN ^ "2" -val dtor_coinductN = dtorN ^ "_" ^ coinductN +val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN val dtor_rel_coinductN = dtor_relN ^ "_" ^ coinductN val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN val strongN = "strong_" -val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN +val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strongN ^ coinductN val dtor_rel_strong_coinductN = dtor_relN ^ "_" ^ strongN ^ coinductN val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strongN ^ coinductN val hsetN = "Hset" diff -r 040cfb087b3a -r 4e5bd3883429 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:00:59 2012 +0200 @@ -2180,8 +2180,9 @@ val timer = time (timer "corec definitions & thms"); - val (dtor_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_rel_coinduct_thm, - dtor_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, dtor_rel_strong_coinduct_thm) = + val (dtor_map_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_rel_coinduct_thm, + dtor_map_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, + dtor_rel_strong_coinduct_thm) = let val zs = Jzs1 @ Jzs2; val frees = phis @ zs; @@ -2251,9 +2252,9 @@ val dtor_prems = mk_dtor_prems false; val dtor_upto_prems = mk_dtor_prems true; - val dtor_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (dtor_prems, concl)); - val dtor_coinduct = Skip_Proof.prove lthy [] [] dtor_coinduct_goal - (K (mk_dtor_coinduct_tac m ks raw_coind_thm bis_def)) + val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (dtor_prems, concl)); + val dtor_map_coinduct = Skip_Proof.prove lthy [] [] dtor_map_coinduct_goal + (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def)) |> Thm.close_derivation; val cTs = map (SOME o certifyT lthy o TFree) coinduct_params; @@ -2265,10 +2266,10 @@ (K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids))) |> Thm.close_derivation; - val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) + val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] (fold_rev Logic.all zs (Logic.list_implies (dtor_upto_prems, concl))) - (K (mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def + (K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def (tcoalg_thm RS bis_diag_thm)))) |> Thm.close_derivation; @@ -2278,8 +2279,8 @@ val dtor_rel_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_coinduct; val dtor_rel_strong_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_strong_coinduct; in - (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), dtor_srel_coinduct, - dtor_rel_coinduct, dtor_strong_coinduct, dtor_srel_strong_coinduct, + (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_srel_coinduct, + dtor_rel_coinduct, dtor_map_strong_coinduct, dtor_srel_strong_coinduct, dtor_rel_strong_coinduct) end; @@ -2546,7 +2547,7 @@ val cphis = map9 mk_cphi setss_by_bnf Jzs' Jzs fs_maps fs_copy_maps Jys' Jys Jys'_copy Jys_copy; - val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm; + val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -2965,8 +2966,8 @@ [(dtor_rel_coinductN, [dtor_rel_coinduct_thm]), (dtor_rel_strong_coinductN, [dtor_rel_strong_coinduct_thm])] @ (if note_all then - [(dtor_coinductN, [dtor_coinduct_thm]), - (dtor_strong_coinductN, [dtor_strong_coinduct_thm]), + [(dtor_map_coinductN, [dtor_map_coinduct_thm]), + (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]), (dtor_srel_coinductN, [dtor_srel_coinduct_thm]), (dtor_srel_strong_coinductN, [dtor_srel_strong_coinduct_thm])] else @@ -2992,7 +2993,7 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - ((dtors, ctors, Jrels, unfolds, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms, + ((dtors, ctors, Jrels, unfolds, corecs, dtor_map_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms), lthy |> Local_Theory.notes (common_notes @ notes) |> snd) end; diff -r 040cfb087b3a -r 4e5bd3883429 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Sep 26 10:00:59 2012 +0200 @@ -37,14 +37,14 @@ val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic val mk_corec_tac: int -> thm list -> thm -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic - val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic + val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic + val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> + thm -> thm -> tactic val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm -> thm list -> thm list -> tactic val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm list -> thm list list -> tactic - val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> - thm -> thm -> tactic val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic @@ -1144,7 +1144,7 @@ rtac impI, REPEAT_DETERM o etac conjE, CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) srel_Ids] 1; -fun mk_dtor_coinduct_tac m ks raw_coind bis_def = +fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def = let val n = length ks; in @@ -1165,8 +1165,8 @@ rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1 end; -fun mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def bis_diag = - EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct), +fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag = + EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct), EVERY' (map (fn i => EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp}, atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,