# HG changeset patch # User blanchet # Date 1348404773 -7200 # Node ID 8bb6e2d7346be5b7e684959fbf3462c7bf2a9a25 # Parent 24094fa47e0d853bb70c355746711a38ab598798 renamed coinduction principles to have "dtor" in the name diff -r 24094fa47e0d -r 8bb6e2d7346b 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 @@ -45,17 +45,21 @@ val disc_corecsN: string val dtorN: string val dtor_coinductN: string - val dtor_mapN: string - val dtor_relN: 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_uniqueN: string + val dtor_relN: string + val dtor_rel_coinductN: string + val dtor_rel_strong_coinductN: string val dtor_set_inclN: string val dtor_set_set_inclN: string 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 @@ -75,8 +79,6 @@ val nchotomyN: string val recN: string val recsN: string - val rel_coinductN: string - val rel_strong_coinductN: string val relsN: string val rvN: string val sel_corecsN: string @@ -85,8 +87,6 @@ val set_inclN: string val set_set_inclN: string val simpsN: string - val srel_coinductN: string - val srel_strong_coinductN: string val strTN: string val str_initN: string val strongN: string @@ -235,21 +235,21 @@ val ctor_exhaustN = mk_exhaustN ctorN val dtor_injectN = mk_injectN dtorN val dtor_exhaustN = mk_exhaustN dtorN +val ctor_relN = ctorN ^ "_" ^ relN +val dtor_relN = dtorN ^ "_" ^ relN +val ctor_srelN = ctorN ^ "_" ^ srelN +val dtor_srelN = dtorN ^ "_" ^ srelN val inductN = "induct" val coinductN = coN ^ inductN val ctor_inductN = ctorN ^ "_" ^ inductN val ctor_induct2N = ctor_inductN ^ "2" val dtor_coinductN = dtorN ^ "_" ^ coinductN -val rel_coinductN = relN ^ "_" ^ coinductN -val srel_coinductN = srelN ^ "_" ^ coinductN -val ctor_srelN = ctorN ^ "_" ^ srelN -val dtor_srelN = dtorN ^ "_" ^ srelN -val ctor_relN = ctorN ^ "_" ^ relN -val dtor_relN = dtorN ^ "_" ^ relN +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 rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN -val srel_strong_coinductN = srelN ^ "_" ^ strongN ^ coinductN +val dtor_rel_strong_coinductN = dtor_relN ^ "_" ^ strongN ^ coinductN +val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strongN ^ coinductN val hsetN = "Hset" val hset_recN = hsetN ^ "_rec" val set_inclN = "set_incl" diff -r 24094fa47e0d -r 8bb6e2d7346b 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 @@ -2178,8 +2178,8 @@ val timer = time (timer "corec definitions & thms"); - val (dtor_coinduct_thm, coinduct_params, srel_coinduct_thm, rel_coinduct_thm, - dtor_strong_coinduct_thm, srel_strong_coinduct_thm, rel_strong_coinduct_thm) = + 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) = let val zs = Jzs1 @ Jzs2; val frees = phis @ zs; @@ -2213,12 +2213,13 @@ val srel_prems = map5 (mk_srel_prem false) phis dtors srels Jzs Jzs_copy; val srel_upto_prems = map5 (mk_srel_prem true) phis dtors srels Jzs Jzs_copy; - val srel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl)); - val coinduct_params = rev (Term.add_tfrees srel_coinduct_goal []); - - val srel_coinduct = unfold_thms lthy @{thms diag_UNIV} - (Skip_Proof.prove lthy [] [] srel_coinduct_goal - (K (mk_srel_coinduct_tac ks raw_coind_thm bis_srel_thm)) + val dtor_srel_coinduct_goal = + fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl)); + val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []); + + val dtor_srel_coinduct = unfold_thms lthy @{thms diag_UNIV} + (Skip_Proof.prove lthy [] [] dtor_srel_coinduct_goal + (K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm)) |> Thm.close_derivation); fun mk_dtor_prem upto_eq phi dtor map_nth sets Jz Jz_copy FJz = @@ -2256,10 +2257,10 @@ 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 srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) + val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] (fold_rev Logic.all zs (Logic.list_implies (srel_upto_prems, concl))) - (K (mk_srel_strong_coinduct_tac m cTs cts srel_coinduct srel_monos srel_Ids))) + (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) @@ -2272,11 +2273,12 @@ val rel_of_srel_thms = srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv}; - val rel_coinduct = unfold_thms lthy rel_of_srel_thms srel_coinduct; - val rel_strong_coinduct = unfold_thms lthy rel_of_srel_thms srel_strong_coinduct; + 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 []), srel_coinduct, rel_coinduct, - dtor_strong_coinduct, srel_strong_coinduct, rel_strong_coinduct) + (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), dtor_srel_coinduct, + dtor_rel_coinduct, dtor_strong_coinduct, dtor_srel_strong_coinduct, + dtor_rel_strong_coinduct) end; val timer = time (timer "coinduction"); @@ -2957,10 +2959,10 @@ val common_notes = [(dtor_coinductN, [dtor_coinduct_thm]), (dtor_strong_coinductN, [dtor_strong_coinduct_thm]), - (rel_coinductN, [rel_coinduct_thm]), - (rel_strong_coinductN, [rel_strong_coinduct_thm]), - (srel_coinductN, [srel_coinduct_thm]), - (srel_strong_coinductN, [srel_strong_coinduct_thm])] + (dtor_rel_coinductN, [dtor_rel_coinduct_thm]), + (dtor_rel_strong_coinductN, [dtor_rel_strong_coinduct_thm]), + (dtor_srel_coinductN, [dtor_srel_coinduct_thm]), + (dtor_srel_strong_coinductN, [dtor_srel_strong_coinduct_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r 24094fa47e0d -r 8bb6e2d7346b 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 @@ -38,6 +38,9 @@ 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_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 -> @@ -108,9 +111,6 @@ val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> tactic val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic - val mk_srel_coinduct_tac: 'a list -> thm -> thm -> tactic - val mk_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm -> - thm list -> thm list -> tactic val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list -> 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 @@ -1123,7 +1123,7 @@ REPEAT_DETERM_N m o rtac refl, EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1; -fun mk_srel_coinduct_tac ks raw_coind bis_srel = +fun mk_dtor_srel_coinduct_tac ks raw_coind bis_srel = EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI, CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks, CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI, @@ -1132,8 +1132,8 @@ CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp, rtac CollectI, etac @{thm prod_caseI}])) ks] 1; -fun mk_srel_strong_coinduct_tac m cTs cts srel_coinduct srel_monos srel_Ids = - EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts srel_coinduct), +fun mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids = + EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_srel_coinduct), EVERY' (map2 (fn srel_mono => fn srel_Id => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE, etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp), diff -r 24094fa47e0d -r 8bb6e2d7346b 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 @@ -1784,9 +1784,9 @@ val Ibnf_notes = [(ctor_mapN, map single folded_ctor_map_thms), (ctor_relN, map single ctor_Irel_thms), - (ctor_srelN, map single ctor_Isrel_thms), (ctor_set_inclN, ctor_set_incl_thmss), - (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @ + (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss), + (ctor_srelN, map single ctor_Isrel_thms)] @ 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 =>