# HG changeset patch # User blanchet # Date 1347617367 -7200 # Node ID 3edd1c90f6e6ecc93303eb6c393b62e81782279b # Parent 8aebe857aaaa8084a900e91cfc70b660bde3186d renamed "mk_UnN" to "mk_UnIN" diff -r 8aebe857aaaa -r 3edd1c90f6e6 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200 @@ -499,6 +499,7 @@ ((wrap, define_iter_likes), lthy') end; + (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there *) val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_set_defss = map set_defs_of_bnf pre_bnfs; val nesting_map_ids = map map_id_of_bnf nesting_bnfs; diff -r 8aebe857aaaa -r 3edd1c90f6e6 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 14 12:09:27 2012 +0200 @@ -206,7 +206,7 @@ fun mk_set_hset_incl_hset_tac n defs rec_Suc i = EVERY' (map (TRY oo stac) defs @ map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2, - mk_UnN n i] @ + mk_UnIN n i] @ [etac @{thm UN_I}, atac]) 1; fun mk_set_incl_hin_tac incls = @@ -535,7 +535,7 @@ hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp), rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1, CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY' - [rtac (mk_UnN n i), dtac (def RS subst_id), + [rtac (mk_UnIN n i), dtac (def RS subst_id), REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' atac), CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans, @@ -678,7 +678,7 @@ rtac Lev_0, rtac @{thm singletonI}, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]}, - rtac Lev_Suc, rtac (mk_UnN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, + rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, etac conjI, atac]) ks]) (Lev_0s ~~ Lev_Sucs)] 1 @@ -753,7 +753,7 @@ then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac, CONJ_WRAP' (fn (i'', Lev_0'') => EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]}, - rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i''), + rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, rtac (Lev_0'' RS equalityD2 RS set_mp), rtac @{thm singletonI}]) @@ -770,7 +770,7 @@ CONJ_WRAP' (fn i' => rtac impI THEN' CONJ_WRAP' (fn i'' => EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp), - rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnN n i), + rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI, atac, dtac (sym RS trans RS sym), rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans), @@ -972,7 +972,7 @@ else etac (mk_InN_not_InM i' i'' RS notE)]) (rev ks), rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]}, - rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i'), rtac CollectI, + rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac, rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI, rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI, @@ -986,7 +986,7 @@ atac, atac, hyp_subst_tac, atac] else etac (mk_InN_not_InM i' i'' RS notE)]) (rev ks), - rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i'), rtac CollectI, + rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac, CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt), @@ -1196,7 +1196,7 @@ REPEAT_DETERM_N n o rtac @{thm Un_upper1}, REPEAT_DETERM_N n o EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets => - EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnN n i), etac @{thm UN_I}, + EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I}, etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE, EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)]) (1 upto n) set_hsets set_hset_hsetss)] 1; diff -r 8aebe857aaaa -r 3edd1c90f6e6 src/HOL/Codatatype/Tools/bnf_util.ML --- a/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 14 12:09:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 14 12:09:27 2012 +0200 @@ -111,7 +111,7 @@ val mk_nthI: int -> int -> thm val mk_nth_conv: int -> int -> thm val mk_ordLeq_csum: int -> int -> thm -> thm - val mk_UnN: int -> int -> thm + val mk_UnIN: int -> int -> thm val ctrans: thm val o_apply: thm @@ -542,12 +542,12 @@ end; local - fun mk_UnN' 0 = @{thm UnI2} - | mk_UnN' m = mk_UnN' (m - 1) RS @{thm UnI1}; + fun mk_UnIN' 0 = @{thm UnI2} + | mk_UnIN' m = mk_UnIN' (m - 1) RS @{thm UnI1}; in - fun mk_UnN 1 1 = @{thm TrueE[OF TrueI]} - | mk_UnN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1}) - | mk_UnN n m = mk_UnN' (n - m) + fun mk_UnIN 1 1 = @{thm TrueE[OF TrueI]} + | mk_UnIN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1}) + | mk_UnIN n m = mk_UnIN' (n - m) end; fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);