# HG changeset patch # User huffman # Date 1287525711 25200 # Node ID 3adb92ee2f2213cac89934e475f6bbfefb7e2ca7 # Parent 391746914dba9daee54ef519bbd513e62fcfa2a6 rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML diff -r 391746914dba -r 3adb92ee2f22 src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Tue Oct 19 14:28:14 2010 -0700 +++ b/src/HOLCF/Domain.thy Tue Oct 19 15:01:51 2010 -0700 @@ -11,8 +11,8 @@ ("Tools/cont_proc.ML") ("Tools/Domain/domain_constructors.ML") ("Tools/Domain/domain_axioms.ML") - ("Tools/Domain/domain_theorems.ML") - ("Tools/Domain/domain_extender.ML") + ("Tools/Domain/domain_induction.ML") + ("Tools/Domain/domain.ML") begin default_sort pcpo @@ -113,7 +113,7 @@ use "Tools/cont_proc.ML" use "Tools/Domain/domain_axioms.ML" use "Tools/Domain/domain_constructors.ML" -use "Tools/Domain/domain_theorems.ML" -use "Tools/Domain/domain_extender.ML" +use "Tools/Domain/domain_induction.ML" +use "Tools/Domain/domain.ML" end diff -r 391746914dba -r 3adb92ee2f22 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Tue Oct 19 14:28:14 2010 -0700 +++ b/src/HOLCF/IsaMakefile Tue Oct 19 15:01:51 2010 -0700 @@ -70,12 +70,12 @@ Tools/cont_consts.ML \ Tools/cont_proc.ML \ Tools/holcf_library.ML \ - Tools/Domain/domain_extender.ML \ + Tools/Domain/domain.ML \ Tools/Domain/domain_axioms.ML \ Tools/Domain/domain_constructors.ML \ + Tools/Domain/domain_induction.ML \ Tools/Domain/domain_isomorphism.ML \ Tools/Domain/domain_take_proofs.ML \ - Tools/Domain/domain_theorems.ML \ Tools/fixrec.ML \ Tools/pcpodef.ML \ Tools/repdef.ML \ diff -r 391746914dba -r 3adb92ee2f22 src/HOLCF/Tools/Domain/domain.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain.ML Tue Oct 19 15:01:51 2010 -0700 @@ -0,0 +1,279 @@ + +(* Title: HOLCF/Tools/Domain/domain.ML + Author: David von Oheimb + Author: Brian Huffman + +Theory extender for domain command, including theory syntax. +*) + +signature DOMAIN = +sig + val add_domain_cmd: + binding -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list + -> theory -> theory + + val add_domain: + binding -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list + -> theory -> theory + + val add_new_domain_cmd: + binding -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list + -> theory -> theory + + val add_new_domain: + binding -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list + -> theory -> theory +end; + +structure Domain :> DOMAIN = +struct + +open HOLCF_Library; + +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); + +(* ----- general testing and preprocessing of constructor list -------------- *) +fun check_and_sort_domain + (arg_sort : bool -> sort) + (dtnvs : (string * typ list) list) + (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) + (thy : theory) + : ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list = + let + val defaultS = Sign.defaultS thy; + + val test_dupl_typs = + case duplicates (op =) (map fst dtnvs) of + [] => false | dups => error ("Duplicate types: " ^ commas_quote dups); + + val all_cons = map (Binding.name_of o first) (flat cons''); + val test_dupl_cons = + case duplicates (op =) all_cons of + [] => false | dups => error ("Duplicate constructors: " + ^ commas_quote dups); + val all_sels = + (map Binding.name_of o map_filter second o maps second) (flat cons''); + val test_dupl_sels = + case duplicates (op =) all_sels of + [] => false | dups => error("Duplicate selectors: "^commas_quote dups); + + fun test_dupl_tvars s = + case duplicates (op =) (map(fst o dest_TFree)s) of + [] => false | dups => error("Duplicate type arguments: " + ^commas_quote dups); + val test_dupl_tvars' = exists test_dupl_tvars (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; + 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 (op =) (s, defaultS) orelse + eq_set (op =) (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 => Type (s, map (analyse false) typl) + | SOME typevars => + if indirect + then error ("Indirect recursion of type " ^ + quote (Syntax.string_of_typ_global thy 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 (Syntax.string_of_typ_global thy t) ^ + " with different arguments")) + | analyse indirect (TVar _) = error "extender:analyse"; + fun check_pcpo lazy T = + let val sort = arg_sort lazy in + if Sign.of_sort thy (T, sort) then T + else error ("Constructor argument type is not of sort " ^ + Syntax.string_of_sort_global thy sort ^ ": " ^ + Syntax.string_of_typ_global thy 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 -------------------------------- *) + +type info = + Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info; + +fun gen_add_domain + (prep_typ : theory -> 'a -> typ) + (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory) + (arg_sort : bool -> sort) + (comp_dbind : binding) + (eqs''' : ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * 'a) list * mixfix) list) list) + (thy : theory) = + let + val dtnvs : (binding * typ list * mixfix) list = + let + fun readS (SOME s) = Syntax.read_sort_global thy s + | readS NONE = Sign.defaultS thy; + fun readTFree (a, s) = TFree (a, readS s); + in + map (fn (vs,dname:binding,mx,_) => + (dname, map readTFree vs, mx)) eqs''' + end; + + 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, arg_sort false); + + (* this theory is used just for parsing and error checking *) + val tmp_thy = thy + |> Theory.copy + |> Sign.add_types (map thy_type dtnvs) + |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; + + val dbinds : binding list = + map (fn (_,dbind,_,_) => dbind) eqs'''; + val cons''' : + (binding * (bool * binding option * 'a) list * mixfix) list list = + map (fn (_,_,_,cons) => cons) eqs'''; + val cons'' : + (binding * (bool * binding option * typ) list * mixfix) list list = + map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons'''; + val dtnvs' : (string * typ list) list = + 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 arg_sort dtnvs' cons'' tmp_thy; + val dts : typ list = map (Type o fst) eqs'; + + fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T; + fun mk_con_typ (bind, args, mx) = + if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); + fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); + val repTs : typ list = map mk_eq_typ eqs'; + + val iso_spec : (binding * mixfix * (typ * typ)) list = + map (fn ((dbind, _, mx), eq) => (dbind, mx, eq)) + (dtnvs ~~ (dts ~~ repTs)); + + val ((iso_infos, take_info), thy) = add_isos iso_spec thy; + + val (constr_infos, thy) = + thy + |> fold_map (fn ((dbind, (_,cs)), info) => + Domain_Constructors.add_domain_constructors dbind cs info) + (dbinds ~~ eqs' ~~ iso_infos); + + val (take_rews, thy) = + Domain_Induction.comp_theorems comp_dbind + dbinds take_info constr_infos thy; + in + thy + end; + +fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = + let + fun prep (dbind, mx, (lhsT, rhsT)) = + let val (dname, vs) = dest_Type lhsT; + in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end; + in + Domain_Isomorphism.domain_isomorphism (map prep spec) + end; + +fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo}; +fun rep_arg lazy = @{sort bifinite}; + +val add_domain = + gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg; + +val add_new_domain = + gen_add_domain Sign.certify_typ define_isos rep_arg; + +val add_domain_cmd = + gen_add_domain Syntax.read_typ_global Domain_Axioms.add_axioms pcpo_arg; + +val add_new_domain_cmd = + gen_add_domain Syntax.read_typ_global define_isos rep_arg; + + +(** outer syntax **) + +val _ = Keyword.keyword "lazy"; + +val dest_decl : (bool * binding option * string) parser = + Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false -- + (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1 + || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")" + >> (fn t => (true,NONE,t)) + || Parse.typ >> (fn t => (false,NONE,t)); + +val cons_decl = + Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix; + +val domain_decl = + (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) -- + (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl); + +val domains_decl = + Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") -- + Parse.and_list1 domain_decl; + +fun mk_domain + (definitional : bool) + (opt_name : binding 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_dbind = + case opt_name of NONE => Binding.name (space_implode "_" names) + | SOME s => s; + in + if definitional + then add_new_domain_cmd comp_dbind specs + else add_domain_cmd comp_dbind specs + end; + +val _ = + Outer_Syntax.command "domain" "define recursive domains (HOLCF)" + Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false)); + +val _ = + Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)" + Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true)); + +end; diff -r 391746914dba -r 3adb92ee2f22 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Oct 19 14:28:14 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,278 +0,0 @@ -(* Title: HOLCF/Tools/Domain/domain_extender.ML - Author: David von Oheimb - Author: Brian Huffman - -Theory extender for domain command, including theory syntax. -*) - -signature DOMAIN_EXTENDER = -sig - val add_domain_cmd: - binding -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list - -> theory -> theory - - val add_domain: - binding -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * typ) list * mixfix) list) list - -> theory -> theory - - val add_new_domain_cmd: - binding -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list - -> theory -> theory - - val add_new_domain: - binding -> - ((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 HOLCF_Library; - -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); - -(* ----- general testing and preprocessing of constructor list -------------- *) -fun check_and_sort_domain - (arg_sort : bool -> sort) - (dtnvs : (string * typ list) list) - (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) - (thy : theory) - : ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list = - let - val defaultS = Sign.defaultS thy; - - val test_dupl_typs = - case duplicates (op =) (map fst dtnvs) of - [] => false | dups => error ("Duplicate types: " ^ commas_quote dups); - - val all_cons = map (Binding.name_of o first) (flat cons''); - val test_dupl_cons = - case duplicates (op =) all_cons of - [] => false | dups => error ("Duplicate constructors: " - ^ commas_quote dups); - val all_sels = - (map Binding.name_of o map_filter second o maps second) (flat cons''); - val test_dupl_sels = - case duplicates (op =) all_sels of - [] => false | dups => error("Duplicate selectors: "^commas_quote dups); - - fun test_dupl_tvars s = - case duplicates (op =) (map(fst o dest_TFree)s) of - [] => false | dups => error("Duplicate type arguments: " - ^commas_quote dups); - val test_dupl_tvars' = exists test_dupl_tvars (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; - 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 (op =) (s, defaultS) orelse - eq_set (op =) (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 => Type (s, map (analyse false) typl) - | SOME typevars => - if indirect - then error ("Indirect recursion of type " ^ - quote (Syntax.string_of_typ_global thy 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 (Syntax.string_of_typ_global thy t) ^ - " with different arguments")) - | analyse indirect (TVar _) = error "extender:analyse"; - fun check_pcpo lazy T = - let val sort = arg_sort lazy in - if Sign.of_sort thy (T, sort) then T - else error ("Constructor argument type is not of sort " ^ - Syntax.string_of_sort_global thy sort ^ ": " ^ - Syntax.string_of_typ_global thy 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 -------------------------------- *) - -type info = - Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info; - -fun gen_add_domain - (prep_typ : theory -> 'a -> typ) - (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory) - (arg_sort : bool -> sort) - (comp_dbind : binding) - (eqs''' : ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * 'a) list * mixfix) list) list) - (thy : theory) = - let - val dtnvs : (binding * typ list * mixfix) list = - let - fun readS (SOME s) = Syntax.read_sort_global thy s - | readS NONE = Sign.defaultS thy; - fun readTFree (a, s) = TFree (a, readS s); - in - map (fn (vs,dname:binding,mx,_) => - (dname, map readTFree vs, mx)) eqs''' - end; - - 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, arg_sort false); - - (* this theory is used just for parsing and error checking *) - val tmp_thy = thy - |> Theory.copy - |> Sign.add_types (map thy_type dtnvs) - |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; - - val dbinds : binding list = - map (fn (_,dbind,_,_) => dbind) eqs'''; - val cons''' : - (binding * (bool * binding option * 'a) list * mixfix) list list = - map (fn (_,_,_,cons) => cons) eqs'''; - val cons'' : - (binding * (bool * binding option * typ) list * mixfix) list list = - map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons'''; - val dtnvs' : (string * typ list) list = - 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 arg_sort dtnvs' cons'' tmp_thy; - val dts : typ list = map (Type o fst) eqs'; - - fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T; - fun mk_con_typ (bind, args, mx) = - if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); - fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); - val repTs : typ list = map mk_eq_typ eqs'; - - val iso_spec : (binding * mixfix * (typ * typ)) list = - map (fn ((dbind, _, mx), eq) => (dbind, mx, eq)) - (dtnvs ~~ (dts ~~ repTs)); - - val ((iso_infos, take_info), thy) = add_isos iso_spec thy; - - val (constr_infos, thy) = - thy - |> fold_map (fn ((dbind, (_,cs)), info) => - Domain_Constructors.add_domain_constructors dbind cs info) - (dbinds ~~ eqs' ~~ iso_infos); - - val (take_rews, thy) = - Domain_Theorems.comp_theorems comp_dbind - dbinds take_info constr_infos thy; - in - thy - end; - -fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = - let - fun prep (dbind, mx, (lhsT, rhsT)) = - let val (dname, vs) = dest_Type lhsT; - in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end; - in - Domain_Isomorphism.domain_isomorphism (map prep spec) - end; - -fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo}; -fun rep_arg lazy = @{sort bifinite}; - -val add_domain = - gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg; - -val add_new_domain = - gen_add_domain Sign.certify_typ define_isos rep_arg; - -val add_domain_cmd = - gen_add_domain Syntax.read_typ_global Domain_Axioms.add_axioms pcpo_arg; - -val add_new_domain_cmd = - gen_add_domain Syntax.read_typ_global define_isos rep_arg; - - -(** outer syntax **) - -val _ = Keyword.keyword "lazy"; - -val dest_decl : (bool * binding option * string) parser = - Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false -- - (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1 - || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")" - >> (fn t => (true,NONE,t)) - || Parse.typ >> (fn t => (false,NONE,t)); - -val cons_decl = - Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix; - -val domain_decl = - (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) -- - (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl); - -val domains_decl = - Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") -- - Parse.and_list1 domain_decl; - -fun mk_domain - (definitional : bool) - (opt_name : binding 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_dbind = - case opt_name of NONE => Binding.name (space_implode "_" names) - | SOME s => s; - in - if definitional - then add_new_domain_cmd comp_dbind specs - else add_domain_cmd comp_dbind specs - end; - -val _ = - Outer_Syntax.command "domain" "define recursive domains (HOLCF)" - Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false)); - -val _ = - Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)" - Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true)); - -end; diff -r 391746914dba -r 3adb92ee2f22 src/HOLCF/Tools/Domain/domain_induction.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_induction.ML Tue Oct 19 15:01:51 2010 -0700 @@ -0,0 +1,438 @@ +(* Title: HOLCF/Tools/Domain/domain_induction.ML + Author: David von Oheimb + Author: Brian Huffman + +Proofs of high-level (co)induction rules for domain command. +*) + +signature DOMAIN_INDUCTION = +sig + val comp_theorems : + binding -> binding list -> + Domain_Take_Proofs.take_induct_info -> + Domain_Constructors.constr_info list -> + theory -> thm list * theory + + val quiet_mode: bool Unsynchronized.ref; + val trace_domain: bool Unsynchronized.ref; +end; + +structure Domain_Induction :> DOMAIN_INDUCTION = +struct + +val quiet_mode = Unsynchronized.ref false; +val trace_domain = Unsynchronized.ref false; + +fun message s = if !quiet_mode then () else writeln s; +fun trace s = if !trace_domain then tracing s else (); + +open HOLCF_Library; + +(******************************************************************************) +(***************************** proofs about take ******************************) +(******************************************************************************) + +fun take_theorems + (dbinds : binding list) + (take_info : Domain_Take_Proofs.take_induct_info) + (constr_infos : Domain_Constructors.constr_info list) + (thy : theory) : thm list list * theory = +let + val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info; + val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy; + + val n = Free ("n", @{typ nat}); + val n' = @{const Suc} $ n; + + local + val newTs = map (#absT o #iso_info) constr_infos; + val subs = newTs ~~ map (fn t => t $ n) take_consts; + fun is_ID (Const (c, _)) = (c = @{const_name ID}) + | is_ID _ = false; + in + fun map_of_arg v T = + let val m = Domain_Take_Proofs.map_of_typ thy subs T; + in if is_ID m then v else mk_capply (m, v) end; + end + + fun prove_take_apps + ((dbind, take_const), constr_info) thy = + let + val {iso_info, con_specs, con_betas, ...} = constr_info; + val {abs_inverse, ...} = iso_info; + fun prove_take_app (con_const, args) = + let + val Ts = map snd args; + val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs)); + val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts); + val goal = mk_trp (mk_eq (lhs, rhs)); + val rules = + [abs_inverse] @ con_betas @ @{thms take_con_rules} + @ take_Suc_thms @ deflation_thms @ deflation_take_thms; + val tac = simp_tac (HOL_basic_ss addsimps rules) 1; + in + Goal.prove_global thy [] [] goal (K tac) + end; + val take_apps = map prove_take_app con_specs; + in + yield_singleton Global_Theory.add_thmss + ((Binding.qualified true "take_rews" dbind, take_apps), + [Simplifier.simp_add]) thy + end; +in + fold_map prove_take_apps + (dbinds ~~ take_consts ~~ constr_infos) thy +end; + +(******************************************************************************) +(****************************** induction rules *******************************) +(******************************************************************************) + +val case_UU_allI = + @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}; + +fun prove_induction + (comp_dbind : binding) + (constr_infos : Domain_Constructors.constr_info list) + (take_info : Domain_Take_Proofs.take_induct_info) + (take_rews : thm list) + (thy : theory) = +let + val comp_dname = Binding.name_of comp_dbind; + + val iso_infos = map #iso_info constr_infos; + val exhausts = map #exhaust constr_infos; + val con_rews = maps #con_rews constr_infos; + val {take_consts, take_induct_thms, ...} = take_info; + + val newTs = map #absT iso_infos; + val P_names = Datatype_Prop.indexify_names (map (K "P") newTs); + val x_names = Datatype_Prop.indexify_names (map (K "x") newTs); + val P_types = map (fn T => T --> HOLogic.boolT) newTs; + val Ps = map Free (P_names ~~ P_types); + val xs = map Free (x_names ~~ newTs); + val n = Free ("n", HOLogic.natT); + + fun con_assm defined p (con, args) = + let + val Ts = map snd args; + val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); + fun ind_hyp (v, T) t = + case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t + | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t); + val t1 = mk_trp (p $ list_ccomb (con, vs)); + val t2 = fold_rev ind_hyp (vs ~~ Ts) t1; + val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2); + in fold_rev Logic.all vs (if defined then t3 else t2) end; + fun eq_assms ((p, T), cons) = + mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons; + val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos); + + val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); + fun quant_tac ctxt i = EVERY + (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names); + + (* FIXME: move this message to domain_take_proofs.ML *) + val is_finite = #is_finite take_info; + val _ = if is_finite + then message ("Proving finiteness rule for domain "^comp_dname^" ...") + else (); + + val _ = trace " Proving finite_ind..."; + val finite_ind = + let + val concls = + map (fn ((P, t), x) => P $ mk_capply (t $ n, x)) + (Ps ~~ take_consts ~~ xs); + val goal = mk_trp (foldr1 mk_conj concls); + + fun tacf {prems, context} = + let + (* Prove stronger prems, without definedness side conditions *) + fun con_thm p (con, args) = + let + val subgoal = con_assm false p (con, args); + val rules = prems @ con_rews @ simp_thms; + val simplify = asm_simp_tac (HOL_basic_ss addsimps rules); + fun arg_tac (lazy, _) = + rtac (if lazy then allI else case_UU_allI) 1; + val tacs = + rewrite_goals_tac @{thms atomize_all atomize_imp} :: + map arg_tac args @ + [REPEAT (rtac impI 1), ALLGOALS simplify]; + in + Goal.prove context [] [] subgoal (K (EVERY tacs)) + end; + fun eq_thms (p, cons) = map (con_thm p) cons; + val conss = map #con_specs constr_infos; + val prems' = maps eq_thms (Ps ~~ conss); + + 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 con_tac _ = + asm_simp_tac take_ss 1 THEN + (resolve_tac prems' THEN_ALL_NEW etac spec) 1; + fun cases_tacs (cons, exhaust) = + res_inst_tac context [(("y", 0), "x")] exhaust 1 :: + asm_simp_tac (take_ss addsimps prems) 1 :: + map con_tac cons; + val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts) + in + EVERY (map DETERM tacs) + end; + in Goal.prove_global thy [] assms goal tacf end; + + val _ = trace " Proving ind..."; + val ind = + let + val concls = map (op $) (Ps ~~ xs); + val goal = mk_trp (foldr1 mk_conj concls); + val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps; + fun tacf {prems, context} = + let + fun finite_tac (take_induct, fin_ind) = + rtac take_induct 1 THEN + (if is_finite then all_tac else resolve_tac prems 1) THEN + (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1; + val fin_inds = Project_Rule.projections context finite_ind; + in + TRY (safe_tac HOL_cs) THEN + EVERY (map finite_tac (take_induct_thms ~~ fin_inds)) + end; + in Goal.prove_global thy [] (adms @ assms) goal tacf end + + (* case names for induction rules *) + val dnames = map (fst o dest_Type) newTs; + val case_ns = + let + val adms = + if is_finite then [] else + if length dnames = 1 then ["adm"] else + map (fn s => "adm_" ^ Long_Name.base_name s) dnames; + val bottoms = + if length dnames = 1 then ["bottom"] else + map (fn s => "bottom_" ^ Long_Name.base_name s) dnames; + fun one_eq bot constr_info = + let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c)); + in bot :: map name_of (#con_specs constr_info) end; + in adms @ flat (map2 one_eq bottoms constr_infos) end; + + val inducts = Project_Rule.projections (ProofContext.init_global thy) ind; + fun ind_rule (dname, rule) = + ((Binding.empty, rule), + [Rule_Cases.case_names case_ns, Induct.induct_type dname]); + +in + thy + |> snd o Global_Theory.add_thms [ + ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []), + ((Binding.qualified true "induct" comp_dbind, ind ), [])] + |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts))) +end; (* prove_induction *) + +(******************************************************************************) +(************************ bisimulation and coinduction ************************) +(******************************************************************************) + +fun prove_coinduction + (comp_dbind : binding, dbinds : binding list) + (constr_infos : Domain_Constructors.constr_info list) + (take_info : Domain_Take_Proofs.take_induct_info) + (take_rews : thm list list) + (thy : theory) : theory = +let + val iso_infos = map #iso_info constr_infos; + val newTs = map #absT iso_infos; + + val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info; + + val R_names = Datatype_Prop.indexify_names (map (K "R") newTs); + val R_types = map (fn T => T --> T --> boolT) newTs; + val Rs = map Free (R_names ~~ R_types); + val n = Free ("n", natT); + val reserved = "x" :: "y" :: R_names; + + (* declare bisimulation predicate *) + val bisim_bind = Binding.suffix_name "_bisim" comp_dbind; + val bisim_type = R_types ---> boolT; + val (bisim_const, thy) = + Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; + + (* define bisimulation predicate *) + local + fun one_con T (con, args) = + let + val Ts = map snd args; + val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts); + val ns2 = map (fn n => n^"'") ns1; + val vs1 = map Free (ns1 ~~ Ts); + val vs2 = map Free (ns2 ~~ Ts); + val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1)); + val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2)); + fun rel ((v1, v2), T) = + case AList.lookup (op =) (newTs ~~ Rs) T of + NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2; + val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2]); + in + Library.foldr mk_ex (vs1 @ vs2, eqs) + end; + fun one_eq ((T, R), cons) = + let + val x = Free ("x", T); + val y = Free ("y", T); + val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T)); + val disjs = disj1 :: map (one_con T) cons; + in + mk_all (x, mk_all (y, mk_imp (R $ x $ y, foldr1 mk_disj disjs))) + end; + val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos); + val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs); + val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs); + in + val (bisim_def_thm, thy) = thy |> + yield_singleton (Global_Theory.add_defs false) + ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []); + end (* local *) + + (* prove coinduction lemma *) + val coind_lemma = + let + val assm = mk_trp (list_comb (bisim_const, Rs)); + fun one ((T, R), take_const) = + let + val x = Free ("x", T); + val y = Free ("y", T); + val lhs = mk_capply (take_const $ n, x); + val rhs = mk_capply (take_const $ n, y); + in + mk_all (x, mk_all (y, mk_imp (R $ x $ y, mk_eq (lhs, rhs)))) + end; + val goal = + mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts))); + val rules = @{thm Rep_CFun_strict1} :: take_0_thms; + fun tacf {prems, context} = + let + val prem' = rewrite_rule [bisim_def_thm] (hd prems); + val prems' = Project_Rule.projections context prem'; + val dests = map (fn th => th RS spec RS spec RS mp) prems'; + fun one_tac (dest, rews) = + dtac dest 1 THEN safe_tac HOL_cs THEN + ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews)); + in + rtac @{thm nat.induct} 1 THEN + simp_tac (HOL_ss addsimps rules) 1 THEN + safe_tac HOL_cs THEN + EVERY (map one_tac (dests ~~ take_rews)) + end + in + Goal.prove_global thy [] [assm] goal tacf + end; + + (* prove individual coinduction rules *) + fun prove_coind ((T, R), take_lemma) = + let + val x = Free ("x", T); + val y = Free ("y", T); + val assm1 = mk_trp (list_comb (bisim_const, Rs)); + val assm2 = mk_trp (R $ x $ y); + val goal = mk_trp (mk_eq (x, y)); + fun tacf {prems, context} = + let + val rule = hd prems RS coind_lemma; + in + rtac take_lemma 1 THEN + asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1 + end; + in + Goal.prove_global thy [] [assm1, assm2] goal tacf + end; + val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms); + val coind_binds = map (Binding.qualified true "coinduct") dbinds; + +in + thy |> snd o Global_Theory.add_thms + (map Thm.no_attributes (coind_binds ~~ coinds)) +end; (* let *) + +(******************************************************************************) +(******************************* main function ********************************) +(******************************************************************************) + +fun comp_theorems + (comp_dbind : binding) + (dbinds : binding list) + (take_info : Domain_Take_Proofs.take_induct_info) + (constr_infos : Domain_Constructors.constr_info list) + (thy : theory) = +let +val comp_dname = Binding.name_of comp_dbind; + +(* Test for emptiness *) +(* FIXME: reimplement emptiness test +local + open Domain_Library; + val dnames = map (fst o fst) eqs; + val conss = map snd eqs; + fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => + is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso + ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse + rec_of arg <> n andalso rec_to (rec_of arg::ns) + (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) + ) o snd) cons; + fun warn (n,cons) = + if rec_to [] false (n,cons) + then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) + else false; +in + val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; + val is_emptys = map warn n__eqs; +end; +*) + +(* Test for indirect recursion *) +local + val newTs = map (#absT o #iso_info) constr_infos; + fun indirect_typ (Type (_, Ts)) = + exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts + | indirect_typ _ = false; + fun indirect_arg (_, T) = indirect_typ T; + fun indirect_con (_, args) = exists indirect_arg args; + fun indirect_eq cons = exists indirect_con cons; +in + val is_indirect = exists indirect_eq (map #con_specs constr_infos); + val _ = + if is_indirect + then message "Indirect recursion detected, skipping proofs of (co)induction rules" + else message ("Proving induction properties of domain "^comp_dname^" ..."); +end; + +(* theorems about take *) + +val (take_rewss, thy) = + take_theorems dbinds take_info constr_infos thy; + +val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info; + +val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss; + +(* prove induction rules, unless definition is indirect recursive *) +val thy = + if is_indirect then thy else + prove_induction comp_dbind constr_infos take_info take_rews thy; + +val thy = + if is_indirect then thy else + prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy; + +in + (take_rews, thy) +end; (* let *) +end; (* struct *) diff -r 391746914dba -r 3adb92ee2f22 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Oct 19 14:28:14 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,438 +0,0 @@ -(* Title: HOLCF/Tools/Domain/domain_theorems.ML - Author: David von Oheimb - Author: Brian Huffman - -Proof generator for domain command. -*) - -signature DOMAIN_THEOREMS = -sig - val comp_theorems : - binding -> binding list -> - Domain_Take_Proofs.take_induct_info -> - Domain_Constructors.constr_info list -> - theory -> thm list * theory - - val quiet_mode: bool Unsynchronized.ref; - val trace_domain: bool Unsynchronized.ref; -end; - -structure Domain_Theorems :> DOMAIN_THEOREMS = -struct - -val quiet_mode = Unsynchronized.ref false; -val trace_domain = Unsynchronized.ref false; - -fun message s = if !quiet_mode then () else writeln s; -fun trace s = if !trace_domain then tracing s else (); - -open HOLCF_Library; - -(******************************************************************************) -(***************************** proofs about take ******************************) -(******************************************************************************) - -fun take_theorems - (dbinds : binding list) - (take_info : Domain_Take_Proofs.take_induct_info) - (constr_infos : Domain_Constructors.constr_info list) - (thy : theory) : thm list list * theory = -let - val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info; - val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy; - - val n = Free ("n", @{typ nat}); - val n' = @{const Suc} $ n; - - local - val newTs = map (#absT o #iso_info) constr_infos; - val subs = newTs ~~ map (fn t => t $ n) take_consts; - fun is_ID (Const (c, _)) = (c = @{const_name ID}) - | is_ID _ = false; - in - fun map_of_arg v T = - let val m = Domain_Take_Proofs.map_of_typ thy subs T; - in if is_ID m then v else mk_capply (m, v) end; - end - - fun prove_take_apps - ((dbind, take_const), constr_info) thy = - let - val {iso_info, con_specs, con_betas, ...} = constr_info; - val {abs_inverse, ...} = iso_info; - fun prove_take_app (con_const, args) = - let - val Ts = map snd args; - val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts); - val vs = map Free (ns ~~ Ts); - val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs)); - val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts); - val goal = mk_trp (mk_eq (lhs, rhs)); - val rules = - [abs_inverse] @ con_betas @ @{thms take_con_rules} - @ take_Suc_thms @ deflation_thms @ deflation_take_thms; - val tac = simp_tac (HOL_basic_ss addsimps rules) 1; - in - Goal.prove_global thy [] [] goal (K tac) - end; - val take_apps = map prove_take_app con_specs; - in - yield_singleton Global_Theory.add_thmss - ((Binding.qualified true "take_rews" dbind, take_apps), - [Simplifier.simp_add]) thy - end; -in - fold_map prove_take_apps - (dbinds ~~ take_consts ~~ constr_infos) thy -end; - -(******************************************************************************) -(****************************** induction rules *******************************) -(******************************************************************************) - -val case_UU_allI = - @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}; - -fun prove_induction - (comp_dbind : binding) - (constr_infos : Domain_Constructors.constr_info list) - (take_info : Domain_Take_Proofs.take_induct_info) - (take_rews : thm list) - (thy : theory) = -let - val comp_dname = Binding.name_of comp_dbind; - - val iso_infos = map #iso_info constr_infos; - val exhausts = map #exhaust constr_infos; - val con_rews = maps #con_rews constr_infos; - val {take_consts, take_induct_thms, ...} = take_info; - - val newTs = map #absT iso_infos; - val P_names = Datatype_Prop.indexify_names (map (K "P") newTs); - val x_names = Datatype_Prop.indexify_names (map (K "x") newTs); - val P_types = map (fn T => T --> HOLogic.boolT) newTs; - val Ps = map Free (P_names ~~ P_types); - val xs = map Free (x_names ~~ newTs); - val n = Free ("n", HOLogic.natT); - - fun con_assm defined p (con, args) = - let - val Ts = map snd args; - val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts); - val vs = map Free (ns ~~ Ts); - val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); - fun ind_hyp (v, T) t = - case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t - | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t); - val t1 = mk_trp (p $ list_ccomb (con, vs)); - val t2 = fold_rev ind_hyp (vs ~~ Ts) t1; - val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2); - in fold_rev Logic.all vs (if defined then t3 else t2) end; - fun eq_assms ((p, T), cons) = - mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons; - val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos); - - val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); - fun quant_tac ctxt i = EVERY - (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names); - - (* FIXME: move this message to domain_take_proofs.ML *) - val is_finite = #is_finite take_info; - val _ = if is_finite - then message ("Proving finiteness rule for domain "^comp_dname^" ...") - else (); - - val _ = trace " Proving finite_ind..."; - val finite_ind = - let - val concls = - map (fn ((P, t), x) => P $ mk_capply (t $ n, x)) - (Ps ~~ take_consts ~~ xs); - val goal = mk_trp (foldr1 mk_conj concls); - - fun tacf {prems, context} = - let - (* Prove stronger prems, without definedness side conditions *) - fun con_thm p (con, args) = - let - val subgoal = con_assm false p (con, args); - val rules = prems @ con_rews @ simp_thms; - val simplify = asm_simp_tac (HOL_basic_ss addsimps rules); - fun arg_tac (lazy, _) = - rtac (if lazy then allI else case_UU_allI) 1; - val tacs = - rewrite_goals_tac @{thms atomize_all atomize_imp} :: - map arg_tac args @ - [REPEAT (rtac impI 1), ALLGOALS simplify]; - in - Goal.prove context [] [] subgoal (K (EVERY tacs)) - end; - fun eq_thms (p, cons) = map (con_thm p) cons; - val conss = map #con_specs constr_infos; - val prems' = maps eq_thms (Ps ~~ conss); - - 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 con_tac _ = - asm_simp_tac take_ss 1 THEN - (resolve_tac prems' THEN_ALL_NEW etac spec) 1; - fun cases_tacs (cons, exhaust) = - res_inst_tac context [(("y", 0), "x")] exhaust 1 :: - asm_simp_tac (take_ss addsimps prems) 1 :: - map con_tac cons; - val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts) - in - EVERY (map DETERM tacs) - end; - in Goal.prove_global thy [] assms goal tacf end; - - val _ = trace " Proving ind..."; - val ind = - let - val concls = map (op $) (Ps ~~ xs); - val goal = mk_trp (foldr1 mk_conj concls); - val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps; - fun tacf {prems, context} = - let - fun finite_tac (take_induct, fin_ind) = - rtac take_induct 1 THEN - (if is_finite then all_tac else resolve_tac prems 1) THEN - (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1; - val fin_inds = Project_Rule.projections context finite_ind; - in - TRY (safe_tac HOL_cs) THEN - EVERY (map finite_tac (take_induct_thms ~~ fin_inds)) - end; - in Goal.prove_global thy [] (adms @ assms) goal tacf end - - (* case names for induction rules *) - val dnames = map (fst o dest_Type) newTs; - val case_ns = - let - val adms = - if is_finite then [] else - if length dnames = 1 then ["adm"] else - map (fn s => "adm_" ^ Long_Name.base_name s) dnames; - val bottoms = - if length dnames = 1 then ["bottom"] else - map (fn s => "bottom_" ^ Long_Name.base_name s) dnames; - fun one_eq bot constr_info = - let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c)); - in bot :: map name_of (#con_specs constr_info) end; - in adms @ flat (map2 one_eq bottoms constr_infos) end; - - val inducts = Project_Rule.projections (ProofContext.init_global thy) ind; - fun ind_rule (dname, rule) = - ((Binding.empty, rule), - [Rule_Cases.case_names case_ns, Induct.induct_type dname]); - -in - thy - |> snd o Global_Theory.add_thms [ - ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []), - ((Binding.qualified true "induct" comp_dbind, ind ), [])] - |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts))) -end; (* prove_induction *) - -(******************************************************************************) -(************************ bisimulation and coinduction ************************) -(******************************************************************************) - -fun prove_coinduction - (comp_dbind : binding, dbinds : binding list) - (constr_infos : Domain_Constructors.constr_info list) - (take_info : Domain_Take_Proofs.take_induct_info) - (take_rews : thm list list) - (thy : theory) : theory = -let - val iso_infos = map #iso_info constr_infos; - val newTs = map #absT iso_infos; - - val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info; - - val R_names = Datatype_Prop.indexify_names (map (K "R") newTs); - val R_types = map (fn T => T --> T --> boolT) newTs; - val Rs = map Free (R_names ~~ R_types); - val n = Free ("n", natT); - val reserved = "x" :: "y" :: R_names; - - (* declare bisimulation predicate *) - val bisim_bind = Binding.suffix_name "_bisim" comp_dbind; - val bisim_type = R_types ---> boolT; - val (bisim_const, thy) = - Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; - - (* define bisimulation predicate *) - local - fun one_con T (con, args) = - let - val Ts = map snd args; - val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts); - val ns2 = map (fn n => n^"'") ns1; - val vs1 = map Free (ns1 ~~ Ts); - val vs2 = map Free (ns2 ~~ Ts); - val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1)); - val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2)); - fun rel ((v1, v2), T) = - case AList.lookup (op =) (newTs ~~ Rs) T of - NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2; - val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2]); - in - Library.foldr mk_ex (vs1 @ vs2, eqs) - end; - fun one_eq ((T, R), cons) = - let - val x = Free ("x", T); - val y = Free ("y", T); - val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T)); - val disjs = disj1 :: map (one_con T) cons; - in - mk_all (x, mk_all (y, mk_imp (R $ x $ y, foldr1 mk_disj disjs))) - end; - val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos); - val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs); - val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs); - in - val (bisim_def_thm, thy) = thy |> - yield_singleton (Global_Theory.add_defs false) - ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []); - end (* local *) - - (* prove coinduction lemma *) - val coind_lemma = - let - val assm = mk_trp (list_comb (bisim_const, Rs)); - fun one ((T, R), take_const) = - let - val x = Free ("x", T); - val y = Free ("y", T); - val lhs = mk_capply (take_const $ n, x); - val rhs = mk_capply (take_const $ n, y); - in - mk_all (x, mk_all (y, mk_imp (R $ x $ y, mk_eq (lhs, rhs)))) - end; - val goal = - mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts))); - val rules = @{thm Rep_CFun_strict1} :: take_0_thms; - fun tacf {prems, context} = - let - val prem' = rewrite_rule [bisim_def_thm] (hd prems); - val prems' = Project_Rule.projections context prem'; - val dests = map (fn th => th RS spec RS spec RS mp) prems'; - fun one_tac (dest, rews) = - dtac dest 1 THEN safe_tac HOL_cs THEN - ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews)); - in - rtac @{thm nat.induct} 1 THEN - simp_tac (HOL_ss addsimps rules) 1 THEN - safe_tac HOL_cs THEN - EVERY (map one_tac (dests ~~ take_rews)) - end - in - Goal.prove_global thy [] [assm] goal tacf - end; - - (* prove individual coinduction rules *) - fun prove_coind ((T, R), take_lemma) = - let - val x = Free ("x", T); - val y = Free ("y", T); - val assm1 = mk_trp (list_comb (bisim_const, Rs)); - val assm2 = mk_trp (R $ x $ y); - val goal = mk_trp (mk_eq (x, y)); - fun tacf {prems, context} = - let - val rule = hd prems RS coind_lemma; - in - rtac take_lemma 1 THEN - asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1 - end; - in - Goal.prove_global thy [] [assm1, assm2] goal tacf - end; - val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms); - val coind_binds = map (Binding.qualified true "coinduct") dbinds; - -in - thy |> snd o Global_Theory.add_thms - (map Thm.no_attributes (coind_binds ~~ coinds)) -end; (* let *) - -(******************************************************************************) -(******************************* main function ********************************) -(******************************************************************************) - -fun comp_theorems - (comp_dbind : binding) - (dbinds : binding list) - (take_info : Domain_Take_Proofs.take_induct_info) - (constr_infos : Domain_Constructors.constr_info list) - (thy : theory) = -let -val comp_dname = Binding.name_of comp_dbind; - -(* Test for emptiness *) -(* FIXME: reimplement emptiness test -local - open Domain_Library; - val dnames = map (fst o fst) eqs; - val conss = map snd eqs; - fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => - is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso - ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse - rec_of arg <> n andalso rec_to (rec_of arg::ns) - (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) - ) o snd) cons; - fun warn (n,cons) = - if rec_to [] false (n,cons) - then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) - else false; -in - val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; - val is_emptys = map warn n__eqs; -end; -*) - -(* Test for indirect recursion *) -local - val newTs = map (#absT o #iso_info) constr_infos; - fun indirect_typ (Type (_, Ts)) = - exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts - | indirect_typ _ = false; - fun indirect_arg (_, T) = indirect_typ T; - fun indirect_con (_, args) = exists indirect_arg args; - fun indirect_eq cons = exists indirect_con cons; -in - val is_indirect = exists indirect_eq (map #con_specs constr_infos); - val _ = - if is_indirect - then message "Indirect recursion detected, skipping proofs of (co)induction rules" - else message ("Proving induction properties of domain "^comp_dname^" ..."); -end; - -(* theorems about take *) - -val (take_rewss, thy) = - take_theorems dbinds take_info constr_infos thy; - -val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info; - -val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss; - -(* prove induction rules, unless definition is indirect recursive *) -val thy = - if is_indirect then thy else - prove_induction comp_dbind constr_infos take_info take_rews thy; - -val thy = - if is_indirect then thy else - prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy; - -in - (take_rews, thy) -end; (* let *) -end; (* struct *)