change domain package's treatment of variable names in theorems to be like datatype package
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Wed Feb 24 14:13:15 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Feb 24 14:20:07 2010 -0800
@@ -154,18 +154,13 @@
val dts = map (Type o fst) eqs';
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
- fun typid (Type (id,_)) =
- let val c = hd (Symbol.explode (Long_Name.base_name id))
- in if Symbol.is_letter c then c else "t" end
- | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
- | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
fun one_con (con,args,mx) =
(Binding.name_of con, (* FIXME preverse binding (!?) *)
mx,
ListPair.map (fn ((lazy,sel,tp),vn) =>
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
Option.map Binding.name_of sel,vn))
- (args,(mk_var_names(map (typid o third) args)))
+ (args, Datatype_Prop.make_tnames (map third args))
) : cons;
val eqs : eq list =
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
@@ -230,18 +225,13 @@
val dts = map (Type o fst) eqs';
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
- fun typid (Type (id,_)) =
- let val c = hd (Symbol.explode (Long_Name.base_name id))
- in if Symbol.is_letter c then c else "t" end
- | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
- | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
fun one_con (con,args,mx) =
(Binding.name_of con, (* FIXME preverse binding (!?) *)
mx,
ListPair.map (fn ((lazy,sel,tp),vn) =>
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
Option.map Binding.name_of sel,vn))
- (args,(mk_var_names(map (typid o third) args)))
+ (args, Datatype_Prop.make_tnames (map third args))
) : cons;
val eqs : eq list =
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
--- a/src/HOLCF/Tools/Domain/domain_library.ML Wed Feb 24 14:13:15 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Wed Feb 24 14:20:07 2010 -0800
@@ -162,7 +162,6 @@
val dis_name : string -> string;
val mat_name : string -> string;
val pat_name : string -> string;
- val mk_var_names : string list -> string list;
end;
structure Domain_Library :> DOMAIN_LIBRARY =
@@ -191,22 +190,6 @@
fun pat_name con = (extern_name con) ^ "_pat";
fun pat_name_ con = (strip_esc con) ^ "_pat";
-(* make distinct names out of the type list,
- forbidding "o","n..","x..","f..","P.." as names *)
-(* a number string is added if necessary *)
-fun mk_var_names ids : string list =
- let
- fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
- fun index_vnames(vn::vns,occupied) =
- (case AList.lookup (op =) occupied vn of
- NONE => if vn mem vns
- then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied)
- else vn :: index_vnames(vns, occupied)
- | SOME(i) => (vn^(string_of_int (i+1)))
- :: index_vnames(vns,(vn,i+1)::occupied))
- | index_vnames([],occupied) = [];
- in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
-
fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Feb 24 14:13:15 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Feb 24 14:20:07 2010 -0800
@@ -118,6 +118,9 @@
else cut_facts_tac prems 1 :: tacsf context;
in pg'' thy defs t tacs end;
+(* FIXME!!!!!!!!! *)
+(* We should NEVER re-parse variable names as strings! *)
+(* The names can conflict with existing constants or other syntax! *)
fun case_UU_tac ctxt rews i v =
InductTacs.case_tac ctxt (v^"=UU") i THEN
asm_simp_tac (HOLCF_ss addsimps rews) i;
@@ -232,13 +235,14 @@
fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
end;
-local
+local
val iso_swap = iso_locale RS iso_iso_swap;
fun one_con (con, _, args) =
let
- val vns = map vname args;
+ val vns = Name.variant_list ["x"] (map vname args);
+ val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
val eqn = %:x_name === con_app2 con %: vns;
- val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
+ val conj = foldr1 mk_conj (eqn :: map (defined o %:) nonlazy_vns);
in Library.foldr mk_ex (vns, conj) end;
val conj_assoc = @{thm conj_assoc};
@@ -459,6 +463,7 @@
val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
fun tacs1 ctxt =
if vnn mem nlas
+ (* FIXME! case_UU_tac *)
then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
else [];
val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
@@ -468,6 +473,7 @@
let
val nlas = nonlazy args;
val goal = mk_trp (%%:sel ` con_app con args === UU);
+ (* FIXME! case_UU_tac *)
fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
@@ -625,6 +631,7 @@
val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
+ (* FIXME! case_UU_tac *)
fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
val rules = [ax_abs_iso] @ @{thms domain_map_simps};
val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
@@ -639,6 +646,7 @@
let
val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
val rews = the_list copy_strict @ copy_apps @ con_rews;
+ (* FIXME! case_UU_tac *)
fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
[asm_simp_tac (HOLCF_ss addsimps rews) 1];
in
@@ -775,11 +783,14 @@
local
fun one_con p (con, _, args) =
let
+ val P_names = map P_name (1 upto (length dnames));
+ val vns = Name.variant_list P_names (map vname args);
+ val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
val t2 = lift ind_hyp (filter is_rec args, t1);
- val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
- in Library.foldr mk_All (map vname args, t3) end;
+ val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2);
+ in Library.foldr mk_All (vns, t3) end;
fun one_eq ((p, cons), concl) =
mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
@@ -838,6 +849,7 @@
simp_tac (take_ss addsimps prems) 1,
TRY (safe_tac HOL_cs)];
fun arg_tac arg =
+ (* FIXME! case_UU_tac *)
case_UU_tac context (prems @ con_rews) 1
(List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
fun con_tacs (con, _, args) =
@@ -948,6 +960,7 @@
let
val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
fun tacs ctxt = [
+ (* FIXME! case_UU_tac *)
case_UU_tac ctxt take_rews 1 "x",
eresolve_tac finite_lemmas1a 1,
step_tac HOL_cs 1,
--- a/src/HOLCF/ex/Dnat.thy Wed Feb 24 14:13:15 2010 -0800
+++ b/src/HOLCF/ex/Dnat.thy Wed Feb 24 14:20:07 2010 -0800
@@ -62,10 +62,10 @@
apply (rule allI)
apply (rule_tac x = y in dnat.casedist)
apply (fast intro!: UU_I)
- apply (thin_tac "ALL y. d << y --> d = UU | d = y")
+ apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
apply simp
apply (simp (no_asm_simp))
- apply (drule_tac x="da" in spec)
+ apply (drule_tac x="dnata" in spec)
apply simp
done
--- a/src/HOLCF/ex/Domain_ex.thy Wed Feb 24 14:13:15 2010 -0800
+++ b/src/HOLCF/ex/Domain_ex.thy Wed Feb 24 14:20:07 2010 -0800
@@ -99,7 +99,7 @@
text {* Trivial datatypes will produce a warning message. *}
-domain triv = triv1 triv triv
+domain triv = Triv triv triv
-- "domain Domain_ex.triv is empty!"
lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
--- a/src/HOLCF/ex/Stream.thy Wed Feb 24 14:13:15 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy Wed Feb 24 14:20:07 2010 -0800
@@ -379,8 +379,8 @@
lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < Fin (Suc n))"
apply (rule stream.casedist [of x], auto)
apply (simp add: zero_inat_def)
- apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
- apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
+ apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
+ apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
done
lemma slen_take_lemma4 [rule_format]: