move take-related definitions and proofs to new module; simplify map_of_typ functions
--- 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 {*
--- 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) =
--- 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
--- 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;
--- /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;
--- 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;