# HG changeset patch # User traytel # Date 1347178558 -7200 # Node ID 2652319c394e7a98b15ed4cb43dfa7d41e46d72a # Parent 510c6d4a73ec3d4cacaf11b0a27d2150dbc9866d open typedef for datatypes diff -r 510c6d4a73ec -r 2652319c394e src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Sat Sep 08 22:54:37 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Sun Sep 09 10:15:58 2012 +0200 @@ -936,7 +936,7 @@ val ((T_names, (T_glob_infos, T_loc_infos)), lthy) = lthy - |> fold_map3 (fn b => fn mx => fn car_init => typedef true NONE (b, params, mx) car_init NONE + |> fold_map3 (fn b => fn mx => fn car_init => typedef false NONE (b, params, mx) car_init NONE (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms, rtac alg_init_thm] 1)) bs mixfixes car_inits |>> apsnd split_list o split_list; @@ -947,7 +947,6 @@ val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> initT)) T_glob_infos Ts; val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, initT --> T)) T_glob_infos Ts; - val set_defs = map (the o #set_def) T_loc_infos; val type_defs = map #type_definition T_loc_infos; val Reps = map #Rep T_loc_infos; val Rep_casess = map #Rep_cases T_loc_infos; @@ -955,9 +954,6 @@ val Rep_inverses = map #Rep_inverse T_loc_infos; val Abs_inverses = map #Abs_inverse T_loc_infos; - val T_subset1s = map mk_T_subset1 set_defs; - val T_subset2s = map mk_T_subset2 set_defs; - fun mk_inver_thm mk_tac rep abs X thm = Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop (mk_inver rep abs X)) @@ -965,8 +961,7 @@ |> Thm.close_derivation; val inver_Reps = map4 (mk_inver_thm rtac) Abs_Ts Rep_Ts (map HOLogic.mk_UNIV Ts) Rep_inverses; - val inver_Abss = map4 (mk_inver_thm etac) Rep_Ts Abs_Ts car_inits - (map2 (curry op RS) T_subset1s Abs_inverses); + val inver_Abss = map4 (mk_inver_thm etac) Rep_Ts Abs_Ts car_inits Abs_inverses; val timer = time (timer "THE TYPEDEFs & Rep/Abs thms"); @@ -1036,9 +1031,8 @@ val (mor_Rep_thm, mor_Abs_thm) = let val copy = alg_init_thm RS copy_alg_thm; - fun mk_bij inj subset1 subset2 Rep cases = @{thm bij_betwI'} OF - [inj, Rep RS subset2, subset1 RS cases]; - val bijs = map5 mk_bij Rep_injects T_subset1s T_subset2s Reps Rep_casess; + fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases]; + val bijs = map3 mk_bij Rep_injects Reps Rep_casess; val mor_Rep = Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop (mk_mor UNIVs flds car_inits str_inits Rep_Ts)) @@ -1118,7 +1112,7 @@ val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks)); val unique_mor = Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique))) - (K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms T_subset2s Reps + (K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms Reps mor_comp_thm mor_Abs_thm mor_iter_thm)) |> Thm.close_derivation; in @@ -1303,7 +1297,7 @@ (Skip_Proof.prove lthy [] [] (fold_rev Logic.all (phis @ Izs) goal) (K (mk_fld_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm - Rep_inverses Abs_inverses Reps T_subset1s T_subset2s)) + Rep_inverses Abs_inverses Reps)) |> Thm.close_derivation, rev (Term.add_tfrees goal [])) end; diff -r 510c6d4a73ec -r 2652319c394e src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Sat Sep 08 22:54:37 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Sun Sep 09 10:15:58 2012 +0200 @@ -22,7 +22,7 @@ val mk_fld_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_fld_induct_tac: int -> thm list list -> thm -> thm list -> thm -> thm list -> thm list -> - thm list -> thm list -> thm list -> tactic + thm list -> tactic val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic @@ -32,8 +32,7 @@ val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic val mk_iso_alt_tac: thm list -> thm -> tactic - val mk_iter_unique_mor_tac: thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm -> - tactic + val mk_iter_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic val mk_least_min_alg_tac: thm -> thm -> tactic val mk_lfp_map_wpull_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list list -> thm list list list -> thm list -> tactic @@ -497,12 +496,12 @@ REPEAT_DETERM_N (length iter_defs) o etac exE THEN' rtac (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac mor) 1; -fun mk_iter_unique_mor_tac type_defs init_unique_mors subsets Reps mor_comp mor_Abs mor_iter = +fun mk_iter_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_iter = let - fun mk_subset subset Rep = etac subset ORELSE' rtac (Rep RS subset); fun mk_unique type_def = EVERY' [rtac @{thm surj_fun_eq}, rtac (type_def RS @{thm type_definition.Abs_image}), - rtac ballI, resolve_tac init_unique_mors, EVERY' (map2 mk_subset subsets Reps), + rtac ballI, resolve_tac init_unique_mors, + EVERY' (map (fn thm => atac ORELSE' rtac thm) Reps), rtac mor_comp, rtac mor_Abs, atac, rtac mor_comp, rtac mor_Abs, rtac mor_iter]; in @@ -522,33 +521,30 @@ EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iter RS @{thm arg_cong[of _ _ snd]}), rtac @{thm snd_convol'}] 1; -fun mk_fld_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps - subset1s subset2s = +fun mk_fld_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = let val n = length set_natural'ss; val ks = 1 upto n; - fun mk_IH_tac Rep_inv Abs_inv set_natural' subset = + fun mk_IH_tac Rep_inv Abs_inv set_natural' = DETERM o EVERY' [dtac @{thm meta_mp}, rtac (Rep_inv RS arg_cong RS subst), etac bspec, dtac @{thm set_rev_mp}, rtac equalityD1, rtac set_natural', etac imageE, - hyp_subst_tac, rtac (Abs_inv RS ssubst), rtac subset, etac @{thm set_mp}, + hyp_subst_tac, rtac (Abs_inv RS ssubst), etac @{thm set_mp}, atac, atac]; fun mk_closed_tac (k, (morE, set_natural's)) = EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI, rtac (mor_Abs RS morE RS arg_cong RS ssubst), atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec}, - EVERY' (map4 mk_IH_tac Rep_invs Abs_invs (drop m set_natural's) subset1s), atac]; + EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_natural's)), atac]; - fun mk_induct_tac ((Rep, Rep_inv), subset) = - EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RS subset RSN (2, bspec))]; + fun mk_induct_tac (Rep, Rep_inv) = + EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))]; in (rtac mp THEN' rtac impI THEN' - DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac - ((Reps ~~ Rep_invs) ~~ subset2s) THEN' + DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN' rtac init_induct THEN' - DETERM o CONJ_WRAP' mk_closed_tac - (ks ~~ (morEs ~~ set_natural'ss))) 1 + DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_natural'ss))) 1 end; fun mk_fld_induct2_tac cTs cts fld_induct weak_fld_inducts {context = ctxt, prems = _} =