--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 05 17:53:00 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Oct 06 10:49:27 2010 -0700
@@ -48,7 +48,7 @@
structure DeflData = Theory_Data
(
- (* terms like "foo_defl" *)
+ (* terms like "foo_sfp" *)
type T = term Symtab.table;
val empty = Symtab.empty;
val extend = I;
@@ -57,7 +57,7 @@
structure RepData = Theory_Data
(
- (* theorems like "REP('a foo) = foo_defl$REP('a)" *)
+ (* theorems like "SFP('a foo) = foo_sfp$SFP('a)" *)
type T = thm list;
val empty = [];
val extend = I;
@@ -83,11 +83,11 @@
);
fun add_type_constructor
- (tname, defl_const, map_name, REP_thm,
+ (tname, defl_const, map_name, SFP_thm,
isodefl_thm, map_ID_thm, defl_map_thm) =
DeflData.map (Symtab.insert (K true) (tname, defl_const))
#> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
- #> RepData.map (Thm.add_thm REP_thm)
+ #> RepData.map (Thm.add_thm SFP_thm)
#> IsodeflData.map (Thm.add_thm isodefl_thm)
#> MapIdData.map (Thm.add_thm map_ID_thm);
@@ -104,19 +104,19 @@
infixr 6 ->>;
infix -->>;
-val deflT = @{typ "udom alg_defl"};
+val sfpT = @{typ "sfp"};
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 mk_SFP T =
+ Const (@{const_name sfp}, Term.itselfT T --> sfpT) $ 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);
+ Const (@{const_name isodefl}, (T ->> T) --> sfpT --> HOLogic.boolT);
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
@@ -218,13 +218,13 @@
let
fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
| is_closed_typ _ = false;
- fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
+ fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, sfpT)
| defl_of (TVar _) = error ("defl_of_typ: TVar")
| defl_of (T as Type (c, Ts)) =
case Symtab.lookup tab c of
SOME t => list_ccomb (t, map defl_of Ts)
| NONE => if is_closed_typ T
- then mk_Rep_of T
+ then mk_SFP T
else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
in defl_of T end;
@@ -443,7 +443,7 @@
(* declare deflation combinator constants *)
fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy =
let
- val defl_type = map (K deflT) vs -->> deflT;
+ val defl_type = map (K sfpT) vs -->> sfpT;
val defl_bind = Binding.suffix_name "_defl" tbind;
in
Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
@@ -470,34 +470,34 @@
fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy =
let
fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
- val reps = map (mk_Rep_of o tfree) vs;
+ val reps = map (mk_SFP o tfree) vs;
val defl = list_ccomb (defl_const, reps);
- val ((_, _, _, {REP, ...}), thy) =
+ val ((_, _, _, {SFP, ...}), thy) =
Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy;
in
- (REP, thy)
+ (SFP, thy)
end;
- val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
- val thy = RepData.map (fold Thm.add_thm REP_thms) thy;
+ val (SFP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
+ val thy = RepData.map (fold Thm.add_thm SFP_thms) thy;
- (* prove REP equations *)
- fun mk_REP_eq_thm (lhsT, rhsT) =
+ (* prove SFP equations *)
+ fun mk_SFP_eq_thm (lhsT, rhsT) =
let
- val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
- val REP_simps = RepData.get thy;
+ val goal = mk_eqs (mk_SFP lhsT, mk_SFP rhsT);
+ val SFP_simps = RepData.get thy;
val tac =
- rewrite_goals_tac (map mk_meta_eq REP_simps)
+ rewrite_goals_tac (map mk_meta_eq SFP_simps)
THEN resolve_tac defl_unfold_thms 1;
in
Goal.prove_global thy [] [] goal (K tac)
end;
- val REP_eq_thms = map mk_REP_eq_thm dom_eqns;
+ val SFP_eq_thms = map mk_SFP_eq_thm dom_eqns;
- (* register REP equations *)
- val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dbinds;
+ (* register SFP equations *)
+ val SFP_eq_binds = map (Binding.prefix_name "SFP_eq_") dbinds;
val (_, thy) = thy |>
(Global_Theory.add_thms o map Thm.no_attributes)
- (REP_eq_binds ~~ REP_eq_thms);
+ (SFP_eq_binds ~~ SFP_eq_thms);
(* define rep/abs functions *)
fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy =
@@ -516,10 +516,10 @@
|>> ListPair.unzip;
(* prove isomorphism and isodefl rules *)
- fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
+ fun mk_iso_thms ((tbind, SFP_eq), (rep_def, abs_def)) thy =
let
fun make thm =
- Drule.zero_var_indexes (thm OF [REP_eq, abs_def, rep_def]);
+ Drule.zero_var_indexes (thm OF [SFP_eq, abs_def, rep_def]);
val rep_iso_thm = make @{thm domain_rep_iso};
val abs_iso_thm = make @{thm domain_abs_iso};
val isodefl_thm = make @{thm isodefl_abs_rep};
@@ -532,7 +532,7 @@
end;
val ((iso_thms, isodefl_abs_rep_thms), thy) =
thy
- |> fold_map mk_iso_thms (dbinds ~~ REP_eq_thms ~~ rep_abs_defs)
+ |> fold_map mk_iso_thms (dbinds ~~ SFP_eq_thms ~~ rep_abs_defs)
|>> ListPair.unzip;
(* collect info about rep/abs *)
@@ -561,7 +561,7 @@
val isodefl_thm =
let
fun unprime a = Library.unprefix "'" a;
- fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT);
+ fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), sfpT);
fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T);
fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T);
fun mk_goal ((map_const, defl_const), (T, rhsT)) =
@@ -579,9 +579,9 @@
@{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
val bottom_rules =
@{thms fst_strict snd_strict isodefl_bottom simp_thms};
- val REP_simps = map (fn th => th RS sym) (RepData.get thy);
+ val SFP_simps = map (fn th => th RS sym) (RepData.get thy);
val isodefl_rules =
- @{thms conjI isodefl_ID_REP}
+ @{thms conjI isodefl_ID_SFP}
@ isodefl_abs_rep_thms
@ IsodeflData.get thy;
in
@@ -595,7 +595,7 @@
simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
simp_tac beta_ss 1,
simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
- simp_tac (HOL_basic_ss addsimps REP_simps) 1,
+ simp_tac (HOL_basic_ss addsimps SFP_simps) 1,
REPEAT (etac @{thm conjE} 1),
REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
end;
@@ -613,23 +613,23 @@
(* prove map_ID theorems *)
fun prove_map_ID_thm
- (((map_const, (lhsT, _)), REP_thm), isodefl_thm) =
+ (((map_const, (lhsT, _)), SFP_thm), isodefl_thm) =
let
val Ts = snd (dest_Type lhsT);
val lhs = list_ccomb (map_const, map mk_ID Ts);
val goal = mk_eqs (lhs, mk_ID lhsT);
val tac = EVERY
- [rtac @{thm isodefl_REP_imp_ID} 1,
- stac REP_thm 1,
+ [rtac @{thm isodefl_SFP_imp_ID} 1,
+ stac SFP_thm 1,
rtac isodefl_thm 1,
- REPEAT (rtac @{thm isodefl_ID_REP} 1)];
+ REPEAT (rtac @{thm isodefl_ID_SFP} 1)];
in
Goal.prove_global thy [] [] goal (K tac)
end;
val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds;
val map_ID_thms =
map prove_map_ID_thm
- (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms);
+ (map_consts ~~ dom_eqns ~~ SFP_thms ~~ isodefl_thms);
val (_, thy) = thy |>
(Global_Theory.add_thms o map Thm.no_attributes)
(map_ID_binds ~~ map_ID_thms);