change domain package's treatment of variable names in theorems to be like datatype package
authorhuffman
Wed Feb 24 14:20:07 2010 -0800 (2010-02-24)
changeset 354432e0f9516947e
parent 35442 992f9cb60b25
child 35444 73f645fdd4ff
change domain package's treatment of variable names in theorems to be like datatype package
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/ex/Dnat.thy
src/HOLCF/ex/Domain_ex.thy
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Feb 24 14:13:15 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Feb 24 14:20:07 2010 -0800
     1.3 @@ -154,18 +154,13 @@
     1.4      val dts  = map (Type o fst) eqs';
     1.5      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     1.6      fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
     1.7 -    fun typid (Type  (id,_)) =
     1.8 -        let val c = hd (Symbol.explode (Long_Name.base_name id))
     1.9 -        in if Symbol.is_letter c then c else "t" end
    1.10 -      | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
    1.11 -      | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
    1.12      fun one_con (con,args,mx) =
    1.13          (Binding.name_of con,  (* FIXME preverse binding (!?) *)
    1.14           mx,
    1.15           ListPair.map (fn ((lazy,sel,tp),vn) =>
    1.16             mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
    1.17                     Option.map Binding.name_of sel,vn))
    1.18 -                      (args,(mk_var_names(map (typid o third) args)))
    1.19 +                      (args, Datatype_Prop.make_tnames (map third args))
    1.20          ) : cons;
    1.21      val eqs : eq list =
    1.22          map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
    1.23 @@ -230,18 +225,13 @@
    1.24      val dts  = map (Type o fst) eqs';
    1.25      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
    1.26      fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
    1.27 -    fun typid (Type  (id,_)) =
    1.28 -        let val c = hd (Symbol.explode (Long_Name.base_name id))
    1.29 -        in if Symbol.is_letter c then c else "t" end
    1.30 -      | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
    1.31 -      | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
    1.32      fun one_con (con,args,mx) =
    1.33          (Binding.name_of con,   (* FIXME preverse binding (!?) *)
    1.34           mx,
    1.35           ListPair.map (fn ((lazy,sel,tp),vn) =>
    1.36             mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
    1.37                     Option.map Binding.name_of sel,vn))
    1.38 -                      (args,(mk_var_names(map (typid o third) args)))
    1.39 +                      (args, Datatype_Prop.make_tnames (map third args))
    1.40          ) : cons;
    1.41      val eqs : eq list =
    1.42          map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
     2.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Wed Feb 24 14:13:15 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Wed Feb 24 14:20:07 2010 -0800
     2.3 @@ -162,7 +162,6 @@
     2.4    val dis_name : string -> string;
     2.5    val mat_name : string -> string;
     2.6    val pat_name : string -> string;
     2.7 -  val mk_var_names : string list -> string list;
     2.8  end;
     2.9  
    2.10  structure Domain_Library :> DOMAIN_LIBRARY =
    2.11 @@ -191,22 +190,6 @@
    2.12  fun pat_name  con = (extern_name con) ^ "_pat";
    2.13  fun pat_name_ con = (strip_esc   con) ^ "_pat";
    2.14  
    2.15 -(* make distinct names out of the type list, 
    2.16 -                                       forbidding "o","n..","x..","f..","P.." as names *)
    2.17 -(* a number string is added if necessary *)
    2.18 -fun mk_var_names ids : string list =
    2.19 -    let
    2.20 -      fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
    2.21 -      fun index_vnames(vn::vns,occupied) =
    2.22 -          (case AList.lookup (op =) occupied vn of
    2.23 -             NONE => if vn mem vns
    2.24 -                     then (vn^"1") :: index_vnames(vns,(vn,1)  ::occupied)
    2.25 -                     else  vn      :: index_vnames(vns,          occupied)
    2.26 -           | SOME(i) => (vn^(string_of_int (i+1)))
    2.27 -                        :: index_vnames(vns,(vn,i+1)::occupied))
    2.28 -        | index_vnames([],occupied) = [];
    2.29 -    in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
    2.30 -
    2.31  fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
    2.32  fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
    2.33  fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
     3.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Feb 24 14:13:15 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Feb 24 14:20:07 2010 -0800
     3.3 @@ -118,6 +118,9 @@
     3.4        else cut_facts_tac prems 1 :: tacsf context;
     3.5    in pg'' thy defs t tacs end;
     3.6  
     3.7 +(* FIXME!!!!!!!!! *)
     3.8 +(* We should NEVER re-parse variable names as strings! *)
     3.9 +(* The names can conflict with existing constants or other syntax! *)
    3.10  fun case_UU_tac ctxt rews i v =
    3.11    InductTacs.case_tac ctxt (v^"=UU") i THEN
    3.12    asm_simp_tac (HOLCF_ss addsimps rews) i;
    3.13 @@ -232,13 +235,14 @@
    3.14    fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
    3.15  end;
    3.16  
    3.17 -local 
    3.18 +local
    3.19    val iso_swap = iso_locale RS iso_iso_swap;
    3.20    fun one_con (con, _, args) =
    3.21      let
    3.22 -      val vns = map vname args;
    3.23 +      val vns = Name.variant_list ["x"] (map vname args);
    3.24 +      val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
    3.25        val eqn = %:x_name === con_app2 con %: vns;
    3.26 -      val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
    3.27 +      val conj = foldr1 mk_conj (eqn :: map (defined o %:) nonlazy_vns);
    3.28      in Library.foldr mk_ex (vns, conj) end;
    3.29  
    3.30    val conj_assoc = @{thm conj_assoc};
    3.31 @@ -459,6 +463,7 @@
    3.32        val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
    3.33        fun tacs1 ctxt =
    3.34          if vnn mem nlas
    3.35 +                        (* FIXME! case_UU_tac *)
    3.36          then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
    3.37          else [];
    3.38        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    3.39 @@ -468,6 +473,7 @@
    3.40      let
    3.41        val nlas = nonlazy args;
    3.42        val goal = mk_trp (%%:sel ` con_app con args === UU);
    3.43 +                        (* FIXME! case_UU_tac *)
    3.44        fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
    3.45        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    3.46      in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
    3.47 @@ -625,6 +631,7 @@
    3.48        val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
    3.49        val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
    3.50        val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
    3.51 +                        (* FIXME! case_UU_tac *)
    3.52        fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
    3.53        val rules = [ax_abs_iso] @ @{thms domain_map_simps};
    3.54        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
    3.55 @@ -639,6 +646,7 @@
    3.56      let
    3.57        val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
    3.58        val rews = the_list copy_strict @ copy_apps @ con_rews;
    3.59 +                        (* FIXME! case_UU_tac *)
    3.60        fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
    3.61          [asm_simp_tac (HOLCF_ss addsimps rews) 1];
    3.62      in
    3.63 @@ -775,11 +783,14 @@
    3.64  local
    3.65    fun one_con p (con, _, args) =
    3.66      let
    3.67 +      val P_names = map P_name (1 upto (length dnames));
    3.68 +      val vns = Name.variant_list P_names (map vname args);
    3.69 +      val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
    3.70        fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
    3.71        val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
    3.72        val t2 = lift ind_hyp (filter is_rec args, t1);
    3.73 -      val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
    3.74 -    in Library.foldr mk_All (map vname args, t3) end;
    3.75 +      val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2);
    3.76 +    in Library.foldr mk_All (vns, t3) end;
    3.77  
    3.78    fun one_eq ((p, cons), concl) =
    3.79      mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
    3.80 @@ -838,6 +849,7 @@
    3.81              simp_tac (take_ss addsimps prems) 1,
    3.82              TRY (safe_tac HOL_cs)];
    3.83            fun arg_tac arg =
    3.84 +                        (* FIXME! case_UU_tac *)
    3.85              case_UU_tac context (prems @ con_rews) 1
    3.86                (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
    3.87            fun con_tacs (con, _, args) = 
    3.88 @@ -948,6 +960,7 @@
    3.89            let
    3.90              val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
    3.91              fun tacs ctxt = [
    3.92 +                        (* FIXME! case_UU_tac *)
    3.93                case_UU_tac ctxt take_rews 1 "x",
    3.94                eresolve_tac finite_lemmas1a 1,
    3.95                step_tac HOL_cs 1,
     4.1 --- a/src/HOLCF/ex/Dnat.thy	Wed Feb 24 14:13:15 2010 -0800
     4.2 +++ b/src/HOLCF/ex/Dnat.thy	Wed Feb 24 14:20:07 2010 -0800
     4.3 @@ -62,10 +62,10 @@
     4.4    apply (rule allI)
     4.5    apply (rule_tac x = y in dnat.casedist)
     4.6      apply (fast intro!: UU_I)
     4.7 -   apply (thin_tac "ALL y. d << y --> d = UU | d = y")
     4.8 +   apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
     4.9     apply simp
    4.10    apply (simp (no_asm_simp))
    4.11 -  apply (drule_tac x="da" in spec)
    4.12 +  apply (drule_tac x="dnata" in spec)
    4.13    apply simp
    4.14    done
    4.15  
     5.1 --- a/src/HOLCF/ex/Domain_ex.thy	Wed Feb 24 14:13:15 2010 -0800
     5.2 +++ b/src/HOLCF/ex/Domain_ex.thy	Wed Feb 24 14:20:07 2010 -0800
     5.3 @@ -99,7 +99,7 @@
     5.4  
     5.5  text {* Trivial datatypes will produce a warning message. *}
     5.6  
     5.7 -domain triv = triv1 triv triv
     5.8 +domain triv = Triv triv triv
     5.9    -- "domain Domain_ex.triv is empty!"
    5.10  
    5.11  lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
     6.1 --- a/src/HOLCF/ex/Stream.thy	Wed Feb 24 14:13:15 2010 -0800
     6.2 +++ b/src/HOLCF/ex/Stream.thy	Wed Feb 24 14:20:07 2010 -0800
     6.3 @@ -379,8 +379,8 @@
     6.4  lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
     6.5   apply (rule stream.casedist [of x], auto)
     6.6     apply (simp add: zero_inat_def)
     6.7 -  apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
     6.8 - apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
     6.9 +  apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
    6.10 + apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
    6.11  done
    6.12  
    6.13  lemma slen_take_lemma4 [rule_format]: