--- 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 *)
--- 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 *)
--- 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 *)
-
--- 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 *)
--- 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 *)
--- 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 *)