author oheimb Wed, 29 Oct 1997 14:23:49 +0100 changeset 4030 ca44afcc259c parent 4029 22f2d1b17f97 child 4031 42cbf6256d60
debugging concerning sort variables theorems are now proved immediately after generating the syntax
 src/HOLCF/domain/extender.ML file | annotate | diff | comparison | revisions src/HOLCF/domain/interface.ML file | annotate | diff | comparison | revisions src/HOLCF/domain/theorems.ML file | annotate | diff | comparison | revisions
--- 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;
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;

-(* ----- 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;

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,
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 (rewrite_rule axs_take_def finite_ind) 1,