--- a/src/HOLCF/Domain.thy Tue Jul 21 16:14:51 2009 +0200
+++ b/src/HOLCF/Domain.thy Tue Jul 21 16:14:56 2009 +0200
@@ -9,11 +9,11 @@
uses
("Tools/cont_consts.ML")
("Tools/cont_proc.ML")
- ("Tools/domain/domain_library.ML")
- ("Tools/domain/domain_syntax.ML")
- ("Tools/domain/domain_axioms.ML")
- ("Tools/domain/domain_theorems.ML")
- ("Tools/domain/domain_extender.ML")
+ ("Tools/Domain/domain_library.ML")
+ ("Tools/Domain/domain_syntax.ML")
+ ("Tools/Domain/domain_axioms.ML")
+ ("Tools/Domain/domain_theorems.ML")
+ ("Tools/Domain/domain_extender.ML")
begin
defaultsort pcpo
@@ -274,10 +274,10 @@
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
-use "Tools/domain/domain_library.ML"
-use "Tools/domain/domain_syntax.ML"
-use "Tools/domain/domain_axioms.ML"
-use "Tools/domain/domain_theorems.ML"
-use "Tools/domain/domain_extender.ML"
+use "Tools/Domain/domain_library.ML"
+use "Tools/Domain/domain_syntax.ML"
+use "Tools/Domain/domain_axioms.ML"
+use "Tools/Domain/domain_theorems.ML"
+use "Tools/Domain/domain_extender.ML"
end
--- a/src/HOLCF/IsaMakefile Tue Jul 21 16:14:51 2009 +0200
+++ b/src/HOLCF/IsaMakefile Tue Jul 21 16:14:56 2009 +0200
@@ -62,11 +62,11 @@
Tools/adm_tac.ML \
Tools/cont_consts.ML \
Tools/cont_proc.ML \
- Tools/domain/domain_extender.ML \
- Tools/domain/domain_axioms.ML \
- Tools/domain/domain_library.ML \
- Tools/domain/domain_syntax.ML \
- Tools/domain/domain_theorems.ML \
+ Tools/Domain/domain_extender.ML \
+ Tools/Domain/domain_axioms.ML \
+ Tools/Domain/domain_library.ML \
+ Tools/Domain/domain_syntax.ML \
+ Tools/Domain/domain_theorems.ML \
Tools/fixrec.ML \
Tools/pcpodef.ML \
holcf_logic.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Jul 21 16:14:56 2009 +0200
@@ -0,0 +1,235 @@
+(* Title: HOLCF/Tools/Domain/domain_axioms.ML
+ Author: David von Oheimb
+
+Syntax generator for domain command.
+*)
+
+signature DOMAIN_AXIOMS =
+sig
+ val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
+
+ val calc_axioms :
+ string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
+ string * (string * term) list * (string * term) list
+
+ val add_axioms :
+ bstring -> Domain_Library.eq list -> theory -> theory
+end;
+
+
+structure Domain_Axioms :> DOMAIN_AXIOMS =
+struct
+
+open Domain_Library;
+
+infixr 0 ===>;infixr 0 ==>;infix 0 == ;
+infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
+infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
+
+(* FIXME: use theory data for this *)
+val copy_tab : string Symtab.table =
+ Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}),
+ (@{type_name "++"}, @{const_name "ssum_fun"}),
+ (@{type_name "**"}, @{const_name "sprod_fun"}),
+ (@{type_name "*"}, @{const_name "cprod_fun"}),
+ (@{type_name "u"}, @{const_name "u_fun"})];
+
+fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
+and copy r (DatatypeAux.DtRec i) = r i
+ | copy r (DatatypeAux.DtTFree a) = ID
+ | copy r (DatatypeAux.DtType (c, ds)) =
+ case Symtab.lookup copy_tab c of
+ SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds)
+ | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
+
+fun calc_axioms
+ (comp_dname : string)
+ (eqs : eq list)
+ (n : int)
+ (eqn as ((dname,_),cons) : eq)
+ : string * (string * term) list * (string * term) list =
+ let
+
+ (* ----- 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 dnam = Long_Name.base_name dname;
+
+ val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
+ val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
+
+ val when_def = ("when_def",%%:(dname^"_when") ==
+ List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
+ Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
+
+ val copy_def =
+ let fun r i = cproj (Bound 0) eqs i;
+ in ("copy_def", %%:(dname^"_copy") ==
+ /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end;
+
+ (* -- definitions concerning the constructors, discriminators and selectors - *)
+
+ fun con_def m n (_,args) = let
+ fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
+ fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
+ fun inj y 1 _ = y
+ | inj y _ 0 = mk_sinl y
+ | inj y i j = mk_sinr (inj y (i-1) (j-1));
+ in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
+
+ val con_defs = mapn (fn n => fn (con,args) =>
+ (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
+
+ val dis_defs = let
+ fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
+ list_ccomb(%%:(dname^"_when"),map
+ (fn (con',args) => (List.foldr /\#
+ (if con'=con then TT else FF) args)) cons))
+ in map ddef cons end;
+
+ val mat_defs =
+ let
+ fun mdef (con,_) =
+ let
+ val k = Bound 0
+ val x = Bound 1
+ fun one_con (con', args') =
+ if con'=con then k else List.foldr /\# mk_fail args'
+ val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
+ val rhs = /\ "x" (/\ "k" (w ` x))
+ in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
+ in map mdef cons end;
+
+ val pat_defs =
+ let
+ fun pdef (con,args) =
+ let
+ val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
+ val xs = map (bound_arg args) args;
+ val r = Bound (length args);
+ val rhs = case args of [] => mk_return HOLogic.unit
+ | _ => mk_ctuple_pat ps ` mk_ctuple xs;
+ fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
+ in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) ==
+ list_ccomb(%%:(dname^"_when"), map one_con cons))
+ end
+ in map pdef cons end;
+
+ val sel_defs = let
+ fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel ==
+ list_ccomb(%%:(dname^"_when"),map
+ (fn (con',args) => if con'<>con then UU else
+ List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
+ in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
+
+
+ (* ----- axiom and definitions concerning induction ------------------------- *)
+
+ val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
+ `%x_name === %:x_name));
+ val take_def =
+ ("take_def",
+ %%:(dname^"_take") ==
+ mk_lam("n",cproj
+ (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
+ val finite_def =
+ ("finite_def",
+ %%:(dname^"_finite") ==
+ mk_lam(x_name,
+ mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
+
+ in (dnam,
+ [abs_iso_ax, rep_iso_ax, reach_ax],
+ [when_def, copy_def] @
+ con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
+ [take_def, finite_def])
+ end; (* let (calc_axioms) *)
+
+
+(* legacy type inference *)
+
+fun legacy_infer_term thy t =
+ singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
+
+fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+
+fun infer_props thy = map (apsnd (legacy_infer_prop thy));
+
+
+fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
+fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
+
+fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
+fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
+
+fun add_matchers (((dname,_),cons) : eq) thy =
+ let
+ val con_names = map fst cons;
+ val mat_names = map mat_name con_names;
+ fun qualify n = Sign.full_name thy (Binding.name n);
+ val ms = map qualify con_names ~~ map qualify mat_names;
+ in Fixrec.add_matchers ms thy end;
+
+fun add_axioms comp_dnam (eqs : eq list) thy' =
+ let
+ val comp_dname = Sign.full_bname thy' comp_dnam;
+ val dnames = map (fst o fst) eqs;
+ val x_name = idx_name dnames "x";
+ fun copy_app dname = %%:(dname^"_copy")`Bound 0;
+ val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
+ /\ "f"(mk_ctuple (map copy_app dnames)));
+
+ fun one_con (con,args) = let
+ val nonrec_args = filter_out is_rec args;
+ val rec_args = List.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)) eqs (rec_of ra) $
+ Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
+ val capps =
+ List.foldr mk_conj
+ (mk_conj(
+ Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
+ Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
+ (mapn rel_app 1 rec_args);
+ in List.foldr mk_ex
+ (Library.foldr mk_conj
+ (map (defined o Bound) nonlazy_idxs,capps)) allvns
+ end;
+ fun one_comp n (_,cons) =
+ mk_all(x_name(n+1),
+ mk_all(x_name(n+1)^"'",
+ mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
+ foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
+ ::map one_con cons))));
+ val bisim_def =
+ ("bisim_def",
+ %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
+
+ fun add_one (thy,(dnam,axs,dfs)) =
+ thy |> Sign.add_path dnam
+ |> add_defs_infer dfs
+ |> add_axioms_infer axs
+ |> Sign.parent_path;
+
+ val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
+
+ in thy |> Sign.add_path comp_dnam
+ |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
+ |> Sign.parent_path
+ |> fold add_matchers eqs
+ end; (* let (add_axioms) *)
+
+end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Jul 21 16:14:56 2009 +0200
@@ -0,0 +1,204 @@
+(* Title: HOLCF/Tools/Domain/domain_extender.ML
+ Author: David von Oheimb
+
+Theory extender for domain command, including theory syntax.
+*)
+
+signature DOMAIN_EXTENDER =
+sig
+ val add_domain_cmd: string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list
+ -> theory -> theory
+ val add_domain: string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
+ -> theory -> theory
+end;
+
+structure Domain_Extender :> DOMAIN_EXTENDER =
+struct
+
+open Domain_Library;
+
+(* ----- general testing and preprocessing of constructor list -------------- *)
+fun check_and_sort_domain
+ (dtnvs : (string * typ list) list)
+ (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
+ (sg : theory)
+ : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list =
+ let
+ val defaultS = Sign.defaultS sg;
+ val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
+ [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
+ val test_dupl_cons =
+ (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of
+ [] => false | dups => error ("Duplicate constructors: "
+ ^ commas_quote dups));
+ val test_dupl_sels =
+ (case duplicates (op =) (map Binding.name_of (List.mapPartial second
+ (List.concat (map second (List.concat cons''))))) of
+ [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
+ val test_dupl_tvars =
+ exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
+ [] => false | dups => error("Duplicate type arguments: "
+ ^commas_quote dups)) (map snd dtnvs);
+ (* test for free type variables, illegal sort constraints on rhs,
+ non-pcpo-types and invalid use of recursive type;
+ replace sorts in type variables on rhs *)
+ fun analyse_equation ((dname,typevars),cons') =
+ let
+ val tvars = map dest_TFree typevars;
+ val distinct_typevars = map TFree tvars;
+ fun rm_sorts (TFree(s,_)) = TFree(s,[])
+ | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
+ | rm_sorts (TVar(s,_)) = TVar(s,[])
+ and remove_sorts l = map rm_sorts l;
+ val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
+ fun analyse indirect (TFree(v,s)) =
+ (case AList.lookup (op =) tvars v of
+ NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
+ | SOME sort => if eq_set_string (s,defaultS) orelse
+ eq_set_string (s,sort )
+ then TFree(v,sort)
+ else error ("Inconsistent sort constraint" ^
+ " for type variable " ^ quote v))
+ | analyse indirect (t as Type(s,typl)) =
+ (case AList.lookup (op =) dtnvs s of
+ NONE => if s mem indirect_ok
+ then Type(s,map (analyse false) typl)
+ else Type(s,map (analyse true) typl)
+ | SOME typevars => if indirect
+ then error ("Indirect recursion of type " ^
+ quote (string_of_typ sg t))
+ else if dname <> s orelse
+ (** BUG OR FEATURE?:
+ mutual recursion may use different arguments **)
+ remove_sorts typevars = remove_sorts typl
+ then Type(s,map (analyse true) typl)
+ else error ("Direct recursion of type " ^
+ quote (string_of_typ sg t) ^
+ " with different arguments"))
+ | analyse indirect (TVar _) = Imposs "extender:analyse";
+ fun check_pcpo lazy T =
+ let val ok = if lazy then cpo_type else pcpo_type
+ in if ok sg T then T else error
+ ("Constructor argument type is not of sort pcpo: " ^
+ string_of_typ sg T)
+ end;
+ fun analyse_arg (lazy, sel, T) =
+ (lazy, sel, check_pcpo lazy (analyse false T));
+ fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
+ in ((dname,distinct_typevars), map analyse_con cons') end;
+ in ListPair.map analyse_equation (dtnvs,cons'')
+ end; (* let *)
+
+(* ----- calls for building new thy and thms -------------------------------- *)
+
+fun gen_add_domain
+ (prep_typ : theory -> 'a -> typ)
+ (comp_dnam : string)
+ (eqs''' : ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * 'a) list * mixfix) list) list)
+ (thy''' : theory) =
+ let
+ fun readS (SOME s) = Syntax.read_sort_global thy''' s
+ | readS NONE = Sign.defaultS thy''';
+ fun readTFree (a, s) = TFree (a, readS s);
+
+ val dtnvs = map (fn (vs,dname:binding,mx,_) =>
+ (dname, map readTFree vs, mx)) eqs''';
+ val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
+ fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
+ fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
+ val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
+ |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+ val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
+ val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+ val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list =
+ check_and_sort_domain dtnvs' cons'' thy'';
+ val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
+ val dts = map (Type o fst) eqs';
+ val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+ fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
+ fun typid (Type (id,_)) =
+ let val c = hd (Symbol.explode (Long_Name.base_name id))
+ in if Symbol.is_letter c then c else "t" end
+ | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
+ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
+ fun one_con (con,args,mx) =
+ ((Syntax.const_name mx (Binding.name_of con)),
+ ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
+ DatatypeAux.dtyp_of_typ new_dts tp),
+ Option.map Binding.name_of sel,vn))
+ (args,(mk_var_names(map (typid o third) args)))
+ ) : cons;
+ val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
+ val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
+ val ((rewss, take_rews), theorems_thy) =
+ thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+ in
+ theorems_thy
+ |> Sign.add_path (Long_Name.base_name comp_dnam)
+ |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
+ |> Sign.parent_path
+ end;
+
+val add_domain = gen_add_domain Sign.certify_typ;
+val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
+
+
+(** outer syntax **)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ = OuterKeyword.keyword "lazy";
+
+val dest_decl : (bool * binding option * string) parser =
+ P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
+ (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
+ || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
+ >> (fn t => (true,NONE,t))
+ || P.typ >> (fn t => (false,NONE,t));
+
+val cons_decl =
+ P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
+
+val type_var' : (string * string option) parser =
+ (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
+
+val type_args' : (string * string option) list parser =
+ type_var' >> single ||
+ P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
+ Scan.succeed [];
+
+val domain_decl =
+ (type_args' -- P.binding -- P.opt_infix) --
+ (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+
+val domains_decl =
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+ P.and_list1 domain_decl;
+
+fun mk_domain (opt_name : string option,
+ doms : ((((string * string option) list * binding) * mixfix) *
+ ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
+ let
+ val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
+ val specs : ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list =
+ map (fn (((vs, t), mx), cons) =>
+ (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
+ val comp_dnam =
+ case opt_name of NONE => space_implode "_" names | SOME s => s;
+ in add_domain_cmd comp_dnam specs end;
+
+val _ =
+ OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
+ (domains_decl >> (Toplevel.theory o mk_domain));
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Tue Jul 21 16:14:56 2009 +0200
@@ -0,0 +1,399 @@
+(* Title: HOLCF/Tools/Domain/domain_library.ML
+ Author: David von Oheimb
+
+Library for domain command.
+*)
+
+
+(* ----- general support ---------------------------------------------------- *)
+
+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 Fail "foldr''"
+ | itr [a] = f2 a
+ | itr (a::l) = f(a, itr l)
+ in itr l end;
+
+fun map_cumulr f start xs =
+ List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
+ (y::ys,res2)) ([],start) xs;
+
+fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x;
+fun upd_first f (x,y,z) = (f x, y, z);
+fun upd_second f (x,y,z) = ( x, f y, z);
+fun upd_third f (x,y,z) = ( x, y, f z);
+
+fun atomize ctxt thm =
+ let
+ val r_inst = read_instantiate ctxt;
+ 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", 0), "?" ^ s)] spec))
+ | _ => [thm];
+ in map zero_var_indexes (at thm) end;
+
+(* infix syntax *)
+
+infixr 5 -->;
+infixr 6 ->>;
+infixr 0 ===>;
+infixr 0 ==>;
+infix 0 ==;
+infix 1 ===;
+infix 1 ~=;
+infix 1 <<;
+infix 1 ~<<;
+
+infix 9 ` ;
+infix 9 `% ;
+infix 9 `%%;
+
+
+(* ----- specific support for domain ---------------------------------------- *)
+
+signature DOMAIN_LIBRARY =
+sig
+ val Imposs : string -> 'a;
+ val cpo_type : theory -> typ -> bool;
+ val pcpo_type : theory -> typ -> bool;
+ val string_of_typ : theory -> typ -> string;
+
+ (* Creating HOLCF types *)
+ val mk_cfunT : typ * typ -> typ;
+ val ->> : typ * typ -> typ;
+ val mk_ssumT : typ * typ -> typ;
+ val mk_sprodT : typ * typ -> typ;
+ val mk_uT : typ -> typ;
+ val oneT : typ;
+ val trT : typ;
+ val mk_maybeT : typ -> typ;
+ val mk_ctupleT : typ list -> typ;
+ val mk_TFree : string -> typ;
+ val pcpoS : sort;
+
+ (* Creating HOLCF terms *)
+ val %: : string -> term;
+ val %%: : string -> term;
+ val ` : term * term -> term;
+ val `% : term * string -> term;
+ val /\ : string -> term -> term;
+ val UU : term;
+ val TT : term;
+ val FF : term;
+ val ID : term;
+ val oo : term * term -> term;
+ val mk_up : term -> term;
+ val mk_sinl : term -> term;
+ val mk_sinr : term -> term;
+ val mk_stuple : term list -> term;
+ val mk_ctuple : term list -> term;
+ val mk_fix : term -> term;
+ val mk_iterate : term * term * term -> term;
+ val mk_fail : term;
+ val mk_return : term -> term;
+ val cproj : term -> 'a list -> int -> term;
+ val list_ccomb : term * term list -> term;
+ (*
+ val con_app : string -> ('a * 'b * string) list -> term;
+ *)
+ val con_app2 : string -> ('a -> term) -> 'a list -> term;
+ val proj : term -> 'a list -> int -> term;
+ val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a;
+ val mk_ctuple_pat : term list -> term;
+ val mk_branch : term -> term;
+
+ (* Creating propositions *)
+ val mk_conj : term * term -> term;
+ val mk_disj : term * term -> term;
+ val mk_imp : term * term -> term;
+ val mk_lam : string * term -> term;
+ val mk_all : string * term -> term;
+ val mk_ex : string * term -> term;
+ val mk_constrain : typ * term -> term;
+ val mk_constrainall : string * typ * term -> term;
+ val === : term * term -> term;
+ val << : term * term -> term;
+ val ~<< : term * term -> term;
+ val strict : term -> term;
+ val defined : term -> term;
+ val mk_adm : term -> term;
+ val mk_compact : term -> term;
+ val lift : ('a -> term) -> 'a list * term -> term;
+ val lift_defined : ('a -> term) -> 'a list * term -> term;
+
+ (* Creating meta-propositions *)
+ val mk_trp : term -> term; (* HOLogic.mk_Trueprop *)
+ val == : term * term -> term;
+ val ===> : term * term -> term;
+ val ==> : term * term -> term;
+ val mk_All : string * term -> term;
+
+ (* Domain specifications *)
+ eqtype arg;
+ type cons = string * arg list;
+ type eq = (string * typ list) * cons list;
+ val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
+ val is_lazy : arg -> bool;
+ val rec_of : arg -> int;
+ val dtyp_of : arg -> Datatype.dtyp;
+ val sel_of : arg -> string option;
+ val vname : arg -> string;
+ val upd_vname : (string -> string) -> arg -> arg;
+ val is_rec : arg -> bool;
+ val is_nonlazy_rec : arg -> bool;
+ val nonlazy : arg list -> string list;
+ val nonlazy_rec : arg list -> string list;
+ val %# : arg -> term;
+ val /\# : arg * term -> term;
+ val when_body : cons list -> (int * int -> term) -> term;
+ val when_funs : 'a list -> string list;
+ val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
+ val idx_name : 'a list -> string -> int -> string;
+ val app_rec_arg : (int -> term) -> arg -> term;
+ val con_app : string -> arg list -> term;
+ val dtyp_of_eq : eq -> Datatype.dtyp;
+
+
+ (* Name mangling *)
+ val strip_esc : string -> string;
+ val extern_name : string -> string;
+ val dis_name : string -> string;
+ val mat_name : string -> string;
+ val pat_name : string -> string;
+ val mk_var_names : string list -> string list;
+end;
+
+structure Domain_Library :> DOMAIN_LIBRARY =
+struct
+
+exception Impossible of string;
+fun Imposs msg = raise Impossible ("Domain:"^msg);
+
+(* ----- name handling ----- *)
+
+val strip_esc =
+ let fun strip ("'" :: c :: cs) = c :: strip cs
+ | strip ["'"] = []
+ | strip (c :: cs) = c :: strip cs
+ | strip [] = [];
+ in implode o strip o Symbol.explode end;
+
+fun extern_name con =
+ case Symbol.explode con of
+ ("o"::"p"::" "::rest) => implode rest
+ | _ => con;
+fun dis_name con = "is_"^ (extern_name con);
+fun dis_name_ con = "is_"^ (strip_esc con);
+fun mat_name con = "match_"^ (extern_name con);
+fun mat_name_ con = "match_"^ (strip_esc con);
+fun pat_name con = (extern_name con) ^ "_pat";
+fun pat_name_ con = (strip_esc con) ^ "_pat";
+
+(* make distinct names out of the type list,
+ forbidding "o","n..","x..","f..","P.." as names *)
+(* a number string is added if necessary *)
+fun mk_var_names ids : string list =
+ let
+ fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
+ fun index_vnames(vn::vns,occupied) =
+ (case AList.lookup (op =) occupied vn of
+ NONE => if vn mem vns
+ then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied)
+ else vn :: index_vnames(vns, occupied)
+ | SOME(i) => (vn^(string_of_int (i+1)))
+ :: index_vnames(vns,(vn,i+1)::occupied))
+ | index_vnames([],occupied) = [];
+ in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
+
+fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
+fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
+fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
+
+(* ----- constructor list handling ----- *)
+
+type arg =
+ (bool * Datatype.dtyp) * (* (lazy, recursive element) *)
+ string option * (* selector name *)
+ string; (* argument name *)
+
+type cons =
+ string * (* operator name of constr *)
+ arg 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 mk_arg = I;
+
+fun rec_of ((_,dtyp),_,_) =
+ case dtyp of DatatypeAux.DtRec i => i | _ => ~1;
+(* FIXME: what about indirect recursion? *)
+
+fun is_lazy arg = fst (first arg);
+fun dtyp_of arg = snd (first arg);
+val sel_of = second;
+val vname = third;
+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 nonlazy_rec args = map vname (List.filter is_nonlazy_rec args);
+
+
+(* ----- combinators for making dtyps ----- *)
+
+fun mk_uD T = DatatypeAux.DtType(@{type_name "u"}, [T]);
+fun mk_sprodD (T, U) = DatatypeAux.DtType(@{type_name "**"}, [T, U]);
+fun mk_ssumD (T, U) = DatatypeAux.DtType(@{type_name "++"}, [T, U]);
+fun mk_liftD T = DatatypeAux.DtType(@{type_name "lift"}, [T]);
+val unitD = DatatypeAux.DtType(@{type_name "unit"}, []);
+val boolD = DatatypeAux.DtType(@{type_name "bool"}, []);
+val oneD = mk_liftD unitD;
+val trD = mk_liftD boolD;
+fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds;
+fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
+
+fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D;
+fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
+fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
+
+
+(* ----- support for type and mixfix expressions ----- *)
+
+fun mk_uT T = Type(@{type_name "u"}, [T]);
+fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
+fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+val oneT = @{typ one};
+val trT = @{typ tr};
+
+val op ->> = mk_cfunT;
+
+fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});
+
+(* ----- support for term expressions ----- *)
+
+fun %: s = Free(s,dummyT);
+fun %# arg = %:(vname arg);
+fun %%: s = Const(s,dummyT);
+
+local open HOLogic in
+val mk_trp = mk_Trueprop;
+fun mk_conj (S,T) = conj $ S $ T;
+fun mk_disj (S,T) = disj $ S $ T;
+fun mk_imp (S,T) = imp $ S $ T;
+fun mk_lam (x,T) = Abs(x,dummyT,T);
+fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
+fun mk_ex (x,P) = mk_exists (x,dummyT,P);
+val mk_constrain = uncurry TypeInfer.constrain;
+fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
+end
+
+fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
+
+infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T;
+infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T;
+infix 0 ==; fun S == T = %%:"==" $ S $ T;
+infix 1 ===; fun S === T = %%:"op =" $ S $ T;
+infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
+infix 1 <<; fun S << T = %%: @{const_name Porder.below} $ S $ T;
+infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T);
+
+infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
+infix 9 `% ; fun f`% s = f` %: s;
+infix 9 `%%; fun f`%%s = f` %%:s;
+
+fun mk_adm t = %%: @{const_name adm} $ t;
+fun mk_compact t = %%: @{const_name compact} $ t;
+val ID = %%: @{const_name ID};
+fun mk_strictify t = %%: @{const_name strictify}`t;
+fun mk_cfst t = %%: @{const_name cfst}`t;
+fun mk_csnd t = %%: @{const_name csnd}`t;
+(*val csplitN = "Cprod.csplit";*)
+(*val sfstN = "Sprod.sfst";*)
+(*val ssndN = "Sprod.ssnd";*)
+fun mk_ssplit t = %%: @{const_name ssplit}`t;
+fun mk_sinl t = %%: @{const_name sinl}`t;
+fun mk_sinr t = %%: @{const_name sinr}`t;
+fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y;
+fun mk_up t = %%: @{const_name up}`t;
+fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u;
+val ONE = @{term ONE};
+val TT = @{term TT};
+val FF = @{term FF};
+fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z;
+fun mk_fix t = %%: @{const_name fix}`t;
+fun mk_return t = %%: @{const_name Fixrec.return}`t;
+val mk_fail = %%: @{const_name Fixrec.fail};
+
+fun mk_branch t = %%: @{const_name Fixrec.branch} $ t;
+
+val pcpoS = @{sort pcpo};
+
+val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *)
+fun con_app2 con f args = list_ccomb(%%:con,map f args);
+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) I (%# arg);
+fun prj _ _ x ( _::[]) _ = x
+ | prj f1 _ x (_::y::ys) 0 = f1 x y
+ | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
+fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
+fun cproj x = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x;
+fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
+
+fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T);
+fun /\# (arg,T) = /\ (vname arg) T;
+infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T;
+val UU = %%: @{const_name UU};
+fun strict f = f`UU === UU;
+fun defined t = t ~= UU;
+fun cpair (t,u) = %%: @{const_name cpair}`t`u;
+fun spair (t,u) = %%: @{const_name spair}`t`u;
+fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
+ | mk_ctuple ts = foldr1 cpair ts;
+fun mk_stuple [] = ONE
+ | mk_stuple ts = foldr1 spair ts;
+fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *)
+ | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
+fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
+fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
+val mk_ctuple_pat = foldr1 cpair_pat;
+fun lift_defined f = lift (fn x => defined (f x));
+fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
+
+fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) =
+ (case cont_eta_contract body of
+ body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) =>
+ if not (0 mem loose_bnos f) then incr_boundvars ~1 f
+ else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')
+ | body' => Const("Cfun.Abs_CFun",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 when_funs cons = if length cons = 1 then ["f"]
+ 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 t => mk_fup (ID, t))
+ else I) (Bound(l2-m));
+ in cont_eta_contract
+ (foldr''
+ (fn (a,t) => mk_ssplit (/\# (a,t)))
+ (args,
+ fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
+ ) end;
+ in (if length cons = 1 andalso length(snd(hd cons)) <= 1
+ then mk_strictify else I)
+ (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
+
+end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Jul 21 16:14:56 2009 +0200
@@ -0,0 +1,181 @@
+(* Title: HOLCF/Tools/Domain/domain_syntax.ML
+ Author: David von Oheimb
+
+Syntax generator for domain command.
+*)
+
+signature DOMAIN_SYNTAX =
+sig
+ val calc_syntax:
+ typ ->
+ (string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list ->
+ (binding * typ * mixfix) list * ast Syntax.trrule list
+
+ val add_syntax:
+ string ->
+ ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list ->
+ theory -> theory
+end;
+
+
+structure Domain_Syntax :> DOMAIN_SYNTAX =
+struct
+
+open Domain_Library;
+infixr 5 -->; infixr 6 ->>;
+
+fun calc_syntax
+ (dtypeprod : typ)
+ ((dname : string, typevars : typ list),
+ (cons': (binding * (bool * binding option * typ) list * mixfix) list))
+ : (binding * typ * mixfix) list * ast Syntax.trrule list =
+ let
+ (* ----- constants concerning the isomorphism ------------------------------- *)
+
+ local
+ fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
+ fun prod (_,args,_) = case args of [] => oneT
+ | _ => foldr1 mk_sprodT (map opt_lazy args);
+ fun freetvar s = let val tvar = mk_TFree s in
+ if tvar mem typevars then freetvar ("t"^s) else tvar end;
+ fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
+ in
+ val dtype = Type(dname,typevars);
+ val dtype2 = foldr1 mk_ssumT (map prod cons');
+ val dnam = Long_Name.base_name dname;
+ fun dbind s = Binding.name (dnam ^ s);
+ val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn);
+ val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn);
+ val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
+ val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
+ end;
+
+ (* ----- constants concerning constructors, discriminators, and selectors --- *)
+
+ 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 Symbol.explode end;
+ fun dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con));
+ fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con));
+ fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
+ fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx);
+ fun dis (con,args,mx) = (dis_name_ con, dtype->>trT,
+ Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
+ (* strictly speaking, these constants have one argument,
+ but the mixfix (without arguments) is introduced only
+ to generate parse rules for non-alphanumeric names*)
+ fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in
+ if tvar mem typevars then freetvar ("t"^s) n else tvar end;
+ fun mk_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
+ fun mat (con,args,mx) = (mat_name_ con,
+ mk_matT(dtype, map third args, freetvar "t" 1),
+ Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
+ fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
+ fun sel (con,args,mx) = List.mapPartial sel1 args;
+ fun mk_patT (a,b) = a ->> mk_maybeT b;
+ fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
+ fun pat (con,args,mx) = (pat_name_ con,
+ (mapn pat_arg_typ 1 args)
+ --->
+ mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
+ Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
+
+ in
+ val consts_con = map con cons';
+ val consts_dis = map dis cons';
+ val consts_mat = map mat cons';
+ val consts_pat = map pat cons';
+ val consts_sel = List.concat(map sel cons');
+ end;
+
+ (* ----- constants concerning induction ------------------------------------- *)
+
+ val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
+ val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
+
+ (* ----- case translation --------------------------------------------------- *)
+
+ local open Syntax in
+ local
+ fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
+ fun expvar n = Variable ("e"^(string_of_int n));
+ fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
+ (string_of_int m));
+ fun argvars n args = mapn (argvar n) 1 args;
+ fun app s (l,r) = mk_appl (Constant s) [l,r];
+ val cabs = app "_cabs";
+ val capp = app "Rep_CFun";
+ fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
+ fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
+ fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
+ fun when1 n m = if n = m then arg1 n else K (Constant "UU");
+
+ fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
+ fun app_pat x = mk_appl (Constant "_pat") [x];
+ fun args_list [] = Constant "_noargs"
+ | args_list xs = foldr1 (app "_args") xs;
+ in
+ val case_trans =
+ ParsePrintRule
+ (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
+ capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
+
+ fun one_abscon_trans n (con,mx,args) =
+ ParsePrintRule
+ (cabs (con1 n (con,mx,args), expvar n),
+ Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'));
+ val abscon_trans = mapn one_abscon_trans 1 cons';
+
+ fun one_case_trans (con,args,mx) =
+ let
+ val cname = c_ast con mx;
+ val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
+ val ns = 1 upto length args;
+ val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
+ val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
+ val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
+ in
+ [ParseRule (app_pat (Library.foldl capp (cname, xs)),
+ mk_appl pname (map app_pat xs)),
+ ParseRule (app_var (Library.foldl capp (cname, xs)),
+ app_var (args_list xs)),
+ PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
+ app "_match" (mk_appl pname ps, args_list vs))]
+ end;
+ val Case_trans = List.concat (map one_case_trans cons');
+ end;
+ end;
+
+ in ([const_rep, const_abs, const_when, const_copy] @
+ consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
+ [const_take, const_finite],
+ (case_trans::(abscon_trans @ Case_trans)))
+ end; (* let *)
+
+(* ----- putting all the syntax stuff together ------------------------------ *)
+
+fun add_syntax
+ (comp_dnam : string)
+ (eqs' : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list)
+ (thy'' : theory) =
+ let
+ val dtypes = map (Type o fst) eqs';
+ val boolT = HOLogic.boolT;
+ val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
+ val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+ val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
+ val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
+ val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
+ in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @
+ (if length eqs'>1 then [const_copy] else[])@
+ [const_bisim])
+ |> Sign.add_trrules_i (List.concat(map snd ctt))
+ end; (* let *)
+
+end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Jul 21 16:14:56 2009 +0200
@@ -0,0 +1,1053 @@
+(* Title: HOLCF/Tools/Domain/domain_theorems.ML
+ Author: David von Oheimb
+ New proofs/tactics by Brian Huffman
+
+Proof generator for domain command.
+*)
+
+val HOLCF_ss = @{simpset};
+
+signature DOMAIN_THEOREMS =
+sig
+ val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
+ val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
+ val quiet_mode: bool ref;
+ val trace_domain: bool ref;
+end;
+
+structure Domain_Theorems :> DOMAIN_THEOREMS =
+struct
+
+val quiet_mode = ref false;
+val trace_domain = ref false;
+
+fun message s = if !quiet_mode then () else writeln s;
+fun trace s = if !trace_domain then tracing s else ();
+
+local
+
+val adm_impl_admw = @{thm adm_impl_admw};
+val adm_all = @{thm adm_all};
+val adm_conj = @{thm adm_conj};
+val adm_subst = @{thm adm_subst};
+val antisym_less_inverse = @{thm below_antisym_inverse};
+val beta_cfun = @{thm beta_cfun};
+val cfun_arg_cong = @{thm cfun_arg_cong};
+val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
+val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR};
+val chain_iterate = @{thm chain_iterate};
+val compact_ONE = @{thm compact_ONE};
+val compact_sinl = @{thm compact_sinl};
+val compact_sinr = @{thm compact_sinr};
+val compact_spair = @{thm compact_spair};
+val compact_up = @{thm compact_up};
+val contlub_cfun_arg = @{thm contlub_cfun_arg};
+val contlub_cfun_fun = @{thm contlub_cfun_fun};
+val fix_def2 = @{thm fix_def2};
+val injection_eq = @{thm injection_eq};
+val injection_less = @{thm injection_below};
+val lub_equal = @{thm lub_equal};
+val monofun_cfun_arg = @{thm monofun_cfun_arg};
+val retraction_strict = @{thm retraction_strict};
+val spair_eq = @{thm spair_eq};
+val spair_less = @{thm spair_below};
+val sscase1 = @{thm sscase1};
+val ssplit1 = @{thm ssplit1};
+val strictify1 = @{thm strictify1};
+val wfix_ind = @{thm wfix_ind};
+
+val iso_intro = @{thm iso.intro};
+val iso_abs_iso = @{thm iso.abs_iso};
+val iso_rep_iso = @{thm iso.rep_iso};
+val iso_abs_strict = @{thm iso.abs_strict};
+val iso_rep_strict = @{thm iso.rep_strict};
+val iso_abs_defin' = @{thm iso.abs_defin'};
+val iso_rep_defin' = @{thm iso.rep_defin'};
+val iso_abs_defined = @{thm iso.abs_defined};
+val iso_rep_defined = @{thm iso.rep_defined};
+val iso_compact_abs = @{thm iso.compact_abs};
+val iso_compact_rep = @{thm iso.compact_rep};
+val iso_iso_swap = @{thm iso.iso_swap};
+
+val exh_start = @{thm exh_start};
+val ex_defined_iffs = @{thms ex_defined_iffs};
+val exh_casedist0 = @{thm exh_casedist0};
+val exh_casedists = @{thms exh_casedists};
+
+open Domain_Library;
+infixr 0 ===>;
+infixr 0 ==>;
+infix 0 == ;
+infix 1 ===;
+infix 1 ~= ;
+infix 1 <<;
+infix 1 ~<<;
+infix 9 ` ;
+infix 9 `% ;
+infix 9 `%%;
+infixr 9 oo;
+
+(* ----- general proof facilities ------------------------------------------- *)
+
+fun legacy_infer_term thy t =
+ let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
+ in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end;
+
+fun pg'' thy defs t tacs =
+ let
+ val t' = legacy_infer_term thy t;
+ val asms = Logic.strip_imp_prems t';
+ val prop = Logic.strip_imp_concl t';
+ fun tac {prems, context} =
+ rewrite_goals_tac defs THEN
+ EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
+ in Goal.prove_global thy [] asms prop tac end;
+
+fun pg' thy defs t tacsf =
+ let
+ fun tacs {prems, context} =
+ if null prems then tacsf context
+ else cut_facts_tac prems 1 :: tacsf context;
+ in pg'' thy defs t tacs end;
+
+fun case_UU_tac ctxt rews i v =
+ InductTacs.case_tac ctxt (v^"=UU") i THEN
+ asm_simp_tac (HOLCF_ss addsimps rews) i;
+
+val chain_tac =
+ REPEAT_DETERM o resolve_tac
+ [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL];
+
+(* ----- general proofs ----------------------------------------------------- *)
+
+val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
+
+val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)}
+
+in
+
+fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
+let
+
+val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
+val pg = pg' thy;
+
+(* ----- getting the axioms and definitions --------------------------------- *)
+
+local
+ fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
+in
+ val ax_abs_iso = ga "abs_iso" dname;
+ val ax_rep_iso = ga "rep_iso" dname;
+ val ax_when_def = ga "when_def" dname;
+ fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname;
+ val axs_con_def = map (get_def extern_name) cons;
+ val axs_dis_def = map (get_def dis_name) cons;
+ val axs_mat_def = map (get_def mat_name) cons;
+ val axs_pat_def = map (get_def pat_name) cons;
+ val axs_sel_def =
+ let
+ fun def_of_sel sel = ga (sel^"_def") dname;
+ fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
+ fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
+ in
+ maps defs_of_con cons
+ end;
+ val ax_copy_def = ga "copy_def" dname;
+end; (* local *)
+
+(* ----- theorems concerning the isomorphism -------------------------------- *)
+
+val dc_abs = %%:(dname^"_abs");
+val dc_rep = %%:(dname^"_rep");
+val dc_copy = %%:(dname^"_copy");
+val x_name = "x";
+
+val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
+val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
+val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
+val abs_defin' = iso_locale RS iso_abs_defin';
+val rep_defin' = iso_locale RS iso_rep_defin';
+val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
+
+(* ----- generating beta reduction rules from definitions-------------------- *)
+
+val _ = trace " Proving beta reduction rules...";
+
+local
+ fun arglist (Const _ $ Abs (s, _, t)) =
+ let
+ val (vars,body) = arglist t;
+ in (s :: vars, body) end
+ | arglist t = ([], t);
+ fun bind_fun vars t = Library.foldr mk_All (vars, t);
+ fun bound_vars 0 = []
+ | bound_vars i = Bound (i-1) :: bound_vars (i - 1);
+in
+ fun appl_of_def def =
+ let
+ val (_ $ con $ lam) = concl_of def;
+ val (vars, rhs) = arglist lam;
+ val lhs = list_ccomb (con, bound_vars (length vars));
+ val appl = bind_fun vars (lhs == rhs);
+ val cs = ContProc.cont_thms lam;
+ val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
+ in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
+end;
+
+val _ = trace "Proving when_appl...";
+val when_appl = appl_of_def ax_when_def;
+val _ = trace "Proving con_appls...";
+val con_appls = map appl_of_def axs_con_def;
+
+local
+ fun arg2typ n arg =
+ let val t = TVar (("'a", n), pcpoS)
+ in (n + 1, if is_lazy arg then mk_uT t else t) end;
+
+ fun args2typ n [] = (n, oneT)
+ | args2typ n [arg] = arg2typ n arg
+ | args2typ n (arg::args) =
+ let
+ val (n1, t1) = arg2typ n arg;
+ val (n2, t2) = args2typ n1 args
+ in (n2, mk_sprodT (t1, t2)) end;
+
+ fun cons2typ n [] = (n,oneT)
+ | cons2typ n [con] = args2typ n (snd con)
+ | cons2typ n (con::cons) =
+ let
+ val (n1, t1) = args2typ n (snd con);
+ val (n2, t2) = cons2typ n1 cons
+ in (n2, mk_ssumT (t1, t2)) end;
+in
+ fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
+end;
+
+local
+ val iso_swap = iso_locale RS iso_iso_swap;
+ fun one_con (con, args) =
+ let
+ val vns = map vname args;
+ val eqn = %:x_name === con_app2 con %: vns;
+ val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
+ in Library.foldr mk_ex (vns, conj) end;
+
+ val conj_assoc = @{thm conj_assoc};
+ val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
+ val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
+ val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
+ val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
+
+ (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
+ val tacs = [
+ rtac disjE 1,
+ etac (rep_defin' RS disjI1) 2,
+ etac disjI2 2,
+ rewrite_goals_tac [mk_meta_eq iso_swap],
+ rtac thm3 1];
+in
+ val _ = trace " Proving exhaust...";
+ val exhaust = pg con_appls (mk_trp exh) (K tacs);
+ val _ = trace " Proving casedist...";
+ val casedist =
+ standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
+end;
+
+local
+ fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
+ fun bound_fun i _ = Bound (length cons - i);
+ val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
+in
+ val _ = trace " Proving when_strict...";
+ val when_strict =
+ let
+ val axs = [when_appl, mk_meta_eq rep_strict];
+ val goal = bind_fun (mk_trp (strict when_app));
+ val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
+ in pg axs goal (K tacs) end;
+
+ val _ = trace " Proving when_apps...";
+ val when_apps =
+ let
+ fun one_when n (con,args) =
+ let
+ val axs = when_appl :: con_appls;
+ val goal = bind_fun (lift_defined %: (nonlazy args,
+ mk_trp (when_app`(con_app con args) ===
+ list_ccomb (bound_fun n 0, map %# args))));
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
+ in pg axs goal (K tacs) end;
+ in mapn one_when 1 cons end;
+end;
+val when_rews = when_strict :: when_apps;
+
+(* ----- theorems concerning the constructors, discriminators and selectors - *)
+
+local
+ fun dis_strict (con, _) =
+ let
+ val goal = mk_trp (strict (%%:(dis_name con)));
+ in pg axs_dis_def goal (K [rtac when_strict 1]) end;
+
+ fun dis_app c (con, args) =
+ let
+ val lhs = %%:(dis_name c) ` con_app con args;
+ val rhs = if con = c then TT else FF;
+ val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs_dis_def goal (K tacs) end;
+
+ val _ = trace " Proving dis_apps...";
+ val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
+
+ fun dis_defin (con, args) =
+ let
+ val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
+ val tacs =
+ [rtac casedist 1,
+ contr_tac 1,
+ DETERM_UNTIL_SOLVED (CHANGED
+ (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
+ in pg [] goal (K tacs) end;
+
+ val _ = trace " Proving dis_stricts...";
+ val dis_stricts = map dis_strict cons;
+ val _ = trace " Proving dis_defins...";
+ val dis_defins = map dis_defin cons;
+in
+ val dis_rews = dis_stricts @ dis_defins @ dis_apps;
+end;
+
+local
+ fun mat_strict (con, _) =
+ let
+ val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1];
+ in pg axs_mat_def goal (K tacs) end;
+
+ val _ = trace " Proving mat_stricts...";
+ val mat_stricts = map mat_strict cons;
+
+ fun one_mat c (con, args) =
+ let
+ val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs";
+ val rhs =
+ if con = c
+ then list_ccomb (%:"rhs", map %# args)
+ else mk_fail;
+ val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs_mat_def goal (K tacs) end;
+
+ val _ = trace " Proving mat_apps...";
+ val mat_apps =
+ maps (fn (c,_) => map (one_mat c) cons) cons;
+in
+ val mat_rews = mat_stricts @ mat_apps;
+end;
+
+local
+ fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
+
+ fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
+
+ fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
+ | pat_rhs (con,args) =
+ (mk_branch (mk_ctuple_pat (ps args)))
+ `(%:"rhs")`(mk_ctuple (map %# args));
+
+ fun pat_strict c =
+ let
+ val axs = @{thm branch_def} :: axs_pat_def;
+ val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
+ val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
+ in pg axs goal (K tacs) end;
+
+ fun pat_app c (con, args) =
+ let
+ val axs = @{thm branch_def} :: axs_pat_def;
+ val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
+ val rhs = if con = fst c then pat_rhs c else mk_fail;
+ val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs goal (K tacs) end;
+
+ val _ = trace " Proving pat_stricts...";
+ val pat_stricts = map pat_strict cons;
+ val _ = trace " Proving pat_apps...";
+ val pat_apps = maps (fn c => map (pat_app c) cons) cons;
+in
+ val pat_rews = pat_stricts @ pat_apps;
+end;
+
+local
+ fun con_strict (con, args) =
+ let
+ val rules = abs_strict :: @{thms con_strict_rules};
+ fun one_strict vn =
+ let
+ fun f arg = if vname arg = vn then UU else %# arg;
+ val goal = mk_trp (con_app2 con f args === UU);
+ val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
+ in pg con_appls goal (K tacs) end;
+ in map one_strict (nonlazy args) end;
+
+ fun con_defin (con, args) =
+ let
+ fun iff_disj (t, []) = HOLogic.mk_not t
+ | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
+ val lhs = con_app con args === UU;
+ val rhss = map (fn x => %:x === UU) (nonlazy args);
+ val goal = mk_trp (iff_disj (lhs, rhss));
+ val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
+ val rules = rule1 :: @{thms con_defined_iff_rules};
+ val tacs = [simp_tac (HOL_ss addsimps rules) 1];
+ in pg con_appls goal (K tacs) end;
+in
+ val _ = trace " Proving con_stricts...";
+ val con_stricts = maps con_strict cons;
+ val _ = trace " Proving con_defins...";
+ val con_defins = map con_defin cons;
+ val con_rews = con_stricts @ con_defins;
+end;
+
+local
+ val rules =
+ [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
+ fun con_compact (con, args) =
+ let
+ val concl = mk_trp (mk_compact (con_app con args));
+ val goal = lift (fn x => mk_compact (%#x)) (args, concl);
+ val tacs = [
+ rtac (iso_locale RS iso_compact_abs) 1,
+ REPEAT (resolve_tac rules 1 ORELSE atac 1)];
+ in pg con_appls goal (K tacs) end;
+in
+ val _ = trace " Proving con_compacts...";
+ val con_compacts = map con_compact cons;
+end;
+
+local
+ fun one_sel sel =
+ pg axs_sel_def (mk_trp (strict (%%:sel)))
+ (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
+
+ fun sel_strict (_, args) =
+ List.mapPartial (Option.map one_sel o sel_of) args;
+in
+ val _ = trace " Proving sel_stricts...";
+ val sel_stricts = maps sel_strict cons;
+end;
+
+local
+ fun sel_app_same c n sel (con, args) =
+ let
+ val nlas = nonlazy args;
+ val vns = map vname args;
+ val vnn = List.nth (vns, n);
+ val nlas' = List.filter (fn v => v <> vnn) nlas;
+ val lhs = (%%:sel)`(con_app con args);
+ val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
+ fun tacs1 ctxt =
+ if vnn mem nlas
+ then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
+ else [];
+ val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
+
+ fun sel_app_diff c n sel (con, args) =
+ let
+ val nlas = nonlazy args;
+ val goal = mk_trp (%%:sel ` con_app con args === UU);
+ fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
+ val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
+
+ fun sel_app c n sel (con, args) =
+ if con = c
+ then sel_app_same c n sel (con, args)
+ else sel_app_diff c n sel (con, args);
+
+ fun one_sel c n sel = map (sel_app c n sel) cons;
+ fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
+ fun one_con (c, args) =
+ flat (map_filter I (mapn (one_sel' c) 0 args));
+in
+ val _ = trace " Proving sel_apps...";
+ val sel_apps = maps one_con cons;
+end;
+
+local
+ fun sel_defin sel =
+ let
+ val goal = defined (%:x_name) ==> defined (%%:sel`%x_name);
+ val tacs = [
+ rtac casedist 1,
+ contr_tac 1,
+ DETERM_UNTIL_SOLVED (CHANGED
+ (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
+ in pg [] goal (K tacs) end;
+in
+ val _ = trace " Proving sel_defins...";
+ val sel_defins =
+ if length cons = 1
+ then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
+ (filter_out is_lazy (snd (hd cons)))
+ else [];
+end;
+
+val sel_rews = sel_stricts @ sel_defins @ sel_apps;
+
+val _ = trace " Proving dist_les...";
+val distincts_le =
+ let
+ fun dist (con1, args1) (con2, args2) =
+ let
+ val goal = lift_defined %: (nonlazy args1,
+ mk_trp (con_app con1 args1 ~<< con_app con2 args2));
+ fun tacs ctxt = [
+ rtac @{thm rev_contrapos} 1,
+ eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
+ @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
+ @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
+ in pg [] goal tacs end;
+
+ fun distinct (con1, args1) (con2, args2) =
+ let
+ val arg1 = (con1, args1);
+ val arg2 =
+ (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
+ (args2, Name.variant_list (map vname args1) (map vname args2)));
+ in [dist arg1 arg2, dist arg2 arg1] end;
+ fun distincts [] = []
+ | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
+ in distincts cons end;
+val dist_les = flat (flat distincts_le);
+
+val _ = trace " Proving dist_eqs...";
+val dist_eqs =
+ 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;
+ fun distincts [] = []
+ | distincts ((c,leqs)::cs) =
+ flat
+ (ListPair.map (distinct c) ((map #1 cs),leqs)) @
+ distincts cs;
+ in map standard (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);
+ val concl =
+ foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs));
+ val prem = rel (con_app con largs, con_app con rargs);
+ val sargs = case largs of [_] => [] | _ => nonlazy args;
+ val prop = lift_defined %: (sargs, mk_trp (prem === concl));
+ in pg con_appls prop end;
+ val cons' = List.filter (fn (_,args) => args<>[]) cons;
+in
+ val _ = trace " Proving inverts...";
+ val inverts =
+ let
+ val abs_less = ax_abs_iso RS (allI RS injection_less);
+ val tacs =
+ [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
+ in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
+
+ val _ = trace " Proving injects...";
+ val injects =
+ let
+ val abs_eq = ax_abs_iso RS (allI RS injection_eq);
+ val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
+ in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end;
+end;
+
+(* ----- theorems concerning one induction step ----------------------------- *)
+
+val copy_strict =
+ let
+ val _ = trace " Proving copy_strict...";
+ val goal = mk_trp (strict (dc_copy `% "f"));
+ val rules = [abs_strict, rep_strict] @ @{thms domain_fun_stricts};
+ val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
+ in pg [ax_copy_def] goal (K tacs) end;
+
+local
+ fun copy_app (con, args) =
+ let
+ val lhs = dc_copy`%"f"`(con_app con args);
+ fun one_rhs arg =
+ if DatatypeAux.is_rec_type (dtyp_of arg)
+ then Domain_Axioms.copy_of_dtyp (cproj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
+ else (%# arg);
+ val rhs = con_app2 con one_rhs args;
+ val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
+ val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
+ val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts};
+ fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
+ val rules = [ax_abs_iso] @ @{thms domain_fun_simps};
+ val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
+ in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
+in
+ val _ = trace " Proving copy_apps...";
+ val copy_apps = map copy_app cons;
+end;
+
+local
+ fun one_strict (con, args) =
+ let
+ val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
+ val rews = copy_strict :: copy_apps @ con_rews;
+ fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
+ [asm_simp_tac (HOLCF_ss addsimps rews) 1];
+ in pg [] goal tacs end;
+
+ fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
+in
+ val _ = trace " Proving copy_stricts...";
+ val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
+end;
+
+val copy_rews = copy_strict :: copy_apps @ copy_stricts;
+
+in
+ thy
+ |> Sign.add_path (Long_Name.base_name dname)
+ |> snd o PureThy.add_thmss [
+ ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
+ ((Binding.name "exhaust" , [exhaust] ), []),
+ ((Binding.name "casedist" , [casedist] ), [Induct.cases_type dname]),
+ ((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]),
+ ((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]),
+ ((Binding.name "con_rews" , con_rews ), [Simplifier.simp_add]),
+ ((Binding.name "sel_rews" , sel_rews ), [Simplifier.simp_add]),
+ ((Binding.name "dis_rews" , dis_rews ), [Simplifier.simp_add]),
+ ((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]),
+ ((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]),
+ ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]),
+ ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
+ ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
+ ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]),
+ ((Binding.name "match_rews", mat_rews ), [Simplifier.simp_add])]
+ |> Sign.parent_path
+ |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
+ pat_rews @ dist_les @ dist_eqs @ copy_rews)
+end; (* let *)
+
+fun comp_theorems (comp_dnam, eqs: eq list) thy =
+let
+val global_ctxt = ProofContext.init thy;
+
+val dnames = map (fst o fst) eqs;
+val conss = map snd eqs;
+val comp_dname = Sign.full_bname thy comp_dnam;
+
+val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
+val pg = pg' thy;
+
+(* ----- getting the composite axiom and definitions ------------------------ *)
+
+local
+ fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
+in
+ val axs_reach = map (ga "reach" ) dnames;
+ val axs_take_def = map (ga "take_def" ) dnames;
+ val axs_finite_def = map (ga "finite_def") dnames;
+ val ax_copy2_def = ga "copy_def" comp_dnam;
+ val ax_bisim_def = ga "bisim_def" comp_dnam;
+end;
+
+local
+ fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s);
+ fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
+in
+ val cases = map (gt "casedist" ) dnames;
+ val con_rews = maps (gts "con_rews" ) dnames;
+ val copy_rews = maps (gts "copy_rews") dnames;
+end;
+
+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_Cprod_ss = simpset_of @{theory Fix};
+ val copy_con_rews = copy_rews @ con_rews;
+ val copy_take_defs =
+ (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
+ val _ = trace " Proving take_stricts...";
+ val take_stricts =
+ let
+ fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
+ val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
+ fun tacs ctxt = [
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1,
+ simp_tac iterate_Cprod_ss 1,
+ asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
+ in pg copy_take_defs goal tacs end;
+
+ val take_stricts' = rewrite_rule copy_take_defs take_stricts;
+ fun take_0 n dn =
+ let
+ val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
+ in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
+ val take_0s = mapn take_0 1 dnames;
+ fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
+ val _ = trace " Proving take_apps...";
+ val take_apps =
+ let
+ fun mk_eqn dn (con, args) =
+ let
+ fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
+ fun one_rhs arg =
+ if DatatypeAux.is_rec_type (dtyp_of arg)
+ then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg)
+ else (%# arg);
+ val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
+ val rhs = con_app2 con one_rhs args;
+ in Library.foldr mk_all (map vname args, lhs === rhs) end;
+ fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
+ val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
+ val simps = List.filter (has_fewer_prems 1) copy_rews;
+ fun con_tac ctxt (con, args) =
+ if nonlazy_rec args = []
+ then all_tac
+ else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN
+ asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
+ fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons;
+ fun tacs ctxt =
+ simp_tac iterate_Cprod_ss 1 ::
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
+ simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
+ asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
+ TRY (safe_tac HOL_cs) ::
+ maps (eq_tacs ctxt) eqs;
+ in pg copy_take_defs goal tacs end;
+in
+ val take_rews = map standard
+ (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
+end; (* local *)
+
+local
+ fun one_con p (con,args) =
+ let
+ fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
+ val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
+ val t2 = lift ind_hyp (List.filter is_rec args, t1);
+ val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
+ in Library.foldr mk_All (map vname args, t3) end;
+
+ fun one_eq ((p, cons), concl) =
+ mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
+
+ fun ind_term concf = Library.foldr one_eq
+ (mapn (fn n => fn x => (P_name n, x)) 1 conss,
+ mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
+ val take_ss = HOL_ss addsimps take_rews;
+ fun quant_tac ctxt i = EVERY
+ (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
+
+ fun ind_prems_tac prems = EVERY
+ (maps (fn cons =>
+ (resolve_tac prems 1 ::
+ maps (fn (_,args) =>
+ resolve_tac prems 1 ::
+ map (K(atac 1)) (nonlazy args) @
+ map (K(atac 1)) (List.filter is_rec args))
+ cons))
+ conss);
+ local
+ (* 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, (List.nth(conss,rec_of arg))))
+ ) 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 (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
+ else false;
+ fun lazy_rec_to ns = rec_to exists I 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 (* local *)
+ val _ = trace " Proving finite_ind...";
+ val finite_ind =
+ let
+ fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
+ val goal = ind_term concf;
+
+ fun tacf {prems, context} =
+ let
+ val tacs1 = [
+ quant_tac context 1,
+ simp_tac HOL_ss 1,
+ InductTacs.induct_tac context [[SOME "n"]] 1,
+ simp_tac (take_ss addsimps prems) 1,
+ TRY (safe_tac HOL_cs)];
+ fun arg_tac arg =
+ case_UU_tac context (prems @ con_rews) 1
+ (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
+ fun con_tacs (con, args) =
+ asm_simp_tac take_ss 1 ::
+ map arg_tac (List.filter is_nonlazy_rec args) @
+ [resolve_tac prems 1] @
+ map (K (atac 1)) (nonlazy args) @
+ map (K (etac spec 1)) (List.filter is_rec args);
+ fun cases_tacs (cons, cases) =
+ res_inst_tac context [(("x", 0), "x")] cases 1 ::
+ asm_simp_tac (take_ss addsimps prems) 1 ::
+ maps con_tacs cons;
+ in
+ tacs1 @ maps cases_tacs (conss ~~ cases)
+ end;
+ in pg'' thy [] goal tacf
+ handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI)
+ end;
+
+ val _ = trace " Proving take_lemmas...";
+ val take_lemmas =
+ let
+ fun take_lemma n (dn, ax_reach) =
+ let
+ val lhs = dc_take dn $ Bound 0 `%(x_name n);
+ val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
+ val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
+ val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
+ fun tacf {prems, context} = [
+ res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
+ res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
+ stac fix_def2 1,
+ REPEAT (CHANGED
+ (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
+ stac contlub_cfun_fun 1,
+ stac contlub_cfun_fun 2,
+ rtac lub_equal 3,
+ chain_tac 1,
+ rtac allI 1,
+ resolve_tac prems 1];
+ in pg'' thy axs_take_def goal tacf end;
+ in mapn take_lemma 1 (dnames ~~ axs_reach) end;
+
+(* ----- theorems concerning finiteness and induction ----------------------- *)
+
+ val _ = trace " Proving finites, ind...";
+ val (finites, ind) =
+ (
+ if is_finite
+ then (* finite case *)
+ let
+ fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
+ fun dname_lemma dn =
+ let
+ val prem1 = mk_trp (defined (%:"x"));
+ val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
+ val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
+ val concl = mk_trp (take_enough dn);
+ val goal = prem1 ===> prem2 ===> concl;
+ val tacs = [
+ etac disjE 1,
+ etac notE 1,
+ resolve_tac take_lemmas 1,
+ asm_simp_tac take_ss 1,
+ atac 1];
+ in pg [] goal (K tacs) end;
+ val _ = trace " Proving finite_lemmas1a";
+ val finite_lemmas1a = map dname_lemma dnames;
+
+ val _ = trace " Proving finite_lemma1b";
+ val finite_lemma1b =
+ let
+ fun mk_eqn n ((dn, args), _) =
+ let
+ val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
+ val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
+ in
+ mk_constrainall
+ (x_name n, Type (dn,args), mk_disj (disj1, disj2))
+ end;
+ val goal =
+ mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
+ fun arg_tacs ctxt vn = [
+ eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
+ etac disjE 1,
+ asm_simp_tac (HOL_ss addsimps con_rews) 1,
+ asm_simp_tac take_ss 1];
+ fun con_tacs ctxt (con, args) =
+ asm_simp_tac take_ss 1 ::
+ maps (arg_tacs ctxt) (nonlazy_rec args);
+ fun foo_tacs ctxt n (cons, cases) =
+ simp_tac take_ss 1 ::
+ rtac allI 1 ::
+ res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
+ asm_simp_tac take_ss 1 ::
+ maps (con_tacs ctxt) cons;
+ fun tacs ctxt =
+ rtac allI 1 ::
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
+ simp_tac take_ss 1 ::
+ TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
+ flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
+ in pg [] goal tacs end;
+
+ fun one_finite (dn, l1b) =
+ let
+ val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
+ fun tacs ctxt = [
+ case_UU_tac ctxt 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];
+ in pg axs_finite_def goal tacs end;
+
+ val _ = trace " Proving finites";
+ val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b);
+ val _ = trace " Proving ind";
+ val ind =
+ let
+ fun concf n dn = %:(P_name n) $ %:(x_name n);
+ fun tacf {prems, context} =
+ let
+ fun finite_tacs (finite, fin_ind) = [
+ rtac(rewrite_rule axs_finite_def finite RS exE)1,
+ etac subst 1,
+ rtac fin_ind 1,
+ ind_prems_tac prems];
+ in
+ TRY (safe_tac HOL_cs) ::
+ maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
+ end;
+ in pg'' thy [] (ind_term concf) tacf end;
+ in (finites, ind) end (* let *)
+
+ else (* infinite case *)
+ let
+ fun one_finite n dn =
+ read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
+ val finites = mapn one_finite 1 dnames;
+
+ val goal =
+ let
+ fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
+ fun concf n dn = %:(P_name n) $ %:(x_name n);
+ in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
+ fun tacf {prems, context} =
+ map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
+ quant_tac context 1,
+ rtac (adm_impl_admw RS wfix_ind) 1,
+ REPEAT_DETERM (rtac adm_all 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];
+ val ind = (pg'' thy [] goal tacf
+ handle ERROR _ =>
+ (warning "Cannot prove infinite induction rule"; refl));
+ in (finites, ind) end
+ )
+ handle THM _ =>
+ (warning "Induction proofs failed (THM raised)."; ([], TrueI))
+ | ERROR _ =>
+ (warning "Induction proofs failed (ERROR raised)."; ([], TrueI));
+
+
+end; (* local *)
+
+(* ----- theorem concerning coinduction ------------------------------------- *)
+
+local
+ val xs = mapn (fn n => K (x_name n)) 1 dnames;
+ fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
+ val take_ss = HOL_ss addsimps take_rews;
+ val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
+ val _ = trace " Proving coind_lemma...";
+ val coind_lemma =
+ let
+ fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
+ fun mk_eqn n dn =
+ (dc_take dn $ %:"n" ` bnd_arg n 0) ===
+ (dc_take dn $ %:"n" ` bnd_arg n 1);
+ fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
+ val goal =
+ mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
+ Library.foldr mk_all2 (xs,
+ Library.foldr mk_imp (mapn mk_prj 0 dnames,
+ foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
+ fun x_tacs ctxt n x = [
+ rotate_tac (n+1) 1,
+ etac all2E 1,
+ eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
+ TRY (safe_tac HOL_cs),
+ REPEAT (CHANGED (asm_simp_tac take_ss 1))];
+ fun tacs ctxt = [
+ rtac impI 1,
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1,
+ simp_tac take_ss 1,
+ safe_tac HOL_cs] @
+ flat (mapn (x_tacs ctxt) 0 xs);
+ in pg [ax_bisim_def] goal tacs end;
+in
+ val _ = trace " Proving coind...";
+ val coind =
+ let
+ fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
+ fun mk_eqn x = %:x === %:(x^"'");
+ val goal =
+ mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
+ Logic.list_implies (mapn mk_prj 0 xs,
+ mk_trp (foldr1 mk_conj (map mk_eqn xs)));
+ val tacs =
+ TRY (safe_tac HOL_cs) ::
+ maps (fn take_lemma => [
+ rtac take_lemma 1,
+ cut_facts_tac [coind_lemma] 1,
+ fast_tac HOL_cs 1])
+ take_lemmas;
+ in pg [] goal (K tacs) end;
+end; (* local *)
+
+val inducts = ProjectRule.projections (ProofContext.init thy) ind;
+fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
+val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
+
+in thy |> Sign.add_path comp_dnam
+ |> snd o PureThy.add_thmss [
+ ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]),
+ ((Binding.name "take_lemmas", take_lemmas ), []),
+ ((Binding.name "finites" , finites ), []),
+ ((Binding.name "finite_ind" , [finite_ind]), []),
+ ((Binding.name "ind" , [ind] ), []),
+ ((Binding.name "coind" , [coind] ), [])]
+ |> (if induct_failed then I
+ else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
+ |> Sign.parent_path |> pair take_rews
+end; (* let *)
+end; (* local *)
+end; (* struct *)
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Tue Jul 21 16:14:51 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,235 +0,0 @@
-(* Title: HOLCF/Tools/domain/domain_axioms.ML
- Author: David von Oheimb
-
-Syntax generator for domain command.
-*)
-
-signature DOMAIN_AXIOMS =
-sig
- val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
-
- val calc_axioms :
- string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
- string * (string * term) list * (string * term) list
-
- val add_axioms :
- bstring -> Domain_Library.eq list -> theory -> theory
-end;
-
-
-structure Domain_Axioms :> DOMAIN_AXIOMS =
-struct
-
-open Domain_Library;
-
-infixr 0 ===>;infixr 0 ==>;infix 0 == ;
-infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
-infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
-
-(* FIXME: use theory data for this *)
-val copy_tab : string Symtab.table =
- Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}),
- (@{type_name "++"}, @{const_name "ssum_fun"}),
- (@{type_name "**"}, @{const_name "sprod_fun"}),
- (@{type_name "*"}, @{const_name "cprod_fun"}),
- (@{type_name "u"}, @{const_name "u_fun"})];
-
-fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
-and copy r (DatatypeAux.DtRec i) = r i
- | copy r (DatatypeAux.DtTFree a) = ID
- | copy r (DatatypeAux.DtType (c, ds)) =
- case Symtab.lookup copy_tab c of
- SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds)
- | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
-
-fun calc_axioms
- (comp_dname : string)
- (eqs : eq list)
- (n : int)
- (eqn as ((dname,_),cons) : eq)
- : string * (string * term) list * (string * term) list =
- let
-
- (* ----- 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 dnam = Long_Name.base_name dname;
-
- val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
- val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
-
- val when_def = ("when_def",%%:(dname^"_when") ==
- List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
- Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
-
- val copy_def =
- let fun r i = cproj (Bound 0) eqs i;
- in ("copy_def", %%:(dname^"_copy") ==
- /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end;
-
- (* -- definitions concerning the constructors, discriminators and selectors - *)
-
- fun con_def m n (_,args) = let
- fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
- fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
- fun inj y 1 _ = y
- | inj y _ 0 = mk_sinl y
- | inj y i j = mk_sinr (inj y (i-1) (j-1));
- in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
-
- val con_defs = mapn (fn n => fn (con,args) =>
- (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
-
- val dis_defs = let
- fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
- list_ccomb(%%:(dname^"_when"),map
- (fn (con',args) => (List.foldr /\#
- (if con'=con then TT else FF) args)) cons))
- in map ddef cons end;
-
- val mat_defs =
- let
- fun mdef (con,_) =
- let
- val k = Bound 0
- val x = Bound 1
- fun one_con (con', args') =
- if con'=con then k else List.foldr /\# mk_fail args'
- val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
- val rhs = /\ "x" (/\ "k" (w ` x))
- in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
- in map mdef cons end;
-
- val pat_defs =
- let
- fun pdef (con,args) =
- let
- val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
- val xs = map (bound_arg args) args;
- val r = Bound (length args);
- val rhs = case args of [] => mk_return HOLogic.unit
- | _ => mk_ctuple_pat ps ` mk_ctuple xs;
- fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
- in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) ==
- list_ccomb(%%:(dname^"_when"), map one_con cons))
- end
- in map pdef cons end;
-
- val sel_defs = let
- fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel ==
- list_ccomb(%%:(dname^"_when"),map
- (fn (con',args) => if con'<>con then UU else
- List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
- in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
-
-
- (* ----- axiom and definitions concerning induction ------------------------- *)
-
- val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
- `%x_name === %:x_name));
- val take_def =
- ("take_def",
- %%:(dname^"_take") ==
- mk_lam("n",cproj
- (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
- val finite_def =
- ("finite_def",
- %%:(dname^"_finite") ==
- mk_lam(x_name,
- mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
-
- in (dnam,
- [abs_iso_ax, rep_iso_ax, reach_ax],
- [when_def, copy_def] @
- con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
- [take_def, finite_def])
- end; (* let (calc_axioms) *)
-
-
-(* legacy type inference *)
-
-fun legacy_infer_term thy t =
- singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
-
-fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
-
-fun infer_props thy = map (apsnd (legacy_infer_prop thy));
-
-
-fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
-fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
-
-fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
-fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
-
-fun add_matchers (((dname,_),cons) : eq) thy =
- let
- val con_names = map fst cons;
- val mat_names = map mat_name con_names;
- fun qualify n = Sign.full_name thy (Binding.name n);
- val ms = map qualify con_names ~~ map qualify mat_names;
- in Fixrec.add_matchers ms thy end;
-
-fun add_axioms comp_dnam (eqs : eq list) thy' =
- let
- val comp_dname = Sign.full_bname thy' comp_dnam;
- val dnames = map (fst o fst) eqs;
- val x_name = idx_name dnames "x";
- fun copy_app dname = %%:(dname^"_copy")`Bound 0;
- val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
- /\ "f"(mk_ctuple (map copy_app dnames)));
-
- fun one_con (con,args) = let
- val nonrec_args = filter_out is_rec args;
- val rec_args = List.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)) eqs (rec_of ra) $
- Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
- val capps =
- List.foldr mk_conj
- (mk_conj(
- Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
- Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
- (mapn rel_app 1 rec_args);
- in List.foldr mk_ex
- (Library.foldr mk_conj
- (map (defined o Bound) nonlazy_idxs,capps)) allvns
- end;
- fun one_comp n (_,cons) =
- mk_all(x_name(n+1),
- mk_all(x_name(n+1)^"'",
- mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
- foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
- ::map one_con cons))));
- val bisim_def =
- ("bisim_def",
- %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
-
- fun add_one (thy,(dnam,axs,dfs)) =
- thy |> Sign.add_path dnam
- |> add_defs_infer dfs
- |> add_axioms_infer axs
- |> Sign.parent_path;
-
- val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
-
- in thy |> Sign.add_path comp_dnam
- |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
- |> Sign.parent_path
- |> fold add_matchers eqs
- end; (* let (add_axioms) *)
-
-end; (* struct *)
--- a/src/HOLCF/Tools/domain/domain_extender.ML Tue Jul 21 16:14:51 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,204 +0,0 @@
-(* Title: HOLCF/Tools/domain/domain_extender.ML
- Author: David von Oheimb
-
-Theory extender for domain command, including theory syntax.
-*)
-
-signature DOMAIN_EXTENDER =
-sig
- val add_domain_cmd: string ->
- ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * string) list * mixfix) list) list
- -> theory -> theory
- val add_domain: string ->
- ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * typ) list * mixfix) list) list
- -> theory -> theory
-end;
-
-structure Domain_Extender :> DOMAIN_EXTENDER =
-struct
-
-open Domain_Library;
-
-(* ----- general testing and preprocessing of constructor list -------------- *)
-fun check_and_sort_domain
- (dtnvs : (string * typ list) list)
- (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
- (sg : theory)
- : ((string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list) list =
- let
- val defaultS = Sign.defaultS sg;
- val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
- [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
- val test_dupl_cons =
- (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of
- [] => false | dups => error ("Duplicate constructors: "
- ^ commas_quote dups));
- val test_dupl_sels =
- (case duplicates (op =) (map Binding.name_of (List.mapPartial second
- (List.concat (map second (List.concat cons''))))) of
- [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
- val test_dupl_tvars =
- exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
- [] => false | dups => error("Duplicate type arguments: "
- ^commas_quote dups)) (map snd dtnvs);
- (* test for free type variables, illegal sort constraints on rhs,
- non-pcpo-types and invalid use of recursive type;
- replace sorts in type variables on rhs *)
- fun analyse_equation ((dname,typevars),cons') =
- let
- val tvars = map dest_TFree typevars;
- val distinct_typevars = map TFree tvars;
- fun rm_sorts (TFree(s,_)) = TFree(s,[])
- | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
- | rm_sorts (TVar(s,_)) = TVar(s,[])
- and remove_sorts l = map rm_sorts l;
- val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
- fun analyse indirect (TFree(v,s)) =
- (case AList.lookup (op =) tvars v of
- NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
- | SOME sort => if eq_set_string (s,defaultS) orelse
- eq_set_string (s,sort )
- then TFree(v,sort)
- else error ("Inconsistent sort constraint" ^
- " for type variable " ^ quote v))
- | analyse indirect (t as Type(s,typl)) =
- (case AList.lookup (op =) dtnvs s of
- NONE => if s mem indirect_ok
- then Type(s,map (analyse false) typl)
- else Type(s,map (analyse true) typl)
- | SOME typevars => if indirect
- then error ("Indirect recursion of type " ^
- quote (string_of_typ sg t))
- else if dname <> s orelse
- (** BUG OR FEATURE?:
- mutual recursion may use different arguments **)
- remove_sorts typevars = remove_sorts typl
- then Type(s,map (analyse true) typl)
- else error ("Direct recursion of type " ^
- quote (string_of_typ sg t) ^
- " with different arguments"))
- | analyse indirect (TVar _) = Imposs "extender:analyse";
- fun check_pcpo lazy T =
- let val ok = if lazy then cpo_type else pcpo_type
- in if ok sg T then T else error
- ("Constructor argument type is not of sort pcpo: " ^
- string_of_typ sg T)
- end;
- fun analyse_arg (lazy, sel, T) =
- (lazy, sel, check_pcpo lazy (analyse false T));
- fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
- in ((dname,distinct_typevars), map analyse_con cons') end;
- in ListPair.map analyse_equation (dtnvs,cons'')
- end; (* let *)
-
-(* ----- calls for building new thy and thms -------------------------------- *)
-
-fun gen_add_domain
- (prep_typ : theory -> 'a -> typ)
- (comp_dnam : string)
- (eqs''' : ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * 'a) list * mixfix) list) list)
- (thy''' : theory) =
- let
- fun readS (SOME s) = Syntax.read_sort_global thy''' s
- | readS NONE = Sign.defaultS thy''';
- fun readTFree (a, s) = TFree (a, readS s);
-
- val dtnvs = map (fn (vs,dname:binding,mx,_) =>
- (dname, map readTFree vs, mx)) eqs''';
- val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
- fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
- fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
- val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
- |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
- val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
- val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
- val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list =
- check_and_sort_domain dtnvs' cons'' thy'';
- val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
- val dts = map (Type o fst) eqs';
- val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
- fun typid (Type (id,_)) =
- let val c = hd (Symbol.explode (Long_Name.base_name id))
- in if Symbol.is_letter c then c else "t" end
- | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
- | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
- fun one_con (con,args,mx) =
- ((Syntax.const_name mx (Binding.name_of con)),
- ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
- DatatypeAux.dtyp_of_typ new_dts tp),
- Option.map Binding.name_of sel,vn))
- (args,(mk_var_names(map (typid o third) args)))
- ) : cons;
- val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
- val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
- val ((rewss, take_rews), theorems_thy) =
- thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
- ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
- in
- theorems_thy
- |> Sign.add_path (Long_Name.base_name comp_dnam)
- |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
- |> Sign.parent_path
- end;
-
-val add_domain = gen_add_domain Sign.certify_typ;
-val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
-
-
-(** outer syntax **)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "lazy";
-
-val dest_decl : (bool * binding option * string) parser =
- P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
- (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
- || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
- >> (fn t => (true,NONE,t))
- || P.typ >> (fn t => (false,NONE,t));
-
-val cons_decl =
- P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
-
-val type_var' : (string * string option) parser =
- (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
-
-val type_args' : (string * string option) list parser =
- type_var' >> single ||
- P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
- Scan.succeed [];
-
-val domain_decl =
- (type_args' -- P.binding -- P.opt_infix) --
- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
-
-val domains_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
- P.and_list1 domain_decl;
-
-fun mk_domain (opt_name : string option,
- doms : ((((string * string option) list * binding) * mixfix) *
- ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
- let
- val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
- val specs : ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * string) list * mixfix) list) list =
- map (fn (((vs, t), mx), cons) =>
- (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
- val comp_dnam =
- case opt_name of NONE => space_implode "_" names | SOME s => s;
- in add_domain_cmd comp_dnam specs end;
-
-val _ =
- OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
- (domains_decl >> (Toplevel.theory o mk_domain));
-
-end;
-
-end;
--- a/src/HOLCF/Tools/domain/domain_library.ML Tue Jul 21 16:14:51 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,399 +0,0 @@
-(* Title: HOLCF/Tools/domain/domain_library.ML
- Author: David von Oheimb
-
-Library for domain command.
-*)
-
-
-(* ----- general support ---------------------------------------------------- *)
-
-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 Fail "foldr''"
- | itr [a] = f2 a
- | itr (a::l) = f(a, itr l)
- in itr l end;
-
-fun map_cumulr f start xs =
- List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
- (y::ys,res2)) ([],start) xs;
-
-fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x;
-fun upd_first f (x,y,z) = (f x, y, z);
-fun upd_second f (x,y,z) = ( x, f y, z);
-fun upd_third f (x,y,z) = ( x, y, f z);
-
-fun atomize ctxt thm =
- let
- val r_inst = read_instantiate ctxt;
- 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", 0), "?" ^ s)] spec))
- | _ => [thm];
- in map zero_var_indexes (at thm) end;
-
-(* infix syntax *)
-
-infixr 5 -->;
-infixr 6 ->>;
-infixr 0 ===>;
-infixr 0 ==>;
-infix 0 ==;
-infix 1 ===;
-infix 1 ~=;
-infix 1 <<;
-infix 1 ~<<;
-
-infix 9 ` ;
-infix 9 `% ;
-infix 9 `%%;
-
-
-(* ----- specific support for domain ---------------------------------------- *)
-
-signature DOMAIN_LIBRARY =
-sig
- val Imposs : string -> 'a;
- val cpo_type : theory -> typ -> bool;
- val pcpo_type : theory -> typ -> bool;
- val string_of_typ : theory -> typ -> string;
-
- (* Creating HOLCF types *)
- val mk_cfunT : typ * typ -> typ;
- val ->> : typ * typ -> typ;
- val mk_ssumT : typ * typ -> typ;
- val mk_sprodT : typ * typ -> typ;
- val mk_uT : typ -> typ;
- val oneT : typ;
- val trT : typ;
- val mk_maybeT : typ -> typ;
- val mk_ctupleT : typ list -> typ;
- val mk_TFree : string -> typ;
- val pcpoS : sort;
-
- (* Creating HOLCF terms *)
- val %: : string -> term;
- val %%: : string -> term;
- val ` : term * term -> term;
- val `% : term * string -> term;
- val /\ : string -> term -> term;
- val UU : term;
- val TT : term;
- val FF : term;
- val ID : term;
- val oo : term * term -> term;
- val mk_up : term -> term;
- val mk_sinl : term -> term;
- val mk_sinr : term -> term;
- val mk_stuple : term list -> term;
- val mk_ctuple : term list -> term;
- val mk_fix : term -> term;
- val mk_iterate : term * term * term -> term;
- val mk_fail : term;
- val mk_return : term -> term;
- val cproj : term -> 'a list -> int -> term;
- val list_ccomb : term * term list -> term;
- (*
- val con_app : string -> ('a * 'b * string) list -> term;
- *)
- val con_app2 : string -> ('a -> term) -> 'a list -> term;
- val proj : term -> 'a list -> int -> term;
- val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a;
- val mk_ctuple_pat : term list -> term;
- val mk_branch : term -> term;
-
- (* Creating propositions *)
- val mk_conj : term * term -> term;
- val mk_disj : term * term -> term;
- val mk_imp : term * term -> term;
- val mk_lam : string * term -> term;
- val mk_all : string * term -> term;
- val mk_ex : string * term -> term;
- val mk_constrain : typ * term -> term;
- val mk_constrainall : string * typ * term -> term;
- val === : term * term -> term;
- val << : term * term -> term;
- val ~<< : term * term -> term;
- val strict : term -> term;
- val defined : term -> term;
- val mk_adm : term -> term;
- val mk_compact : term -> term;
- val lift : ('a -> term) -> 'a list * term -> term;
- val lift_defined : ('a -> term) -> 'a list * term -> term;
-
- (* Creating meta-propositions *)
- val mk_trp : term -> term; (* HOLogic.mk_Trueprop *)
- val == : term * term -> term;
- val ===> : term * term -> term;
- val ==> : term * term -> term;
- val mk_All : string * term -> term;
-
- (* Domain specifications *)
- eqtype arg;
- type cons = string * arg list;
- type eq = (string * typ list) * cons list;
- val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
- val is_lazy : arg -> bool;
- val rec_of : arg -> int;
- val dtyp_of : arg -> Datatype.dtyp;
- val sel_of : arg -> string option;
- val vname : arg -> string;
- val upd_vname : (string -> string) -> arg -> arg;
- val is_rec : arg -> bool;
- val is_nonlazy_rec : arg -> bool;
- val nonlazy : arg list -> string list;
- val nonlazy_rec : arg list -> string list;
- val %# : arg -> term;
- val /\# : arg * term -> term;
- val when_body : cons list -> (int * int -> term) -> term;
- val when_funs : 'a list -> string list;
- val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
- val idx_name : 'a list -> string -> int -> string;
- val app_rec_arg : (int -> term) -> arg -> term;
- val con_app : string -> arg list -> term;
- val dtyp_of_eq : eq -> Datatype.dtyp;
-
-
- (* Name mangling *)
- val strip_esc : string -> string;
- val extern_name : string -> string;
- val dis_name : string -> string;
- val mat_name : string -> string;
- val pat_name : string -> string;
- val mk_var_names : string list -> string list;
-end;
-
-structure Domain_Library :> DOMAIN_LIBRARY =
-struct
-
-exception Impossible of string;
-fun Imposs msg = raise Impossible ("Domain:"^msg);
-
-(* ----- name handling ----- *)
-
-val strip_esc =
- let fun strip ("'" :: c :: cs) = c :: strip cs
- | strip ["'"] = []
- | strip (c :: cs) = c :: strip cs
- | strip [] = [];
- in implode o strip o Symbol.explode end;
-
-fun extern_name con =
- case Symbol.explode con of
- ("o"::"p"::" "::rest) => implode rest
- | _ => con;
-fun dis_name con = "is_"^ (extern_name con);
-fun dis_name_ con = "is_"^ (strip_esc con);
-fun mat_name con = "match_"^ (extern_name con);
-fun mat_name_ con = "match_"^ (strip_esc con);
-fun pat_name con = (extern_name con) ^ "_pat";
-fun pat_name_ con = (strip_esc con) ^ "_pat";
-
-(* make distinct names out of the type list,
- forbidding "o","n..","x..","f..","P.." as names *)
-(* a number string is added if necessary *)
-fun mk_var_names ids : string list =
- let
- fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
- fun index_vnames(vn::vns,occupied) =
- (case AList.lookup (op =) occupied vn of
- NONE => if vn mem vns
- then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied)
- else vn :: index_vnames(vns, occupied)
- | SOME(i) => (vn^(string_of_int (i+1)))
- :: index_vnames(vns,(vn,i+1)::occupied))
- | index_vnames([],occupied) = [];
- in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
-
-fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
-fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
-fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
-
-(* ----- constructor list handling ----- *)
-
-type arg =
- (bool * Datatype.dtyp) * (* (lazy, recursive element) *)
- string option * (* selector name *)
- string; (* argument name *)
-
-type cons =
- string * (* operator name of constr *)
- arg 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 mk_arg = I;
-
-fun rec_of ((_,dtyp),_,_) =
- case dtyp of DatatypeAux.DtRec i => i | _ => ~1;
-(* FIXME: what about indirect recursion? *)
-
-fun is_lazy arg = fst (first arg);
-fun dtyp_of arg = snd (first arg);
-val sel_of = second;
-val vname = third;
-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 nonlazy_rec args = map vname (List.filter is_nonlazy_rec args);
-
-
-(* ----- combinators for making dtyps ----- *)
-
-fun mk_uD T = DatatypeAux.DtType(@{type_name "u"}, [T]);
-fun mk_sprodD (T, U) = DatatypeAux.DtType(@{type_name "**"}, [T, U]);
-fun mk_ssumD (T, U) = DatatypeAux.DtType(@{type_name "++"}, [T, U]);
-fun mk_liftD T = DatatypeAux.DtType(@{type_name "lift"}, [T]);
-val unitD = DatatypeAux.DtType(@{type_name "unit"}, []);
-val boolD = DatatypeAux.DtType(@{type_name "bool"}, []);
-val oneD = mk_liftD unitD;
-val trD = mk_liftD boolD;
-fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds;
-fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
-
-fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D;
-fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
-fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
-
-
-(* ----- support for type and mixfix expressions ----- *)
-
-fun mk_uT T = Type(@{type_name "u"}, [T]);
-fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
-fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
-fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
-val oneT = @{typ one};
-val trT = @{typ tr};
-
-val op ->> = mk_cfunT;
-
-fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});
-
-(* ----- support for term expressions ----- *)
-
-fun %: s = Free(s,dummyT);
-fun %# arg = %:(vname arg);
-fun %%: s = Const(s,dummyT);
-
-local open HOLogic in
-val mk_trp = mk_Trueprop;
-fun mk_conj (S,T) = conj $ S $ T;
-fun mk_disj (S,T) = disj $ S $ T;
-fun mk_imp (S,T) = imp $ S $ T;
-fun mk_lam (x,T) = Abs(x,dummyT,T);
-fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
-fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-val mk_constrain = uncurry TypeInfer.constrain;
-fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
-end
-
-fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
-
-infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T;
-infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T;
-infix 0 ==; fun S == T = %%:"==" $ S $ T;
-infix 1 ===; fun S === T = %%:"op =" $ S $ T;
-infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
-infix 1 <<; fun S << T = %%: @{const_name Porder.below} $ S $ T;
-infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T);
-
-infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
-infix 9 `% ; fun f`% s = f` %: s;
-infix 9 `%%; fun f`%%s = f` %%:s;
-
-fun mk_adm t = %%: @{const_name adm} $ t;
-fun mk_compact t = %%: @{const_name compact} $ t;
-val ID = %%: @{const_name ID};
-fun mk_strictify t = %%: @{const_name strictify}`t;
-fun mk_cfst t = %%: @{const_name cfst}`t;
-fun mk_csnd t = %%: @{const_name csnd}`t;
-(*val csplitN = "Cprod.csplit";*)
-(*val sfstN = "Sprod.sfst";*)
-(*val ssndN = "Sprod.ssnd";*)
-fun mk_ssplit t = %%: @{const_name ssplit}`t;
-fun mk_sinl t = %%: @{const_name sinl}`t;
-fun mk_sinr t = %%: @{const_name sinr}`t;
-fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y;
-fun mk_up t = %%: @{const_name up}`t;
-fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u;
-val ONE = @{term ONE};
-val TT = @{term TT};
-val FF = @{term FF};
-fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z;
-fun mk_fix t = %%: @{const_name fix}`t;
-fun mk_return t = %%: @{const_name Fixrec.return}`t;
-val mk_fail = %%: @{const_name Fixrec.fail};
-
-fun mk_branch t = %%: @{const_name Fixrec.branch} $ t;
-
-val pcpoS = @{sort pcpo};
-
-val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *)
-fun con_app2 con f args = list_ccomb(%%:con,map f args);
-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) I (%# arg);
-fun prj _ _ x ( _::[]) _ = x
- | prj f1 _ x (_::y::ys) 0 = f1 x y
- | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
-fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
-fun cproj x = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x;
-fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
-
-fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T);
-fun /\# (arg,T) = /\ (vname arg) T;
-infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T;
-val UU = %%: @{const_name UU};
-fun strict f = f`UU === UU;
-fun defined t = t ~= UU;
-fun cpair (t,u) = %%: @{const_name cpair}`t`u;
-fun spair (t,u) = %%: @{const_name spair}`t`u;
-fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
- | mk_ctuple ts = foldr1 cpair ts;
-fun mk_stuple [] = ONE
- | mk_stuple ts = foldr1 spair ts;
-fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *)
- | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
-fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
-fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
-val mk_ctuple_pat = foldr1 cpair_pat;
-fun lift_defined f = lift (fn x => defined (f x));
-fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
-
-fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) =
- (case cont_eta_contract body of
- body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) =>
- if not (0 mem loose_bnos f) then incr_boundvars ~1 f
- else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')
- | body' => Const("Cfun.Abs_CFun",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 when_funs cons = if length cons = 1 then ["f"]
- 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 t => mk_fup (ID, t))
- else I) (Bound(l2-m));
- in cont_eta_contract
- (foldr''
- (fn (a,t) => mk_ssplit (/\# (a,t)))
- (args,
- fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
- ) end;
- in (if length cons = 1 andalso length(snd(hd cons)) <= 1
- then mk_strictify else I)
- (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
-
-end; (* struct *)
--- a/src/HOLCF/Tools/domain/domain_syntax.ML Tue Jul 21 16:14:51 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,181 +0,0 @@
-(* Title: HOLCF/Tools/domain/domain_syntax.ML
- Author: David von Oheimb
-
-Syntax generator for domain command.
-*)
-
-signature DOMAIN_SYNTAX =
-sig
- val calc_syntax:
- typ ->
- (string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list ->
- (binding * typ * mixfix) list * ast Syntax.trrule list
-
- val add_syntax:
- string ->
- ((string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list) list ->
- theory -> theory
-end;
-
-
-structure Domain_Syntax :> DOMAIN_SYNTAX =
-struct
-
-open Domain_Library;
-infixr 5 -->; infixr 6 ->>;
-
-fun calc_syntax
- (dtypeprod : typ)
- ((dname : string, typevars : typ list),
- (cons': (binding * (bool * binding option * typ) list * mixfix) list))
- : (binding * typ * mixfix) list * ast Syntax.trrule list =
- let
- (* ----- constants concerning the isomorphism ------------------------------- *)
-
- local
- fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
- fun prod (_,args,_) = case args of [] => oneT
- | _ => foldr1 mk_sprodT (map opt_lazy args);
- fun freetvar s = let val tvar = mk_TFree s in
- if tvar mem typevars then freetvar ("t"^s) else tvar end;
- fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
- in
- val dtype = Type(dname,typevars);
- val dtype2 = foldr1 mk_ssumT (map prod cons');
- val dnam = Long_Name.base_name dname;
- fun dbind s = Binding.name (dnam ^ s);
- val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn);
- val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn);
- val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
- val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
- end;
-
- (* ----- constants concerning constructors, discriminators, and selectors --- *)
-
- 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 Symbol.explode end;
- fun dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con));
- fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con));
- fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
- fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx);
- fun dis (con,args,mx) = (dis_name_ con, dtype->>trT,
- Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
- (* strictly speaking, these constants have one argument,
- but the mixfix (without arguments) is introduced only
- to generate parse rules for non-alphanumeric names*)
- fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in
- if tvar mem typevars then freetvar ("t"^s) n else tvar end;
- fun mk_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
- fun mat (con,args,mx) = (mat_name_ con,
- mk_matT(dtype, map third args, freetvar "t" 1),
- Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
- fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
- fun sel (con,args,mx) = List.mapPartial sel1 args;
- fun mk_patT (a,b) = a ->> mk_maybeT b;
- fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
- fun pat (con,args,mx) = (pat_name_ con,
- (mapn pat_arg_typ 1 args)
- --->
- mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
- Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
-
- in
- val consts_con = map con cons';
- val consts_dis = map dis cons';
- val consts_mat = map mat cons';
- val consts_pat = map pat cons';
- val consts_sel = List.concat(map sel cons');
- end;
-
- (* ----- constants concerning induction ------------------------------------- *)
-
- val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
- val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
-
- (* ----- case translation --------------------------------------------------- *)
-
- local open Syntax in
- local
- fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
- fun expvar n = Variable ("e"^(string_of_int n));
- fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
- (string_of_int m));
- fun argvars n args = mapn (argvar n) 1 args;
- fun app s (l,r) = mk_appl (Constant s) [l,r];
- val cabs = app "_cabs";
- val capp = app "Rep_CFun";
- fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
- fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
- fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
- fun when1 n m = if n = m then arg1 n else K (Constant "UU");
-
- fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
- fun app_pat x = mk_appl (Constant "_pat") [x];
- fun args_list [] = Constant "_noargs"
- | args_list xs = foldr1 (app "_args") xs;
- in
- val case_trans =
- ParsePrintRule
- (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
- capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
-
- fun one_abscon_trans n (con,mx,args) =
- ParsePrintRule
- (cabs (con1 n (con,mx,args), expvar n),
- Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'));
- val abscon_trans = mapn one_abscon_trans 1 cons';
-
- fun one_case_trans (con,args,mx) =
- let
- val cname = c_ast con mx;
- val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
- val ns = 1 upto length args;
- val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
- val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
- val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
- in
- [ParseRule (app_pat (Library.foldl capp (cname, xs)),
- mk_appl pname (map app_pat xs)),
- ParseRule (app_var (Library.foldl capp (cname, xs)),
- app_var (args_list xs)),
- PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
- app "_match" (mk_appl pname ps, args_list vs))]
- end;
- val Case_trans = List.concat (map one_case_trans cons');
- end;
- end;
-
- in ([const_rep, const_abs, const_when, const_copy] @
- consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
- [const_take, const_finite],
- (case_trans::(abscon_trans @ Case_trans)))
- end; (* let *)
-
-(* ----- putting all the syntax stuff together ------------------------------ *)
-
-fun add_syntax
- (comp_dnam : string)
- (eqs' : ((string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list) list)
- (thy'' : theory) =
- let
- val dtypes = map (Type o fst) eqs';
- val boolT = HOLogic.boolT;
- val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
- val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
- val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
- val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
- val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
- in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @
- (if length eqs'>1 then [const_copy] else[])@
- [const_bisim])
- |> Sign.add_trrules_i (List.concat(map snd ctt))
- end; (* let *)
-
-end; (* struct *)
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Jul 21 16:14:51 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1054 +0,0 @@
-(* Title: HOLCF/Tools/domain/domain_theorems.ML
- ID: $Id$
- Author: David von Oheimb
- New proofs/tactics by Brian Huffman
-
-Proof generator for domain command.
-*)
-
-val HOLCF_ss = @{simpset};
-
-signature DOMAIN_THEOREMS =
-sig
- val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
- val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
- val quiet_mode: bool ref;
- val trace_domain: bool ref;
-end;
-
-structure Domain_Theorems :> DOMAIN_THEOREMS =
-struct
-
-val quiet_mode = ref false;
-val trace_domain = ref false;
-
-fun message s = if !quiet_mode then () else writeln s;
-fun trace s = if !trace_domain then tracing s else ();
-
-local
-
-val adm_impl_admw = @{thm adm_impl_admw};
-val adm_all = @{thm adm_all};
-val adm_conj = @{thm adm_conj};
-val adm_subst = @{thm adm_subst};
-val antisym_less_inverse = @{thm below_antisym_inverse};
-val beta_cfun = @{thm beta_cfun};
-val cfun_arg_cong = @{thm cfun_arg_cong};
-val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
-val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR};
-val chain_iterate = @{thm chain_iterate};
-val compact_ONE = @{thm compact_ONE};
-val compact_sinl = @{thm compact_sinl};
-val compact_sinr = @{thm compact_sinr};
-val compact_spair = @{thm compact_spair};
-val compact_up = @{thm compact_up};
-val contlub_cfun_arg = @{thm contlub_cfun_arg};
-val contlub_cfun_fun = @{thm contlub_cfun_fun};
-val fix_def2 = @{thm fix_def2};
-val injection_eq = @{thm injection_eq};
-val injection_less = @{thm injection_below};
-val lub_equal = @{thm lub_equal};
-val monofun_cfun_arg = @{thm monofun_cfun_arg};
-val retraction_strict = @{thm retraction_strict};
-val spair_eq = @{thm spair_eq};
-val spair_less = @{thm spair_below};
-val sscase1 = @{thm sscase1};
-val ssplit1 = @{thm ssplit1};
-val strictify1 = @{thm strictify1};
-val wfix_ind = @{thm wfix_ind};
-
-val iso_intro = @{thm iso.intro};
-val iso_abs_iso = @{thm iso.abs_iso};
-val iso_rep_iso = @{thm iso.rep_iso};
-val iso_abs_strict = @{thm iso.abs_strict};
-val iso_rep_strict = @{thm iso.rep_strict};
-val iso_abs_defin' = @{thm iso.abs_defin'};
-val iso_rep_defin' = @{thm iso.rep_defin'};
-val iso_abs_defined = @{thm iso.abs_defined};
-val iso_rep_defined = @{thm iso.rep_defined};
-val iso_compact_abs = @{thm iso.compact_abs};
-val iso_compact_rep = @{thm iso.compact_rep};
-val iso_iso_swap = @{thm iso.iso_swap};
-
-val exh_start = @{thm exh_start};
-val ex_defined_iffs = @{thms ex_defined_iffs};
-val exh_casedist0 = @{thm exh_casedist0};
-val exh_casedists = @{thms exh_casedists};
-
-open Domain_Library;
-infixr 0 ===>;
-infixr 0 ==>;
-infix 0 == ;
-infix 1 ===;
-infix 1 ~= ;
-infix 1 <<;
-infix 1 ~<<;
-infix 9 ` ;
-infix 9 `% ;
-infix 9 `%%;
-infixr 9 oo;
-
-(* ----- general proof facilities ------------------------------------------- *)
-
-fun legacy_infer_term thy t =
- let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
- in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end;
-
-fun pg'' thy defs t tacs =
- let
- val t' = legacy_infer_term thy t;
- val asms = Logic.strip_imp_prems t';
- val prop = Logic.strip_imp_concl t';
- fun tac {prems, context} =
- rewrite_goals_tac defs THEN
- EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
- in Goal.prove_global thy [] asms prop tac end;
-
-fun pg' thy defs t tacsf =
- let
- fun tacs {prems, context} =
- if null prems then tacsf context
- else cut_facts_tac prems 1 :: tacsf context;
- in pg'' thy defs t tacs end;
-
-fun case_UU_tac ctxt rews i v =
- InductTacs.case_tac ctxt (v^"=UU") i THEN
- asm_simp_tac (HOLCF_ss addsimps rews) i;
-
-val chain_tac =
- REPEAT_DETERM o resolve_tac
- [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL];
-
-(* ----- general proofs ----------------------------------------------------- *)
-
-val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
-
-val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)}
-
-in
-
-fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
-let
-
-val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
-val pg = pg' thy;
-
-(* ----- getting the axioms and definitions --------------------------------- *)
-
-local
- fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
-in
- val ax_abs_iso = ga "abs_iso" dname;
- val ax_rep_iso = ga "rep_iso" dname;
- val ax_when_def = ga "when_def" dname;
- fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname;
- val axs_con_def = map (get_def extern_name) cons;
- val axs_dis_def = map (get_def dis_name) cons;
- val axs_mat_def = map (get_def mat_name) cons;
- val axs_pat_def = map (get_def pat_name) cons;
- val axs_sel_def =
- let
- fun def_of_sel sel = ga (sel^"_def") dname;
- fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
- fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
- in
- maps defs_of_con cons
- end;
- val ax_copy_def = ga "copy_def" dname;
-end; (* local *)
-
-(* ----- theorems concerning the isomorphism -------------------------------- *)
-
-val dc_abs = %%:(dname^"_abs");
-val dc_rep = %%:(dname^"_rep");
-val dc_copy = %%:(dname^"_copy");
-val x_name = "x";
-
-val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
-val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
-val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
-val abs_defin' = iso_locale RS iso_abs_defin';
-val rep_defin' = iso_locale RS iso_rep_defin';
-val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
-
-(* ----- generating beta reduction rules from definitions-------------------- *)
-
-val _ = trace " Proving beta reduction rules...";
-
-local
- fun arglist (Const _ $ Abs (s, _, t)) =
- let
- val (vars,body) = arglist t;
- in (s :: vars, body) end
- | arglist t = ([], t);
- fun bind_fun vars t = Library.foldr mk_All (vars, t);
- fun bound_vars 0 = []
- | bound_vars i = Bound (i-1) :: bound_vars (i - 1);
-in
- fun appl_of_def def =
- let
- val (_ $ con $ lam) = concl_of def;
- val (vars, rhs) = arglist lam;
- val lhs = list_ccomb (con, bound_vars (length vars));
- val appl = bind_fun vars (lhs == rhs);
- val cs = ContProc.cont_thms lam;
- val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
- in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
-end;
-
-val _ = trace "Proving when_appl...";
-val when_appl = appl_of_def ax_when_def;
-val _ = trace "Proving con_appls...";
-val con_appls = map appl_of_def axs_con_def;
-
-local
- fun arg2typ n arg =
- let val t = TVar (("'a", n), pcpoS)
- in (n + 1, if is_lazy arg then mk_uT t else t) end;
-
- fun args2typ n [] = (n, oneT)
- | args2typ n [arg] = arg2typ n arg
- | args2typ n (arg::args) =
- let
- val (n1, t1) = arg2typ n arg;
- val (n2, t2) = args2typ n1 args
- in (n2, mk_sprodT (t1, t2)) end;
-
- fun cons2typ n [] = (n,oneT)
- | cons2typ n [con] = args2typ n (snd con)
- | cons2typ n (con::cons) =
- let
- val (n1, t1) = args2typ n (snd con);
- val (n2, t2) = cons2typ n1 cons
- in (n2, mk_ssumT (t1, t2)) end;
-in
- fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
-end;
-
-local
- val iso_swap = iso_locale RS iso_iso_swap;
- fun one_con (con, args) =
- let
- val vns = map vname args;
- val eqn = %:x_name === con_app2 con %: vns;
- val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
- in Library.foldr mk_ex (vns, conj) end;
-
- val conj_assoc = @{thm conj_assoc};
- val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
- val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
- val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
- val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
-
- (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
- val tacs = [
- rtac disjE 1,
- etac (rep_defin' RS disjI1) 2,
- etac disjI2 2,
- rewrite_goals_tac [mk_meta_eq iso_swap],
- rtac thm3 1];
-in
- val _ = trace " Proving exhaust...";
- val exhaust = pg con_appls (mk_trp exh) (K tacs);
- val _ = trace " Proving casedist...";
- val casedist =
- standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
-end;
-
-local
- fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
- fun bound_fun i _ = Bound (length cons - i);
- val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
-in
- val _ = trace " Proving when_strict...";
- val when_strict =
- let
- val axs = [when_appl, mk_meta_eq rep_strict];
- val goal = bind_fun (mk_trp (strict when_app));
- val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
- in pg axs goal (K tacs) end;
-
- val _ = trace " Proving when_apps...";
- val when_apps =
- let
- fun one_when n (con,args) =
- let
- val axs = when_appl :: con_appls;
- val goal = bind_fun (lift_defined %: (nonlazy args,
- mk_trp (when_app`(con_app con args) ===
- list_ccomb (bound_fun n 0, map %# args))));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
- in pg axs goal (K tacs) end;
- in mapn one_when 1 cons end;
-end;
-val when_rews = when_strict :: when_apps;
-
-(* ----- theorems concerning the constructors, discriminators and selectors - *)
-
-local
- fun dis_strict (con, _) =
- let
- val goal = mk_trp (strict (%%:(dis_name con)));
- in pg axs_dis_def goal (K [rtac when_strict 1]) end;
-
- fun dis_app c (con, args) =
- let
- val lhs = %%:(dis_name c) ` con_app con args;
- val rhs = if con = c then TT else FF;
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_dis_def goal (K tacs) end;
-
- val _ = trace " Proving dis_apps...";
- val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
-
- fun dis_defin (con, args) =
- let
- val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
- val tacs =
- [rtac casedist 1,
- contr_tac 1,
- DETERM_UNTIL_SOLVED (CHANGED
- (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
- in pg [] goal (K tacs) end;
-
- val _ = trace " Proving dis_stricts...";
- val dis_stricts = map dis_strict cons;
- val _ = trace " Proving dis_defins...";
- val dis_defins = map dis_defin cons;
-in
- val dis_rews = dis_stricts @ dis_defins @ dis_apps;
-end;
-
-local
- fun mat_strict (con, _) =
- let
- val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
- val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1];
- in pg axs_mat_def goal (K tacs) end;
-
- val _ = trace " Proving mat_stricts...";
- val mat_stricts = map mat_strict cons;
-
- fun one_mat c (con, args) =
- let
- val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs";
- val rhs =
- if con = c
- then list_ccomb (%:"rhs", map %# args)
- else mk_fail;
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_mat_def goal (K tacs) end;
-
- val _ = trace " Proving mat_apps...";
- val mat_apps =
- maps (fn (c,_) => map (one_mat c) cons) cons;
-in
- val mat_rews = mat_stricts @ mat_apps;
-end;
-
-local
- fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
-
- fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
-
- fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
- | pat_rhs (con,args) =
- (mk_branch (mk_ctuple_pat (ps args)))
- `(%:"rhs")`(mk_ctuple (map %# args));
-
- fun pat_strict c =
- let
- val axs = @{thm branch_def} :: axs_pat_def;
- val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
- val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
- in pg axs goal (K tacs) end;
-
- fun pat_app c (con, args) =
- let
- val axs = @{thm branch_def} :: axs_pat_def;
- val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
- val rhs = if con = fst c then pat_rhs c else mk_fail;
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs goal (K tacs) end;
-
- val _ = trace " Proving pat_stricts...";
- val pat_stricts = map pat_strict cons;
- val _ = trace " Proving pat_apps...";
- val pat_apps = maps (fn c => map (pat_app c) cons) cons;
-in
- val pat_rews = pat_stricts @ pat_apps;
-end;
-
-local
- fun con_strict (con, args) =
- let
- val rules = abs_strict :: @{thms con_strict_rules};
- fun one_strict vn =
- let
- fun f arg = if vname arg = vn then UU else %# arg;
- val goal = mk_trp (con_app2 con f args === UU);
- val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
- in pg con_appls goal (K tacs) end;
- in map one_strict (nonlazy args) end;
-
- fun con_defin (con, args) =
- let
- fun iff_disj (t, []) = HOLogic.mk_not t
- | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
- val lhs = con_app con args === UU;
- val rhss = map (fn x => %:x === UU) (nonlazy args);
- val goal = mk_trp (iff_disj (lhs, rhss));
- val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
- val rules = rule1 :: @{thms con_defined_iff_rules};
- val tacs = [simp_tac (HOL_ss addsimps rules) 1];
- in pg con_appls goal (K tacs) end;
-in
- val _ = trace " Proving con_stricts...";
- val con_stricts = maps con_strict cons;
- val _ = trace " Proving con_defins...";
- val con_defins = map con_defin cons;
- val con_rews = con_stricts @ con_defins;
-end;
-
-local
- val rules =
- [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
- fun con_compact (con, args) =
- let
- val concl = mk_trp (mk_compact (con_app con args));
- val goal = lift (fn x => mk_compact (%#x)) (args, concl);
- val tacs = [
- rtac (iso_locale RS iso_compact_abs) 1,
- REPEAT (resolve_tac rules 1 ORELSE atac 1)];
- in pg con_appls goal (K tacs) end;
-in
- val _ = trace " Proving con_compacts...";
- val con_compacts = map con_compact cons;
-end;
-
-local
- fun one_sel sel =
- pg axs_sel_def (mk_trp (strict (%%:sel)))
- (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
-
- fun sel_strict (_, args) =
- List.mapPartial (Option.map one_sel o sel_of) args;
-in
- val _ = trace " Proving sel_stricts...";
- val sel_stricts = maps sel_strict cons;
-end;
-
-local
- fun sel_app_same c n sel (con, args) =
- let
- val nlas = nonlazy args;
- val vns = map vname args;
- val vnn = List.nth (vns, n);
- val nlas' = List.filter (fn v => v <> vnn) nlas;
- val lhs = (%%:sel)`(con_app con args);
- val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
- fun tacs1 ctxt =
- if vnn mem nlas
- then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
- else [];
- val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
-
- fun sel_app_diff c n sel (con, args) =
- let
- val nlas = nonlazy args;
- val goal = mk_trp (%%:sel ` con_app con args === UU);
- fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
- val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
-
- fun sel_app c n sel (con, args) =
- if con = c
- then sel_app_same c n sel (con, args)
- else sel_app_diff c n sel (con, args);
-
- fun one_sel c n sel = map (sel_app c n sel) cons;
- fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
- fun one_con (c, args) =
- flat (map_filter I (mapn (one_sel' c) 0 args));
-in
- val _ = trace " Proving sel_apps...";
- val sel_apps = maps one_con cons;
-end;
-
-local
- fun sel_defin sel =
- let
- val goal = defined (%:x_name) ==> defined (%%:sel`%x_name);
- val tacs = [
- rtac casedist 1,
- contr_tac 1,
- DETERM_UNTIL_SOLVED (CHANGED
- (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
- in pg [] goal (K tacs) end;
-in
- val _ = trace " Proving sel_defins...";
- val sel_defins =
- if length cons = 1
- then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
- (filter_out is_lazy (snd (hd cons)))
- else [];
-end;
-
-val sel_rews = sel_stricts @ sel_defins @ sel_apps;
-
-val _ = trace " Proving dist_les...";
-val distincts_le =
- let
- fun dist (con1, args1) (con2, args2) =
- let
- val goal = lift_defined %: (nonlazy args1,
- mk_trp (con_app con1 args1 ~<< con_app con2 args2));
- fun tacs ctxt = [
- rtac @{thm rev_contrapos} 1,
- eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
- @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
- @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
- in pg [] goal tacs end;
-
- fun distinct (con1, args1) (con2, args2) =
- let
- val arg1 = (con1, args1);
- val arg2 =
- (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
- (args2, Name.variant_list (map vname args1) (map vname args2)));
- in [dist arg1 arg2, dist arg2 arg1] end;
- fun distincts [] = []
- | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
- in distincts cons end;
-val dist_les = flat (flat distincts_le);
-
-val _ = trace " Proving dist_eqs...";
-val dist_eqs =
- 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;
- fun distincts [] = []
- | distincts ((c,leqs)::cs) =
- flat
- (ListPair.map (distinct c) ((map #1 cs),leqs)) @
- distincts cs;
- in map standard (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);
- val concl =
- foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs));
- val prem = rel (con_app con largs, con_app con rargs);
- val sargs = case largs of [_] => [] | _ => nonlazy args;
- val prop = lift_defined %: (sargs, mk_trp (prem === concl));
- in pg con_appls prop end;
- val cons' = List.filter (fn (_,args) => args<>[]) cons;
-in
- val _ = trace " Proving inverts...";
- val inverts =
- let
- val abs_less = ax_abs_iso RS (allI RS injection_less);
- val tacs =
- [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
- in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
-
- val _ = trace " Proving injects...";
- val injects =
- let
- val abs_eq = ax_abs_iso RS (allI RS injection_eq);
- val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
- in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end;
-end;
-
-(* ----- theorems concerning one induction step ----------------------------- *)
-
-val copy_strict =
- let
- val _ = trace " Proving copy_strict...";
- val goal = mk_trp (strict (dc_copy `% "f"));
- val rules = [abs_strict, rep_strict] @ @{thms domain_fun_stricts};
- val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
- in pg [ax_copy_def] goal (K tacs) end;
-
-local
- fun copy_app (con, args) =
- let
- val lhs = dc_copy`%"f"`(con_app con args);
- fun one_rhs arg =
- if DatatypeAux.is_rec_type (dtyp_of arg)
- then Domain_Axioms.copy_of_dtyp (cproj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
- else (%# arg);
- val rhs = con_app2 con one_rhs args;
- val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
- val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
- val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts};
- fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
- val rules = [ax_abs_iso] @ @{thms domain_fun_simps};
- val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
- in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
-in
- val _ = trace " Proving copy_apps...";
- val copy_apps = map copy_app cons;
-end;
-
-local
- fun one_strict (con, args) =
- let
- val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
- val rews = copy_strict :: copy_apps @ con_rews;
- fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
- [asm_simp_tac (HOLCF_ss addsimps rews) 1];
- in pg [] goal tacs end;
-
- fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
-in
- val _ = trace " Proving copy_stricts...";
- val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
-end;
-
-val copy_rews = copy_strict :: copy_apps @ copy_stricts;
-
-in
- thy
- |> Sign.add_path (Long_Name.base_name dname)
- |> snd o PureThy.add_thmss [
- ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
- ((Binding.name "exhaust" , [exhaust] ), []),
- ((Binding.name "casedist" , [casedist] ), [Induct.cases_type dname]),
- ((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]),
- ((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]),
- ((Binding.name "con_rews" , con_rews ), [Simplifier.simp_add]),
- ((Binding.name "sel_rews" , sel_rews ), [Simplifier.simp_add]),
- ((Binding.name "dis_rews" , dis_rews ), [Simplifier.simp_add]),
- ((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]),
- ((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]),
- ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]),
- ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
- ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
- ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]),
- ((Binding.name "match_rews", mat_rews ), [Simplifier.simp_add])]
- |> Sign.parent_path
- |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
- pat_rews @ dist_les @ dist_eqs @ copy_rews)
-end; (* let *)
-
-fun comp_theorems (comp_dnam, eqs: eq list) thy =
-let
-val global_ctxt = ProofContext.init thy;
-
-val dnames = map (fst o fst) eqs;
-val conss = map snd eqs;
-val comp_dname = Sign.full_bname thy comp_dnam;
-
-val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
-val pg = pg' thy;
-
-(* ----- getting the composite axiom and definitions ------------------------ *)
-
-local
- fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
-in
- val axs_reach = map (ga "reach" ) dnames;
- val axs_take_def = map (ga "take_def" ) dnames;
- val axs_finite_def = map (ga "finite_def") dnames;
- val ax_copy2_def = ga "copy_def" comp_dnam;
- val ax_bisim_def = ga "bisim_def" comp_dnam;
-end;
-
-local
- fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s);
- fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
-in
- val cases = map (gt "casedist" ) dnames;
- val con_rews = maps (gts "con_rews" ) dnames;
- val copy_rews = maps (gts "copy_rews") dnames;
-end;
-
-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_Cprod_ss = simpset_of @{theory Fix};
- val copy_con_rews = copy_rews @ con_rews;
- val copy_take_defs =
- (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
- val _ = trace " Proving take_stricts...";
- val take_stricts =
- let
- fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
- val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
- fun tacs ctxt = [
- InductTacs.induct_tac ctxt [[SOME "n"]] 1,
- simp_tac iterate_Cprod_ss 1,
- asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
- in pg copy_take_defs goal tacs end;
-
- val take_stricts' = rewrite_rule copy_take_defs take_stricts;
- fun take_0 n dn =
- let
- val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
- in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
- val take_0s = mapn take_0 1 dnames;
- fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
- val _ = trace " Proving take_apps...";
- val take_apps =
- let
- fun mk_eqn dn (con, args) =
- let
- fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
- fun one_rhs arg =
- if DatatypeAux.is_rec_type (dtyp_of arg)
- then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg)
- else (%# arg);
- val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
- val rhs = con_app2 con one_rhs args;
- in Library.foldr mk_all (map vname args, lhs === rhs) end;
- fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
- val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
- val simps = List.filter (has_fewer_prems 1) copy_rews;
- fun con_tac ctxt (con, args) =
- if nonlazy_rec args = []
- then all_tac
- else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN
- asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
- fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons;
- fun tacs ctxt =
- simp_tac iterate_Cprod_ss 1 ::
- InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
- simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
- asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
- TRY (safe_tac HOL_cs) ::
- maps (eq_tacs ctxt) eqs;
- in pg copy_take_defs goal tacs end;
-in
- val take_rews = map standard
- (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
-end; (* local *)
-
-local
- fun one_con p (con,args) =
- let
- fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
- val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
- val t2 = lift ind_hyp (List.filter is_rec args, t1);
- val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
- in Library.foldr mk_All (map vname args, t3) end;
-
- fun one_eq ((p, cons), concl) =
- mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
-
- fun ind_term concf = Library.foldr one_eq
- (mapn (fn n => fn x => (P_name n, x)) 1 conss,
- mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
- val take_ss = HOL_ss addsimps take_rews;
- fun quant_tac ctxt i = EVERY
- (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
-
- fun ind_prems_tac prems = EVERY
- (maps (fn cons =>
- (resolve_tac prems 1 ::
- maps (fn (_,args) =>
- resolve_tac prems 1 ::
- map (K(atac 1)) (nonlazy args) @
- map (K(atac 1)) (List.filter is_rec args))
- cons))
- conss);
- local
- (* 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, (List.nth(conss,rec_of arg))))
- ) 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 (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
- else false;
- fun lazy_rec_to ns = rec_to exists I 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 (* local *)
- val _ = trace " Proving finite_ind...";
- val finite_ind =
- let
- fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
- val goal = ind_term concf;
-
- fun tacf {prems, context} =
- let
- val tacs1 = [
- quant_tac context 1,
- simp_tac HOL_ss 1,
- InductTacs.induct_tac context [[SOME "n"]] 1,
- simp_tac (take_ss addsimps prems) 1,
- TRY (safe_tac HOL_cs)];
- fun arg_tac arg =
- case_UU_tac context (prems @ con_rews) 1
- (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
- fun con_tacs (con, args) =
- asm_simp_tac take_ss 1 ::
- map arg_tac (List.filter is_nonlazy_rec args) @
- [resolve_tac prems 1] @
- map (K (atac 1)) (nonlazy args) @
- map (K (etac spec 1)) (List.filter is_rec args);
- fun cases_tacs (cons, cases) =
- res_inst_tac context [(("x", 0), "x")] cases 1 ::
- asm_simp_tac (take_ss addsimps prems) 1 ::
- maps con_tacs cons;
- in
- tacs1 @ maps cases_tacs (conss ~~ cases)
- end;
- in pg'' thy [] goal tacf
- handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI)
- end;
-
- val _ = trace " Proving take_lemmas...";
- val take_lemmas =
- let
- fun take_lemma n (dn, ax_reach) =
- let
- val lhs = dc_take dn $ Bound 0 `%(x_name n);
- val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
- val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
- val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
- fun tacf {prems, context} = [
- res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
- res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
- stac fix_def2 1,
- REPEAT (CHANGED
- (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
- stac contlub_cfun_fun 1,
- stac contlub_cfun_fun 2,
- rtac lub_equal 3,
- chain_tac 1,
- rtac allI 1,
- resolve_tac prems 1];
- in pg'' thy axs_take_def goal tacf end;
- in mapn take_lemma 1 (dnames ~~ axs_reach) end;
-
-(* ----- theorems concerning finiteness and induction ----------------------- *)
-
- val _ = trace " Proving finites, ind...";
- val (finites, ind) =
- (
- if is_finite
- then (* finite case *)
- let
- fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
- fun dname_lemma dn =
- let
- val prem1 = mk_trp (defined (%:"x"));
- val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
- val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
- val concl = mk_trp (take_enough dn);
- val goal = prem1 ===> prem2 ===> concl;
- val tacs = [
- etac disjE 1,
- etac notE 1,
- resolve_tac take_lemmas 1,
- asm_simp_tac take_ss 1,
- atac 1];
- in pg [] goal (K tacs) end;
- val _ = trace " Proving finite_lemmas1a";
- val finite_lemmas1a = map dname_lemma dnames;
-
- val _ = trace " Proving finite_lemma1b";
- val finite_lemma1b =
- let
- fun mk_eqn n ((dn, args), _) =
- let
- val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
- val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
- in
- mk_constrainall
- (x_name n, Type (dn,args), mk_disj (disj1, disj2))
- end;
- val goal =
- mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
- fun arg_tacs ctxt vn = [
- eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
- etac disjE 1,
- asm_simp_tac (HOL_ss addsimps con_rews) 1,
- asm_simp_tac take_ss 1];
- fun con_tacs ctxt (con, args) =
- asm_simp_tac take_ss 1 ::
- maps (arg_tacs ctxt) (nonlazy_rec args);
- fun foo_tacs ctxt n (cons, cases) =
- simp_tac take_ss 1 ::
- rtac allI 1 ::
- res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
- asm_simp_tac take_ss 1 ::
- maps (con_tacs ctxt) cons;
- fun tacs ctxt =
- rtac allI 1 ::
- InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
- simp_tac take_ss 1 ::
- TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
- flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
- in pg [] goal tacs end;
-
- fun one_finite (dn, l1b) =
- let
- val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
- fun tacs ctxt = [
- case_UU_tac ctxt 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];
- in pg axs_finite_def goal tacs end;
-
- val _ = trace " Proving finites";
- val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b);
- val _ = trace " Proving ind";
- val ind =
- let
- fun concf n dn = %:(P_name n) $ %:(x_name n);
- fun tacf {prems, context} =
- let
- fun finite_tacs (finite, fin_ind) = [
- rtac(rewrite_rule axs_finite_def finite RS exE)1,
- etac subst 1,
- rtac fin_ind 1,
- ind_prems_tac prems];
- in
- TRY (safe_tac HOL_cs) ::
- maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
- end;
- in pg'' thy [] (ind_term concf) tacf end;
- in (finites, ind) end (* let *)
-
- else (* infinite case *)
- let
- fun one_finite n dn =
- read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
- val finites = mapn one_finite 1 dnames;
-
- val goal =
- let
- fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
- fun concf n dn = %:(P_name n) $ %:(x_name n);
- in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
- fun tacf {prems, context} =
- map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
- quant_tac context 1,
- rtac (adm_impl_admw RS wfix_ind) 1,
- REPEAT_DETERM (rtac adm_all 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];
- val ind = (pg'' thy [] goal tacf
- handle ERROR _ =>
- (warning "Cannot prove infinite induction rule"; refl));
- in (finites, ind) end
- )
- handle THM _ =>
- (warning "Induction proofs failed (THM raised)."; ([], TrueI))
- | ERROR _ =>
- (warning "Induction proofs failed (ERROR raised)."; ([], TrueI));
-
-
-end; (* local *)
-
-(* ----- theorem concerning coinduction ------------------------------------- *)
-
-local
- val xs = mapn (fn n => K (x_name n)) 1 dnames;
- fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
- val take_ss = HOL_ss addsimps take_rews;
- val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
- val _ = trace " Proving coind_lemma...";
- val coind_lemma =
- let
- fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
- fun mk_eqn n dn =
- (dc_take dn $ %:"n" ` bnd_arg n 0) ===
- (dc_take dn $ %:"n" ` bnd_arg n 1);
- fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
- val goal =
- mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
- Library.foldr mk_all2 (xs,
- Library.foldr mk_imp (mapn mk_prj 0 dnames,
- foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
- fun x_tacs ctxt n x = [
- rotate_tac (n+1) 1,
- etac all2E 1,
- eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
- TRY (safe_tac HOL_cs),
- REPEAT (CHANGED (asm_simp_tac take_ss 1))];
- fun tacs ctxt = [
- rtac impI 1,
- InductTacs.induct_tac ctxt [[SOME "n"]] 1,
- simp_tac take_ss 1,
- safe_tac HOL_cs] @
- flat (mapn (x_tacs ctxt) 0 xs);
- in pg [ax_bisim_def] goal tacs end;
-in
- val _ = trace " Proving coind...";
- val coind =
- let
- fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
- fun mk_eqn x = %:x === %:(x^"'");
- val goal =
- mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
- Logic.list_implies (mapn mk_prj 0 xs,
- mk_trp (foldr1 mk_conj (map mk_eqn xs)));
- val tacs =
- TRY (safe_tac HOL_cs) ::
- maps (fn take_lemma => [
- rtac take_lemma 1,
- cut_facts_tac [coind_lemma] 1,
- fast_tac HOL_cs 1])
- take_lemmas;
- in pg [] goal (K tacs) end;
-end; (* local *)
-
-val inducts = ProjectRule.projections (ProofContext.init thy) ind;
-fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
-val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
-
-in thy |> Sign.add_path comp_dnam
- |> snd o PureThy.add_thmss [
- ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]),
- ((Binding.name "take_lemmas", take_lemmas ), []),
- ((Binding.name "finites" , finites ), []),
- ((Binding.name "finite_ind" , [finite_ind]), []),
- ((Binding.name "ind" , [ind] ), []),
- ((Binding.name "coind" , [coind] ), [])]
- |> (if induct_failed then I
- else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
- |> Sign.parent_path |> pair take_rews
-end; (* let *)
-end; (* local *)
-end; (* struct *)