# HG changeset patch # User oheimb # Date 878131429 -3600 # Node ID ca44afcc259cc1273b91793339d2ee683da7b0af # Parent 22f2d1b17f9755575b527140cb538e4dec1fc5fb debugging concerning sort variables theorems are now proved immediately after generating the syntax diff -r 22f2d1b17f97 -r ca44afcc259c src/HOLCF/domain/extender.ML --- 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'); diff -r 22f2d1b17f97 -r ca44afcc259c src/HOLCF/domain/interface.ML --- 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; diff -r 22f2d1b17f97 -r ca44afcc259c src/HOLCF/domain/theorems.ML --- 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,