debugging concerning sort variables
theorems are now proved immediately after generating the syntax
--- a/src/HOLCF/domain/extender.ML Tue Oct 28 17:58:35 1997 +0100
+++ b/src/HOLCF/domain/extender.ML Wed Oct 29 14:23:49 1997 +0100
@@ -37,6 +37,9 @@
fun analyse_equation ((dname,typevars),cons') =
let
val tvars = map rep_TFree typevars;
+ fun distinct_name s = "'"^Sign.base_name dname^"_"^s;
+ val distinct_typevars = map (fn (n,sort) =>
+ TFree (distinct_name n,sort)) tvars;
fun rm_sorts (TFree(s,_)) = TFree(s,[])
| rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
| rm_sorts (TVar(s,_)) = TVar(s,[])
@@ -44,20 +47,21 @@
fun analyse(TFree(v,s)) = (case assoc_string(tvars,v) of
None => error ("Free type variable " ^ v ^ " on rhs.")
| Some sort => if eq_set_string (s,defaultS) orelse
- eq_set_string (s,sort ) then TFree(v,sort)
+ eq_set_string (s,sort )
+ then TFree(distinct_name v,sort)
else error ("Additional constraint on rhs "^
"for type variable "^quote v))
- | analyse(Type(s,typl)) = (case assoc_string (dtnvs,s) of
- None => Type(s,map analyse typl)
- | Some tvs => if remove_sorts tvs = remove_sorts typl
+ | analyse(Type(s,typl)) = if s <> dname
+ then Type(s,map analyse typl)
+ else if remove_sorts typevars = remove_sorts typl
then Type(s,map analyse typl)
else error ("Recursion of type " ^ s ^
- " with different arguments"))
+ " with different arguments")
| analyse(TVar _) = Imposs "extender:analyse";
fun check_pcpo t = (pcpo_type sg t orelse
error("Not a pcpo type: "^string_of_typ sg t); t);
val analyse_con = upd_third (map (upd_third (check_pcpo o analyse)));
- in ((dname,typevars), map analyse_con cons') end;
+ in ((dname,distinct_typevars), map analyse_con cons') end;
in ListPair.map analyse_equation (dtnvs,cons'')
end; (* let *)
@@ -86,7 +90,7 @@
list list end;
fun test_equal_type tn (cn,_,(_,rt)) = fst (rep_Type rt) = tn orelse
error("Inappropriate result type for constructor "^cn);
- val typs = ListPair.map (fn (tn, cnstrs) => (map (test_equal_type tn) cnstrs;
+ val typs = ListPair.map (fn (tn, cnstrs) =>(map (test_equal_type tn) cnstrs;
snd(third(hd(cnstrs))))) (typs',cnstrss);
val test_typs = ListPair.map (fn (typ,cnstrs) =>
if not (pcpo_type sg' typ)
@@ -99,15 +103,15 @@
fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
| occurs _ _ = false;
fun proper_arg cn atyp = forall (fn typ => let
- val tn = fst (rep_Type typ)
- in atyp=typ orelse not (occurs tn atyp) orelse
- error("Illegal use of type "^ tn ^
- " as argument of constructor " ^cn)end )typs;
+ val tn = fst (rep_Type typ)
+ in atyp=typ orelse not (occurs tn atyp) orelse
+ error("Illegal use of type "^ tn ^
+ " as argument of constructor " ^cn)end )typs;
fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
in map (map proper_curry) cnstrss end;
in (typs, flat cnstrss) end;
-(* ----- calls for building new thy and thms -------------------------------------- *)
+(* ----- calls for building new thy and thms -------------------------------- *)
in
@@ -129,13 +133,15 @@
fun cons cons' = (map (fn (con,syn,args) =>
((ThyOps.const_name con syn),
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
- find (tp,dts) handle LIST "find" => ~1),
+ find (tp,dts) handle LIST "find" => ~1),
sel,vn))
(args,(mk_var_names(map third args)))
)) cons') : cons list;
val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
- val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
- in (thy,eqs) end;
+ val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
+ val thmss = map (Domain_Theorems.theorems thy eqs) eqs;
+ val comp_thms = Domain_Theorems.comp_theorems thy (comp_dnam, eqs, thmss);
+ in (thy, thmss, comp_thms) end;
fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
val (typs,cnstrs) = check_gen_by (sign_of thy') (typs',cnstrss');
--- a/src/HOLCF/domain/interface.ML Tue Oct 28 17:58:35 1997 +0100
+++ b/src/HOLCF/domain/interface.ML Wed Oct 29 14:23:49 1997 +0100
@@ -10,7 +10,7 @@
open ThyParse;
open Domain_Library;
-(* --- generation of bindings for axioms and theorems in trailer of .thy.ML - *)
+(* --- generation of bindings for axioms and theorems in .thy.ML - *)
fun gt_ax name = "get_axiom thy " ^ quote name;
fun gen_val dname name = "val "^name^" = "^ gt_ax (dname^"_"^name)^";";
@@ -19,7 +19,7 @@
\con_rews @ sel_rews @ dis_rews @ dists_le @ dists_eq @\n\
\copy_rews";
- fun gen_domain eqname num ((dname,_), cons') = let
+ fun gen_struct thms_str num ((dname,_), cons') = let
val axioms1 = ["abs_iso", "rep_iso", "when_def"];
(* con_defs , sel_defs, dis_defs *)
val axioms2 = ["copy_def"];
@@ -35,8 +35,7 @@
gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def"))
cons')^"\n"^
cat_lines(map (gen_val dname) axioms2)^"\n"^
- "val ("^ theorems ^") =\n\
- \Domain_Theorems.theorems thy "^eqname^";\n" ^
+ "val ("^ theorems ^") = "^thms_str^";\n" ^
(if num > 1 then "val rews = " ^rews1 ^";\n" else "")
end;
@@ -59,14 +58,14 @@
val thy_ext_string = let
fun mk_conslist cons' =
- mk_list (map (fn (c,syn,ts)=>
+ mk_list (map (fn (c,syn,ts)=> "\n"^
mk_triple(quote c, syn, mk_list (map (fn (b,s ,tp) =>
mk_triple(Bool.toString b, quote s, tp)) ts))) cons');
- in "val (thy, "^comp_dname^"_equations) = thy |> Domain_Extender.add_domain \n"
- ^ mk_pair(quote comp_dname, mk_list(map (fn ((n,vs),cs) =>
+ in "val (thy, thmss, comp_thms) = thy |> Domain_Extender.add_domain "
+ ^ mk_pair(quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
mk_pair (mk_pair (quote n, mk_list vs),
mk_conslist cs)) eqs'))
- ^ ";\nval thy = thy"
+ ^ ";\n"
end;
(* ----- string for calling (comp_)theorems and producing the structures ---- *)
@@ -76,32 +75,35 @@
val comp_axioms = [(* copy, *) "reach", "take_def", "finite_def"
(*, "bisim_def" *)];
val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
- ["take_lemma","finite"]))^", finite_ind, ind, coind";
- fun eqname n = "(hd(funpow "^string_of_int n^" tl "^comp_dname^"_equations), "
- ^comp_dname^"_equations)";
+ ["take_lemma","finite"]))^", finite_ind, ind, coind";
+ fun thms_str n = "hd (funpow "^string_of_int n^" tl thmss)";
fun collect sep name = if num = 1 then name else
implode (separate sep (map (fn s => s^"."^name) dnames));
in
- implode (separate "end; (* struct *)\n\n"
- (mapn (fn n => gen_domain (eqname n) num) 0 eqs'))^(if num > 1 then
- "end; (* struct *)\n\n\
- \structure "^comp_dname^" = struct\n" else "") ^
+ implode (separate "end; (* struct *)\n"
+ (mapn (fn n => gen_struct (thms_str n) num) 0 eqs')) ^
+ (if num > 1 then "end; (* struct *)\n\n\
+ \structure "^comp_dname^" = struct\n" else "") ^
(if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
- implode ((map (fn s => gen_vall (plural s)
- (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n") comp_axioms)) ^
- gen_val comp_dname "bisim_def" ^"\n\
- \val ("^ comp_theorems ^") =\n\
- \Domain_Theorems.comp_theorems thy \
- \(" ^ quote comp_dname ^ ","^ comp_dname ^"_equations,\n\
- \ ["^collect " ," "cases" ^"],\n\
- \ "^collect "@" "con_rews " ^",\n\
- \ "^collect " @" "copy_rews" ^");\n\
- \val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ " @ take_rews;\n\
- \end; (* struct *)"
+ implode (map (fn s => gen_vall (plural s)
+ (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n")
+ comp_axioms) ^
+ gen_val comp_dname "bisim_def" ^"\n\
+ \val ("^ comp_theorems ^") = comp_thms;\n\
+ \val rews = "^(if num>1 then collect" @ " "rews"else rews1)^
+ " @ take_rews;\n\
+ \end; (* struct *)\n"
end;
- in (thy_ext_string, val_gen_string) end;
+ in ("local\n"^
+ thy_ext_string^
+ "in\n"^
+ "val thy = thy;\n"^
+ val_gen_string^
+ "end; (* local *)\n\n"^
+ "val thy = thy",
+ "") end;
-(* ----- strings for calling add_gen_by and producing the value binding ----------- *)
+(* ----- strings for calling add_gen_by and producing the value binding ----- *)
fun mk_gen_by (finite,eqs) = let
val typs = map fst eqs;
@@ -113,7 +115,7 @@
mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
"val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
-(* ----- parser for domain declaration equation ----------------------------------- *)
+(* ----- parser for domain declaration equation ----------------------------- *)
val name' = name >> strip_quotes;
val type_var' = type_var >> strip_quotes;
--- a/src/HOLCF/domain/theorems.ML Tue Oct 28 17:58:35 1997 +0100
+++ b/src/HOLCF/domain/theorems.ML Wed Oct 29 14:23:49 1997 +0100
@@ -59,16 +59,19 @@
in
-fun theorems thy (((dname,_),cons) : eq, eqs :eq list) =
+type thms = (thm list * thm * thm * thm list *
+ thm list * thm list * thm list * thm list * thm list * thm list *
+ thm list * thm list);
+fun (theorems thy: eq list -> eq -> thms) eqs ((dname,_),cons) =
let
-val dummy = writeln ("Proving isomorphism properties of domain "^dname^"...");
+val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
val pg = pg' thy;
(*
infixr 0 y;
val b = 0;
fun _ y t = by t;
-fun g defs t = let val sg = sign_of thy;
+fun g defs t = let val sg = sign_of thy;
val ct = Thm.cterm_of sg (inferT sg t);
in goalw_cterm defs ct end;
*)
@@ -328,14 +331,16 @@
end; (* let *)
-fun comp_theorems thy (comp_dnam, eqs: eq list, casess, con_rews, copy_rews) =
+fun comp_theorems thy (comp_dnam, eqs: eq list, thmss: thms list) =
let
-
+val casess = map #3 thmss;
+val con_rews = flat (map #5 thmss);
+val copy_rews = flat (map #12 thmss);
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
-val dummy = writeln("Proving induction properties of domain "^comp_dname^"...");
+val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
val pg = pg' thy;
(* ----- getting the composite axiom and definitions ------------------------ *)
@@ -361,9 +366,10 @@
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
- strict(dc_take dn $ %"n")) eqs)))([
+ strict(dc_take dn $ %"n")) eqs))) ([
+ if n_eqs = 1 then all_tac else rewtac ax_copy2_def,
nat_ind_tac "n" 1,
- simp_tac iterate_Cprod_ss 1,
+ simp_tac iterate_Cprod_ss 1,
asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
val take_stricts' = rewrite_rule copy_take_defs take_stricts;
val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0")
@@ -420,8 +426,8 @@
(lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
) o snd) cons;
fun all_rec_to ns = rec_to forall not all_rec_to ns;
- fun warn (n,cons) = if all_rec_to [] false (n,cons) then (writeln
- ("WARNING: domain "^nth_elem(n,dnames)^" is empty!"); true) else false;
+ fun warn (n,cons) = if all_rec_to [] false (n,cons) then (warning
+ ("domain "^nth_elem(n,dnames)^" is empty!"); true) else false;
fun lazy_rec_to ns = rec_to exists Id lazy_rec_to ns;
in val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
@@ -530,9 +536,9 @@
axs_reach @ [
quant_tac 1,
rtac (adm_impl_admw RS wfix_ind) 1,
- REPEAT_DETERM(rtac adm_all2 1),
- REPEAT_DETERM(TRY(rtac adm_conj 1) THEN
- rtac adm_subst 1 THEN
+ REPEAT_DETERM(rtac adm_all2 1),
+ REPEAT_DETERM(TRY(rtac adm_conj 1) THEN
+ rtac adm_subst 1 THEN
cont_tacR 1 THEN resolve_tac prems 1),
strip_tac 1,
rtac (rewrite_rule axs_take_def finite_ind) 1,