--- a/src/HOLCF/Eventual.thy Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/Eventual.thy Sat Mar 13 17:36:53 2010 -0800
@@ -13,16 +13,8 @@
apply (simp add: Compl_partition2 inf)
done
-lemma MOST_comp: "\<lbrakk>inj f; MOST x. P x\<rbrakk> \<Longrightarrow> MOST x. P (f x)"
-unfolding MOST_iff_finiteNeg
-by (drule (1) finite_vimageI, simp)
-
-lemma INFM_comp: "\<lbrakk>inj f; INFM x. P (f x)\<rbrakk> \<Longrightarrow> INFM x. P x"
-unfolding Inf_many_def
-by (clarify, drule (1) finite_vimageI, simp)
-
lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
-by (rule MOST_comp [OF inj_Suc])
+by (rule MOST_inj [OF _ inj_Suc])
lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
unfolding MOST_nat
--- a/src/HOLCF/ROOT.ML Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/ROOT.ML Sat Mar 13 17:36:53 2010 -0800
@@ -4,6 +4,6 @@
HOLCF -- a semantic extension of HOL by the LCF logic.
*)
-no_document use_thys ["Nat_Bijection"];
+no_document use_thys ["Nat_Bijection", "Infinite_Set"];
use_thys ["HOLCF"];
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Mar 13 17:36:53 2010 -0800
@@ -35,8 +35,6 @@
(thy : theory)
: Domain_Take_Proofs.iso_info * theory =
let
- val dname = Long_Name.base_name (Binding.name_of dbind);
-
val abs_bind = Binding.suffix_name "_abs" dbind;
val rep_bind = Binding.suffix_name "_rep" dbind;
@@ -53,17 +51,16 @@
val rep_iso_eqn =
Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x)));
- val thy = Sign.add_path dname thy;
+ val abs_iso_bind = Binding.qualified true "abs_iso" dbind;
+ val rep_iso_bind = Binding.qualified true "rep_iso" dbind;
val (abs_iso_thm, thy) =
yield_singleton PureThy.add_axioms
- ((Binding.name "abs_iso", abs_iso_eqn), []) thy;
+ ((abs_iso_bind, abs_iso_eqn), []) thy;
val (rep_iso_thm, thy) =
yield_singleton PureThy.add_axioms
- ((Binding.name "rep_iso", rep_iso_eqn), []) thy;
-
- val thy = Sign.parent_path thy;
+ ((rep_iso_bind, rep_iso_eqn), []) thy;
val result =
{
@@ -83,21 +80,17 @@
(thy : theory)
: thm * theory =
let
- val dname = Long_Name.base_name (Binding.name_of dbind);
-
val i = Free ("i", natT);
val T = (fst o dest_cfunT o range_type o fastype_of) take_const;
val lub_take_eqn =
mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T));
- val thy = Sign.add_path dname thy;
+ val lub_take_bind = Binding.qualified true "lub_take" dbind;
val (lub_take_thm, thy) =
yield_singleton PureThy.add_axioms
- ((Binding.name "lub_take", lub_take_eqn), []) thy;
-
- val thy = Sign.parent_path thy;
+ ((lub_take_bind, lub_take_eqn), []) thy;
in
(lub_take_thm, thy)
end;
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Mar 13 17:36:53 2010 -0800
@@ -8,7 +8,7 @@
signature DOMAIN_CONSTRUCTORS =
sig
val add_domain_constructors :
- string
+ binding
-> (binding * (bool * binding option * typ) list * mixfix) list
-> Domain_Take_Proofs.iso_info
-> theory
@@ -367,7 +367,7 @@
fun add_case_combinator
(spec : (term * (bool * typ) list) list)
(lhsT : typ)
- (dname : string)
+ (dbind : binding)
(con_betas : thm list)
(casedist : thm)
(iso_locale : thm)
@@ -420,7 +420,7 @@
(* definition of case combinator *)
local
- val case_bind = Binding.name (dname ^ "_when");
+ val case_bind = Binding.suffix_name "_when" dbind;
fun one_con f (_, args) =
let
fun argT (lazy, T) = if lazy then mk_upT T else T;
@@ -1011,11 +1011,12 @@
(******************************************************************************)
fun add_domain_constructors
- (dname : string)
+ (dbind : binding)
(spec : (binding * (bool * binding option * typ) list * mixfix) list)
(iso_info : Domain_Take_Proofs.iso_info)
(thy : theory) =
let
+ val dname = Binding.name_of dbind;
(* retrieve facts about rep/abs *)
val lhsT = #absT iso_info;
@@ -1049,7 +1050,7 @@
fun prep_con c (b, args, mx) = (c, map prep_arg args);
val case_spec = map2 prep_con con_consts spec;
in
- add_case_combinator case_spec lhsT dname
+ add_case_combinator case_spec lhsT dbind
con_betas casedist iso_locale rep_const thy
end;
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Sat Mar 13 17:36:53 2010 -0800
@@ -7,25 +7,25 @@
signature DOMAIN_EXTENDER =
sig
val add_domain_cmd:
- string ->
+ binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
val add_domain:
- string ->
+ binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
val add_new_domain_cmd:
- string ->
+ binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
val add_new_domain:
- string ->
+ binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
@@ -126,7 +126,7 @@
fun gen_add_domain
(prep_typ : theory -> 'a -> typ)
- (comp_dnam : string)
+ (comp_dbind : binding)
(eqs''' : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * 'a) list * mixfix) list) list)
(thy : theory) =
@@ -166,7 +166,6 @@
val eqs' : ((string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list) list =
check_and_sort_domain false dtnvs' cons'' thy;
-(* val thy = Domain_Syntax.add_syntax eqs' thy; *)
val dts : typ list = map (Type o fst) eqs';
val new_dts : (string * string list) list =
map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
@@ -189,22 +188,21 @@
val ((rewss, take_rews), theorems_thy) =
thy
- |> fold_map (fn ((eq, (x,cs)), info) =>
- Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
- (eqs ~~ eqs' ~~ iso_infos)
- ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info;
+ |> fold_map (fn (((dbind, eq), (_,cs)), info) =>
+ Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
+ (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
+ ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
in
theorems_thy
- |> Sign.add_path (Long_Name.base_name comp_dnam)
|> PureThy.add_thmss
- [((Binding.name "rews", flat rewss @ take_rews), [])]
+ [((Binding.qualified true "rews" comp_dbind,
+ flat rewss @ take_rews), [])]
|> snd
- |> Sign.parent_path
end;
fun gen_add_new_domain
(prep_typ : theory -> 'a -> typ)
- (comp_dnam : string)
+ (comp_dbind : binding)
(eqs''' : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * 'a) list * mixfix) list) list)
(thy : theory) =
@@ -229,6 +227,8 @@
|> Sign.add_types (map thy_type dtnvs)
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+ val dbinds : binding list =
+ map (fn (_,dbind,_,_) => dbind) eqs''';
val cons''' :
(binding * (bool * binding option * 'a) list * mixfix) list list =
map (fn (_,_,_,cons) => cons) eqs''';
@@ -265,17 +265,16 @@
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
val ((rewss, take_rews), theorems_thy) =
thy
- |> fold_map (fn ((eq, (x,cs)), info) =>
- Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
- (eqs ~~ eqs' ~~ iso_infos)
- ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info;
+ |> fold_map (fn (((dbind, eq), (x,cs)), info) =>
+ Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
+ (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
+ ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
in
theorems_thy
- |> Sign.add_path (Long_Name.base_name comp_dnam)
|> PureThy.add_thmss
- [((Binding.name "rews", flat rewss @ take_rews), [])]
+ [((Binding.qualified true "rews" comp_dbind,
+ flat rewss @ take_rews), [])]
|> snd
- |> Sign.parent_path
end;
val add_domain = gen_add_domain Sign.certify_typ;
@@ -314,12 +313,12 @@
(P.$$$ "=" |-- P.enum1 "|" cons_decl);
val domains_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+ Scan.option (P.$$$ "(" |-- P.binding --| P.$$$ ")") --
P.and_list1 domain_decl;
fun mk_domain
(definitional : bool)
- (opt_name : string option,
+ (opt_name : binding option,
doms : ((((string * string option) list * binding) * mixfix) *
((binding * (bool * binding option * string) list) * mixfix) list) list ) =
let
@@ -328,12 +327,13 @@
(binding * (bool * binding option * string) list * mixfix) list) list =
map (fn (((vs, t), mx), cons) =>
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
- val comp_dnam =
- case opt_name of NONE => space_implode "_" names | SOME s => s;
+ val comp_dbind =
+ case opt_name of NONE => Binding.name (space_implode "_" names)
+ | SOME s => s;
in
if definitional
- then add_new_domain_cmd comp_dnam specs
- else add_domain_cmd comp_dnam specs
+ then add_new_domain_cmd comp_dbind specs
+ else add_domain_cmd comp_dbind specs
end;
val _ =
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Mar 13 17:36:53 2010 -0800
@@ -236,12 +236,9 @@
((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;
+fun add_qualified_thm name (dbind, thm) =
+ yield_singleton PureThy.add_thms
+ ((Binding.qualified true name dbind, thm), []);
(******************************************************************************)
(******************************* main function ********************************)
@@ -306,7 +303,7 @@
| dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^
" : " ^ commas dups))
end) doms;
- val dom_binds = map (fn (_, tbind, _, _, _) => tbind) doms;
+ val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms;
val morphs = map (fn (_, _, _, _, morphs) => morphs) doms;
(* declare deflation combinator constants *)
@@ -331,7 +328,7 @@
val defl_specs = map mk_defl_spec dom_eqns;
(* register recursive definition of deflation combinators *)
- val defl_binds = map (Binding.suffix_name "_defl") dom_binds;
+ val defl_binds = map (Binding.suffix_name "_defl") dbinds;
val ((defl_apply_thms, defl_unfold_thms), thy) =
add_fixdefs (defl_binds ~~ defl_specs) thy;
@@ -363,7 +360,7 @@
val REP_eq_thms = map mk_REP_eq_thm dom_eqns;
(* register REP equations *)
- val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dom_binds;
+ val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dbinds;
val (_, thy) = thy |>
(PureThy.add_thms o map Thm.no_attributes)
(REP_eq_binds ~~ REP_eq_thms);
@@ -381,32 +378,27 @@
(((rep_const, abs_const), (rep_def, abs_def)), thy)
end;
val ((rep_abs_consts, rep_abs_defs), thy) = thy
- |> fold_map mk_rep_abs (dom_binds ~~ morphs ~~ dom_eqns)
+ |> fold_map mk_rep_abs (dbinds ~~ morphs ~~ dom_eqns)
|>> ListPair.unzip;
(* prove isomorphism and isodefl rules *)
fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
let
- fun make thm = Drule.export_without_context (thm OF [REP_eq, abs_def, rep_def]);
+ fun make thm =
+ Drule.export_without_context (thm OF [REP_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};
- val rep_iso_bind = Binding.name "rep_iso";
- val abs_iso_bind = Binding.name "abs_iso";
- val isodefl_bind = Binding.name "isodefl_abs_rep";
- val (_, thy) = thy
- |> Sign.add_path (Binding.name_of tbind)
- |> (PureThy.add_thms o map Thm.no_attributes)
- [(rep_iso_bind, rep_iso_thm),
- (abs_iso_bind, abs_iso_thm),
- (isodefl_bind, isodefl_thm)]
- ||> Sign.parent_path;
+ val thy = thy
+ |> snd o add_qualified_thm "rep_iso" (tbind, rep_iso_thm)
+ |> snd o add_qualified_thm "abs_iso" (tbind, abs_iso_thm)
+ |> snd o add_qualified_thm "isodefl_abs_rep" (tbind, isodefl_thm);
in
(((rep_iso_thm, abs_iso_thm), isodefl_thm), thy)
end;
val ((iso_thms, isodefl_abs_rep_thms), thy) =
thy
- |> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs)
+ |> fold_map mk_iso_thms (dbinds ~~ REP_eq_thms ~~ rep_abs_defs)
|>> ListPair.unzip;
(* collect info about rep/abs *)
@@ -434,7 +426,7 @@
Sign.declare_const ((map_bind, map_type), NoSyn) thy
end;
val (map_consts, thy) = thy |>
- fold_map declare_map_const (dom_binds ~~ dom_eqns);
+ fold_map declare_map_const (dbinds ~~ dom_eqns);
(* defining equations for map functions *)
local
@@ -457,7 +449,7 @@
end;
(* register recursive definition of map functions *)
- val map_binds = map (Binding.suffix_name "_map") dom_binds;
+ val map_binds = map (Binding.suffix_name "_map") dbinds;
val ((map_apply_thms, map_unfold_thms), thy) =
add_fixdefs (map_binds ~~ map_specs) thy;
@@ -503,7 +495,7 @@
REPEAT (etac @{thm conjE} 1),
REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
end;
- val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds;
+ val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds;
fun conjuncts [] thm = []
| conjuncts (n::[]) thm = [(n, thm)]
| conjuncts (n::ns) thm = let
@@ -530,7 +522,7 @@
in
Goal.prove_global thy [] [] goal (K tac)
end;
- val map_ID_binds = map (Binding.suffix_name "_map_ID") dom_binds;
+ 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);
@@ -577,7 +569,7 @@
REPEAT (etac @{thm conjE} 1),
REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)])
end;
- val deflation_map_binds = dom_binds |>
+ val deflation_map_binds = dbinds |>
map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map");
val (deflation_map_thms, thy) = thy |>
(PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
@@ -597,7 +589,7 @@
(* definitions and proofs related to take functions *)
val (take_info, thy) =
Domain_Take_Proofs.define_take_functions
- (dom_binds ~~ iso_infos) thy;
+ (dbinds ~~ iso_infos) thy;
val { take_consts, take_defs, chain_take_thms, take_0_thms,
take_Suc_thms, deflation_take_thms,
finite_consts, finite_defs } = take_info;
@@ -632,7 +624,7 @@
end;
(* prove lub of take equals ID *)
- fun prove_lub_take (((bind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
+ fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
let
val n = Free ("n", natT);
val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT);
@@ -643,16 +635,16 @@
REPEAT (etac @{thm Pair_inject} 1), atac 1];
val lub_take_thm = Goal.prove_global thy [] [] goal (K tac);
in
- add_qualified_thm "lub_take" (Binding.name_of bind, lub_take_thm) thy
+ add_qualified_thm "lub_take" (dbind, lub_take_thm) thy
end;
val (lub_take_thms, thy) =
fold_map prove_lub_take
- (dom_binds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy;
+ (dbinds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy;
(* prove additional take theorems *)
val (take_info2, thy) =
Domain_Take_Proofs.add_lub_take_theorems
- (dom_binds ~~ iso_infos) take_info lub_take_thms thy;
+ (dbinds ~~ iso_infos) take_info lub_take_thms thy;
in
((iso_infos, take_info2), thy)
end;
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Mar 13 17:36:53 2010 -0800
@@ -203,40 +203,17 @@
(********************* 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_def name (dbind, eqn) =
+ yield_singleton (PureThy.add_defs false)
+ ((Binding.qualified true name dbind, eqn), []);
-fun add_qualified_def name (path, eqn) thy =
- thy
- |> Sign.add_path path
- |> yield_singleton (PureThy.add_defs false)
- (Thm.no_attributes (Binding.name name, eqn))
- ||> Sign.parent_path;
+fun add_qualified_thm name (dbind, thm) =
+ yield_singleton PureThy.add_thms
+ ((Binding.qualified true name dbind, thm), []);
-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;
-
-fun add_qualified_simp_thm name (path, thm) thy =
- thy
- |> Sign.add_path path
- |> yield_singleton PureThy.add_thms
- ((Binding.name name, thm), [Simplifier.simp_add])
- ||> Sign.parent_path;
+fun add_qualified_simp_thm name (dbind, thm) =
+ yield_singleton PureThy.add_thms
+ ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]);
(******************************************************************************)
(************************** defining take functions ***************************)
@@ -248,11 +225,10 @@
let
(* retrieve components of spec *)
- val dom_binds = map fst spec;
+ val dbinds = 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;
@@ -268,7 +244,7 @@
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);
+ val copy_args = map snd (mk_projs dbinds copy_arg);
fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
let
val body = map_of_typ thy (newTs ~~ copy_args) rhsT;
@@ -283,40 +259,39 @@
val n = Free ("n", HOLogic.natT);
val rhs = mk_iterate (n, take_functional);
in
- map (lambda n o snd) (mk_projs dom_binds rhs)
+ map (lambda n o snd) (mk_projs dbinds rhs)
end;
(* define take constants *)
- fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy =
+ fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy =
let
val take_type = HOLogic.natT --> lhsT ->> lhsT;
- val take_bind = Binding.suffix_name "_take" tbind;
+ val take_bind = Binding.suffix_name "_take" dbind;
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) =
- add_qualified_def "take_def"
- (Binding.name_of tbind, take_eqn) thy;
+ add_qualified_def "take_def" (dbind, take_eqn) thy;
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)
+ |> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns)
|>> ListPair.unzip;
(* prove chain_take lemmas *)
- fun prove_chain_take (take_const, dname) thy =
+ fun prove_chain_take (take_const, dbind) 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 thm = Goal.prove_global thy [] [] goal (K tac);
in
- add_qualified_simp_thm "chain_take" (dname, thm) thy
+ add_qualified_simp_thm "chain_take" (dbind, thm) thy
end;
val (chain_take_thms, thy) =
- fold_map prove_chain_take (take_consts ~~ dnames) thy;
+ fold_map prove_chain_take (take_consts ~~ dbinds) thy;
(* prove take_0 lemmas *)
- fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy =
+ fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy =
let
val lhs = take_const $ @{term "0::nat"};
val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
@@ -324,16 +299,16 @@
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
+ add_qualified_thm "take_0" (dbind, take_0_thm) thy
end;
val (take_0_thms, thy) =
- fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
+ fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy;
(* prove take_Suc lemmas *)
val n = Free ("n", natT);
val take_is = map (fn t => t $ n) take_consts;
fun prove_take_Suc
- (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
+ (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy =
let
val lhs = take_const $ (@{term Suc} $ n);
val body = map_of_typ thy (newTs ~~ take_is) rhsT;
@@ -344,11 +319,11 @@
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
+ add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy
end;
val (take_Suc_thms, thy) =
fold_map prove_take_Suc
- (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy;
+ (take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy;
(* prove deflation theorems for take functions *)
val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
@@ -385,52 +360,52 @@
val (deflation_take_thms, thy) =
fold_map (add_qualified_thm "deflation_take")
(map (apsnd Drule.export_without_context)
- (conjuncts dnames deflation_take_thm)) thy;
+ (conjuncts dbinds deflation_take_thm)) thy;
(* prove strictness of take functions *)
- fun prove_take_strict (deflation_take, dname) thy =
+ fun prove_take_strict (deflation_take, dbind) thy =
let
val take_strict_thm =
Drule.export_without_context
(@{thm deflation_strict} OF [deflation_take]);
in
- add_qualified_thm "take_strict" (dname, take_strict_thm) thy
+ add_qualified_thm "take_strict" (dbind, take_strict_thm) thy
end;
val (take_strict_thms, thy) =
fold_map prove_take_strict
- (deflation_take_thms ~~ dnames) thy;
+ (deflation_take_thms ~~ dbinds) thy;
(* prove take/take rules *)
- fun prove_take_take ((chain_take, deflation_take), dname) thy =
+ fun prove_take_take ((chain_take, deflation_take), dbind) thy =
let
val take_take_thm =
Drule.export_without_context
(@{thm deflation_chain_min} OF [chain_take, deflation_take]);
in
- add_qualified_thm "take_take" (dname, take_take_thm) thy
+ add_qualified_thm "take_take" (dbind, take_take_thm) thy
end;
val (take_take_thms, thy) =
fold_map prove_take_take
- (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
+ (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy;
(* prove take_below rules *)
- fun prove_take_below (deflation_take, dname) thy =
+ fun prove_take_below (deflation_take, dbind) thy =
let
val take_below_thm =
Drule.export_without_context
(@{thm deflation.below} OF [deflation_take]);
in
- add_qualified_thm "take_below" (dname, take_below_thm) thy
+ add_qualified_thm "take_below" (dbind, take_below_thm) thy
end;
val (take_below_thms, thy) =
fold_map prove_take_below
- (deflation_take_thms ~~ dnames) thy;
+ (deflation_take_thms ~~ dbinds) thy;
(* define finiteness predicates *)
- fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy =
+ fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy =
let
val finite_type = lhsT --> boolT;
- val finite_bind = Binding.suffix_name "_finite" tbind;
+ val finite_bind = Binding.suffix_name "_finite" dbind;
val (finite_const, thy) =
Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
val x = Free ("x", lhsT);
@@ -440,11 +415,10 @@
(lambda n (mk_eq (mk_capply (take_const $ n, x), x))));
val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
val (finite_def_thm, thy) =
- add_qualified_def "finite_def"
- (Binding.name_of tbind, finite_eqn) thy;
+ add_qualified_def "finite_def" (dbind, finite_eqn) thy;
in ((finite_const, finite_def_thm), thy) end;
val ((finite_consts, finite_defs), thy) = thy
- |> fold_map define_finite_const (dom_binds ~~ take_consts ~~ dom_eqns)
+ |> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns)
|>> ListPair.unzip;
val result =
@@ -469,10 +443,9 @@
(lub_take_thms : thm list)
(thy : theory) =
let
- val dom_binds = map fst spec;
+ val dbinds = map fst spec;
val iso_infos = map snd spec;
val absTs = map #absT iso_infos;
- val dnames = map Binding.name_of dom_binds;
val {take_consts, ...} = take_info;
val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info;
val {finite_consts, finite_defs, ...} = take_info;
@@ -530,9 +503,9 @@
val thy = thy
|> fold (snd oo add_qualified_thm "finite")
- (dnames ~~ finite_thms)
+ (dbinds ~~ finite_thms)
|> fold (snd oo add_qualified_thm "take_induct")
- (dnames ~~ take_induct_thms);
+ (dbinds ~~ take_induct_thms);
in
((finite_thms, take_induct_thms), thy)
end;
@@ -545,39 +518,38 @@
let
(* retrieve components of spec *)
- val dom_binds = map fst spec;
+ val dbinds = map fst spec;
val iso_infos = map snd spec;
val absTs = map #absT iso_infos;
val repTs = map #repT iso_infos;
- val dnames = map Binding.name_of dom_binds;
val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info;
val {chain_take_thms, deflation_take_thms, ...} = take_info;
(* prove take lemmas *)
- fun prove_take_lemma ((chain_take, lub_take), dname) thy =
+ fun prove_take_lemma ((chain_take, lub_take), dbind) thy =
let
val take_lemma =
Drule.export_without_context
(@{thm lub_ID_take_lemma} OF [chain_take, lub_take]);
in
- add_qualified_thm "take_lemma" (dname, take_lemma) thy
+ add_qualified_thm "take_lemma" (dbind, take_lemma) thy
end;
val (take_lemma_thms, thy) =
fold_map prove_take_lemma
- (chain_take_thms ~~ lub_take_thms ~~ dnames) thy;
+ (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy;
(* prove reach lemmas *)
- fun prove_reach_lemma ((chain_take, lub_take), dname) thy =
+ fun prove_reach_lemma ((chain_take, lub_take), dbind) thy =
let
val thm =
Drule.export_without_context
(@{thm lub_ID_reach} OF [chain_take, lub_take]);
in
- add_qualified_thm "reach" (dname, thm) thy
+ add_qualified_thm "reach" (dbind, thm) thy
end;
val (reach_thms, thy) =
fold_map prove_reach_lemma
- (chain_take_thms ~~ lub_take_thms ~~ dnames) thy;
+ (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy;
(* test for finiteness of domain definitions *)
local
@@ -608,7 +580,7 @@
val take_inducts =
map prove_take_induct (chain_take_thms ~~ lub_take_thms);
val thy = fold (snd oo add_qualified_thm "take_induct")
- (dnames ~~ take_inducts) thy;
+ (dbinds ~~ take_inducts) thy;
in
((NONE, take_inducts), thy)
end;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 17:36:53 2010 -0800
@@ -10,13 +10,15 @@
signature DOMAIN_THEOREMS =
sig
val theorems:
- Domain_Library.eq * Domain_Library.eq list
- -> typ * (binding * (bool * binding option * typ) list * mixfix) list
- -> Domain_Take_Proofs.iso_info
- -> theory -> thm list * theory;
+ Domain_Library.eq * Domain_Library.eq list ->
+ binding ->
+ (binding * (bool * binding option * typ) list * mixfix) list ->
+ Domain_Take_Proofs.iso_info ->
+ Domain_Take_Proofs.take_induct_info ->
+ theory -> thm list * theory;
val comp_theorems :
- bstring * Domain_Library.eq list ->
+ binding * Domain_Library.eq list ->
Domain_Take_Proofs.take_induct_info ->
theory -> thm list * theory
@@ -82,8 +84,10 @@
fun theorems
(((dname, _), cons) : eq, eqs : eq list)
- (dom_eqn : typ * (binding * (bool * binding option * typ) list * mixfix) list)
+ (dbind : binding)
+ (spec : (binding * (bool * binding option * typ) list * mixfix) list)
(iso_info : Domain_Take_Proofs.iso_info)
+ (take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
let
@@ -103,15 +107,15 @@
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
in
val ax_take_0 = ga "take_0" dname;
- val ax_take_Suc = ga "take_Suc" dname;
val ax_take_strict = ga "take_strict" dname;
end; (* local *)
+val {take_Suc_thms, deflation_take_thms, ...} = take_info;
+
(* ----- define constructors ------------------------------------------------ *)
val (result, thy) =
- Domain_Constructors.add_domain_constructors
- (Long_Name.base_name dname) (snd dom_eqn) iso_info thy;
+ Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
val con_appls = #con_betas result;
val {exhaust, casedist, ...} = result;
@@ -138,8 +142,6 @@
fun dc_take dn = %%:(dn^"_take");
val dnames = map (fst o fst) eqs;
val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
- fun get_deflation_take dn = PureThy.get_thm thy (dn ^ ".deflation_take");
- val axs_deflation_take = map get_deflation_take dnames;
fun copy_of_dtyp tab r dt =
if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
@@ -162,9 +164,9 @@
val rhs = con_app2 con one_rhs args;
val goal = mk_trp (lhs === rhs);
val rules =
- [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}]
- @ @{thms take_con_rules ID1 deflation_strict}
- @ deflation_thms @ axs_deflation_take;
+ [ax_abs_iso]
+ @ @{thms take_con_rules ID1 cfcomp2 deflation_strict}
+ @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
in pg con_appls goal (K tacs) end;
val take_apps = map one_take_app cons;
@@ -173,33 +175,34 @@
end;
val case_ns =
- "bottom" :: map (fn (b,_,_) => Binding.name_of b) (snd dom_eqn);
+ "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
+
+fun qualified name = Binding.qualified true name dbind;
+val simp = Simplifier.simp_add;
+val fixrec_simp = Fixrec.fixrec_simp_add;
in
thy
- |> Sign.add_path (Long_Name.base_name dname)
- |> snd o PureThy.add_thmss [
- ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
- ((Binding.name "exhaust" , [exhaust] ), []),
- ((Binding.name "casedist" , [casedist] ),
- [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
- ((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]),
- ((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]),
- ((Binding.name "con_rews" , con_rews ),
- [Simplifier.simp_add, Fixrec.fixrec_simp_add]),
- ((Binding.name "sel_rews" , sel_rews ), [Simplifier.simp_add]),
- ((Binding.name "dis_rews" , dis_rews ), [Simplifier.simp_add]),
- ((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]),
- ((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]),
- ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]),
- ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
- ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
- ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]),
- ((Binding.name "match_rews", mat_rews ),
- [Simplifier.simp_add, Fixrec.fixrec_simp_add])]
- |> Sign.parent_path
- |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
- pat_rews @ dist_les @ dist_eqs)
+ |> PureThy.add_thmss [
+ ((qualified "iso_rews" , iso_rews ), [simp]),
+ ((qualified "exhaust" , [exhaust] ), []),
+ ((qualified "casedist" , [casedist] ),
+ [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
+ ((qualified "when_rews" , when_rews ), [simp]),
+ ((qualified "compacts" , con_compacts), [simp]),
+ ((qualified "con_rews" , con_rews ), [simp, fixrec_simp]),
+ ((qualified "sel_rews" , sel_rews ), [simp]),
+ ((qualified "dis_rews" , dis_rews ), [simp]),
+ ((qualified "pat_rews" , pat_rews ), [simp]),
+ ((qualified "dist_les" , dist_les ), [simp]),
+ ((qualified "dist_eqs" , dist_eqs ), [simp]),
+ ((qualified "inverts" , inverts ), [simp]),
+ ((qualified "injects" , injects ), [simp]),
+ ((qualified "take_rews" , take_rews ), [simp]),
+ ((qualified "match_rews", mat_rews ), [simp, fixrec_simp])]
+ |> snd
+ |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
+ pat_rews @ dist_les @ dist_eqs)
end; (* let *)
(******************************************************************************)
@@ -207,11 +210,12 @@
(******************************************************************************)
fun prove_induction
- (comp_dnam, eqs : eq list)
+ (comp_dbind : binding, eqs : eq list)
(take_rews : thm list)
(take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
let
+ val comp_dname = Sign.full_name thy comp_dbind;
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
fun dc_take dn = %%:(dn^"_take");
@@ -286,7 +290,7 @@
val is_emptys = map warn n__eqs;
val is_finite = #is_finite take_info;
val _ = if is_finite
- then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
+ then message ("Proving finiteness rule for domain "^comp_dname^" ...")
else ();
end;
val _ = trace " Proving finite_ind...";
@@ -400,12 +404,12 @@
((Binding.empty, [rule]),
[Rule_Cases.case_names case_ns, Induct.induct_type dname]);
-in thy |> Sign.add_path comp_dnam
- |> snd o PureThy.add_thmss [
- ((Binding.name "finite_ind" , [finite_ind]), []),
- ((Binding.name "ind" , [ind] ), [])]
- |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
- |> Sign.parent_path
+in
+ thy
+ |> snd o PureThy.add_thmss [
+ ((Binding.qualified true "finite_ind" comp_dbind, [finite_ind]), []),
+ ((Binding.qualified true "ind" comp_dbind, [ind] ), [])]
+ |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
end; (* prove_induction *)
(******************************************************************************)
@@ -413,13 +417,13 @@
(******************************************************************************)
fun prove_coinduction
- (comp_dnam, eqs : eq list)
+ (comp_dbind : binding, eqs : eq list)
(take_lemmas : thm list)
(thy : theory) : theory =
let
val dnames = map (fst o fst) eqs;
-val comp_dname = Sign.full_bname thy comp_dnam;
+val comp_dname = Sign.full_name thy comp_dbind;
fun dc_take dn = %%:(dn^"_take");
val x_name = idx_name dnames "x";
val n_eqs = length eqs;
@@ -433,7 +437,7 @@
open HOLCF_Library
val dtypes = map (Type o fst) eqs;
val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes);
- val bisim_bind = Binding.name (comp_dnam ^ "_bisim");
+ val bisim_bind = Binding.suffix_name "_bisim" comp_dbind;
val bisim_type = relprod --> boolT;
in
val (bisim_const, thy) =
@@ -449,10 +453,6 @@
fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
- val comp_dname = Sign.full_bname thy comp_dnam;
- val dnames = map (fst o fst) eqs;
- val x_name = idx_name dnames "x";
-
fun one_con (con, args) =
let
val nonrec_args = filter_out is_rec args;
@@ -494,11 +494,9 @@
mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs));
in
- val ([ax_bisim_def], thy) =
- thy
- |> Sign.add_path comp_dnam
- |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)]
- ||> Sign.parent_path;
+ val (ax_bisim_def, thy) =
+ yield_singleton add_defs_infer
+ (Binding.qualified true "bisim_def" comp_dbind, bisim_eqn) thy;
end; (* local *)
(* ----- theorem concerning coinduction ------------------------------------- *)
@@ -555,20 +553,19 @@
in pg [] goal (K tacs) end;
end; (* local *)
-in thy |> Sign.add_path comp_dnam
- |> snd o PureThy.add_thmss [((Binding.name "coind", [coind]), [])]
- |> Sign.parent_path
+in thy |> snd o PureThy.add_thmss
+ [((Binding.qualified true "coind" comp_dbind, [coind]), [])]
end; (* let *)
fun comp_theorems
- (comp_dnam : string, eqs : eq list)
+ (comp_dbind : binding, eqs : eq list)
(take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
let
val map_tab = Domain_Take_Proofs.get_map_tab thy;
val dnames = map (fst o fst) eqs;
-val comp_dname = Sign.full_bname thy comp_dnam;
+val comp_dname = Sign.full_name thy comp_dbind;
(* ----- getting the composite axiom and definitions ------------------------ *)
@@ -596,11 +593,11 @@
(* prove induction rules, unless definition is indirect recursive *)
val thy =
if is_indirect then thy else
- prove_induction (comp_dnam, eqs) take_rews take_info thy;
+ prove_induction (comp_dbind, eqs) take_rews take_info thy;
val thy =
if is_indirect then thy else
- prove_coinduction (comp_dnam, eqs) take_lemmas thy;
+ prove_coinduction (comp_dbind, eqs) take_lemmas thy;
in
(take_rews, thy)
--- a/src/HOLCF/Tools/fixrec.ML Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/Tools/fixrec.ML Sat Mar 13 17:36:53 2010 -0800
@@ -101,10 +101,10 @@
fun name_of (Const (n, T)) = n
| name_of (Free (n, T)) = n
- | name_of _ = fixrec_err "name_of"
+ | name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t]);
val lhs_name =
- name_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
+ name_of o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
in
@@ -138,7 +138,7 @@
| defs (l::[]) r = [one_def l r]
| defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
val fixdefs = defs lhss fixpoint;
- val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
+ val (fixdef_thms : (term * (string * thm)) list, lthy) = lthy
|> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs);
fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
@@ -148,7 +148,7 @@
|> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
|> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict};
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
- |> Local_Defs.unfold lthy' @{thms split_conv};
+ |> Local_Defs.unfold lthy @{thms split_conv};
fun unfolds [] thm = []
| unfolds (n::[]) thm = [(n, thm)]
| unfolds (n::ns) thm = let
@@ -158,21 +158,21 @@
val unfold_thms = unfolds names tuple_unfold_thm;
val induct_note : Attrib.binding * Thm.thm list =
let
- val thm_name = Binding.name (all_names ^ "_induct");
+ val thm_name = Binding.qualify true all_names (Binding.name "induct");
in
((thm_name, []), [tuple_induct_thm])
end;
fun unfold_note (name, thm) : Attrib.binding * Thm.thm list =
let
- val thm_name = Binding.name (name ^ "_unfold");
+ val thm_name = Binding.qualify true name (Binding.name "unfold");
val src = Attrib.internal (K add_unfold);
in
((thm_name, [src]), [thm])
end;
- val (thmss, lthy'') = lthy'
+ val (thmss, lthy) = lthy
|> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms);
in
- (lthy'', names, fixdef_thms, map snd unfold_thms)
+ (lthy, names, fixdef_thms, map snd unfold_thms)
end;
(*************************************************************************)
@@ -311,7 +311,7 @@
else HOLogic.dest_Trueprop (Logic.strip_imp_concl t);
fun tac (t, i) =
let
- val Const (c, T) = chead_of (fst (HOLogic.dest_eq (concl t)));
+ val Const (c, T) = head_of (chead_of (fst (HOLogic.dest_eq (concl t))));
val unfold_thm = the (Symtab.lookup tab c);
val rule = unfold_thm RS @{thm ssubst_lhs};
in
@@ -377,25 +377,25 @@
val matches = map (compile_pats match_name) (map (map snd) blocks);
val spec' = map (pair Attrib.empty_binding) matches;
- val (lthy', cnames, fixdef_thms, unfold_thms) =
+ val (lthy, cnames, fixdef_thms, unfold_thms) =
add_fixdefs fixes spec' lthy;
in
if strict then let (* only prove simp rules if strict = true *)
val simps : (Attrib.binding * thm) list list =
- map (make_simps lthy') (unfold_thms ~~ blocks);
+ map (make_simps lthy) (unfold_thms ~~ blocks);
fun mk_bind n : Attrib.binding =
- (Binding.name (n ^ "_simps"),
+ (Binding.qualify true n (Binding.name "simps"),
[Attrib.internal (K Simplifier.simp_add)]);
val simps1 : (Attrib.binding * thm list) list =
map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
val simps2 : (Attrib.binding * thm list) list =
map (apsnd (fn thm => [thm])) (flat simps);
- val (_, lthy'') = lthy'
+ val (_, lthy) = lthy
|> fold_map Local_Theory.note (simps1 @ simps2);
in
- lthy''
+ lthy
end
- else lthy'
+ else lthy
end;
in
@@ -415,7 +415,7 @@
val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
val cname = case chead_of t of Const(c,_) => c | _ =>
fixrec_err "function is not declared as constant in theory";
- val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
+ val unfold_thm = PureThy.get_thm thy (cname^".unfold");
val simp = Goal.prove_global thy [] [] eq
(fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
in simp end;
--- a/src/HOLCF/ex/Fixrec_ex.thy Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/ex/Fixrec_ex.thy Sat Mar 13 17:36:53 2010 -0800
@@ -150,8 +150,8 @@
and 'a forest = Empty | Trees (lazy "'a tree") "'a forest"
text {*
- To define mutually recursive functions, separate the equations
- for each function using the keyword @{text "and"}.
+ To define mutually recursive functions, give multiple type signatures
+ separated by the keyword @{text "and"}.
*}
fixrec
@@ -173,13 +173,31 @@
text {*
Theorems generated:
- @{text map_tree_def}
- @{text map_forest_def}
- @{text map_tree_unfold}
- @{text map_forest_unfold}
- @{text map_tree_simps}
- @{text map_forest_simps}
- @{text map_tree_map_forest_induct}
+ @{text map_tree_def} @{thm map_tree_def}
+ @{text map_forest_def} @{thm map_forest_def}
+ @{text map_tree.unfold} @{thm map_tree.unfold}
+ @{text map_forest.unfold} @{thm map_forest.unfold}
+ @{text map_tree.simps} @{thm map_tree.simps}
+ @{text map_forest.simps} @{thm map_forest.simps}
+ @{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct}
*}
+
+subsection {* Using @{text fixrec} inside locales *}
+
+locale test =
+ fixes foo :: "'a \<rightarrow> 'a"
+ assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
+begin
+
+fixrec
+ bar :: "'a u \<rightarrow> 'a"
+where
+ "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
+
+lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
end
+
+end
--- a/src/HOLCF/ex/Powerdomain_ex.thy Sat Mar 13 20:44:12 2010 +0100
+++ b/src/HOLCF/ex/Powerdomain_ex.thy Sat Mar 13 17:36:53 2010 -0800
@@ -85,27 +85,27 @@
where "tree3 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>tree3)
\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
-declare tree1_simps tree2_simps tree3_simps [simp del]
+declare tree1.simps tree2.simps tree3.simps [simp del]
lemma pick_tree1:
"pick\<cdot>tree1 = {Def 1, Def 2, Def 3, Def 4}\<natural>"
-apply (subst tree1_simps)
+apply (subst tree1.simps)
apply simp
apply (simp add: convex_plus_ac)
done
lemma pick_tree2:
"pick\<cdot>tree2 = {Def 1, Def 2, \<bottom>, Def 4}\<natural>"
-apply (subst tree2_simps)
+apply (subst tree2.simps)
apply simp
apply (simp add: convex_plus_ac)
done
lemma pick_tree3:
"pick\<cdot>tree3 = {Def 1, \<bottom>, Def 3, Def 4}\<natural>"
-apply (subst tree3_simps)
+apply (subst tree3.simps)
apply simp
-apply (induct rule: tree3_induct)
+apply (induct rule: tree3.induct)
apply simp
apply simp
apply (simp add: convex_plus_ac)