# HG changeset patch # User blanchet # Date 1348404773 -7200 # Node ID 24094fa47e0d853bb70c355746711a38ab598798 # Parent 53b3c532a08238741c65a1f69eea8e34eb890fb4 renamed "set_incl" etc. to have "ctor" or "dtor" in the name diff -r 53b3c532a082 -r 24094fa47e0d 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 @@ -36,6 +36,8 @@ val ctor_recN: string val ctor_recsN: string val ctor_relN: string + val ctor_set_inclN: string + val ctor_set_set_inclN: string val ctor_srelN: string val disc_unfold_iffN: string val disc_unfoldsN: string @@ -51,6 +53,8 @@ val dtor_exhaustN: string val dtor_injectN: string val dtor_map_uniqueN: string + val dtor_set_inclN: string + val dtor_set_set_inclN: string val dtor_srelN: string val dtor_strong_coinductN: string val dtor_unfoldN: string @@ -249,7 +253,11 @@ val hsetN = "Hset" val hset_recN = hsetN ^ "_rec" val set_inclN = "set_incl" +val ctor_set_inclN = ctorN ^ "_" ^ set_inclN +val dtor_set_inclN = dtorN ^ "_" ^ set_inclN val set_set_inclN = "set_set_incl" +val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN +val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN val caseN = "case" val discN = "disc" diff -r 53b3c532a082 -r 24094fa47e0d 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 @@ -2874,8 +2874,8 @@ val timer = time (timer "registered new codatatypes as BNFs"); - 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 dtor_set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss; + val dtor_set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss; 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; @@ -2906,13 +2906,14 @@ in map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong => fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => - fn set_naturals => fn set_incls => fn set_set_inclss => + fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss => Skip_Proof.prove lthy [] [] goal (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)) + dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss)) |> Thm.close_derivation) ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss' - dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss + dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss + dtor_set_set_incl_thmsss end; val dtor_Jrel_thms = @@ -2941,9 +2942,9 @@ val Jbnf_notes = [(dtor_mapN, map single folded_dtor_map_thms), (dtor_relN, map single dtor_Jrel_thms), - (dtor_srelN, map single dtor_Jsrel_thms), - (set_inclN, set_incl_thmss), - (set_set_inclN, map flat set_set_incl_thmsss)] @ + (dtor_set_inclN, dtor_set_incl_thmss), + (dtor_set_set_inclN, map flat dtor_set_set_incl_thmsss), + (dtor_srelN, map single dtor_Jsrel_thms)] @ 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 => diff -r 53b3c532a082 -r 24094fa47e0d 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 @@ -1495,10 +1495,10 @@ 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 dtor_sets dtor_inject dtor_ctor - set_naturals set_incls set_set_inclss = + set_naturals dtor_set_incls dtor_set_set_inclss = let - val m = length set_incls; - val n = length set_set_inclss; + val m = length dtor_set_incls; + val n = length dtor_set_set_inclss; val (passive_set_naturals, active_set_naturals) = chop m set_naturals; val in_Jsrel = nth in_Jsrels (i - 1); val if_tac = @@ -1508,13 +1508,13 @@ EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural, rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, etac (set_incl RS @{thm subset_trans})]) - passive_set_naturals set_incls), - CONJ_WRAP' (fn (in_Jsrel, (set_natural, set_set_incls)) => + passive_set_naturals dtor_set_incls), + CONJ_WRAP' (fn (in_Jsrel, (set_natural, dtor_set_set_incls)) => EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI}, rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls, + CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls, rtac conjI, rtac refl, rtac refl]) - (in_Jsrels ~~ (active_set_naturals ~~ set_set_inclss)), + (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)), CONJ_WRAP' (fn conv => EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, diff -r 53b3c532a082 -r 24094fa47e0d 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 @@ -1734,8 +1734,8 @@ val Isrel_defs = map srel_def_of_bnf Ibnfs; val Irel_defs = map rel_def_of_bnf Ibnfs; - val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss; - val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss; + 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_set_simp_thmss = map (map fold_sets) set_simp_thmss; val folded_set_simp_thmss' = transpose folded_set_simp_thmss; @@ -1749,13 +1749,14 @@ in map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong => fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor => - fn set_naturals => fn set_incls => fn set_set_inclss => + fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss => Skip_Proof.prove lthy [] [] goal (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)) + ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss)) |> Thm.close_derivation) ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss' - ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss + ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss + ctor_set_set_incl_thmsss end; val ctor_Irel_thms = @@ -1784,8 +1785,8 @@ [(ctor_mapN, map single folded_ctor_map_thms), (ctor_relN, map single ctor_Irel_thms), (ctor_srelN, map single ctor_Isrel_thms), - (set_inclN, set_incl_thmss), - (set_set_inclN, map flat set_set_incl_thmsss)] @ + (ctor_set_inclN, ctor_set_incl_thmss), + (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @ 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 => diff -r 53b3c532a082 -r 24094fa47e0d 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 @@ -771,10 +771,10 @@ REPEAT_DETERM_N n o etac UnE]))))] 1); 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 = + ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss = let - val m = length set_incls; - val n = length set_set_inclss; + val m = length ctor_set_incls; + val n = length ctor_set_set_inclss; val (passive_set_naturals, active_set_naturals) = chop m set_naturals; val in_Isrel = nth in_Isrels (i - 1); @@ -783,19 +783,19 @@ val if_tac = EVERY' [dtac (in_Isrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - EVERY' (map2 (fn set_natural => fn set_incl => + EVERY' (map2 (fn set_natural => fn ctor_set_incl => EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural, rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, - rtac (set_incl RS subset_trans), etac le_arg_cong_ctor_dtor]) - passive_set_naturals set_incls), - CONJ_WRAP' (fn (in_Isrel, (set_natural, set_set_incls)) => + rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor]) + passive_set_naturals ctor_set_incls), + CONJ_WRAP' (fn (in_Isrel, (set_natural, ctor_set_set_incls)) => EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI}, rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor])) - set_set_incls, + ctor_set_set_incls, rtac conjI, rtac refl, rtac refl]) - (in_Isrels ~~ (active_set_naturals ~~ set_set_inclss)), + (in_Isrels ~~ (active_set_naturals ~~ ctor_set_set_inclss)), CONJ_WRAP' (fn conv => EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},