# HG changeset patch
# User huffman
# Date 1267050007 28800
# Node ID 2e0f9516947e3a502b65e097741ac1868beb8e2f
# Parent  992f9cb60b25cbb2ddd434a7e45e1344b8409ccc
change domain package's treatment of variable names in theorems to be like datatype package

diff -r 992f9cb60b25 -r 2e0f9516947e src/HOLCF/Tools/Domain/domain_extender.ML
--- 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';
diff -r 992f9cb60b25 -r 2e0f9516947e src/HOLCF/Tools/Domain/domain_library.ML
--- 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;
diff -r 992f9cb60b25 -r 2e0f9516947e src/HOLCF/Tools/Domain/domain_theorems.ML
--- 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,
diff -r 992f9cb60b25 -r 2e0f9516947e src/HOLCF/ex/Dnat.thy
--- 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
 
diff -r 992f9cb60b25 -r 2e0f9516947e src/HOLCF/ex/Domain_ex.thy
--- 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)
diff -r 992f9cb60b25 -r 2e0f9516947e src/HOLCF/ex/Stream.thy
--- 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]: