# HG changeset patch # User oheimb # Date 828552434 -7200 # Node ID b8a8ae2e5de1ff627087b2b028eee45f83302768 # Parent e18416e3e1d48ded675b0aad677a93ac9bcb8531 Updated: 01-Mar-96 when functional strictified, copy_def based on when_def diff -r e18416e3e1d4 -r b8a8ae2e5de1 src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Wed Apr 03 19:02:04 1996 +0200 +++ b/src/HOLCF/domain/axioms.ML Wed Apr 03 19:27:14 1996 +0200 @@ -1,5 +1,4 @@ (* axioms.ML - ID: $Id$ Author : David von Oheimb Created: 31-May-95 Updated: 12-Jun-95 axioms for discriminators, selectors and induction @@ -24,137 +23,129 @@ fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)= let -(* ----- axioms and definitions concerning the isomorphism ------------------------ *) +(* ----- axioms and definitions concerning the isomorphism ------------------ *) val dc_abs = %%(dname^"_abs"); val dc_rep = %%(dname^"_rep"); val x_name'= "x"; val x_name = idx_name eqs x_name' (n+1); - val ax_abs_iso = (dname^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name') === %x_name')); - val ax_rep_iso = (dname^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name') === %x_name')); + val ax_abs_iso=(dname^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name')); + val ax_rep_iso=(dname^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name')); val ax_when_def = (dname^"_when_def",%%(dname^"_when") == - foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) => - Bound(1+length cons+x-y)))`(dc_rep`Bound 0)))); + foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) => + Bound(1+length cons+x-y)))`(dc_rep`Bound 0)))); - val ax_copy_def = let - fun simp_oo (Const ("fapp", _) $ (Const ("fapp", _) $ - Const ("cfcomp", _) $ fc) $ Const ("ID", _)) = fc - | simp_oo t = t; - fun simp_app (Const ("fapp", _) $ Const ("ID", _) $ t) = t - | simp_app t = t; - fun mk_arg m n arg = (if is_lazy arg - then fn t => %%"lift"`(simp_oo (%%"up" oo t)) else Id) - (if_rec arg (cproj (Bound (2*min[n,m])) eqs) (%%"ID")); - fun mk_prod (t1,t2) = %%"ssplit"`(/\ "x" (/\ "y" (%%"spair"` - simp_app(t1`Bound 1)`simp_app(t2`Bound 0)))); - fun one_con (_,args) = if args = [] then %%"ID" else - foldr' mk_prod (mapn (mk_arg (length args-1)) 1 args); - fun mk_sum (t1,t2) = %%"sswhen"`(simp_oo (%%"sinl" oo t1)) - `(simp_oo (%%"sinr" oo t2)); - in (dname^"_copy_def", %%(dname^"_copy") == /\"f" - (dc_abs oo foldr' mk_sum (map one_con cons) oo dc_rep)) end; + fun con_def outer recu m n (_,args) = let + fun idxs z x arg = (if is_lazy arg then fn t => %%"up"`t else Id) + (if recu andalso is_rec arg then (cproj (Bound z) + (length eqs) (rec_of arg))`Bound(z-x) else Bound(z-x)); + fun parms [] = %%"one" + | parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs); + fun inj y 1 _ = y + | inj y _ 0 = %%"sinl"`y + | inj y i j = %%"sinr"`(inj y (i-1) (j-1)); + in foldr /\# (args, outer (inj (parms args) m n)) end; -(* ----- definitions concerning the constructors, discriminators and selectors ---- *) + val ax_copy_def = (dname^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo + foldl (op `) (%%(dname^"_when") , + mapn (con_def Id true (length cons)) 0 cons))); - val axs_con_def = let - fun idxs z x arg = (if is_lazy arg then fn x => %%"up"`x else Id)(Bound(z-x)); - fun prms [] = %%"one" - | prms vs = foldr' (fn(x,t)=> %%"spair"`x`t) (mapn (idxs (length vs)) 1 vs); - val injs = bin_branchr (fn l=> l@["l"]) (fn l=> l@["r"]); - fun cdef ((con,args),injs) = (extern_name con ^"_def",%%con == - foldr /\# (args,dc_abs` - (foldr (fn (i,t) => %%("sin"^i)`t ) (injs, prms args)))); - in map cdef (cons~~(mapn (fn n => K(injs [] cons n)) 0 cons)) end; +(* -- definitions concerning the constructors, discriminators and selectors - *) + + val axs_con_def = mapn (fn n => fn (con,args) => (extern_name con ^"_def", + %%con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons; val axs_dis_def = let - fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == - mk_cfapp(%%(dname^"_when"),map - (fn (con',args) => (foldr /\# - (args,if con'=con then %%"TT" else %%"FF"))) cons)) - in map ddef cons end; + fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == + mk_cfapp(%%(dname^"_when"),map + (fn (con',args) => (foldr /\# + (args,if con'=con then %%"TT" else %%"FF"))) cons)) + in map ddef cons end; val axs_sel_def = let - fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == - mk_cfapp(%%(dname^"_when"),map - (fn (con',args) => if con'<>con then %%"UU" else - foldr /\# (args,Bound (length args - n))) cons)); - in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end; + fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == + mk_cfapp(%%(dname^"_when"),map + (fn (con',args) => if con'<>con then %%"UU" else + foldr /\# (args,Bound (length args - n))) cons)); + in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end; -(* ----- axiom and definitions concerning induction ------------------------------- *) +(* ----- axiom and definitions concerning induction ------------------------- *) - fun cproj' T = cproj T eqs n; - val ax_reach = (dname^"_reach" , mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy")) - `%x_name === %x_name)); - val ax_take_def = (dname^"_take_def",%%(dname^"_take") == mk_lam("n", - cproj'(%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU"))); + fun cproj' T = cproj T (length eqs) n; + val ax_reach = (dname^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy")) + `%x_name === %x_name)); + val ax_take_def = (dname^"_take_def",%%(dname^"_take") == mk_lam("n",cproj' + (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU"))); val ax_finite_def = (dname^"_finite_def",%%(dname^"_finite") == mk_lam(x_name, - mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); + mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @ axs_con_def @ axs_dis_def @ axs_sel_def @ - [ax_reach, ax_take_def, ax_finite_def] end; + [ax_reach, ax_take_def, ax_finite_def] +end; (* let *) in (* local *) -fun add_axioms (comp_dname, eqs : eq list) thy' =let +fun add_axioms (comp_dname, eqs : eq list) thy' = let val dnames = map (fst o fst) eqs; val x_name = idx_name dnames "x"; fun copy_app dname = %%(dname^"_copy")`Bound 0; - val ax_copy_def = (comp_dname^"_copy_def" , %%(comp_dname^"_copy") == - /\"f"(foldr' cpair (map copy_app dnames))); - val ax_bisim_def = (comp_dname^"_bisim_def",%%(comp_dname^"_bisim") == mk_lam("R", + val ax_copy_def =(comp_dname^"_copy_def" , %%(comp_dname^"_copy") == + /\"f"(foldr' cpair (map copy_app dnames))); + val ax_bisim_def=(comp_dname^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R", let fun one_con (con,args) = let - val nonrec_args = filter_out is_rec args; - val rec_args = filter is_rec args; - val nonrecs_cnt = length nonrec_args; - val recs_cnt = length rec_args; - val allargs = nonrec_args @ rec_args - @ map (upd_vname (fn s=> s^"'")) rec_args; - val allvns = map vname allargs; - fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; - val vns1 = map (vname_arg "" ) args; - val vns2 = map (vname_arg "'") args; - val allargs_cnt = nonrecs_cnt + 2*recs_cnt; - val rec_idxs = (recs_cnt-1) downto 0; - val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) - (allargs~~((allargs_cnt-1) downto 0))); - fun rel_app i ra = proj (Bound(allargs_cnt+2)) dnames (rec_of ra) $ - Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); - val capps = foldr mk_conj (mapn rel_app 1 rec_args, - mk_conj(Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1), - Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2))); + val nonrec_args = filter_out is_rec args; + val rec_args = filter is_rec args; + val recs_cnt = length rec_args; + val allargs = nonrec_args @ rec_args + @ map (upd_vname (fn s=> s^"'")) rec_args; + val allvns = map vname allargs; + fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; + val vns1 = map (vname_arg "" ) args; + val vns2 = map (vname_arg "'") args; + val allargs_cnt = length nonrec_args + 2*recs_cnt; + val rec_idxs = (recs_cnt-1) downto 0; + val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) + (allargs~~((allargs_cnt-1) downto 0))); + fun rel_app i ra = proj (Bound(allargs_cnt+2)) (length eqs) (rec_of ra) $ + Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); + val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj( + Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1), + Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2))); in foldr mk_ex (allvns, foldr mk_conj - (map (defined o Bound) nonlazy_idxs,capps)) end; - fun one_comp n (_,cons) = mk_all(x_name (n+1), mk_all(x_name (n+1)^"'", mk_imp( - proj (Bound 2) dnames n $ Bound 1 $ Bound 0, - foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)::map one_con cons)))); + (map (defined o Bound) nonlazy_idxs,capps)) end; + fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp( + proj (Bound 2) (length eqs) n $ Bound 1 $ Bound 0, + foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) + ::map one_con cons)))); in foldr' mk_conj (mapn one_comp 0 eqs)end )); val thy_axs = flat (mapn (calc_axioms comp_dname eqs) 0 eqs) @ - (if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def]; + (if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def]; in thy' |> add_axioms_i (infer_types thy' thy_axs) end; -fun add_gen_by ((tname,finite),(typs,cnstrs)) thy' = let - fun pred_name typ ="P"^(if typs=[typ] then "" else string_of_int(1+find(typ,typs))); - fun lift_adm t = lift (fn typ => %%"adm" $ %(pred_name typ)) - (if finite then [] else typs,t); - fun lift_pred_UU t = lift (fn typ => %(pred_name typ) $ UU) (typs,t); +fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let + fun P_name typ = "P"^(if typs = [typ] then "" + else string_of_int(1 + find(typ,typs))); + fun lift_adm t = lift (fn typ => %%"adm" $ %(P_name typ)) + (if finite then [] else typs,t); + fun lift_pred_UU t = lift (fn typ => %(P_name typ) $ UU) (typs,t); fun one_cnstr (cnstr,vns,(args,res)) = let - val rec_args = filter (fn (_,typ) => typ mem typs)(vns~~args); - val app = mk_cfapp(%%cnstr,map (bound_arg vns) vns); - in foldr mk_All (vns, - lift (fn (vn,typ) => %(pred_name typ) $ bound_arg vns vn) - (rec_args,defined app ==> %(pred_name res)$app)) end; - fun one_conc typ = let val pn = pred_name typ in - %pn $ %("x"^implode(tl(explode pn))) end; + val rec_args = filter (fn (_,typ) => typ mem typs)(vns~~args); + val app = mk_cfapp(%%cnstr,map (bound_arg vns) vns); + in foldr mk_All (vns, + lift (fn (vn,typ) => %(P_name typ) $ bound_arg vns vn) + (rec_args,defined app ==> %(P_name res)$app)) end; + fun one_conc typ = let val pn = P_name typ + in %pn $ %("x"^implode(tl(explode pn))) end; val concl = mk_trp(foldr' mk_conj (map one_conc typs)); - val induct =(tname^"_induct",lift_adm(lift_pred_UU( - foldr (op ===>) (map one_cnstr cnstrs,concl)))); + val induct = (tname^"_induct",lift_adm(lift_pred_UU( + foldr (op ===>) (map one_cnstr cnstrs,concl)))); in thy' |> add_axioms_i (infer_types thy' [induct]) end; end; (* local *) diff -r e18416e3e1d4 -r b8a8ae2e5de1 src/HOLCF/domain/extender.ML --- a/src/HOLCF/domain/extender.ML Wed Apr 03 19:02:04 1996 +0200 +++ b/src/HOLCF/domain/extender.ML Wed Apr 03 19:27:14 1996 +0200 @@ -1,5 +1,4 @@ (* extender.ML - ID: $Id$ Author : David von Oheimb Created: 17-May-95 Updated: 31-May-95 extracted syntax.ML, theorems.ML @@ -10,7 +9,7 @@ *) -structure Extender = +structure Domain_Extender = struct local @@ -20,78 +19,77 @@ (* ----- general testing and preprocessing of constructor list -------------------- *) fun check_domain(eqs':((string * typ list) * - (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let + (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let val dtnvs = map fst eqs'; val cons' = flat (map snd eqs'); val test_dupl_typs = (case duplicates (map fst dtnvs) of - [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); + [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); val test_dupl_cons = (case duplicates (map first cons') of - [] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups)); + [] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups)); val test_dupl_sels = (case duplicates(map second (flat(map third cons'))) of [] => false | dups => error ("Duplicate selectors: "^commas_quote dups)); val test_dupl_tvars = let fun vname (TFree(v,_)) = v - | vname _ = Imposs "extender:vname"; - in exists (fn tvars => case duplicates (map vname tvars) of - [] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups)) - (map snd dtnvs) end; + | vname _ = Imposs "extender:vname"; + in exists (fn tvars => case duplicates (map vname tvars) of + [] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups)) + (map snd dtnvs) end; (*test for free type variables and invalid use of recursive type*) val analyse_types = forall (fn ((_,typevars),cons') => - forall (fn con' => let - val types = map third (third con'); + forall (fn con' => let + val types = map third (third con'); fun analyse(t as TFree(v,_)) = t mem typevars orelse - error ("Free type variable " ^ v ^ " on rhs.") - | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl - | Some tvs => tvs = typl orelse - error ("Recursion of type " ^ s ^ " with different arguments")) - | analyse(TVar _) = Imposs "extender:analyse" - and analyses ts = forall analyse ts; - in analyses types end) cons' - ) eqs'; + error ("Free type variable " ^ v ^ " on rhs.") + | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl + | Some tvs => tvs = typl orelse + error ("Recursion of type " ^ s ^ " with different arguments")) + | analyse(TVar _) = Imposs "extender:analyse" + and analyses ts = forall analyse ts; + in analyses types end) cons' + ) eqs'; in true end; (* let *) fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let val test_dupl_typs = (case duplicates typs' of [] => false - | dups => error ("Duplicate types: " ^ commas_quote dups)); + | dups => error ("Duplicate types: " ^ commas_quote dups)); val test_dupl_cnstrs = map (fn cnstrs' => (case duplicates cnstrs' of [] => false - | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss'; + | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss'; val tsig = #tsig(Sign.rep_sg(sign_of thy')); val tycons = map fst (#tycons(Type.rep_tsig tsig)); val test_types = forall(fn t=>t mem tycons orelse error("Unknown type: "^t))typs'; val cnstrss = let - fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t - | None => error ("Unknown constructor: "^c); - fun args_result_type (t as (Type(tn,[arg,rest]))) = - if tn = "->" orelse tn = "=>" - then let val (ts,r) = args_result_type rest in (arg::ts,r) end - else ([],t) - | args_result_type t = ([],t); + fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t + | None => error ("Unknown constructor: "^c); + fun args_result_type (t as (Type(tn,[arg,rest]))) = + if tn = "->" orelse tn = "=>" + then let val (ts,r) = args_result_type rest in (arg::ts,r) end + else ([],t) + | args_result_type t = ([],t); in map (map (fn cn => let val (args,res) = args_result_type (type_of cn) in - (cn,mk_var_names args,(args,res)) end)) cnstrss' - : (string * (* operator name of constr *) - string list * (* argument name list *) - (typ list * (* argument types *) - typ)) (* result type *) - list list end; + (cn,mk_var_names args,(args,res)) end)) cnstrss' + : (string * (* operator name of constr *) + string list * (* argument name list *) + (typ list * (* argument types *) + typ)) (* result type *) + list list end; fun test_equal_type tn (cn,_,(_,rt)) = fst (type_name_vars rt) = tn orelse - error("Inappropriate result type for constructor "^cn); - val typs = map (fn (tn, cnstrs) => - (map (test_equal_type tn) cnstrs; snd(third(hd(cnstrs))))) - (typs'~~cnstrss); + error("Inappropriate result type for constructor "^cn); + val typs = map (fn (tn, cnstrs) => (map (test_equal_type tn) cnstrs; + snd(third(hd(cnstrs))))) (typs'~~cnstrss); val test_typs = map (fn (typ,cnstrs) => - if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"]))) - then error("Not a pcpo type: "^fst(type_name_vars typ)) - else map (fn (cn,_,(_,rt)) => rt=typ - orelse error("Non-identical result types for constructors "^ - first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss); + if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"]))) + then error("Not a pcpo type: "^fst(type_name_vars typ)) + else map (fn (cn,_,(_,rt)) => rt=typ + orelse error("Non-identical result types for constructors "^ + first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss); val proper_args = let - 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(type_name_vars 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; + 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(type_name_vars 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; @@ -100,16 +98,16 @@ in fun add_domain (comp_dname,eqs') thy'' = let - val ok_dummy = check_domain eqs'; + val ok = check_domain eqs'; val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs'); val dts = map (Type o fst) eqs'; fun cons cons' = (map (fn (con,syn,args) => - (ThyOps.const_name con syn, - map (fn ((lazy,sel,tp),vn) => ((lazy, - find (tp,dts) handle LIST "find" => ~1), - sel,vn)) - (args~~(mk_var_names(map third args))) - )) cons') : cons list; + (ThyOps.const_name con syn, + map (fn ((lazy,sel,tp),vn) => ((lazy, + 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_dname,eqs); in (thy,eqs) end; @@ -117,7 +115,7 @@ fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let val (typs,cnstrs) = check_gen_by thy' (typs',cnstrss'); in - Domain_Axioms.add_gen_by ((tname,finite),(typs,cnstrs)) thy' end; + Domain_Axioms.add_induct ((tname,finite),(typs,cnstrs)) thy' end; end (* local *) end (* struct *) diff -r e18416e3e1d4 -r b8a8ae2e5de1 src/HOLCF/domain/interface.ML --- a/src/HOLCF/domain/interface.ML Wed Apr 03 19:02:04 1996 +0200 +++ b/src/HOLCF/domain/interface.ML Wed Apr 03 19:27:14 1996 +0200 @@ -1,6 +1,5 @@ (* interface.ML - ID: $Id$ - Author: David von Oheimb + Author: David von Oheimb Created: 17-May-95 Updated: 24-May-95 Updated: 03-Jun-95 incremental change of ThySyn @@ -11,39 +10,38 @@ Copyright 1995 TU Muenchen *) -local +structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData !!!!!! *) -structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData!!!!!!! *) struct local 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 trailer of .thy.ML - *) - fun gt_ax name = "get_axiom thy "^quote name; - fun gen_val dname name = "val "^name^" = " ^gt_ax (dname^"_"^name)^";"; - fun gen_vall name l = "val "^name^" = " ^mk_list l^";"; + fun gt_ax name = "get_axiom thy " ^ quote name; + fun gen_val dname name = "val "^name^" = "^ gt_ax (dname^"_"^name)^";"; + fun gen_vall name l = "val "^name^" = "^ mk_list l^";"; val rews1 = "iso_rews @ when_rews @\n\ - \con_rews @ sel_rews @ dis_rews @ dists_eq @ dists_le @\n\ - \copy_rews"; + \con_rews @ sel_rews @ dis_rews @ dists_le @ dists_eq @\n\ + \copy_rews"; fun gen_domain eqname num ((dname,_), cons') = let val axioms1 = ["abs_iso", "rep_iso", "when_def"]; - (* con_defs , sel_defs, dis_defs *) + (* con_defs , sel_defs, dis_defs *) val axioms2 = ["copy_def"]; val theorems = - "iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n \ - \dists_eq, dists_le, inverts, injects, copy_rews"; + "iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n \ + \dists_le, dists_eq, inverts, injects, copy_rews"; in "structure "^dname^" = struct\n"^ cat_lines(map (gen_val dname) axioms1)^"\n"^ gen_vall"con_defs"(map(fn (con,_,_) => gt_ax(strip_esc con^"_def")) cons')^"\n"^ gen_vall"sel_defs"(flat(map (fn (_,_,args) => map (fn (_,sel,_) => - gt_ax(sel^"_def")) args) cons'))^"\n"^ + gt_ax(sel^"_def")) args) cons'))^"\n"^ gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def")) - cons')^"\n"^ + cons')^"\n"^ cat_lines(map (gen_val dname) axioms2)^"\n"^ "val ("^ theorems ^") =\n\ \Domain_Theorems.theorems thy "^eqname^";\n" ^ @@ -57,117 +55,112 @@ val comp_dname = implode (separate "_" dnames); val conss' = map (fn (dname,cons'') => let - fun sel n m = upd_second (fn None => dname^"_sel_"^(string_of_int n)^ - "_"^(string_of_int m) - | Some s => s) - fun fill_sels n con = upd_third (mapn (sel n) 1) con; + fun sel n m = upd_second (fn None => dname^"_sel_"^(string_of_int n)^ + "_"^(string_of_int m) + | Some s => s) + fun fill_sels n con = upd_third (mapn (sel n) 1) con; in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs'')); val eqs' = dtnvs~~conss'; -(* ----- generation of argument string for calling add_domain --------------------- *) - - - fun string_of_sort_emb [] = "" - | string_of_sort_emb [x] = "\"" ^x^ "\"" - | string_of_sort_emb (x::xs) = "\"" ^x^ "\"" ^ ", "^(string_of_sort_emb xs); - - fun string_of_sort l = "["^ (string_of_sort_emb l)^"]"; +(* ----- string for calling add_domain -------------------------------------- *) - fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v)) - and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,string_of_sort sort) - | mk_typ (Type (name,args)) = "Type" ^mk_tnv(name,args) - | mk_typ _ = Imposs "interface:mk_typ"; - fun mk_conslist cons' = mk_list (map - (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list - (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s, - mk_typ tp)) ts))) cons'); + val thy_ext_string = let + fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v)) + and mk_typ (TFree(name,sort))= "TFree"^mk_pair(quote name, + mk_list(map quote sort)) + | mk_typ (Type (name,args))= "Type" ^mk_tnv(name,args) + | mk_typ _ = Imposs "interface:mk_typ"; + fun mk_conslist cons' = mk_list (map + (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list + (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s, + mk_typ tp)) ts))) cons'); + in "val (thy, "^comp_dname^"_equations) = thy |> Domain_Extender.add_domain \n" + ^ mk_pair(quote comp_dname, + mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs')) + ^ ";\nval thy = thy" + end; + +(* ----- string for calling (comp_)theorems and producing the structures ---------- *) + + val val_gen_string = let + fun plural s = if num > 1 then s^"s" else "["^s^"]"; + 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)"; + fun collect sep name = if num = 1 then name else + implode (separate sep (map (fn s => s^"."^name) dnames)); in - ("val (thy, "^comp_dname^"_equations) = thy |> Extender.add_domain \n" - ^ mk_pair(quote comp_dname, - mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs')) - ^ ";\nval thy = thy", - let - fun plural s = if num > 1 then s^"s" else "["^s^"]"; - val comp_axioms = [(* copy, *) "take_def", "finite_def", "reach" - (*, "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)"; - 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 "") ^ - (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\ + 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 "") ^ + (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 *)" - end - ) end; + \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 *)" + end; + in (thy_ext_string, val_gen_string) end; + +(* ----- strings for calling add_gen_by and producing the value binding ----------- *) fun mk_gen_by (finite,eqs) = let val typs = map fst eqs; val cnstrss = map snd eqs; val tname = implode (separate "_" typs) in - ("|> Extender.add_gen_by " - ^ mk_pair(mk_pair(quote tname,makestring (finite:bool)), - mk_pair(mk_list(map quote typs), - mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))), - "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end; + ("|> Domain_Extender.add_gen_by " + ^ mk_pair(mk_pair(quote tname,makestring (finite:bool)), + mk_pair(mk_list(map quote typs), + mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))), + "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end; (* ----- parser for domain declaration equation ----------------------------------- *) (** val sort = name >> (fn s => [strip_quotes s]) - || "{" $$-- !! (list (name >> strip_quotes) --$$ "}"); + || "{" $$-- !! (list (name >> strip_quotes) --$$ "}"); val tvar = (type_var -- (optional ("::" $$-- !! sort) ["pcpo"])) >> TFree **) val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"])); val type_args = "(" $$-- !! (list1 tvar --$$ ")") - || tvar >> (fn x => [x]) - || empty >> K []; + || tvar >> (fn x => [x]) + || empty >> K []; val con_typ = type_args -- ident >> (fn (x,y) => Type(y,x)); val typ = con_typ - || tvar; + || tvar; val domain_arg = "(" $$-- (optional ($$ "lazy" >> K true) false) - -- (optional ((ident >> Some) --$$ "::") None) - -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp)) - || ident >> (fn x => (false,None,Type(x,[]))) - || tvar >> (fn x => (false,None,x)); + -- (optional ((ident >> Some) --$$ "::") None) + -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp)) + || ident >> (fn x => (false,None,Type(x,[]))) + || tvar >> (fn x => (false,None,x)); val domain_cons = (name >> strip_quotes) -- !! (repeat domain_arg) - -- ThyOps.opt_cmixfix - >> (fn ((con,args),syn) => (con,syn,args)); + -- ThyOps.opt_cmixfix + >> (fn ((con,args),syn) => (con,syn,args)); in val domain_decl = (enum1 "," (con_typ --$$ "=" -- !! - (enum1 "|" domain_cons))) >> mk_domain; + (enum1 "|" domain_cons))) >> mk_domain; val gen_by_decl = (optional ($$ "finite" >> K true) false) -- - (enum1 "," (ident --$$ "by" -- !! - (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by; -end; + (enum1 "," (ident --$$ "by" -- !! + (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by; +end; (* local *) val user_keywords = "lazy"::"by"::"finite":: - (**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**) - ThySynData.user_keywords; + (**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**) + ThySynData.user_keywords; val user_sections = ("domain", domain_decl)::("generated", gen_by_decl):: - (**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**) - ThySynData.user_sections; -end; - -in + (**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**) + ThySynData.user_sections; +end; (* struct *) structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *) - -end; (* local *) - diff -r e18416e3e1d4 -r b8a8ae2e5de1 src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Wed Apr 03 19:02:04 1996 +0200 +++ b/src/HOLCF/domain/library.ML Wed Apr 03 19:27:14 1996 +0200 @@ -1,26 +1,25 @@ (* library.ML - ID: $Id$ - Author: David von Oheimb + Author : David von Oheimb Created: 18-Jul-95 extracted from syntax.ML, axioms.ML, extender.ML, interface.ML Updated: 30-Aug-95 + Updated: 20-Oct-95 small improvement for atomize Copyright 1995 TU Muenchen *) -(* ----- general support ---------------------------------------------------------- *) +(* ----- general support ---------------------------------------------------- *) fun Id x = x; fun mapn f n [] = [] | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; -fun foldr'' f (l,f2) = - let fun itr [] = raise LIST "foldr''" - | itr [a] = f2 a - | itr (a::l) = f(a, itr l) - in itr l end; +fun foldr'' f (l,f2) = let fun itr [] = raise LIST "foldr''" + | itr [a] = f2 a + | itr (a::l) = f(a, itr l) +in itr l end; fun foldr' f l = foldr'' f (l,Id); -fun map_cumulr f start xs = foldr (fn (x,(ys,res)) => case f(x,res) of (y,res2) => - (y::ys,res2)) (xs,([],start)); +fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => + (y::ys,res2)) (xs,([],start)); fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; @@ -28,21 +27,14 @@ fun upd_second f (x,y,z) = ( x, f y, z); fun upd_third f (x,y,z) = ( x, y, f z); -(* fn : ('a -> 'a) -> ('a -> 'a) -> 'a -> 'b list -> int -> 'a *) -fun bin_branchr f1 f2 y is j = let -fun bb y 1 _ = y -| bb y _ 0 = f1 y -| bb y i j = if i=2 then (f2 y) else bb (f2 y) (i-1) (j-1) -in bb y (length is) j end; +fun atomize thm = let val r_inst = read_instantiate; + fun at thm = case concl_of thm of + _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) + | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec)) + | _ => [thm]; +in map zero_var_indexes (at thm) end; -fun atomize thm = case concl_of thm of - _ $ (Const("op &",_) $ _ $ _) => atomize (thm RS conjunct1) @ - atomize (thm RS conjunct2) - | _ $ (Const("All" ,_) $ Abs (s,_,_)) => atomize (thm RS - (read_instantiate [("x","?"^s)] spec)) - | _ => [thm]; - -(* ----- specific support for domain ---------------------------------------------- *) +(* ----- specific support for domain ---------------------------------------- *) structure Domain_Library = struct @@ -51,29 +43,28 @@ (* ----- name handling ----- *) -val strip_esc = let - fun strip ("'" :: c :: cs) = c :: strip cs - | strip ["'"] = [] - | strip (c :: cs) = c :: strip cs - | strip [] = []; +val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs + | strip ["'"] = [] + | strip (c :: cs) = c :: strip cs + | strip [] = []; in implode o strip o explode end; fun extern_name con = case explode con of - ("o"::"p"::" "::rest) => implode rest - | _ => con; + ("o"::"p"::" "::rest) => implode rest + | _ => con; fun dis_name con = "is_"^ (extern_name con); fun dis_name_ con = "is_"^ (strip_esc con); -(*make distinct names out of the type list, - forbidding "o", "x..","f..","P.." as names *) -(*a number string is added if necessary *) +(* make distinct names out of the type list, + forbidding "o", "x..","f..","P.." as names *) +(* a number string is added if necessary *) fun mk_var_names types : string list = let fun typid (Type (id,_) ) = hd (explode id) | typid (TFree (id,_) ) = hd (tl (explode id)) | typid (TVar ((id,_),_)) = hd (tl (explode id)); fun nonreserved id = let val cs = explode id in - if not(hd cs mem ["x","f","P"]) then id - else implode(chr(1+ord (hd cs))::tl cs) end; + if not(hd cs mem ["x","f","P"]) then id + else implode(chr(1+ord (hd cs))::tl cs) end; fun index_vnames(vn::vns,tab) = (case assoc(tab,vn) of None => if vn mem vns @@ -86,24 +77,16 @@ fun type_name_vars (Type(name,typevars)) = (name,typevars) | type_name_vars _ = Imposs "library:type_name_vars"; -(* ----- support for type and mixfix expressions ----- *) - -fun mk_tvar s = TFree("'"^s,["pcpo"]); -fun mk_typ t (S,T) = Type(t,[S,T]); -infixr 5 -->; -infixr 6 ~>; val op ~> = mk_typ "->"; -val NoSyn' = ThyOps.Mixfix NoSyn; - (* ----- constructor list handling ----- *) -type cons = (string * (* operator name of constr *) - ((bool*int)* (* (lazy,recursive element or ~1) *) - string* (* selector name *) - string) (* argument name *) - list); (* argument list *) -type eq = (string * (* name of abstracted type *) - typ list) * (* arguments of abstracted type *) - cons list; (* represented type, as a constructor list *) +type cons = (string * (* operator name of constr *) + ((bool*int)* (* (lazy,recursive element or ~1) *) + string* (* selector name *) + string) (* argument name *) + list); (* argument list *) +type eq = (string * (* name of abstracted type *) + typ list) * (* arguments of abstracted type *) + cons list; (* represented type, as a constructor list *) val rec_of = snd o first; val is_lazy = fst o first; @@ -112,9 +95,16 @@ val upd_vname = upd_third; fun is_rec arg = rec_of arg >=0; fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); -fun nonlazy args = map vname (filter_out is_lazy args); -fun is_one_con_one_arg p cons = length cons = 1 andalso let val args = snd(hd cons) in - length args = 1 andalso p (hd args) end; +fun nonlazy args = map vname (filter_out is_lazy args); +fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); + +(* ----- support for type and mixfix expressions ----- *) + +fun mk_tvar s = TFree("'"^s,["pcpo"]); +fun mk_typ t (S,T) = Type(t,[S,T]); +infixr 5 -->; +infixr 6 ~>; val op ~> = mk_typ "->"; +val NoSyn' = ThyOps.Mixfix NoSyn; (* ----- support for term expressions ----- *) @@ -130,26 +120,26 @@ fun mk_lam (x,T) = Abs(x,dummyT,T); fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); local - fun tf (Type (s,args)) = foldl (op $) (%s,map tf args) - | tf (TFree(s,_ )) = %s - | tf _ = Imposs "mk_constrainall"; + fun tf (Type (s,args)) = foldl (op $) (%s,map tf args) + | tf (TFree(s,_ )) = %s + | tf _ = Imposs "mk_constrainall"; in fun mk_constrain (typ,T) = %%"_constrain" $ T $ tf typ; -fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs"$Abs(x,dummyT,P)$tf typ); +fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs" $ mk_lam(x,P) $ tf typ); end; - + fun mk_ex (x,P) = mk_exists (x,dummyT,P); fun mk_not P = Const("not" ,boolT --> boolT) $ P; end; fun mk_All (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *) -infixr 0 ===>;fun S ===> T = Const("==>", dummyT) $ S $ T; +infixr 0 ===>;fun S ===> T = %%"==>" $ S $ T; infixr 0 ==>;fun S ==> T = mk_trp S ===> mk_trp T; -infix 0 ==; fun S == T = Const("==", dummyT) $ S $ T; -infix 1 ===; fun S === T = Const("op =", dummyT) $ S $ T; +infix 0 ==; fun S == T = %%"==" $ S $ T; +infix 1 ===; fun S === T = %%"op =" $ S $ T; infix 1 ~=; fun S ~= T = mk_not (S === T); -infix 1 <<; fun S << T = Const("op <<", dummyT) $ S $ T; +infix 1 <<; fun S << T = %%"op <<" $ S $ T; infix 1 ~<<; fun S ~<< T = mk_not (S << T); infix 9 ` ; fun f` x = %%"fapp" $ f $ x; @@ -160,8 +150,11 @@ fun con_app con = con_app2 con %#; fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg); -val cproj = bin_branchr (fn S => %%"cfst"`S) (fn S => %%"csnd"`S); -val proj = bin_branchr (fn S => %%"fst" $S) (fn S => %%"snd" $S); +fun prj _ _ y 1 _ = y +| prj f1 _ y _ 0 = f1 y +| prj f1 f2 y i j = prj f1 f2 (f2 y) (i-1) (j-1); +val cproj = prj (fn S => %%"cfst"`S) (fn S => %%"csnd"`S); +val proj = prj (fn S => %%"fst" $S) (fn S => %%"snd" $S); fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); fun /\ v T = %%"fabs" $ mk_lam(v,T); @@ -177,26 +170,27 @@ fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = (case cont_eta_contract body of body' as (Const("fapp",Ta) $ f $ Bound 0) => - if not (0 mem loose_bnos f) then incr_boundvars ~1 f - else Const("fabs",TT) $ Abs(a,T,body') + if not (0 mem loose_bnos f) then incr_boundvars ~1 f + else Const("fabs",TT) $ Abs(a,T,body') | body' => Const("fabs",TT) $ Abs(a,T,body')) | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t | cont_eta_contract t = t; -fun idx_name dnames s n = s ^ (if length dnames = 1 then "" else string_of_int n); +fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); fun when_funs cons = if length cons = 1 then ["f"] - else mapn (fn n => K("f"^(string_of_int n))) 1 cons; + else mapn (fn n => K("f"^(string_of_int n))) 1 cons; fun when_body cons funarg = let - fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) - | one_fun n (_,args) = let - val l2 = length args; - fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x - else Id) (Bound(l2-m)); - in cont_eta_contract (foldr'' - (fn (a,t) => %%"ssplit"`(/\# (a,t))) - (args, - fn a => /\# (a,(mk_cfapp(funarg (l2,n),mapn idxs 1 args)))) - ) end; -in foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons) end; - + fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) + | one_fun n (_,args) = let + val l2 = length args; + fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x + else Id) (Bound(l2-m)); + in cont_eta_contract (foldr'' + (fn (a,t) => %%"ssplit"`(/\# (a,t))) + (args, + fn a=> /\#(a,(mk_cfapp(funarg(l2,n),mapn idxs 1 args)))) + ) end; +in (if length cons = 1 andalso length(snd(hd cons)) <= 1 + then fn t => %%"strictify"`t else Id) + (foldr' (fn (x,y)=> %%"sswhen"`x`y) (mapn one_fun 1 cons)) end; end; (* struct *) diff -r e18416e3e1d4 -r b8a8ae2e5de1 src/HOLCF/domain/syntax.ML --- a/src/HOLCF/domain/syntax.ML Wed Apr 03 19:02:04 1996 +0200 +++ b/src/HOLCF/domain/syntax.ML Wed Apr 03 19:27:14 1996 +0200 @@ -1,5 +1,4 @@ (* syntax.ML - ID: $Id$ Author: David von Oheimb Created: 31-May-95 Updated: 16-Aug-95 case translation @@ -14,21 +13,24 @@ open Domain_Library; infixr 5 -->; infixr 6 ~>; -fun calc_syntax dtypeprod ((dname,typevars), - (cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))= +fun calc_syntax dtypeprod ((dname, typevars), (cons': + (string * ThyOps.cmixfix * (bool*string*typ) list) list)) = let (* ----- constants concerning the isomorphism ------------------------------------- *) local fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t - fun prod (_,_,args) = if args = [] then Type("one",[]) - else foldr' (mk_typ "**") (map opt_lazy args); - + fun prod (_,_,args) = if args = [] then Type("one",[]) + else foldr'(mk_typ "**") (map opt_lazy args); + fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s; + fun when_type (_ ,_,args) = foldr (op ~>) (map third args,freetvar "t"); in val dtype = Type(dname,typevars); val dtype2 = foldr' (mk_typ "++") (map prod cons'); val const_rep = (dname^"_rep" , dtype ~> dtype2, NoSyn'); val const_abs = (dname^"_abs" , dtype2 ~> dtype , NoSyn'); + val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'), + dtype ~> freetvar "t"), NoSyn'); val const_copy = (dname^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn'); end; @@ -42,20 +44,16 @@ local val escape = let - fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs - else c :: esc cs - | esc [] = [] - in implode o esc o explode end; - fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s; - fun when_type (_ ,_,args) = foldr (op ~>) (map third args,freetvar "t"); + fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs + else c :: esc cs + | esc [] = [] + in implode o esc o explode end; fun con (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s); fun dis (con ,s,_ ) = (dis_name_ con, dtype~>Type("tr",[]), - ThyOps.Mixfix(Mixfix("is'_"^ - (if is_infix s then Id else escape)con,[],max_pri))); + ThyOps.Mixfix(Mixfix("is'_"^ + (if is_infix s then Id else escape)con,[],max_pri))); fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args; in - val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'), - dtype ~> freetvar "t"), NoSyn'); val consts_con = map con cons'; val consts_dis = map dis cons'; val consts_sel = flat(map sel cons'); @@ -63,32 +61,32 @@ (* ----- constants concerning induction ------------------------------------------- *) - val const_take = (dname^"_take" ,Type("nat",[]) --> dtype ~> dtype ,NoSyn'); - val const_finite = (dname^"_finite",dtype-->HOLogic.boolT ,NoSyn'); + val const_take = (dname^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn'); + val const_finite = (dname^"_finite", dtype-->HOLogic.boolT , NoSyn'); (* ----- case translation --------------------------------------------------------- *) local open Syntax in val case_trans = let - fun c_ast con syn = Constant (ThyOps.const_name con syn); - fun expvar n = Variable ("e"^(string_of_int n)); - fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^(string_of_int m)); - fun app s (l,r) = mk_appl (Constant s) [l,r]; - fun case1 n (con,syn,args) = mk_appl (Constant "@case1") - [if is_infix syn - then mk_appl (c_ast con syn) (mapn (argvar n) 1 args) - else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)), - expvar n]; - fun arg1 n (con,_,args) = if args = [] then expvar n - else mk_appl (Constant "LAM ") - [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n]; + fun c_ast con syn = Constant (ThyOps.const_name con syn); + fun expvar n = Variable ("e"^(string_of_int n)); + fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^(string_of_int m)); + fun app s (l,r) = mk_appl (Constant s) [l,r]; + fun case1 n (con,syn,args) = mk_appl (Constant "@case1") + [if is_infix syn + then mk_appl (c_ast con syn) (mapn (argvar n) 1 args) + else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)), + expvar n]; + fun arg1 n (con,_,args) = if args = [] then expvar n + else mk_appl (Constant "LAM ") + [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n]; in mk_appl (Constant "@case") [Variable "x", foldr' - (fn (c,cs) => mk_appl (Constant "@case2") [c,cs]) - (mapn case1 1 cons')] <-> + (fn (c,cs) => mk_appl (Constant "@case2") [c,cs]) + (mapn case1 1 cons')] <-> mk_appl (Constant "@fapp") [foldl - (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ]) - (Constant (dname^"_when"),mapn arg1 1 cons'), - Variable "x"] + (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ]) + (Constant (dname^"_when"),mapn arg1 1 cons'), + Variable "x"] end; end; @@ -103,11 +101,10 @@ in (* local *) fun add_syntax (comp_dname,eqs': ((string * typ list) * - (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = + (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = let fun thy_type (dname,typevars) = (dname, length typevars, NoSyn); fun thy_arity (dname,typevars) = (dname, map (K ["pcpo"]) typevars, ["pcpo"]); - (** (fn TFree(_,sort) => sort | _ => Imposs "syntax:thy_arities")**) val thy_types = map (thy_type o fst) eqs'; val thy_arities = map (thy_arity o fst) eqs'; val dtypes = map (Type o fst) eqs'; @@ -118,10 +115,10 @@ val ctt = map (calc_syntax funprod) eqs'; val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false}; in thy'' |> add_types thy_types - |> add_arities thy_arities - |> add_cur_ops_i (flat(map fst ctt)) - |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim]) - |> add_trrules_i (flat(map snd ctt)) + |> add_arities thy_arities + |> add_cur_ops_i (flat(map fst ctt)) + |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim]) + |> add_trrules_i (flat(map snd ctt)) end; (* let *) end; (* local *) diff -r e18416e3e1d4 -r b8a8ae2e5de1 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Wed Apr 03 19:02:04 1996 +0200 +++ b/src/HOLCF/domain/theorems.ML Wed Apr 03 19:27:14 1996 +0200 @@ -1,5 +1,4 @@ (* theorems.ML - ID: $Id$ Author : David von Oheimb Created: 06-Jun-95 Updated: 08-Jun-95 first proof from cterms @@ -12,10 +11,12 @@ Updated: 05-Sep-95 simultaneous domain equations (main part) Updated: 11-Sep-95 simultaneous domain equations (coding finished) Updated: 13-Sep-95 simultaneous domain equations (debugging) - Copyright 1995 TU Muenchen + Updated: 26-Oct-95 debugging and enhancement of proofs for take_apps, ind + Updated: 16-Feb-96 bug concerning domain Triv = triv fixed + Updated: 01-Mar-96 when functional strictified, copy_def based on when_def + Copyright 1995, 1996 TU Muenchen *) - structure Domain_Theorems = struct local @@ -25,58 +26,58 @@ infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; -(* ----- general proof facilities ------------------------------------------------- *) - -fun inferT sg pre_tm = #2(Sign.infer_types sg (K None)(K None)[]true([pre_tm],propT)); +(* ----- general proof facilities ------------------------------------------- *) -(* -infix 0 y; -val b=0; -fun _ y t = by t; -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; -*) +fun inferT sg pre_tm = #2 (Sign.infer_types sg (K None) (K None) [] true + ([pre_tm],propT)); fun pg'' thy defs t = let val sg = sign_of thy; - val ct = Thm.cterm_of sg (inferT sg t); - in prove_goalw_cterm defs ct end; + val ct = Thm.cterm_of sg (inferT sg t); + in prove_goalw_cterm defs ct end; fun pg' thy defs t tacsf=pg'' thy defs t (fn [] => tacsf - | prems=> (cut_facts_tac prems 1)::tacsf); + | prems=> (cut_facts_tac prems 1)::tacsf); fun REPEAT_DETERM_UNTIL p tac = let fun drep st = if p st then Sequence.single st - else (case Sequence.pull(tac st) of - None => Sequence.null - | Some(st',_) => drep st') -in drep end; + else (case Sequence.pull(tapply(tac,st)) of + None => Sequence.null + | Some(st',_) => drep st') +in Tactic drep end; val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1); -local val trueI2 = prove_goal HOL.thy "f~=x ==> True" (fn prems => [rtac TrueI 1]) in +local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in val kill_neq_tac = dtac trueI2 end; -fun case_UU_tac rews i v = res_inst_tac [("Q",v^"=UU")] classical2 i THEN - asm_simp_tac (HOLCF_ss addsimps rews) i; +fun case_UU_tac rews i v = res_inst_tac [("Q",v^"=UU")] classical2 i THEN + asm_simp_tac (HOLCF_ss addsimps rews) i; val chain_tac = REPEAT_DETERM o resolve_tac - [is_chain_iterate, ch2ch_fappR, ch2ch_fappL]; + [is_chain_iterate, ch2ch_fappR, ch2ch_fappL]; + +(* ----- general proofs ----------------------------------------------------- *) -(* ----- general proofs ----------------------------------------------------------- *) +val quant_ss = HOL_ss addsimps (map (fn s => prove_goal HOL.thy s (fn _ =>[ + fast_tac HOL_cs 1]))["(Âx. P x À Q)=((Âx. P x) À Q)", + "(Âx. P À Q x) = (P À (Âx. Q x))"]); + +val all2E = prove_goal HOL.thy "Ë Âx y . P x y; P x y êë R Ì êë R" (fn prems =>[ + resolve_tac prems 1, + cut_facts_tac prems 1, + fast_tac HOL_cs 1]); val swap3 = prove_goal HOL.thy "[| Q ==> P; ~P |] ==> ~Q" (fn prems => [ cut_facts_tac prems 1, etac swap 1, dtac notnotD 1, - etac (hd prems) 1]); + etac (hd prems) 1]); -val dist_eqI = prove_goal Porder0.thy "~ x << y ==> x ~= y" (fn prems => [ - cut_facts_tac prems 1, - etac swap 1, - dtac notnotD 1, - asm_simp_tac HOLCF_ss 1]); -val cfst_strict = prove_goal Cprod3.thy "cfst`UU = UU" (fn _ => [ - (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]); -val csnd_strict = prove_goal Cprod3.thy "csnd`UU = UU" (fn _ => [ - (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]); +val dist_eqI = prove_goal Porder.thy "¿ x Ý y êë x Û y" (fn prems => [ + rtac swap3 1, + etac (antisym_less_inverse RS conjunct1) 1, + resolve_tac prems 1]); +val cfst_strict = prove_goal Cprod3.thy "cfst`Ø = Ø" (fn _ => [ + (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]); +val csnd_strict = prove_goal Cprod3.thy "csnd`Ø = Ø" (fn _ => [ + (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]); in @@ -86,8 +87,17 @@ 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; + val ct = Thm.cterm_of sg (inferT sg t); + in goalw_cterm defs ct end; +*) -(* ----- getting the axioms and definitions --------------------------------------- *) + +(* ----- getting the axioms and definitions --------------------------------- *) local val ga = get_axiom thy in val ax_abs_iso = ga (dname^"_abs_iso" ); @@ -96,11 +106,11 @@ val axs_con_def = map (fn (con,_) => ga (extern_name con ^"_def")) cons; val axs_dis_def = map (fn (con,_) => ga ( dis_name con ^"_def")) cons; val axs_sel_def = flat(map (fn (_,args) => - map (fn arg => ga (sel_of arg ^"_def")) args) cons); + map (fn arg => ga (sel_of arg ^"_def")) args)cons); val ax_copy_def = ga (dname^"_copy_def" ); end; (* local *) -(* ----- theorems concerning the isomorphism -------------------------------------- *) +(* ----- theorems concerning the isomorphism -------------------------------- *) val dc_abs = %%(dname^"_abs"); val dc_rep = %%(dname^"_rep"); @@ -108,251 +118,243 @@ val x_name = "x"; val (rep_strict, abs_strict) = let - val r = ax_rep_iso RS (ax_abs_iso RS (allI RSN(2,allI RS iso_strict))) - in (r RS conjunct1, r RS conjunct2) end; + val r = ax_rep_iso RS (ax_abs_iso RS (allI RSN(2,allI RS iso_strict))) + in (r RS conjunct1, r RS conjunct2) end; val abs_defin' = pg [] ((dc_abs`%x_name === UU) ==> (%x_name === UU)) [ - res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1, - etac ssubst 1, - rtac rep_strict 1]; + res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1, + etac ssubst 1, rtac rep_strict 1]; val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%x_name === UU)) [ - res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1, - etac ssubst 1, - rtac abs_strict 1]; + res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1, + etac ssubst 1, rtac abs_strict 1]; val iso_rews = [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict]; local val iso_swap = pg [] (dc_rep`%"x" === %"y" ==> %"x" === dc_abs`%"y") [ - dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1, - etac (ax_rep_iso RS subst) 1]; + dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1, + etac (ax_rep_iso RS subst) 1]; fun exh foldr1 cn quant foldr2 var = let fun one_con (con,args) = let val vns = map vname args in foldr quant (vns, foldr2 ((%x_name === con_app2 con (var vns) vns):: - map (defined o (var vns)) (nonlazy args))) end + map (defined o (var vns)) (nonlazy args))) end in foldr1 ((cn(%x_name===UU))::map one_con cons) end; in val cases = let - fun common_tac thm = rtac thm 1 THEN contr_tac 1; - fun unit_tac true = common_tac liftE1 - | unit_tac _ = all_tac; - fun prod_tac [] = common_tac oneE - | prod_tac [arg] = unit_tac (is_lazy arg) - | prod_tac (arg::args) = - common_tac sprodE THEN - kill_neq_tac 1 THEN - unit_tac (is_lazy arg) THEN - prod_tac args; - fun sum_one_tac p = SELECT_GOAL(EVERY[ - rtac p 1, - rewrite_goals_tac axs_con_def, - dtac iso_swap 1, - simp_tac HOLCF_ss 1, - UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1; - fun sum_tac [(_,args)] [p] = - prod_tac args THEN sum_one_tac p - | sum_tac ((_,args)::cons') (p::prems) = DETERM( - common_tac ssumE THEN - kill_neq_tac 1 THEN kill_neq_tac 2 THEN - prod_tac args THEN sum_one_tac p) THEN - sum_tac cons' prems - | sum_tac _ _ = Imposs "theorems:sum_tac"; - in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P"))) - (fn T => T ==> %"P") mk_All - (fn l => foldr (op ===>) (map mk_trp l,mk_trp(%"P"))) - bound_arg) - (fn prems => [ - cut_facts_tac [excluded_middle] 1, - etac disjE 1, - rtac (hd prems) 2, - etac rep_defin' 2, - if is_one_con_one_arg (not o is_lazy) cons - then rtac (hd (tl prems)) 1 THEN atac 2 THEN - rewrite_goals_tac axs_con_def THEN - simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1 - else sum_tac cons (tl prems)])end; -val exhaust = pg [] (mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %))) [ - rtac cases 1, - UNTIL_SOLVED(fast_tac HOL_cs 1)]; + fun common_tac thm = rtac thm 1 THEN contr_tac 1; + fun unit_tac true = common_tac liftE1 + | unit_tac _ = all_tac; + fun prod_tac [] = common_tac oneE + | prod_tac [arg] = unit_tac (is_lazy arg) + | prod_tac (arg::args) = + common_tac sprodE THEN + kill_neq_tac 1 THEN + unit_tac (is_lazy arg) THEN + prod_tac args; + fun sum_rest_tac p = SELECT_GOAL(EVERY[ + rtac p 1, + rewrite_goals_tac axs_con_def, + dtac iso_swap 1, + simp_tac HOLCF_ss 1, + UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1; + fun sum_tac [(_,args)] [p] = + prod_tac args THEN sum_rest_tac p + | sum_tac ((_,args)::cons') (p::prems) = DETERM( + common_tac ssumE THEN + kill_neq_tac 1 THEN kill_neq_tac 2 THEN + prod_tac args THEN sum_rest_tac p) THEN + sum_tac cons' prems + | sum_tac _ _ = Imposs "theorems:sum_tac"; + in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P"))) + (fn T => T ==> %"P") mk_All + (fn l => foldr (op ===>) (map mk_trp l, + mk_trp(%"P"))) + bound_arg) + (fn prems => [ + cut_facts_tac [excluded_middle] 1, + etac disjE 1, + rtac (hd prems) 2, + etac rep_defin' 2, + if length cons = 1 andalso + length (snd(hd cons)) = 1 andalso + not(is_lazy(hd(snd(hd cons)))) + then rtac (hd (tl prems)) 1 THEN atac 2 THEN + rewrite_goals_tac axs_con_def THEN + simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1 + else sum_tac cons (tl prems)])end; +val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[ + rtac cases 1, + UNTIL_SOLVED(fast_tac HOL_cs 1)]; end; local -val when_app = foldl (op `) (%%(dname^"_when"), map % (when_funs cons)); -val when_appl = pg [ax_when_def] (mk_trp(when_app`%x_name===when_body cons - (fn (_,n) => %(nth_elem(n-1,when_funs cons)))`(dc_rep`%x_name))) [ - simp_tac HOLCF_ss 1]; + val when_app = foldl (op `) (%%(dname^"_when"), map % (when_funs cons)); + val when_appl = pg [ax_when_def] (mk_trp(when_app`%x_name===when_body cons + (fn (_,n)=> %(nth_elem(n-1,when_funs cons)))`(dc_rep`%x_name)))[ + simp_tac HOLCF_ss 1]; in -val when_strict = pg [] ((if is_one_con_one_arg (K true) cons - then fn t => mk_trp(strict(%"f")) ===> t else Id)(mk_trp(strict when_app))) [ - simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1]; -val when_apps = let fun one_when n (con,args) = pg axs_con_def - (lift_defined % (nonlazy args, mk_trp(when_app`(con_app con args) === - mk_cfapp(%(nth_elem(n,when_funs cons)),map %# args))))[ - asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1]; - in mapn one_when 0 cons end; +val when_strict = pg [] (mk_trp(strict when_app)) [ + simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1]; +val when_apps = let fun one_when n (con,args) = pg axs_con_def (lift_defined % + (nonlazy args, mk_trp(when_app`(con_app con args) === + mk_cfapp(%(nth_elem(n,when_funs cons)),map %# args))))[ + asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1]; + in mapn one_when 0 cons end; end; val when_rews = when_strict::when_apps; -(* ----- theorems concerning the constructors, discriminators and selectors ------- *) +(* ----- theorems concerning the constructors, discriminators and selectors - *) -val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp( - (if is_one_con_one_arg (K true) cons then mk_not else Id) - (strict(%%(dis_name con))))) [ - simp_tac (HOLCF_ss addsimps (if is_one_con_one_arg (K true) cons - then [ax_when_def] else when_rews)) 1]) cons; -val dis_apps = let fun one_dis c (con,args)= pg (axs_dis_def) - (lift_defined % (nonlazy args, (*(if is_one_con_one_arg is_lazy cons - then curry (lift_defined %#) args else Id) -#################*) - (mk_trp((%%(dis_name c))`(con_app con args) === - %%(if con=c then "TT" else "FF"))))) [ - asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in flat(map (fn (c,_) => map (one_dis c) cons) cons) end; -val dis_defins = map (fn (con,args) => pg [] (defined(%x_name)==> - defined(%%(dis_name con)`%x_name)) [ - rtac cases 1, - contr_tac 1, - UNTIL_SOLVED (CHANGED(asm_simp_tac - (HOLCF_ss addsimps dis_apps) 1))]) cons; -val dis_rews = dis_stricts @ dis_defins @ dis_apps; +val dis_rews = let + val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp( + strict(%%(dis_name con)))) [ + simp_tac (HOLCF_ss addsimps when_rews) 1]) cons; + val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def + (lift_defined % (nonlazy args, + (mk_trp((%%(dis_name c))`(con_app con args) === + %%(if con=c then "TT" else "FF"))))) [ + asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in flat(map (fn (c,_) => map (one_dis c) cons) cons) end; + val dis_defins = map (fn (con,args) => pg [] (defined(%x_name) ==> + defined(%%(dis_name con)`%x_name)) [ + rtac cases 1, + contr_tac 1, + UNTIL_SOLVED (CHANGED(asm_simp_tac + (HOLCF_ss addsimps dis_apps) 1))]) cons; +in dis_stricts @ dis_defins @ dis_apps end; val con_stricts = flat(map (fn (con,args) => map (fn vn => - pg (axs_con_def) - (mk_trp(con_app2 con (fn arg => if vname arg = vn - then UU else %# arg) args === UU))[ - asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1] - ) (nonlazy args)) cons); + pg (axs_con_def) + (mk_trp(con_app2 con (fn arg => if vname arg = vn + then UU else %# arg) args === UU))[ + asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1] + ) (nonlazy args)) cons); val con_defins = map (fn (con,args) => pg [] - (lift_defined % (nonlazy args, - mk_trp(defined(con_app con args)))) ([ - rtac swap3 1] @ (if is_one_con_one_arg (K true) cons - then [ - if is_lazy (hd args) then rtac defined_up 2 - else atac 2, - rtac abs_defin' 1, - asm_full_simp_tac (HOLCF_ss addsimps axs_con_def) 1] - else [ - eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1, - asm_simp_tac (HOLCF_ss addsimps dis_rews) 1])))cons; + (lift_defined % (nonlazy args, + mk_trp(defined(con_app con args)))) ([ + rtac swap3 1, + eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1, + asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons; val con_rews = con_stricts @ con_defins; val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%sel))) [ - simp_tac (HOLCF_ss addsimps when_rews) 1]; -in flat(map (fn (_,args) => map (fn arg => one_sel (sel_of arg)) args) cons) end; + simp_tac (HOLCF_ss addsimps when_rews) 1]; +in flat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end; val sel_apps = let fun one_sel c n sel = map (fn (con,args) => - let val nlas = nonlazy args; - val vns = map vname args; - in pg axs_sel_def (lift_defined % - (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas, - mk_trp((%%sel)`(con_app con args) === (if con=c then %(nth_elem(n,vns)) else UU)))) - ( (if con=c then [] - else map(case_UU_tac(when_rews@con_stricts)1) nlas) - @(if con=c andalso ((nth_elem(n,vns)) mem nlas) - then[case_UU_tac (when_rews @ con_stricts) 1 - (nth_elem(n,vns))] else []) - @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons; + let val nlas = nonlazy args; + val vns = map vname args; + in pg axs_sel_def (lift_defined % + (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas, + mk_trp((%%sel)`(con_app con args) === + (if con=c then %(nth_elem(n,vns)) else UU)))) + ( (if con=c then [] + else map(case_UU_tac(when_rews@con_stricts)1) nlas) + @(if con=c andalso ((nth_elem(n,vns)) mem nlas) + then[case_UU_tac (when_rews @ con_stricts) 1 + (nth_elem(n,vns))] else []) + @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons; in flat(map (fn (c,args) => - flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end; -val sel_defins = if length cons = 1 then map (fn arg => pg [] (defined(%x_name) ==> - defined(%%(sel_of arg)`%x_name)) [ - rtac cases 1, - contr_tac 1, - UNTIL_SOLVED (CHANGED(asm_simp_tac - (HOLCF_ss addsimps sel_apps) 1))]) - (filter_out is_lazy (snd(hd cons))) else []; + flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end; +val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%x_name)==> + defined(%%(sel_of arg)`%x_name)) [ + rtac cases 1, + contr_tac 1, + UNTIL_SOLVED (CHANGED(asm_simp_tac + (HOLCF_ss addsimps sel_apps) 1))]) + (filter_out is_lazy (snd(hd cons))) else []; val sel_rews = sel_stricts @ sel_defins @ sel_apps; val distincts_le = let fun dist (con1, args1) (con2, args2) = pg [] - (lift_defined % ((nonlazy args1), - (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([ - rtac swap3 1, - eres_inst_tac [("fo5",dis_name con1)] monofun_cfun_arg 1] - @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2) - @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]); + (lift_defined % ((nonlazy args1), + (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([ + rtac swap3 1, + eres_inst_tac[("fo5",dis_name con1)] monofun_cfun_arg 1] + @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2) + @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]); fun distinct (con1,args1) (con2,args2) = - let val arg1 = (con1, args1); - val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg) - (args2~~variantlist(map vname args2,map vname args1)))); - in [dist arg1 arg2, dist arg2 arg1] end; + let val arg1 = (con1, args1); + val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg) + (args2~~variantlist(map vname args2,map vname args1)))); + in [dist arg1 arg2, dist arg2 arg1] end; fun distincts [] = [] | distincts (c::cs) = (map (distinct c) cs) :: distincts cs; in distincts cons end; val dists_le = flat (flat distincts_le); val dists_eq = let fun distinct (_,args1) ((_,args2),leqs) = let - val (le1,le2) = (hd leqs, hd(tl leqs)); - val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in - if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else - if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else - [eq1, eq2] end; + val (le1,le2) = (hd leqs, hd(tl leqs)); + val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in + if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else + if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else + [eq1, eq2] end; fun distincts [] = [] | distincts ((c,leqs)::cs) = flat(map (distinct c) ((map fst cs)~~leqs)) @ - distincts cs; + distincts cs; in distincts (cons~~distincts_le) end; local fun pgterm rel con args = let - fun append s = upd_vname(fn v => v^s); - val (largs,rargs) = (args, map (append "'") args); - in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===> - lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs), - mk_trp (foldr' mk_conj - (map rel (map %# largs ~~ map %# rargs)))))) end; + fun append s = upd_vname(fn v => v^s); + val (largs,rargs) = (args, map (append "'") args); + in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===> + lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs), + mk_trp (foldr' mk_conj + (map rel (map %# largs ~~ map %# rargs)))))) end; val cons' = filter (fn (_,args) => args<>[]) cons; in val inverts = map (fn (con,args) => - pgterm (op <<) con args (flat(map (fn arg => [ - TRY(rtac conjI 1), - dres_inst_tac [("fo5",sel_of arg)] monofun_cfun_arg 1, - asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1] - ) args))) cons'; + pgterm (op <<) con args (flat(map (fn arg => [ + TRY(rtac conjI 1), + dres_inst_tac [("fo5",sel_of arg)] monofun_cfun_arg 1, + asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1] + ) args))) cons'; val injects = map (fn ((con,args),inv_thm) => - pgterm (op ===) con args [ - etac (antisym_less_inverse RS conjE) 1, - dtac inv_thm 1, REPEAT(atac 1), - dtac inv_thm 1, REPEAT(atac 1), - TRY(safe_tac HOL_cs), - REPEAT(rtac antisym_less 1 ORELSE atac 1)] ) - (cons'~~inverts); + pgterm (op ===) con args [ + etac (antisym_less_inverse RS conjE) 1, + dtac inv_thm 1, REPEAT(atac 1), + dtac inv_thm 1, REPEAT(atac 1), + TRY(safe_tac HOL_cs), + REPEAT(rtac antisym_less 1 ORELSE atac 1)] ) + (cons'~~inverts); end; -(* ----- theorems concerning one induction step ----------------------------------- *) +(* ----- theorems concerning one induction step ----------------------------- *) -val copy_strict = pg [ax_copy_def] ((if is_one_con_one_arg (K true) cons then fn t => - mk_trp(strict(cproj (%"f") eqs (rec_of (hd(snd(hd cons)))))) ===> t - else Id) (mk_trp(strict(dc_copy`%"f")))) [ - asm_simp_tac(HOLCF_ss addsimps [abs_strict,rep_strict, - cfst_strict,csnd_strict]) 1]; -val copy_apps = map (fn (con,args) => pg (ax_copy_def::axs_con_def) - (lift_defined %# (filter is_nonlazy_rec args, - mk_trp(dc_copy`%"f"`(con_app con args) === - (con_app2 con (app_rec_arg (cproj (%"f") eqs)) args)))) - (map (case_UU_tac [ax_abs_iso] 1 o vname) - (filter(fn a=>not(is_rec a orelse is_lazy a))args)@ - [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1]) - )cons; -val copy_stricts = map(fn(con,args)=>pg[](mk_trp(dc_copy`UU`(con_app con args) ===UU)) - (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews - in map (case_UU_tac rews 1) (nonlazy args) @ [ - asm_simp_tac (HOLCF_ss addsimps rews) 1] end)) - (filter (fn (_,args)=>exists is_nonlazy_rec args) cons); +val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [ + asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict, + cfst_strict,csnd_strict]) 1]; +val copy_apps = map (fn (con,args) => pg [ax_copy_def] + (lift_defined % (nonlazy_rec args, + mk_trp(dc_copy`%"f"`(con_app con args) === + (con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args)))) + (map (case_UU_tac (abs_strict::when_strict::con_stricts) + 1 o vname) + (filter (fn a => not (is_rec a orelse is_lazy a)) args) + @[asm_simp_tac (HOLCF_ss addsimps when_apps) 1, + simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons; +val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU` + (con_app con args) ===UU)) + (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews + in map (case_UU_tac rews 1) (nonlazy args) @ [ + asm_simp_tac (HOLCF_ss addsimps rews) 1] end)) + (filter (fn (_,args)=>exists is_nonlazy_rec args) cons); val copy_rews = copy_strict::copy_apps @ copy_stricts; in (iso_rews, exhaust, cases, when_rews, - con_rews, sel_rews, dis_rews, dists_eq, dists_le, inverts, injects, - copy_rews) + con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects, + copy_rews) end; (* let *) fun comp_theorems thy (comp_dname, eqs: eq list, casess, con_rews, copy_rews) = let -val dummy = writeln ("Proving induction properties of domain "^comp_dname^"..."); +val dummy = writeln("Proving induction properties of domain "^comp_dname^"..."); val pg = pg' thy; val dnames = map (fst o fst) eqs; val conss = map snd eqs; -(* ----- getting the composite axiom and definitions ------------------------------ *) +(* ----- getting the composite axiom and definitions ------------------------ *) local val ga = get_axiom thy in val axs_reach = map (fn dn => ga (dn ^ "_reach" )) dnames; @@ -362,230 +364,235 @@ val ax_bisim_def = ga (comp_dname^"_bisim_def"); end; (* local *) -(* ----- theorems concerning finiteness and induction ----------------------------- *) - fun dc_take dn = %%(dn^"_take"); val x_name = idx_name dnames "x"; val P_name = idx_name dnames "P"; +val n_eqs = length eqs; + +(* ----- theorems concerning finite approximation and finite induction ------ *) local - val iterate_ss = simpset_of "Fix"; - val iterate_Cprod_strict_ss = iterate_ss addsimps [cfst_strict, csnd_strict]; - val iterate_Cprod_ss = iterate_ss addsimps [cfst2,csnd2,csplit2]; + val iterate_Cprod_ss = simpset_of "Fix" + addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews; val copy_con_rews = copy_rews @ con_rews; - val copy_take_defs = (if length dnames=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),_)=> - (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([ - nat_ind_tac "n" 1, - simp_tac iterate_ss 1, - simp_tac iterate_Cprod_strict_ss 1, - asm_simp_tac iterate_Cprod_ss 1, - TRY(safe_tac HOL_cs)] @ - map(K(asm_simp_tac (HOL_ss addsimps copy_rews)1))dnames); + 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),_)=> + (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([ + nat_ind_tac "n" 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") - `%x_name n === UU))[ - simp_tac iterate_Cprod_strict_ss 1]) 1 dnames; + val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0") + `%x_name n === UU))[ + simp_tac iterate_Cprod_ss 1]) 1 dnames; + val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1; val take_apps = pg copy_take_defs (mk_trp(foldr' mk_conj - (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all - (map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) === - con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n")) - args)) cons) eqs)))) ([ - nat_ind_tac "n" 1, - simp_tac iterate_Cprod_strict_ss 1, - simp_tac (HOLCF_ss addsimps copy_con_rews) 1, - TRY(safe_tac HOL_cs)] @ - (flat(map (fn ((dn,_),cons) => map (fn (con,args) => EVERY ( - asm_full_simp_tac iterate_Cprod_ss 1:: - map (case_UU_tac (take_stricts'::copy_con_rews) 1) - (nonlazy args) @[ - asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1]) - ) cons) eqs))); + (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all + (map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) === + con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n")) + args)) cons) eqs)))) ([ + simp_tac iterate_Cprod_ss 1, + nat_ind_tac "n" 1, + simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1, + asm_full_simp_tac (HOLCF_ss addsimps + (filter (has_fewer_prems 1) copy_rews)) 1, + TRY(safe_tac HOL_cs)] @ + (flat(map (fn ((dn,_),cons) => map (fn (con,args) => + if nonlazy_rec args = [] then all_tac else + EVERY(map c_UU_tac (nonlazy_rec args)) THEN + asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1 + ) cons) eqs))); in val take_rews = atomize take_stricts @ take_0s @ atomize take_apps; end; (* local *) -val take_lemmas = mapn (fn n => fn(dn,ax_reach) => pg'' thy axs_take_def (mk_All("n", - mk_trp(dc_take dn $ Bound 0 `%(x_name n) === - dc_take dn $ Bound 0 `%(x_name n^"'"))) - ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [ - res_inst_tac[("t",x_name n )](ax_reach RS subst) 1, - res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1, - rtac (fix_def2 RS ssubst) 1, - REPEAT(CHANGED(rtac (contlub_cfun_arg RS ssubst) 1 - THEN chain_tac 1)), - rtac (contlub_cfun_fun RS ssubst) 1, - rtac (contlub_cfun_fun RS ssubst) 2, - rtac lub_equal 3, - chain_tac 1, - rtac allI 1, - resolve_tac prems 1])) 1 (dnames~~axs_reach); - local fun one_con p (con,args) = foldr mk_All (map vname args, - lift_defined (bound_arg (map vname args)) (nonlazy args, - lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg) - (filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args)))); + lift_defined (bound_arg (map vname args)) (nonlazy args, + lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg) + (filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args)))); fun one_eq ((p,cons),concl) = (mk_trp(%p $ UU) ===> - foldr (op ===>) (map (one_con p) cons,concl)); - fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x)) 1 conss, - mk_trp(foldr' mk_conj (mapn (fn n => concf (P_name n,x_name n)) 1 dnames))); + foldr (op ===>) (map (one_con p) cons,concl)); + fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss, + mk_trp(foldr' mk_conj (mapn concf 1 dnames))); val take_ss = HOL_ss addsimps take_rews; - fun ind_tacs tacsf thms1 thms2 prems = TRY(safe_tac HOL_cs):: - flat (mapn (fn n => fn (thm1,thm2) => - tacsf (n,prems) (thm1,thm2) @ - flat (map (fn cons => - (resolve_tac prems 1 :: - flat (map (fn (_,args) => - resolve_tac prems 1:: - map (K(atac 1)) (nonlazy args) @ - map (K(atac 1)) (filter is_rec args)) - cons))) - conss)) - 0 (thms1~~thms2)); + fun quant_tac i = EVERY(mapn(fn n=> fn _=> res_inst_tac[("x",x_name n)]spec i) + 1 dnames); + fun ind_prems_tac prems = EVERY(flat (map (fn cons => ( + resolve_tac prems 1 :: + flat (map (fn (_,args) => + resolve_tac prems 1 :: + map (K(atac 1)) (nonlazy args) @ + map (K(atac 1)) (filter is_rec args)) + cons))) conss)); local - fun all_rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => - is_rec arg andalso not(rec_of arg mem ns) andalso - ((rec_of arg = n andalso not(lazy_rec orelse is_lazy arg)) orelse - rec_of arg <> n andalso all_rec_to (rec_of arg::ns) - (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss)))) - ) o snd) cons; - 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 lazy_rec_to ns lazy_rec (n,cons) = exists (exists (fn arg => - is_rec arg andalso not(rec_of arg mem ns) andalso - ((rec_of arg = n andalso (lazy_rec orelse is_lazy arg)) orelse - rec_of arg <> n andalso lazy_rec_to (rec_of arg::ns) - (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss)))) - ) o snd) cons; - in val is_emptys = map warn (mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs); - val is_finite = forall (not o lazy_rec_to [] false) - (mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs) + (* check whether every/exists constructor of the n-th part of the equation: + it has a possibly indirectly recursive argument that isn't/is possibly + indirectly lazy *) + fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => + is_rec arg andalso not(rec_of arg mem ns) andalso + ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse + rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) + (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 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; + val is_emptys = map warn n__eqs; + val is_finite = forall (not o lazy_rec_to [] false) n__eqs; end; -in -val finite_ind = pg'' thy [] (ind_term (fn (P,x) => fn dn => - mk_all(x,%P $ (dc_take dn $ %"n" `Bound 0)))) (fn prems=> [ - nat_ind_tac "n" 1, - simp_tac (take_ss addsimps prems) 1, - TRY(safe_tac HOL_cs)] - @ flat(mapn (fn n => fn (cons,cases) => [ - res_inst_tac [("x",x_name n)] cases 1, - asm_simp_tac (take_ss addsimps prems) 1] - @ flat(map (fn (con,args) => - asm_simp_tac take_ss 1 :: - map (fn arg => - case_UU_tac (prems@con_rews) 1 ( - nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg)) - (filter is_nonlazy_rec args) @ [ - resolve_tac prems 1] @ - map (K (atac 1)) (nonlazy args) @ - map (K (etac spec 1)) (filter is_rec args)) - cons)) - 1 (conss~~casess))); +in (* local *) +val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %(P_name n)$ + (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [ + quant_tac 1, + simp_tac quant_ss 1, + nat_ind_tac "n" 1, + simp_tac (take_ss addsimps prems) 1, + TRY(safe_tac HOL_cs)] + @ flat(map (fn (cons,cases) => [ + res_inst_tac [("x","x")] cases 1, + asm_simp_tac (take_ss addsimps prems) 1] + @ flat(map (fn (con,args) => + asm_simp_tac take_ss 1 :: + map (fn arg => + case_UU_tac (prems@con_rews) 1 ( + nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg)) + (filter is_nonlazy_rec args) @ [ + resolve_tac prems 1] @ + map (K (atac 1)) (nonlazy args) @ + map (K (etac spec 1)) (filter is_rec args)) + cons)) + (conss~~casess))); + +val take_lemmas =mapn(fn n=> fn(dn,ax_reach)=> pg'' thy axs_take_def(mk_All("n", + mk_trp(dc_take dn $ Bound 0 `%(x_name n) === + dc_take dn $ Bound 0 `%(x_name n^"'"))) + ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [ + res_inst_tac[("t",x_name n )](ax_reach RS subst) 1, + res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1, + rtac (fix_def2 RS ssubst) 1, + REPEAT(CHANGED(rtac(contlub_cfun_arg RS ssubst)1 + THEN chain_tac 1)), + rtac (contlub_cfun_fun RS ssubst) 1, + rtac (contlub_cfun_fun RS ssubst) 2, + rtac lub_equal 3, + chain_tac 1, + rtac allI 1, + resolve_tac prems 1])) 1 (dnames~~axs_reach); + +(* ----- theorems concerning finiteness and induction ----------------------- *) val (finites,ind) = if is_finite then -let - fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x"); - val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===> - mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU), - take_enough dn)) ===> mk_trp(take_enough dn)) [ - etac disjE 1, - etac notE 1, - resolve_tac take_lemmas 1, - asm_simp_tac take_ss 1, - atac 1]) dnames; - val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn - (fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args), - mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU, - dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([ - rtac allI 1, - nat_ind_tac "n" 1, - simp_tac take_ss 1, - TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @ - flat(mapn (fn n => fn (cons,cases) => [ - simp_tac take_ss 1, - rtac allI 1, - res_inst_tac [("x",x_name n)] cases 1, - asm_simp_tac take_ss 1] @ - flat(map (fn (con,args) => - asm_simp_tac take_ss 1 :: - flat(map (fn arg => [ - eres_inst_tac [("x",vname arg)] all_dupE 1, - etac disjE 1, - asm_simp_tac (HOL_ss addsimps con_rews) 1, - asm_simp_tac take_ss 1]) - (filter is_nonlazy_rec args))) - cons)) - 1 (conss~~casess))) handle ERROR => raise ERROR; - val all_finite=map (fn(dn,l1b)=>pg axs_finite_def (mk_trp(%%(dn^"_finite") $ %"x"))[ - case_UU_tac take_rews 1 "x", - eresolve_tac finite_lemmas1a 1, - step_tac HOL_cs 1, - step_tac HOL_cs 1, - cut_facts_tac [l1b] 1, - fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b); -in -(all_finite, - pg'' thy [] (ind_term (fn (P,x) => fn dn => %P $ %x)) - (ind_tacs (fn _ => fn (all_fin,finite_ind) => [ - rtac (rewrite_rule axs_finite_def all_fin RS exE) 1, - etac subst 1, - rtac finite_ind 1]) all_finite (atomize finite_ind)) + let + fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x"); + val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===> + mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU), + take_enough dn)) ===> mk_trp(take_enough dn)) [ + etac disjE 1, + etac notE 1, + resolve_tac take_lemmas 1, + asm_simp_tac take_ss 1, + atac 1]) dnames; + val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn + (fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args), + mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU, + dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([ + rtac allI 1, + nat_ind_tac "n" 1, + simp_tac take_ss 1, + TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @ + flat(mapn (fn n => fn (cons,cases) => [ + simp_tac take_ss 1, + rtac allI 1, + res_inst_tac [("x",x_name n)] cases 1, + asm_simp_tac take_ss 1] @ + flat(map (fn (con,args) => + asm_simp_tac take_ss 1 :: + flat(map (fn vn => [ + eres_inst_tac [("x",vn)] all_dupE 1, + etac disjE 1, + asm_simp_tac (HOL_ss addsimps con_rews) 1, + asm_simp_tac take_ss 1]) + (nonlazy_rec args))) + cons)) + 1 (conss~~casess))) handle ERROR => raise ERROR; + val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp( + %%(dn^"_finite") $ %"x"))[ + case_UU_tac take_rews 1 "x", + eresolve_tac finite_lemmas1a 1, + step_tac HOL_cs 1, + step_tac HOL_cs 1, + cut_facts_tac [l1b] 1, + fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b); + in + (finites, + pg'' thy[](ind_term (fn n => fn dn => %(P_name n) $ %(x_name n)))(fn prems => + TRY(safe_tac HOL_cs) :: + flat (map (fn (finite,fin_ind) => [ + rtac(rewrite_rule axs_finite_def finite RS exE)1, + etac subst 1, + rtac fin_ind 1, + ind_prems_tac prems]) + (finites~~(atomize finite_ind)) )) ) end (* let *) else -(mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) - [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames, - pg'' thy [] (foldr (op ===>) (mapn (fn n =>K(mk_trp(%%"adm" $ %(P_name n))))1 - dnames,ind_term (fn(P,x)=>fn dn=> %P $ %x))) - (ind_tacs (fn (n,prems) => fn (ax_reach,finite_ind) =>[ - rtac (ax_reach RS subst) 1, - res_inst_tac [("x",x_name n)] spec 1, - rtac wfix_ind 1, - rtac adm_impl_admw 1, - resolve_tac adm_thms 1, - rtac adm_subst 1, - cont_tacR 1, - resolve_tac prems 1, - strip_tac 1, - rtac(rewrite_rule axs_take_def finite_ind) 1]) - axs_reach (atomize finite_ind)) + (mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) + [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames, + pg'' thy [] (foldr (op ===>) (mapn (fn n => K(mk_trp(%%"adm" $ %(P_name n)))) + 1 dnames, ind_term (fn n => fn dn => %(P_name n) $ %(x_name n)))) + (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1) + 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 + cont_tacR 1 THEN resolve_tac prems 1), + strip_tac 1, + rtac (rewrite_rule axs_take_def finite_ind) 1, + ind_prems_tac prems]) ) end; (* local *) +(* ----- theorem concerning coinduction ------------------------------------- *) + local val xs = mapn (fn n => K (x_name n)) 1 dnames; - fun bnd_arg n i = Bound(2*(length dnames - n)-i-1); + fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); val take_ss = HOL_ss addsimps take_rews; - val sproj = bin_branchr (fn s => "fst("^s^")") (fn s => "snd("^s^")"); - val coind_lemma = pg [ax_bisim_def] (mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R", - foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs, - foldr mk_imp (mapn (fn n => K(proj (%"R") dnames n $ - bnd_arg n 0 $ bnd_arg n 1)) 0 dnames, - foldr' mk_conj (mapn (fn n => fn dn => - (dc_take dn $ %"n" `bnd_arg n 0 === - (dc_take dn $ %"n" `bnd_arg n 1))) 0 dnames)))))) ([ - rtac impI 1, - nat_ind_tac "n" 1, - simp_tac take_ss 1, - safe_tac HOL_cs] @ - flat(mapn (fn n => fn x => [ - etac allE 1, etac allE 1, - eres_inst_tac [("P1",sproj "R" dnames n^ - " "^x^" "^x^"'")](mp RS disjE) 1, - TRY(safe_tac HOL_cs), - REPEAT(CHANGED(asm_simp_tac take_ss 1))]) - 0 xs)); + val sproj = prj (fn s => "fst("^s^")") (fn s => "snd("^s^")"); + val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R", + foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs, + foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $ + bnd_arg n 0 $ bnd_arg n 1)) 0 dnames, + foldr' mk_conj (mapn (fn n => fn dn => + (dc_take dn $ %"n" `bnd_arg n 0 === + (dc_take dn $ %"n" `bnd_arg n 1)))0 dnames)))))) + ([ rtac impI 1, + nat_ind_tac "n" 1, + simp_tac take_ss 1, + safe_tac HOL_cs] @ + flat(mapn (fn n => fn x => [ + rotate_tac (n+1) 1, + etac all2E 1, + eres_inst_tac [("P1", sproj "R" n_eqs n^ + " "^x^" "^x^"'")](mp RS disjE) 1, + TRY(safe_tac HOL_cs), + REPEAT(CHANGED(asm_simp_tac take_ss 1))]) + 0 xs)); in val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===> - foldr (op ===>) (mapn (fn n => fn x => - mk_trp(proj (%"R") dnames n $ %x $ %(x^"'"))) 0 xs, - mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([ - TRY(safe_tac HOL_cs)] @ - flat(map (fn take_lemma => [ - rtac take_lemma 1, - cut_facts_tac [coind_lemma] 1, - fast_tac HOL_cs 1]) - take_lemmas)); + foldr (op ===>) (mapn (fn n => fn x => + mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs, + mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([ + TRY(safe_tac HOL_cs)] @ + flat(map (fn take_lemma => [ + rtac take_lemma 1, + cut_facts_tac [coind_lemma] 1, + fast_tac HOL_cs 1]) + take_lemmas)); end; (* local *)