# HG changeset patch # User huffman # Date 1267566623 28800 # Node ID a2cfa413eaab3f82150d3b27a13f531bb047d194 # Parent 89eddccbb93d6e0515c693113f90f9bd5269ca3b move take-related definitions and proofs to new module; simplify map_of_typ functions diff -r 89eddccbb93d -r a2cfa413eaab src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Tue Mar 02 13:01:22 2010 -0800 +++ b/src/HOLCF/Representable.thy Tue Mar 02 13:50:23 2010 -0800 @@ -9,6 +9,7 @@ uses ("Tools/repdef.ML") ("Tools/holcf_library.ML") + ("Tools/Domain/domain_take_proofs.ML") ("Tools/Domain/domain_isomorphism.ML") begin @@ -778,6 +779,7 @@ subsection {* Constructing Domain Isomorphisms *} use "Tools/holcf_library.ML" +use "Tools/Domain/domain_take_proofs.ML" use "Tools/Domain/domain_isomorphism.ML" setup {* diff -r 89eddccbb93d -r a2cfa413eaab src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 13:01:22 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 13:50:23 2010 -0800 @@ -135,7 +135,7 @@ val dom_binds = map (Binding.name o Long_Name.base_name) dnames; val thy = if definitional then thy - else snd (Domain_Isomorphism.define_take_functions + else snd (Domain_Take_Proofs.define_take_functions (dom_binds ~~ map get_iso_info eqs') thy); fun add_one' (dnam, axs, dfs) = diff -r 89eddccbb93d -r a2cfa413eaab src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 02 13:01:22 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 02 13:50:23 2010 -0800 @@ -10,7 +10,7 @@ val add_domain_constructors : string -> (binding * (bool * binding option * typ) list * mixfix) list - -> Domain_Isomorphism.iso_info + -> Domain_Take_Proofs.iso_info -> theory -> { con_consts : term list, con_betas : thm list, @@ -1011,7 +1011,7 @@ fun add_domain_constructors (dname : string) (spec : (binding * (bool * binding option * typ) list * mixfix) list) - (iso_info : Domain_Isomorphism.iso_info) + (iso_info : Domain_Take_Proofs.iso_info) (thy : theory) = let diff -r 89eddccbb93d -r a2cfa413eaab src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 13:01:22 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 13:50:23 2010 -0800 @@ -6,37 +6,17 @@ signature DOMAIN_ISOMORPHISM = sig - type iso_info = - { - repT : typ, - absT : typ, - rep_const : term, - abs_const : term, - rep_inverse : thm, - abs_inverse : thm - } val domain_isomorphism : (string list * binding * mixfix * typ * (binding * binding) option) list - -> theory -> iso_info list * theory + -> theory -> Domain_Take_Proofs.iso_info list * theory val domain_isomorphism_cmd : (string list * binding * mixfix * string * (binding * binding) option) list -> theory -> theory val add_type_constructor : (string * term * string * thm * thm * thm * thm) -> theory -> theory - val get_map_tab : - theory -> string Symtab.table - val define_take_functions : - (binding * iso_info) list -> theory -> - { take_consts : term list, - take_defs : thm list, - chain_take_thms : thm list, - take_0_thms : thm list, - take_Suc_thms : thm list, - deflation_take_thms : thm list - } * theory; end; -structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM = +structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = struct val beta_ss = @@ -53,47 +33,51 @@ structure DeflData = Theory_Data ( + (* terms like "foo_defl" *) type T = term Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data = Symtab.merge (K true) data; ); -structure MapData = Theory_Data +structure RepData = Theory_Data ( - type T = string Symtab.table; - val empty = Symtab.empty; - val extend = I; - fun merge data = Symtab.merge (K true) data; -); - -structure Thm_List : THEORY_DATA_ARGS = -struct + (* theorems like "REP('a foo) = foo_defl$REP('a)" *) type T = thm list; val empty = []; val extend = I; val merge = Thm.merge_thms; -end; - -structure RepData = Theory_Data (Thm_List); +); -structure IsodeflData = Theory_Data (Thm_List); +structure MapIdData = Theory_Data +( + (* theorems like "foo_map$ID = ID" *) + type T = thm list; + val empty = []; + val extend = I; + val merge = Thm.merge_thms; +); -structure MapIdData = Theory_Data (Thm_List); - -structure DeflMapData = Theory_Data (Thm_List); +structure IsodeflData = Theory_Data +( + (* theorems like "isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" *) + 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, map_ID_thm, defl_map_thm) = DeflData.map (Symtab.insert (K true) (tname, defl_const)) - #> MapData.map (Symtab.insert (K true) (tname, map_name)) + #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm) #> RepData.map (Thm.add_thm REP_thm) #> IsodeflData.map (Thm.add_thm isodefl_thm) - #> MapIdData.map (Thm.add_thm map_ID_thm) - #> DeflMapData.map (Thm.add_thm defl_map_thm); + #> MapIdData.map (Thm.add_thm map_ID_thm); -val get_map_tab = MapData.get; + +(* val get_map_tab = MapData.get; *) (******************************************************************************) @@ -142,17 +126,7 @@ (****************************** isomorphism info ******************************) (******************************************************************************) -type iso_info = - { - absT : typ, - repT : typ, - abs_const : term, - rep_const : term, - abs_inverse : thm, - rep_inverse : thm - } - -fun deflation_abs_rep (info : iso_info) : thm = +fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm = let val abs_iso = #abs_inverse info; val rep_iso = #rep_inverse info; @@ -250,22 +224,6 @@ else error ("defl_of_typ: type variable under unsupported type constructor " ^ c); in defl_of T end; -fun map_of_typ - (tab : string Symtab.table) - (T : typ) : term = - let - fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts - | is_closed_typ _ = false; - fun map_of (T as TFree (a, _)) = Free (Library.unprefix "'" a, T ->> T) - | map_of (T as TVar _) = error ("map_of_typ: TVar") - | map_of (T as Type (c, Ts)) = - case Symtab.lookup tab c of - SOME t => list_ccomb (Const (t, mapT T), map map_of Ts) - | NONE => if is_closed_typ T - then mk_ID T - else error ("map_of_typ: type variable under unsupported type constructor " ^ c); - in map_of T end; - (******************************************************************************) (********************* declaring definitions and theorems *********************) @@ -293,217 +251,6 @@ ||> Sign.parent_path; (******************************************************************************) -(************************** defining take functions ***************************) -(******************************************************************************) - -fun define_take_functions - (spec : (binding * iso_info) list) - (thy : theory) = - let - - (* retrieve components of spec *) - val dom_binds = map fst spec; - val iso_infos = map snd spec; - val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos; - val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos; - val dnames = map Binding.name_of dom_binds; - - (* get table of map functions *) - val map_tab = MapData.get thy; - - fun mk_projs [] t = [] - | mk_projs (x::[]) t = [(x, t)] - | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); - - fun mk_cfcomp2 ((rep_const, abs_const), f) = - mk_cfcomp (abs_const, mk_cfcomp (f, rep_const)); - - (* defining map functions over dtyps *) - fun copy_of_dtyp recs (T, dt) = - if Datatype_Aux.is_rec_type dt - then copy_of_dtyp' recs (T, dt) - else mk_ID T - and copy_of_dtyp' recs (T, Datatype_Aux.DtRec i) = nth recs i - | copy_of_dtyp' recs (T, Datatype_Aux.DtTFree a) = mk_ID T - | copy_of_dtyp' recs (T, Datatype_Aux.DtType (c, ds)) = - case Symtab.lookup map_tab c of - SOME f => - list_ccomb - (Const (f, mapT T), - map (copy_of_dtyp recs) (snd (dest_Type T) ~~ ds)) - | NONE => - (warning ("copy_of_dtyp: unknown type constructor " ^ c); mk_ID T); - - (* define take functional *) - val new_dts : (string * string list) list = - map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns; - val copy_arg_type = mk_tupleT (map (fn (T, _) => T ->> T) dom_eqns); - val copy_arg = Free ("f", copy_arg_type); - val copy_args = map snd (mk_projs dom_binds copy_arg); - fun one_copy_rhs (rep_abs, (lhsT, rhsT)) = - let - val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT; - val body = copy_of_dtyp copy_args (rhsT, dtyp); - in - mk_cfcomp2 (rep_abs, body) - end; - val take_functional = - big_lambda copy_arg - (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))); - val take_rhss = - let - val i = Free ("i", HOLogic.natT); - val rhs = mk_iterate (i, take_functional) - in - map (Term.lambda i o snd) (mk_projs dom_binds rhs) - end; - - (* define take constants *) - fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy = - let - val take_type = HOLogic.natT --> lhsT ->> lhsT; - val take_bind = Binding.suffix_name "_take" tbind; - val (take_const, thy) = - Sign.declare_const ((take_bind, take_type), NoSyn) thy; - val take_eqn = Logic.mk_equals (take_const, take_rhs); - val (take_def_thm, thy) = - thy - |> Sign.add_path (Binding.name_of tbind) - |> yield_singleton - (PureThy.add_defs false o map Thm.no_attributes) - (Binding.name "take_def", take_eqn) - ||> Sign.parent_path; - in ((take_const, take_def_thm), thy) end; - val ((take_consts, take_defs), thy) = thy - |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns) - |>> ListPair.unzip; - - (* prove chain_take lemmas *) - fun prove_chain_take (take_const, dname) thy = - let - val goal = mk_trp (mk_chain take_const); - val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}; - val tac = simp_tac (HOL_basic_ss addsimps rules) 1; - val chain_take_thm = Goal.prove_global thy [] [] goal (K tac); - in - add_qualified_thm "chain_take" (dname, chain_take_thm) thy - end; - val (chain_take_thms, thy) = - fold_map prove_chain_take (take_consts ~~ dnames) thy; - - (* prove take_0 lemmas *) - fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy = - let - val lhs = take_const $ @{term "0::nat"}; - val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)); - val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}; - val tac = simp_tac (HOL_basic_ss addsimps rules) 1; - val take_0_thm = Goal.prove_global thy [] [] goal (K tac); - in - add_qualified_thm "take_0" (dname, take_0_thm) thy - end; - val (take_0_thms, thy) = - fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy; - - (* prove take_Suc lemmas *) - val i = Free ("i", natT); - val take_is = map (fn t => t $ i) take_consts; - fun prove_take_Suc - (((take_const, rep_abs), dname), (lhsT, rhsT)) thy = - let - val lhs = take_const $ (@{term Suc} $ i); - val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT; - val body = copy_of_dtyp take_is (rhsT, dtyp); - val rhs = mk_cfcomp2 (rep_abs, body); - val goal = mk_eqs (lhs, rhs); - val simps = @{thms iterate_Suc fst_conv snd_conv} - val rules = take_defs @ simps; - val tac = simp_tac (beta_ss addsimps rules) 1; - val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac); - in - add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy - end; - val (take_Suc_thms, thy) = - fold_map prove_take_Suc - (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy; - - (* prove deflation theorems for take functions *) - val deflation_abs_rep_thms = map deflation_abs_rep iso_infos; - val deflation_take_thm = - let - val i = Free ("i", natT); - fun mk_goal take_const = mk_deflation (take_const $ i); - val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)); - val adm_rules = - @{thms adm_conj adm_subst [OF _ adm_deflation] - cont2cont_fst cont2cont_snd cont_id}; - val bottom_rules = - take_0_thms @ @{thms deflation_UU simp_thms}; - val deflation_rules = - @{thms conjI deflation_ID} - @ deflation_abs_rep_thms - @ DeflMapData.get thy; - in - Goal.prove_global thy [] [] goal (fn _ => - EVERY - [rtac @{thm nat.induct} 1, - simp_tac (HOL_basic_ss addsimps bottom_rules) 1, - asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1, - REPEAT (etac @{thm conjE} 1 - ORELSE resolve_tac deflation_rules 1 - ORELSE atac 1)]) - end; - fun conjuncts [] thm = [] - | conjuncts (n::[]) thm = [(n, thm)] - | conjuncts (n::ns) thm = let - val thmL = thm RS @{thm conjunct1}; - val thmR = thm RS @{thm conjunct2}; - in (n, thmL):: conjuncts ns thmR end; - val (deflation_take_thms, thy) = - fold_map (add_qualified_thm "deflation_take") - (map (apsnd Drule.export_without_context) - (conjuncts dnames deflation_take_thm)) thy; - - (* prove strictness of take functions *) - fun prove_take_strict (take_const, dname) thy = - let - val goal = mk_trp (mk_strict (take_const $ Free ("i", natT))); - val tac = rtac @{thm deflation_strict} 1 - THEN resolve_tac deflation_take_thms 1; - val take_strict_thm = Goal.prove_global thy [] [] goal (K tac); - in - add_qualified_thm "take_strict" (dname, take_strict_thm) thy - end; - val (take_strict_thms, thy) = - fold_map prove_take_strict (take_consts ~~ dnames) thy; - - (* prove take/take rules *) - fun prove_take_take ((chain_take, deflation_take), dname) thy = - let - val take_take_thm = - @{thm deflation_chain_min} OF [chain_take, deflation_take]; - in - add_qualified_thm "take_take" (dname, take_take_thm) thy - end; - val (take_take_thms, thy) = - fold_map prove_take_take - (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy; - - val result = - { - take_consts = take_consts, - take_defs = take_defs, - chain_take_thms = chain_take_thms, - take_0_thms = take_0_thms, - take_Suc_thms = take_Suc_thms, - deflation_take_thms = deflation_take_thms - }; - - in - (result, thy) - end; - -(******************************************************************************) (******************************* main function ********************************) (******************************************************************************) @@ -529,7 +276,7 @@ (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list) (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list) (thy: theory) - : iso_info list * theory = + : Domain_Take_Proofs.iso_info list * theory = let val _ = Theory.requires thy "Representable" "domain isomorphisms"; @@ -669,7 +416,7 @@ |>> ListPair.unzip; (* collect info about rep/abs *) - val iso_infos : iso_info list = + val iso_infos : Domain_Take_Proofs.iso_info list = let fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) = { @@ -696,19 +443,24 @@ fold_map declare_map_const (dom_binds ~~ dom_eqns); (* defining equations for map functions *) - val map_tab1 = MapData.get thy; - val map_tab2 = - Symtab.make (map (fst o dest_Type o fst) dom_eqns - ~~ map (fst o dest_Const) map_consts); - val map_tab' = Symtab.merge (K true) (map_tab1, map_tab2); - val thy = MapData.put map_tab' thy; - fun mk_map_spec ((rep_const, abs_const), (lhsT, rhsT)) = - let - val lhs = map_of_typ map_tab' lhsT; - val body = map_of_typ map_tab' rhsT; - val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)); - in mk_eqs (lhs, rhs) end; - val map_specs = map mk_map_spec (rep_abs_consts ~~ dom_eqns); + local + fun unprime a = Library.unprefix "'" a; + fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T); + fun map_lhs (map_const, lhsT) = + (lhsT, list_ccomb (map_const, map mapvar (snd (dest_Type lhsT)))); + val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns); + val Ts = (snd o dest_Type o fst o hd) dom_eqns; + val tab = (Ts ~~ map mapvar Ts) @ tab1; + fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) = + let + val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT; + val body = Domain_Take_Proofs.map_of_typ thy tab rhsT; + val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)); + in mk_eqs (lhs, rhs) end; + in + val map_specs = + map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns); + end; (* register recursive definition of map functions *) val map_binds = map (Binding.suffix_name "_map") dom_binds; @@ -816,7 +568,7 @@ val deflation_rules = @{thms conjI deflation_ID} @ deflation_abs_rep_thms - @ DeflMapData.get thy; + @ Domain_Take_Proofs.get_deflation_thms thy; in Goal.prove_global thy [] assms goal (fn {prems, ...} => EVERY @@ -834,11 +586,22 @@ val (deflation_map_thms, thy) = thy |> (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context)) (conjuncts deflation_map_binds deflation_map_thm); - val thy = DeflMapData.map (fold Thm.add_thm deflation_map_thms) thy; + + (* register map functions in theory data *) + local + fun register_map ((dname, map_name), defl_thm) = + Domain_Take_Proofs.add_map_function (dname, map_name, defl_thm); + val dnames = map (fst o dest_Type o fst) dom_eqns; + val map_names = map (fst o dest_Const) map_consts; + in + val thy = + fold register_map (dnames ~~ map_names ~~ deflation_map_thms) thy; + end; (* definitions and proofs related to take functions *) val (take_info, thy) = - define_take_functions (dom_binds ~~ iso_infos) thy; + Domain_Take_Proofs.define_take_functions + (dom_binds ~~ iso_infos) thy; val {take_consts, take_defs, chain_take_thms, take_0_thms, take_Suc_thms, deflation_take_thms} = take_info; diff -r 89eddccbb93d -r a2cfa413eaab src/HOLCF/Tools/Domain/domain_take_proofs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Mar 02 13:50:23 2010 -0800 @@ -0,0 +1,391 @@ +(* Title: HOLCF/Tools/domain/domain_take_proofs.ML + Author: Brian Huffman + +Defines take functions for the given domain equation +and proves related theorems. +*) + +signature DOMAIN_TAKE_PROOFS = +sig + type iso_info = + { + absT : typ, + repT : typ, + abs_const : term, + rep_const : term, + abs_inverse : thm, + rep_inverse : thm + } + + val define_take_functions : + (binding * iso_info) list -> theory -> + { take_consts : term list, + take_defs : thm list, + chain_take_thms : thm list, + take_0_thms : thm list, + take_Suc_thms : thm list, + deflation_take_thms : thm list + } * theory + + val map_of_typ : + theory -> (typ * term) list -> typ -> term + + val add_map_function : + (string * string * thm) -> theory -> theory + + val get_map_tab : theory -> string Symtab.table + val get_deflation_thms : theory -> thm list +end; + +structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS = +struct + +type iso_info = + { + absT : typ, + repT : typ, + abs_const : term, + rep_const : term, + abs_inverse : thm, + rep_inverse : thm + }; + +val beta_ss = + HOL_basic_ss + addsimps simp_thms + addsimps [@{thm beta_cfun}] + addsimprocs [@{simproc cont_proc}]; + +val beta_tac = simp_tac beta_ss; + +(******************************************************************************) +(******************************** theory data *********************************) +(******************************************************************************) + +structure MapData = Theory_Data +( + (* constant names like "foo_map" *) + type T = string Symtab.table; + val empty = Symtab.empty; + val extend = I; + fun merge data = Symtab.merge (K true) data; +); + +structure DeflMapData = Theory_Data +( + (* theorems like "deflation a ==> deflation (foo_map$a)" *) + type T = thm list; + val empty = []; + val extend = I; + val merge = Thm.merge_thms; +); + +fun add_map_function (tname, map_name, deflation_map_thm) = + MapData.map (Symtab.insert (K true) (tname, map_name)) + #> DeflMapData.map (Thm.add_thm deflation_map_thm); + +val get_map_tab = MapData.get; +val get_deflation_thms = DeflMapData.get; + +(******************************************************************************) +(************************** building types and terms **************************) +(******************************************************************************) + +open HOLCF_Library; + +infixr 6 ->>; +infix -->>; + +val deflT = @{typ "udom alg_defl"}; + +fun mapT (T as Type (_, Ts)) = + (map (fn T => T ->> T) Ts) -->> (T ->> T) + | mapT T = T ->> T; + +fun mk_Rep_of T = + Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T; + +fun coerce_const T = Const (@{const_name coerce}, T); + +fun isodefl_const T = + Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT); + +fun mk_deflation t = + Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t; + +fun mk_lub t = + let + val T = Term.range_type (Term.fastype_of t); + val lub_const = Const (@{const_name lub}, (T --> boolT) --> T); + val UNIV_const = @{term "UNIV :: nat set"}; + val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT; + val image_const = Const (@{const_name image}, image_type); + in + lub_const $ (image_const $ t $ UNIV_const) + end; + +(* splits a cterm into the right and lefthand sides of equality *) +fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); + +fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); + +(******************************************************************************) +(****************************** isomorphism info ******************************) +(******************************************************************************) + +fun deflation_abs_rep (info : iso_info) : thm = + let + val abs_iso = #abs_inverse info; + val rep_iso = #rep_inverse info; + val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]; + in + Drule.export_without_context thm + end + +(******************************************************************************) +(********************* building map functions over types **********************) +(******************************************************************************) + +fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term = + let + val map_tab = get_map_tab thy; + fun auto T = T ->> T; + fun map_of T = + case AList.lookup (op =) sub T of + SOME m => (m, true) | NONE => map_of' T + and map_of' (T as (Type (c, Ts))) = + (case Symtab.lookup map_tab c of + SOME map_name => + let + val map_type = map auto Ts -->> auto T; + val (ms, bs) = map_split map_of Ts; + in + if exists I bs + then (list_ccomb (Const (map_name, map_type), ms), true) + else (mk_ID T, false) + end + | NONE => (mk_ID T, false)) + | map_of' T = (mk_ID T, false); + in + fst (map_of T) + end; + + +(******************************************************************************) +(********************* declaring definitions and theorems *********************) +(******************************************************************************) + +fun define_const + (bind : binding, rhs : term) + (thy : theory) + : (term * thm) * theory = + let + val typ = Term.fastype_of rhs; + val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy; + val eqn = Logic.mk_equals (const, rhs); + val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn); + val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy; + in + ((const, def_thm), thy) + end; + +fun add_qualified_thm name (path, thm) thy = + thy + |> Sign.add_path path + |> yield_singleton PureThy.add_thms + (Thm.no_attributes (Binding.name name, thm)) + ||> Sign.parent_path; + +(******************************************************************************) +(************************** defining take functions ***************************) +(******************************************************************************) + +fun define_take_functions + (spec : (binding * iso_info) list) + (thy : theory) = + let + + (* retrieve components of spec *) + val dom_binds = map fst spec; + val iso_infos = map snd spec; + val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos; + val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos; + val dnames = map Binding.name_of dom_binds; + + (* get table of map functions *) + val map_tab = MapData.get thy; + + fun mk_projs [] t = [] + | mk_projs (x::[]) t = [(x, t)] + | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); + + fun mk_cfcomp2 ((rep_const, abs_const), f) = + mk_cfcomp (abs_const, mk_cfcomp (f, rep_const)); + + (* define take functional *) + val newTs : typ list = map fst dom_eqns; + val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs); + val copy_arg = Free ("f", copy_arg_type); + val copy_args = map snd (mk_projs dom_binds copy_arg); + fun one_copy_rhs (rep_abs, (lhsT, rhsT)) = + let + val body = map_of_typ thy (newTs ~~ copy_args) rhsT; + in + mk_cfcomp2 (rep_abs, body) + end; + val take_functional = + big_lambda copy_arg + (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))); + val take_rhss = + let + val i = Free ("i", HOLogic.natT); + val rhs = mk_iterate (i, take_functional) + in + map (Term.lambda i o snd) (mk_projs dom_binds rhs) + end; + + (* define take constants *) + fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy = + let + val take_type = HOLogic.natT --> lhsT ->> lhsT; + val take_bind = Binding.suffix_name "_take" tbind; + val (take_const, thy) = + Sign.declare_const ((take_bind, take_type), NoSyn) thy; + val take_eqn = Logic.mk_equals (take_const, take_rhs); + val (take_def_thm, thy) = + thy + |> Sign.add_path (Binding.name_of tbind) + |> yield_singleton + (PureThy.add_defs false o map Thm.no_attributes) + (Binding.name "take_def", take_eqn) + ||> Sign.parent_path; + in ((take_const, take_def_thm), thy) end; + val ((take_consts, take_defs), thy) = thy + |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns) + |>> ListPair.unzip; + + (* prove chain_take lemmas *) + fun prove_chain_take (take_const, dname) thy = + let + val goal = mk_trp (mk_chain take_const); + val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}; + val tac = simp_tac (HOL_basic_ss addsimps rules) 1; + val chain_take_thm = Goal.prove_global thy [] [] goal (K tac); + in + add_qualified_thm "chain_take" (dname, chain_take_thm) thy + end; + val (chain_take_thms, thy) = + fold_map prove_chain_take (take_consts ~~ dnames) thy; + + (* prove take_0 lemmas *) + fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy = + let + val lhs = take_const $ @{term "0::nat"}; + val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)); + val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}; + val tac = simp_tac (HOL_basic_ss addsimps rules) 1; + val take_0_thm = Goal.prove_global thy [] [] goal (K tac); + in + add_qualified_thm "take_0" (dname, take_0_thm) thy + end; + val (take_0_thms, thy) = + fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy; + + (* prove take_Suc lemmas *) + val i = Free ("i", natT); + val take_is = map (fn t => t $ i) take_consts; + fun prove_take_Suc + (((take_const, rep_abs), dname), (lhsT, rhsT)) thy = + let + val lhs = take_const $ (@{term Suc} $ i); + val body = map_of_typ thy (newTs ~~ take_is) rhsT; + val rhs = mk_cfcomp2 (rep_abs, body); + val goal = mk_eqs (lhs, rhs); + val simps = @{thms iterate_Suc fst_conv snd_conv} + val rules = take_defs @ simps; + val tac = simp_tac (beta_ss addsimps rules) 1; + val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac); + in + add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy + end; + val (take_Suc_thms, thy) = + fold_map prove_take_Suc + (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy; + + (* prove deflation theorems for take functions *) + val deflation_abs_rep_thms = map deflation_abs_rep iso_infos; + val deflation_take_thm = + let + val i = Free ("i", natT); + fun mk_goal take_const = mk_deflation (take_const $ i); + val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)); + val adm_rules = + @{thms adm_conj adm_subst [OF _ adm_deflation] + cont2cont_fst cont2cont_snd cont_id}; + val bottom_rules = + take_0_thms @ @{thms deflation_UU simp_thms}; + val deflation_rules = + @{thms conjI deflation_ID} + @ deflation_abs_rep_thms + @ DeflMapData.get thy; + in + Goal.prove_global thy [] [] goal (fn _ => + EVERY + [rtac @{thm nat.induct} 1, + simp_tac (HOL_basic_ss addsimps bottom_rules) 1, + asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1, + REPEAT (etac @{thm conjE} 1 + ORELSE resolve_tac deflation_rules 1 + ORELSE atac 1)]) + end; + fun conjuncts [] thm = [] + | conjuncts (n::[]) thm = [(n, thm)] + | conjuncts (n::ns) thm = let + val thmL = thm RS @{thm conjunct1}; + val thmR = thm RS @{thm conjunct2}; + in (n, thmL):: conjuncts ns thmR end; + val (deflation_take_thms, thy) = + fold_map (add_qualified_thm "deflation_take") + (map (apsnd Drule.export_without_context) + (conjuncts dnames deflation_take_thm)) thy; + + (* prove strictness of take functions *) + fun prove_take_strict (take_const, dname) thy = + let + val goal = mk_trp (mk_strict (take_const $ Free ("i", natT))); + val tac = rtac @{thm deflation_strict} 1 + THEN resolve_tac deflation_take_thms 1; + val take_strict_thm = Goal.prove_global thy [] [] goal (K tac); + in + add_qualified_thm "take_strict" (dname, take_strict_thm) thy + end; + val (take_strict_thms, thy) = + fold_map prove_take_strict (take_consts ~~ dnames) thy; + + (* prove take/take rules *) + fun prove_take_take ((chain_take, deflation_take), dname) thy = + let + val take_take_thm = + @{thm deflation_chain_min} OF [chain_take, deflation_take]; + in + add_qualified_thm "take_take" (dname, take_take_thm) thy + end; + val (take_take_thms, thy) = + fold_map prove_take_take + (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy; + + val result = + { + take_consts = take_consts, + take_defs = take_defs, + chain_take_thms = chain_take_thms, + take_0_thms = take_0_thms, + take_Suc_thms = take_Suc_thms, + deflation_take_thms = deflation_take_thms + }; + + in + (result, thy) + end; + +end; diff -r 89eddccbb93d -r a2cfa413eaab src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 13:01:22 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Mar 02 13:50:23 2010 -0800 @@ -106,7 +106,7 @@ let val _ = message ("Proving isomorphism properties of domain "^dname^" ..."); -val map_tab = Domain_Isomorphism.get_map_tab thy; +val map_tab = Domain_Take_Proofs.get_map_tab thy; (* ----- getting the axioms and definitions --------------------------------- *) @@ -139,7 +139,7 @@ val abs_const = Const(dname^"_abs", rhsT ->> lhsT); -val iso_info : Domain_Isomorphism.iso_info = +val iso_info : Domain_Take_Proofs.iso_info = { absT = lhsT, repT = rhsT, @@ -229,7 +229,7 @@ fun comp_theorems (comp_dnam, eqs: eq list) thy = let -val map_tab = Domain_Isomorphism.get_map_tab thy; +val map_tab = Domain_Take_Proofs.get_map_tab thy; val dnames = map (fst o fst) eqs; val conss = map snd eqs;