# HG changeset patch # User blanchet # Date 1348235609 -7200 # Node ID 464812bef4d9b89240c435f0dbb039f00f2c0c69 # Parent acc583e141677a42624b162c6dd05666ed91567e renamed "upto" coinduction "strong" diff -r acc583e14167 -r 464812bef4d9 src/HOL/Codatatype/Tools/bnf_fp.ML --- a/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -54,13 +54,13 @@ val morN: string val nchotomyN: string val pred_coinductN: string - val pred_coinduct_uptoN: string val pred_simpN: string + val pred_strong_coinductN: string val recN: string val recsN: string val rel_coinductN: string - val rel_coinduct_uptoN: string val rel_simpN: string + val rel_strong_coinductN: string val rvN: string val sel_coitersN: string val sel_corecsN: string @@ -69,11 +69,11 @@ val simpsN: string val strTN: string val str_initN: string + val strongN: string val sum_bdN: string val sum_bdTN: string val unfN: string val unf_coinductN: string - val unf_coinduct_uptoN: string val unf_coiterN: string val unf_coiter_uniqueN: string val unf_coitersN: string @@ -82,8 +82,8 @@ val unf_exhaustN: string val unf_fldN: string val unf_injectN: string + val unf_strong_coinductN: string val uniqueN: string - val uptoN: string val mk_exhaustN: string -> string val mk_injectN: string -> string @@ -226,10 +226,10 @@ val simpN = "_simp"; val rel_simpN = relN ^ simpN; val pred_simpN = predN ^ simpN; -val uptoN = "upto" -val unf_coinduct_uptoN = unf_coinductN ^ "_" ^ uptoN -val rel_coinduct_uptoN = rel_coinductN ^ "_" ^ uptoN -val pred_coinduct_uptoN = pred_coinductN ^ "_" ^ uptoN +val strongN = "strong_" +val unf_strong_coinductN = unfN ^ "_" ^ strongN ^ coinductN +val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN +val pred_strong_coinductN = predN ^ "_" ^ strongN ^ coinductN val hsetN = "Hset" val hset_recN = hsetN ^ "_rec" val set_inclN = "set_incl" diff -r acc583e14167 -r 464812bef4d9 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -2176,7 +2176,7 @@ val timer = time (timer "corec definitions & thms"); val (unf_coinduct_thm, coinduct_params, rel_coinduct_thm, pred_coinduct_thm, - unf_coinduct_upto_thm, rel_coinduct_upto_thm, pred_coinduct_upto_thm) = + unf_strong_coinduct_thm, rel_strong_coinduct_thm, pred_strong_coinduct_thm) = let val zs = Jzs1 @ Jzs2; val frees = phis @ zs; @@ -2253,16 +2253,16 @@ val cTs = map (SOME o certifyT lthy o TFree) coinduct_params; val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2; - val rel_coinduct_upto = singleton (Proof_Context.export names_lthy lthy) + val rel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] (fold_rev Logic.all zs (Logic.list_implies (rel_upto_prems, concl))) - (K (mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids))) + (K (mk_rel_strong_coinduct_tac m cTs cts rel_coinduct rel_monos rel_Ids))) |> Thm.close_derivation; - val unf_coinduct_upto = singleton (Proof_Context.export names_lthy lthy) + val unf_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] (fold_rev Logic.all zs (Logic.list_implies (unf_upto_prems, concl))) - (K (mk_unf_coinduct_upto_tac ks cTs cts unf_coinduct bis_def + (K (mk_unf_strong_coinduct_tac ks cTs cts unf_coinduct bis_def (tcoalg_thm RS bis_diag_thm)))) |> Thm.close_derivation; @@ -2270,10 +2270,10 @@ rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv}; val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct; - val pred_coinduct_upto = unfold_defs lthy pred_of_rel_thms rel_coinduct_upto; + val pred_strong_coinduct = unfold_defs lthy pred_of_rel_thms rel_strong_coinduct; in (unf_coinduct, rev (Term.add_tfrees unf_coinduct_goal []), rel_coinduct, pred_coinduct, - unf_coinduct_upto, rel_coinduct_upto, pred_coinduct_upto) + unf_strong_coinduct, rel_strong_coinduct, pred_strong_coinduct) end; val timer = time (timer "coinduction"); @@ -2955,9 +2955,9 @@ [(unf_coinductN, [unf_coinduct_thm]), (rel_coinductN, [rel_coinduct_thm]), (pred_coinductN, [pred_coinduct_thm]), - (unf_coinduct_uptoN, [unf_coinduct_upto_thm]), - (rel_coinduct_uptoN, [rel_coinduct_upto_thm]), - (pred_coinduct_uptoN, [pred_coinduct_upto_thm])] + (unf_strong_coinductN, [unf_strong_coinduct_thm]), + (rel_strong_coinductN, [rel_strong_coinduct_thm]), + (pred_strong_coinductN, [pred_strong_coinduct_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r acc583e14167 -r 464812bef4d9 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200 @@ -88,7 +88,7 @@ val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm list -> thm -> thm list -> tactic val mk_rel_coinduct_tac: 'a list -> thm -> thm -> tactic - val mk_rel_coinduct_upto_tac: int -> ctyp option list -> cterm option list -> thm -> thm list -> + val mk_rel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm -> thm list -> thm list -> tactic val mk_rel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm list -> thm list list -> tactic @@ -111,7 +111,7 @@ cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> thm list list -> thm -> thm list list -> tactic val mk_unf_coinduct_tac: int -> int list -> thm -> thm -> tactic - val mk_unf_coinduct_upto_tac: int list -> ctyp option list -> cterm option list -> thm -> thm -> + val mk_unf_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> thm -> thm -> tactic val mk_unf_o_fld_tac: thm -> thm -> thm -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic @@ -1132,7 +1132,7 @@ CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp, rtac CollectI, etac @{thm prod_caseI}])) ks] 1; -fun mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids = +fun mk_rel_strong_coinduct_tac m cTs cts rel_coinduct rel_monos rel_Ids = EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts rel_coinduct), EVERY' (map2 (fn rel_mono => fn rel_Id => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE, @@ -1165,7 +1165,7 @@ rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1 end; -fun mk_unf_coinduct_upto_tac ks cTs cts unf_coinduct bis_def bis_diag = +fun mk_unf_strong_coinduct_tac ks cTs cts unf_coinduct bis_def bis_diag = EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts unf_coinduct), EVERY' (map (fn i => EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp},