# HG changeset patch # User huffman # Date 1258698311 28800 # Node ID 033831fd9ef3318504e3f3313f22efbacc518fe4 # Parent 31169fdc5ae749e2863132a4c7ea3a250b0bf676 store map_ID thms in theory data; automate proofs of reach lemmas diff -r 31169fdc5ae7 -r 033831fd9ef3 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Thu Nov 19 21:44:37 2009 -0800 +++ b/src/HOLCF/Representable.thy Thu Nov 19 22:25:11 2009 -0800 @@ -1038,28 +1038,28 @@ setup {* fold Domain_Isomorphism.add_type_constructor [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, - @{thm REP_cfun}, @{thm isodefl_cfun}), + @{thm REP_cfun}, @{thm isodefl_cfun}, @{thm cfun_map_ID}), (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, - @{thm REP_ssum}, @{thm isodefl_ssum}), + @{thm REP_ssum}, @{thm isodefl_ssum}, @{thm ssum_map_ID}), (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, - @{thm REP_sprod}, @{thm isodefl_sprod}), + @{thm REP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}), (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, - @{thm REP_cprod}, @{thm isodefl_cprod}), + @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}), (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, - @{thm REP_up}, @{thm isodefl_u}), + @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID}), (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}, - @{thm REP_upper}, @{thm isodefl_upper}), + @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}), (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, - @{thm REP_lower}, @{thm isodefl_lower}), + @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}), (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, - @{thm REP_convex}, @{thm isodefl_convex})] + @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})] *} end diff -r 31169fdc5ae7 -r 033831fd9ef3 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Nov 19 21:44:37 2009 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Nov 19 22:25:11 2009 -0800 @@ -150,7 +150,7 @@ mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); in (dnam, - (if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax]), + (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]), (if definitional then [when_def] else [when_def, copy_def]) @ con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ [take_def, finite_def]) diff -r 31169fdc5ae7 -r 033831fd9ef3 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 21:44:37 2009 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 22:25:11 2009 -0800 @@ -11,7 +11,7 @@ val domain_isomorphism_cmd: (string list * binding * mixfix * string) list -> theory -> theory val add_type_constructor: - (string * term * string * thm * thm) -> theory -> theory + (string * term * string * thm * thm * thm) -> theory -> theory val get_map_tab: theory -> string Symtab.table end; @@ -63,12 +63,21 @@ val merge = Thm.merge_thms; ); +structure MapIdData = Theory_Data +( + type T = thm list; + val empty = []; + val extend = I; + val merge = Thm.merge_thms; +); + fun add_type_constructor - (tname, defl_const, map_name, REP_thm, isodefl_thm) = + (tname, defl_const, map_name, REP_thm, isodefl_thm, map_ID_thm) = DeflData.map (Symtab.insert (K true) (tname, defl_const)) #> MapData.map (Symtab.insert (K true) (tname, map_name)) #> RepData.map (Thm.add_thm REP_thm) - #> IsodeflData.map (Thm.add_thm isodefl_thm); + #> IsodeflData.map (Thm.add_thm isodefl_thm) + #> MapIdData.map (Thm.add_thm map_ID_thm); val get_map_tab = MapData.get; @@ -558,6 +567,7 @@ val (_, thy) = thy |> (PureThy.add_thms o map Thm.no_attributes) (map_ID_binds ~~ map_ID_thms); + val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy; (* define copy combinators *) val new_dts = @@ -568,7 +578,7 @@ let fun mk_copy_args [] t = [] | mk_copy_args (_::[]) t = [t] | mk_copy_args (_::xs) t = - HOLogic.mk_fst t :: mk_copy_args xs (HOLogic.mk_snd t); + mk_fst t :: mk_copy_args xs (mk_snd t); in mk_copy_args doms copy_arg end; fun copy_of_dtyp (T, dt) = if DatatypeAux.is_rec_type dt @@ -628,6 +638,46 @@ ||> Sign.parent_path; in ((c_const, c_def_thms), thy) end; + (* fixed-point lemma for combined copy combinator *) + val fix_copy_lemma = + let + fun mk_map_ID (map_const, (Type (c, Ts), rhsT)) = + Library.foldl mk_capply (map_const, map ID_const Ts); + val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns)); + val goal = mk_eqs (mk_fix c_const, rhs); + val rules = + [@{thm pair_collapse}, @{thm split_def}] + @ map_apply_thms + @ c_def_thms @ copy_defs + @ MapIdData.get thy; + val tac = simp_tac (beta_ss addsimps rules) 1; + in + Goal.prove_global thy [] [] goal (K tac) + end; + + (* prove reach lemmas *) + val reach_thm_projs = + let fun mk_projs (x::[]) t = [(x, t)] + | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); + in mk_projs dom_binds (mk_fix c_const) end; + fun prove_reach_thm (((bind, t), map_ID_thm), (lhsT, rhsT)) thy = + let + val x = Free ("x", lhsT); + val goal = mk_eqs (mk_capply (t, x), x); + val rules = + fix_copy_lemma :: map_ID_thm :: @{thms fst_conv snd_conv ID1}; + val tac = simp_tac (HOL_basic_ss addsimps rules) 1; + val reach_thm = Goal.prove_global thy [] [] goal (K tac); + in + thy + |> Sign.add_path (Binding.name_of bind) + |> yield_singleton (PureThy.add_thms o map Thm.no_attributes) + (Binding.name "reach", reach_thm) + ||> Sign.parent_path + end; + val (reach_thms, thy) = thy |> + fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns); + in thy end;