diff --git a/src/ZF/Datatype.thy b/src/ZF/Datatype.thy --- a/src/ZF/Datatype.thy +++ b/src/ZF/Datatype.thy @@ -1,120 +1,120 @@ (* Title: ZF/Datatype.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge *) section\Datatype and CoDatatype Definitions\ theory Datatype imports Inductive Univ QUniv keywords "datatype" "codatatype" :: thy_decl begin ML_file \Tools/datatype_package.ML\ ML \ (*Typechecking rules for most datatypes involving univ*) structure Data_Arg = struct val intrs = [@{thm SigmaI}, @{thm InlI}, @{thm InrI}, @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ}, @{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}]; val elims = [make_elim @{thm InlD}, make_elim @{thm InrD}, (*for mutual recursion*) @{thm SigmaE}, @{thm sumE}]; (*allows * and + in spec*) end; structure Data_Package = Add_datatype_def_Fun (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP and Su=Standard_Sum and Ind_Package = Ind_Package and Datatype_Arg = Data_Arg val coind = false); (*Typechecking rules for most codatatypes involving quniv*) structure CoData_Arg = struct val intrs = [@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI}, @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv}, @{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}]; val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD}, (*for mutual recursion*) @{thm QSigmaE}, @{thm qsumE}]; (*allows * and + in spec*) end; structure CoData_Package = Add_datatype_def_Fun (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP and Su=Quine_Sum and Ind_Package = CoInd_Package and Datatype_Arg = CoData_Arg val coind = true); (*Simproc for freeness reasoning: compare datatype constructors for equality*) structure DataFree = struct val trace = Unsynchronized.ref false; - fun mk_new ([],[]) = Const(\<^const_name>\True\,FOLogic.oT) + fun mk_new ([],[]) = \<^Const>\True\ | mk_new (largs,rargs) = Balanced_Tree.make FOLogic.mk_conj (map FOLogic.mk_eq (ListPair.zip (largs,rargs))); val datatype_ss = simpset_of \<^context>; fun proc ctxt ct = let val old = Thm.term_of ct val thy = Proof_Context.theory_of ctxt val _ = if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term ctxt old) else () val (lhs,rhs) = FOLogic.dest_eq old val (lhead, largs) = strip_comb lhs and (rhead, rargs) = strip_comb rhs val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname) handle Option.Option => raise Match; val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname) handle Option.Option => raise Match; val new = if #big_rec_name lcon_info = #big_rec_name rcon_info andalso not (null (#free_iffs lcon_info)) then if lname = rname then mk_new (largs, rargs) - else Const(\<^const_name>\False\,FOLogic.oT) + else \<^Const>\False\ else raise Match val _ = if !trace then writeln ("NEW = " ^ Syntax.string_of_term ctxt new) else (); val goal = Logic.mk_equals (old, new) val thm = Goal.prove ctxt [] [] goal (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN simp_tac (put_simpset datatype_ss ctxt addsimps (map (Thm.transfer thy) (#free_iffs lcon_info))) 1) handle ERROR msg => (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal); raise Match) in SOME thm end handle Match => NONE; val conv = Simplifier.make_simproc \<^context> "data_free" {lhss = [\<^term>\(x::i) = y\], proc = K proc}; end; \ setup \ Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv]) \ end diff --git a/src/ZF/Tools/datatype_package.ML b/src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML +++ b/src/ZF/Tools/datatype_package.ML @@ -1,452 +1,452 @@ (* Title: ZF/Tools/datatype_package.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Datatype/Codatatype Definitions. The functor will be instantiated for normal sums/products (datatype defs) and non-standard sums/products (codatatype defs) Sums are used only for mutual recursion; Products are used only to derive "streamlined" induction rules for relations *) type datatype_result = {con_defs : thm list, (*definitions made in thy*) case_eqns : thm list, (*equations for case operator*) recursor_eqns : thm list, (*equations for the recursor*) free_iffs : thm list, (*freeness rewrite rules*) free_SEs : thm list, (*freeness destruct rules*) mk_free : Proof.context -> string -> thm}; (*function to make freeness theorems*) signature DATATYPE_ARG = sig val intrs : thm list val elims : thm list end; signature DATATYPE_PACKAGE = sig (*Insert definitions for the recursive sets, which must *already* be declared as constants in parent theory!*) val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list -> thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result val add_datatype: string * string list -> (string * string list * mixfix) list list -> (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list -> theory -> theory * inductive_result * datatype_result end; functor Add_datatype_def_Fun (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU and Ind_Package : INDUCTIVE_PACKAGE and Datatype_Arg : DATATYPE_ARG val coind : bool): DATATYPE_PACKAGE = struct (*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *) (*univ or quniv constitutes the sum domain for mutual recursion; it is applied to the datatype parameters and to Consts occurring in the definition other than Nat.nat and the datatype sets themselves. FIXME: could insert all constant set expressions, e.g. nat->nat.*) fun data_domain co (rec_tms, con_ty_lists) = let val rec_hds = map head_of rec_tms val dummy = rec_hds |> forall (fn t => is_Const t orelse error ("Datatype set not previously declared as constant: " ^ Syntax.string_of_term_global \<^theory>\IFOL\ t)); val rec_names = (*nat doesn't have to be added*) \<^const_name>\nat\ :: map (#1 o dest_Const) rec_hds val u = if co then \<^const>\QUniv.quniv\ else \<^const>\Univ.univ\ val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t | _ => I)) con_ty_lists []; in u $ Ind_Syntax.union_params (hd rec_tms, cs) end; fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy = let val rec_hds = map head_of rec_tms; val dummy = rec_hds |> forall (fn t => is_Const t orelse error ("Datatype set not previously declared as constant: " ^ Syntax.string_of_term_global thy t)); val rec_names = map (#1 o dest_Const) rec_hds val rec_base_names = map Long_Name.base_name rec_names val big_rec_base_name = space_implode "_" rec_base_names val thy_path = thy |> Sign.add_path big_rec_base_name val big_rec_name = Sign.intern_const thy_path big_rec_base_name; val intr_tms = Ind_Syntax.mk_all_intr_tms thy_path (rec_tms, con_ty_lists); val dummy = writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name); val case_varname = "f"; (*name for case variables*) (** Define the constructors **) (*The empty tuple is 0*) fun mk_tuple [] = \<^const>\zero\ | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; fun mk_inject n k u = Balanced_Tree.access {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k; val npart = length rec_names; (*number of mutually recursive parts*) val full_name = Sign.full_bname thy_path; (*Make constructor definition; kpart is the number of this mutually recursive part*) fun mk_con_defs (kpart, con_ty_list) = let val ncon = length con_ty_list (*number of constructors*) fun mk_def (((id,T,syn), name, args, prems), kcon) = (*kcon is index of constructor*) Misc_Legacy.mk_defpair (list_comb (Const (full_name name, T), args), mk_inject npart kpart (mk_inject ncon kcon (mk_tuple args))) in ListPair.map mk_def (con_ty_list, 1 upto ncon) end; (*** Define the case operator ***) (*Combine split terms using case; yields the case operator for one part*) fun call_case case_list = let fun call_f (free,[]) = Abs("null", \<^typ>\i\, free) | call_f (free,args) = CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) \<^typ>\i\ free in Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end; (** Generating function variables for the case definition Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) (*The function variable for a single constructor*) fun add_case ((_, T, _), name, args, _) (opno, cases) = if Symbol_Pos.is_identifier name then (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases) else (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) :: cases); (*Treatment of a list of constructors, for one part Result adds a list of terms, each a function variable with arguments*) fun add_case_list con_ty_list (opno, case_lists) = let val (opno', case_list) = fold_rev add_case con_ty_list (opno, []) in (opno', case_list :: case_lists) end; (*Treatment of all parts*) val (_, case_lists) = fold_rev add_case_list con_ty_lists (1, []); (*extract the types of all the variables*) val case_typ = maps (map (#2 o #1)) con_ty_lists ---> \<^typ>\i => i\; val case_base_name = big_rec_base_name ^ "_case"; val case_name = full_name case_base_name; (*The list of all the function variables*) val case_args = maps (map #1) case_lists; val case_const = Const (case_name, case_typ); val case_tm = list_comb (case_const, case_args); val case_def = Misc_Legacy.mk_defpair (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists)); (** Generating function variables for the recursor definition Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) (*a recursive call for x is the application rec`x *) val rec_call = \<^const>\apply\ $ Free ("rec", \<^typ>\i\); (*look back down the "case args" (which have been reversed) to determine the de Bruijn index*) fun make_rec_call ([], _) arg = error "Internal error in datatype (variable name mismatch)" | make_rec_call (a::args, i) arg = if a = arg then rec_call $ Bound i else make_rec_call (args, i+1) arg; (*creates one case of the "X_case" definition of the recursor*) fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) = let fun add_abs (Free(a,T), u) = Abs(a,T,u) val ncase_args = length case_args val bound_args = map Bound ((ncase_args - 1) downto 0) val rec_args = map (make_rec_call (rev case_args,0)) (List.drop(recursor_args, ncase_args)) in List.foldr add_abs (list_comb (recursor_var, bound_args @ rec_args)) case_args end (*Find each recursive argument and add a recursive call for it*) fun rec_args [] = [] - | rec_args ((Const(\<^const_name>\mem\,_)$arg$X)::prems) = + | rec_args (\<^Const_>\mem for arg X\::prems) = (case head_of X of Const(a,_) => (*recursive occurrence?*) if member (op =) rec_names a then arg :: rec_args prems else rec_args prems | _ => rec_args prems) | rec_args (_::prems) = rec_args prems; (*Add an argument position for each occurrence of a recursive set. Strictly speaking, the recursive arguments are the LAST of the function variable, but they all have type "i" anyway*) fun add_rec_args args' T = (map (fn _ => \<^typ>\i\) args') ---> T (*Plug in the function variable type needed for the recursor as well as the new arguments (recursive calls)*) fun rec_ty_elem ((id, T, syn), name, args, prems) = let val args' = rec_args prems in ((id, add_rec_args args' T, syn), name, args @ args', prems) end; val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists); (*Treatment of all parts*) val (_, recursor_lists) = fold_rev add_case_list rec_ty_lists (1, []); (*extract the types of all the variables*) val recursor_typ = maps (map (#2 o #1)) rec_ty_lists ---> \<^typ>\i => i\; val recursor_base_name = big_rec_base_name ^ "_rec"; val recursor_name = full_name recursor_base_name; (*The list of all the function variables*) val recursor_args = maps (map #1) recursor_lists; val recursor_tm = list_comb (Const (recursor_name, recursor_typ), recursor_args); val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists); val recursor_def = Misc_Legacy.mk_defpair (recursor_tm, \<^const>\Univ.Vrecursor\ $ absfree ("rec", \<^typ>\i\) (list_comb (case_const, recursor_cases))); (* Build the new theory *) val need_recursor = (not coind andalso recursor_typ <> case_typ); fun add_recursor thy = if need_recursor then thy |> Sign.add_consts [(Binding.name recursor_base_name, recursor_typ, NoSyn)] |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def]) else thy; val (con_defs, thy0) = thy_path |> Sign.add_consts (map (fn (c, T, mx) => (Binding.name c, T, mx)) ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists))) |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) (case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) ||> add_recursor ||> Sign.parent_path; val intr_names = map (Binding.name o #2) (flat con_ty_lists); val (thy1, ind_result) = thy0 |> Ind_Package.add_inductive_i false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms)) (monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims); (**** Now prove the datatype theorems in this theory ****) (*** Prove the case theorems ***) (*Each equation has the form case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) fun mk_case_eqn (((_,T,_), name, args, _), case_free) = FOLogic.mk_Trueprop (FOLogic.mk_eq (case_tm $ (list_comb (Const (Sign.intern_const thy1 name,T), args)), list_comb (case_free, args))); val case_trans = hd con_defs RS @{thm def_trans} and split_trans = Pr.split_eq RS @{thm meta_eq_to_obj_eq} RS @{thm trans}; fun prove_case_eqn (arg, con_def) = Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg)) (*Proves a single case equation. Could use simp_tac, but it's slower!*) (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt [con_def], resolve_tac ctxt [case_trans] 1, REPEAT (resolve_tac ctxt [@{thm refl}, split_trans, Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]); val free_iffs = map Drule.export_without_context (con_defs RL [@{thm def_swap_iff}]); val ([case_eqns], thy2) = thy1 |> Sign.add_path big_rec_base_name |> Global_Theory.add_thmss [((Binding.name "case_eqns", map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs)), [])] ||> Sign.parent_path; (*** Prove the recursor theorems ***) val (recursor_eqns, thy3) = case try (Misc_Legacy.get_def thy2) recursor_base_name of NONE => (writeln " [ No recursion operator ]"; ([], thy2)) | SOME recursor_def => let (*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *) - fun subst_rec (Const(\<^const_name>\apply\,_) $ Free _ $ arg) = recursor_tm $ arg + fun subst_rec \<^Const_>\apply for \Free _\ arg\ = recursor_tm $ arg | subst_rec tm = let val (head, args) = strip_comb tm in list_comb (head, map subst_rec args) end; (*Each equation has the form REC(coni(args)) = f_coni(args, REC(rec_arg), ...) where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive constructor argument.*) fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) = FOLogic.mk_Trueprop (FOLogic.mk_eq (recursor_tm $ (list_comb (Const (Sign.intern_const thy2 name,T), args)), subst_rec (Term.betapplys (recursor_case, args)))); val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS @{thm trans}; fun prove_recursor_eqn arg = Goal.prove_global thy2 [] [] (Ind_Syntax.traceIt "next recursor equation = " thy2 (mk_recursor_eqn arg)) (*Proves a single recursor equation.*) (fn {context = ctxt, ...} => EVERY [resolve_tac ctxt [recursor_trans] 1, simp_tac (put_simpset rank_ss ctxt addsimps case_eqns) 1, IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt addsimps tl con_defs) 1)]); in thy2 |> Sign.add_path big_rec_base_name |> Global_Theory.add_thmss [((Binding.name "recursor_eqns", map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)), [])] ||> Sign.parent_path |>> the_single end val constructors = map (head_of o #1 o Logic.dest_equals o Thm.prop_of) (tl con_defs); val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs); val {intrs, elim, induct, mutual_induct, ...} = ind_result (*Typical theorems have the form ~con1=con2, con1=con2==>False, con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *) fun mk_free ctxt s = let val thy = Proof_Context.theory_of ctxt; in Goal.prove_global thy [] [] (Syntax.read_prop ctxt s) (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' con_defs, fast_tac (put_claset ZF_cs ctxt' addSEs free_SEs @ Su.free_SEs) 1]) end; val dt_info = {inductive = true, constructors = constructors, rec_rewrites = map Thm.trim_context recursor_eqns, case_rewrites = map Thm.trim_context case_eqns, induct = Thm.trim_context induct, mutual_induct = Thm.trim_context mutual_induct, exhaustion = Thm.trim_context elim}; val con_info = {big_rec_name = big_rec_name, constructors = constructors, (*let primrec handle definition by cases*) free_iffs = map Thm.trim_context free_iffs, rec_rewrites = (case recursor_eqns of [] => case_eqns | _ => recursor_eqns) |> map Thm.trim_context}; (*associate with each constructor the datatype name and rewrites*) val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors in (*Updating theory components: simprules and datatype info*) (thy3 |> Sign.add_path big_rec_base_name |> Global_Theory.add_thmss [((Binding.name "simps", case_eqns @ recursor_eqns), [Simplifier.simp_add]), ((Binding.empty, intrs), [Cla.safe_intro NONE]), ((Binding.name "con_defs", con_defs), []), ((Binding.name "free_iffs", free_iffs), []), ((Binding.name "free_elims", free_SEs), [])] |> #2 |> DatatypesData.map (Symtab.update (big_rec_name, dt_info)) |> ConstructorsData.map (fold Symtab.update con_pairs) |> Sign.parent_path, ind_result, {con_defs = con_defs, case_eqns = case_eqns, recursor_eqns = recursor_eqns, free_iffs = free_iffs, free_SEs = free_SEs, mk_free = mk_free}) end; fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy = let val ctxt = Proof_Context.init_global thy; fun read_is strs = map (Syntax.parse_term ctxt #> Type.constraint \<^typ>\i\) strs |> Syntax.check_terms ctxt; val rec_tms = read_is srec_tms; val con_ty_lists = Ind_Syntax.read_constructs ctxt scon_ty_lists; val dom_sum = if sdom = "" then data_domain coind (rec_tms, con_ty_lists) else singleton read_is sdom; val monos = Attrib.eval_thms ctxt raw_monos; val type_intrs = Attrib.eval_thms ctxt raw_type_intrs; val type_elims = Attrib.eval_thms ctxt raw_type_elims; in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end; (* outer syntax *) fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) = #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims); val con_decl = Parse.name -- Scan.optional (\<^keyword>\(\ |-- Parse.list1 Parse.term --| \<^keyword>\)\) [] -- Parse.opt_mixfix >> Scan.triple1; val coind_prefix = if coind then "co" else ""; val _ = Outer_Syntax.command (if coind then \<^command_keyword>\codatatype\ else \<^command_keyword>\datatype\) ("define " ^ coind_prefix ^ "datatype") ((Scan.optional ((\<^keyword>\\\ || \<^keyword>\<=\) |-- Parse.!!! Parse.term) "") -- Parse.and_list1 (Parse.term -- (\<^keyword>\=\ |-- Parse.enum1 "|" con_decl)) -- Scan.optional (\<^keyword>\monos\ |-- Parse.!!! Parse.thms1) [] -- Scan.optional (\<^keyword>\type_intros\ |-- Parse.!!! Parse.thms1) [] -- Scan.optional (\<^keyword>\type_elims\ |-- Parse.!!! Parse.thms1) [] >> (Toplevel.theory o mk_datatype)); end; diff --git a/src/ZF/Tools/induct_tacs.ML b/src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML +++ b/src/ZF/Tools/induct_tacs.ML @@ -1,206 +1,204 @@ (* Title: ZF/Tools/induct_tacs.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Induction and exhaustion tactics for Isabelle/ZF. The theory information needed to support them (and to support primrec). Also a function to install other sets as if they were datatypes. *) signature DATATYPE_TACTICS = sig val exhaust_tac: Proof.context -> string -> (binding * string option * mixfix) list -> int -> tactic val induct_tac: Proof.context -> string -> (binding * string option * mixfix) list -> int -> tactic val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory val rep_datatype: Facts.ref * Token.src list -> Facts.ref * Token.src list -> (Facts.ref * Token.src list) list -> (Facts.ref * Token.src list) list -> theory -> theory end; (** Datatype information, e.g. associated theorems **) type datatype_info = {inductive: bool, (*true if inductive, not coinductive*) constructors : term list, (*the constructors, as Consts*) rec_rewrites : thm list, (*recursor equations*) case_rewrites : thm list, (*case equations*) induct : thm, mutual_induct : thm, exhaustion : thm}; structure DatatypesData = Theory_Data ( type T = datatype_info Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data : T = Symtab.merge (K true) data; ); (** Constructor information: needed to map constructors to datatypes **) type constructor_info = {big_rec_name : string, (*name of the mutually recursive set*) constructors : term list, (*the constructors, as Consts*) free_iffs : thm list, (*freeness simprules*) rec_rewrites : thm list}; (*recursor equations*) structure ConstructorsData = Theory_Data ( type T = constructor_info Symtab.table val empty = Symtab.empty val extend = I fun merge data = Symtab.merge (K true) data; ); structure DatatypeTactics : DATATYPE_TACTICS = struct fun datatype_info thy name = (case Symtab.lookup (DatatypesData.get thy) name of SOME info => info | NONE => error ("Unknown datatype " ^ quote name)); (*Given a variable, find the inductive set associated it in the assumptions*) exception Find_tname of string fun find_tname ctxt var As = - let fun mk_pair (Const(\<^const_name>\mem\,_) $ Free (v,_) $ A) = - (v, #1 (dest_Const (head_of A))) + let fun mk_pair \<^Const_>\mem for \Free (v,_)\ A\ = (v, #1 (dest_Const (head_of A))) | mk_pair _ = raise Match val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop)) As val x = (case try (dest_Free o Syntax.read_term ctxt) var of SOME (x, _) => x | _ => raise Find_tname ("Bad variable " ^ quote var)) in case AList.lookup (op =) pairs x of NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var) | SOME t => t end; (** generic exhaustion and induction tactic for datatypes Differences from HOL: (1) no checking if the induction var occurs in premises, since it always appears in one of them, and it's hard to check for other occurrences (2) exhaustion works for VARIABLES in the premises, not general terms **) fun exhaust_induct_tac exh ctxt var fixes i state = SUBGOAL (fn _ => let val thy = Proof_Context.theory_of ctxt val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i NONE state val tn = find_tname ctxt' var (map Thm.term_of asms) val rule = datatype_info thy tn |> (if exh then #exhaustion else #induct) |> Thm.transfer thy; - val (Const(\<^const_name>\mem\,_) $ Var(ixn,_) $ _) = + val \<^Const_>\mem for \Var(ixn,_)\ _\ = (case Thm.prems_of rule of [] => error "induction is not available for this datatype" | major::_ => FOLogic.dest_Trueprop major) in Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] fixes rule i end handle Find_tname msg => if exh then (*try boolean case analysis instead*) case_tac ctxt var fixes i else error msg) i state; val exhaust_tac = exhaust_induct_tac true; val induct_tac = exhaust_induct_tac false; (**** declare non-datatype as datatype ****) fun rep_datatype_i elim induct case_eqns recursor_eqns thy = let (*analyze the LHS of a case equation to get a constructor*) - fun const_of (Const(\<^const_name>\IFOL.eq\, _) $ (_ $ c) $ _) = c + fun const_of \<^Const_>\IFOL.eq _ for \_ $ c\ _\ = c | const_of eqn = error ("Ill-formed case equation: " ^ Syntax.string_of_term_global thy eqn); val constructors = map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns; - val Const (\<^const_name>\mem\, _) $ _ $ data = - FOLogic.dest_Trueprop (hd (Thm.prems_of elim)); + val \<^Const_>\mem for _ data\ = FOLogic.dest_Trueprop (hd (Thm.prems_of elim)); val Const(big_rec_name, _) = head_of data; val simps = case_eqns @ recursor_eqns; val dt_info = {inductive = true, constructors = constructors, rec_rewrites = map Thm.trim_context recursor_eqns, case_rewrites = map Thm.trim_context case_eqns, induct = Thm.trim_context induct, mutual_induct = Thm.trim_context @{thm TrueI}, (*No need for mutual induction*) exhaustion = Thm.trim_context elim}; val con_info = {big_rec_name = big_rec_name, constructors = constructors, (*let primrec handle definition by cases*) free_iffs = [], (*thus we expect the necessary freeness rewrites to be in the simpset already, as is the case for Nat and disjoint sum*) rec_rewrites = (case recursor_eqns of [] => case_eqns | _ => recursor_eqns) |> map Thm.trim_context}; (*associate with each constructor the datatype name and rewrites*) val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors in thy |> Sign.add_path (Long_Name.base_name big_rec_name) |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy)) |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy)) |> Sign.parent_path end; fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy = let val ctxt = Proof_Context.init_global thy; val elim = Facts.the_single ("elimination", Position.none) (Attrib.eval_thms ctxt [raw_elim]); val induct = Facts.the_single ("induction", Position.none) (Attrib.eval_thms ctxt [raw_induct]); val case_eqns = Attrib.eval_thms ctxt raw_case_eqns; val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns; in rep_datatype_i elim induct case_eqns recursor_eqns thy end; (* theory setup *) val _ = Theory.setup (Method.setup \<^binding>\induct_tac\ (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >> (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s xs))) "induct_tac emulation (dynamic instantiation!)" #> Method.setup \<^binding>\case_tac\ (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >> (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s xs))) "datatype case_tac emulation (dynamic instantiation!)"); (* outer syntax *) val _ = Outer_Syntax.command \<^command_keyword>\rep_datatype\ "represent existing set inductively" ((\<^keyword>\elimination\ |-- Parse.!!! Parse.thm) -- (\<^keyword>\induction\ |-- Parse.!!! Parse.thm) -- (\<^keyword>\case_eqns\ |-- Parse.!!! Parse.thms1) -- Scan.optional (\<^keyword>\recursor_eqns\ |-- Parse.!!! Parse.thms1) [] >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w))); end; val exhaust_tac = DatatypeTactics.exhaust_tac; val induct_tac = DatatypeTactics.induct_tac; diff --git a/src/ZF/Tools/inductive_package.ML b/src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML +++ b/src/ZF/Tools/inductive_package.ML @@ -1,612 +1,611 @@ (* Title: ZF/Tools/inductive_package.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Fixedpoint definition module -- for Inductive/Coinductive Definitions The functor will be instantiated for normal sums/products (inductive defs) and non-standard sums/products (coinductive defs) Sums are used only for mutual recursion; Products are used only to derive "streamlined" induction rules for relations *) type inductive_result = {defs : thm list, (*definitions made in thy*) bnd_mono : thm, (*monotonicity for the lfp definition*) dom_subset : thm, (*inclusion of recursive set in dom*) intrs : thm list, (*introduction rules*) elim : thm, (*case analysis theorem*) induct : thm, (*main induction rule*) mutual_induct : thm}; (*mutual induction rule*) (*Functor's result signature*) signature INDUCTIVE_PACKAGE = sig (*Insert definitions for the recursive sets, which must *already* be declared as constants in parent theory!*) val add_inductive_i: bool -> term list * term -> ((binding * term) * attribute list) list -> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result val add_inductive: string list * string -> ((binding * string) * Token.src list) list -> (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list -> theory -> theory * inductive_result end; (*Declares functions to add fixedpoint/constructor defs to a theory. Recursive sets must *already* be declared as constants.*) functor Add_inductive_def_Fun (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU val coind: bool) : INDUCTIVE_PACKAGE = struct val co_prefix = if coind then "co" else ""; (* utils *) (*make distinct individual variables a1, a2, a3, ..., an. *) fun mk_frees a [] = [] | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (Symbol.bump_string a) Ts; (* add_inductive(_i) *) (*internal version, accepting terms*) fun add_inductive_i verbose (rec_tms, dom_sum) raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy0 = let val ctxt0 = Proof_Context.init_global thy0; val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs; val (intr_names, intr_tms) = split_list (map fst intr_specs); val case_names = Rule_Cases.case_names intr_names; (*recT and rec_params should agree for all mutually recursive components*) val rec_hds = map head_of rec_tms; val dummy = rec_hds |> forall (fn t => is_Const t orelse error ("Recursive set not previously declared as constant: " ^ Syntax.string_of_term ctxt0 t)); (*Now we know they are all Consts, so get their names, type and params*) val rec_names = map (#1 o dest_Const) rec_hds and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); val rec_base_names = map Long_Name.base_name rec_names; val dummy = rec_base_names |> forall (fn a => Symbol_Pos.is_identifier a orelse error ("Base name of recursive set not an identifier: " ^ a)); local (*Checking the introduction rules*) val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy0) intr_tms; fun intr_ok set = case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false; in val dummy = intr_sets |> forall (fn t => intr_ok t orelse error ("Conclusion of rule does not name a recursive set: " ^ Syntax.string_of_term ctxt0 t)); end; val dummy = rec_params |> forall (fn t => is_Free t orelse error ("Param in recursion term not a free variable: " ^ Syntax.string_of_term ctxt0 t)); (*** Construct the fixedpoint definition ***) val mk_variant = singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] intr_tms)); val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w"; - fun dest_tprop (Const(\<^const_name>\Trueprop\,_) $ P) = P + fun dest_tprop \<^Const_>\Trueprop for P\ = P | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ Syntax.string_of_term ctxt0 Q); (*Makes a disjunct from an introduction rule*) fun fp_part intr = (*quantify over rule's free vars except parameters*) let val prems = map dest_tprop (Logic.strip_imp_prems intr) val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds val exfrees = subtract (op =) rec_params (Misc_Legacy.term_frees intr) val zeq = FOLogic.mk_eq (Free(z', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl intr)) in List.foldr FOLogic.mk_exists (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees end; (*The Part(A,h) terms -- compose injections to make h*) fun mk_Part (Bound 0) = Free(X', Ind_Syntax.iT) (*no mutual rec, no Part needed*) | mk_Part h = \<^const>\Part\ $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h); (*Access to balanced disjoint sums via injections*) val parts = map mk_Part (Balanced_Tree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0} (length rec_tms)); (*replace each set by the corresponding Part(A,h)*) val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms; val fp_abs = absfree (X', Ind_Syntax.iT) (Ind_Syntax.mk_Collect (z', dom_sum, Balanced_Tree.make FOLogic.mk_disj part_intrs)); val fp_rhs = Fp.oper $ dom_sum $ fp_abs val dummy = List.app (fn rec_hd => (Logic.occs (rec_hd, fp_rhs) andalso error "Illegal occurrence of recursion operator"; ())) rec_hds; (*** Make the new theory ***) (*A key definition: If no mutual recursion then it equals the one recursive set. If mutual recursion then it differs from all the recursive sets. *) val big_rec_base_name = space_implode "_" rec_base_names; val big_rec_name = Proof_Context.intern_const ctxt0 big_rec_base_name; val _ = if verbose then writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name) else (); (*Big_rec... is the union of the mutually recursive sets*) val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); (*The individual sets must already be declared*) val axpairs = map Misc_Legacy.mk_defpair ((big_rec_tm, fp_rhs) :: (case parts of [_] => [] (*no mutual recursion*) | _ => rec_tms ~~ (*define the sets as Parts*) map (subst_atomic [(Free (X', Ind_Syntax.iT), big_rec_tm)]) parts)); (*tracing: print the fixedpoint definition*) val dummy = if !Ind_Syntax.trace then writeln (cat_lines (map (Syntax.string_of_term ctxt0 o #2) axpairs)) else () (*add definitions of the inductive sets*) val (_, thy1) = thy0 |> Sign.add_path big_rec_base_name |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs); (*fetch fp definitions from the theory*) val big_rec_def::part_rec_defs = map (Misc_Legacy.get_def thy1) (case rec_names of [_] => rec_names | _ => big_rec_base_name::rec_names); (********) val dummy = writeln " Proving monotonicity..."; val bnd_mono0 = Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)) (fn {context = ctxt, ...} => EVERY [resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1, REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]); val dom_subset0 = Drule.export_without_context (big_rec_def RS Fp.subs); val ([bnd_mono, dom_subset], thy2) = thy1 |> Global_Theory.add_thms [((Binding.name "bnd_mono", bnd_mono0), []), ((Binding.name "dom_subset", dom_subset0), [])]; val unfold = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.Tarski); (********) val dummy = writeln " Proving the introduction rules..."; (*Mutual recursion? Helps to derive subset rules for the individual sets.*) val Part_trans = case rec_names of [_] => asm_rl | _ => Drule.export_without_context (@{thm Part_subset} RS @{thm subset_trans}); (*To type-check recursive occurrences of the inductive sets, possibly enclosed in some monotonic operator M.*) val rec_typechecks = [dom_subset] RL (asm_rl :: ([Part_trans] RL monos)) RL [@{thm subsetD}]; (*Type-checking is hardest aspect of proof; disjIn selects the correct disjunct after unfolding*) fun intro_tacsf disjIn ctxt = [DETERM (stac ctxt unfold 1), REPEAT (resolve_tac ctxt [@{thm Part_eqI}, @{thm CollectI}] 1), (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*) resolve_tac ctxt [disjIn] 2, (*Not ares_tac, since refl must be tried before equality assumptions; backtracking may occur if the premises have extra variables!*) DEPTH_SOLVE_1 (resolve_tac ctxt [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac ctxt 2), (*Now solve the equations like Tcons(a,f) = Inl(?b4)*) rewrite_goals_tac ctxt con_defs, REPEAT (resolve_tac ctxt @{thms refl} 2), (*Typechecking; this can fail*) if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:" else all_tac, REPEAT (FIRSTGOAL (dresolve_tac ctxt rec_typechecks ORELSE' eresolve_tac ctxt (asm_rl :: @{thm PartE} :: @{thm SigmaE2} :: type_elims) ORELSE' hyp_subst_tac ctxt)), if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:" else all_tac, DEPTH_SOLVE (swap_res_tac ctxt (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)]; (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*) val mk_disj_rls = Balanced_Tree.accesses {left = fn rl => rl RS @{thm disjI1}, right = fn rl => rl RS @{thm disjI2}, init = @{thm asm_rl}}; val intrs0 = (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms))) |> ListPair.map (fn (t, tacs) => Goal.prove_global thy2 [] [] t (fn {context = ctxt, ...} => EVERY (rewrite_goals_tac ctxt part_rec_defs :: tacs ctxt))); val ([intrs], thy3) = thy2 |> Global_Theory.add_thmss [((Binding.name "intros", intrs0), [])]; val ctxt3 = Proof_Context.init_global thy3; (********) val dummy = writeln " Proving the elimination rule..."; (*Breaks down logical connectives in the monotonic function*) fun basic_elim_tac ctxt = REPEAT (SOMEGOAL (eresolve_tac ctxt (Ind_Syntax.elim_rls @ Su.free_SEs) ORELSE' bound_hyp_subst_tac ctxt)) THEN prune_params_tac ctxt (*Mutual recursion: collapse references to Part(D,h)*) THEN (PRIMITIVE (fold_rule ctxt part_rec_defs)); (*Elimination*) val (elim, thy4) = thy3 |> Global_Theory.add_thm ((Binding.name "elim", rule_by_tactic ctxt3 (basic_elim_tac ctxt3) (unfold RS Ind_Syntax.equals_CollectD)), []); val ctxt4 = Proof_Context.init_global thy4; (*Applies freeness of the given constructors, which *must* be unfolded by the given defs. Cannot simply use the local con_defs because con_defs=[] for inference systems. Proposition A should have the form t:Si where Si is an inductive set*) fun make_cases ctxt A = rule_by_tactic ctxt (basic_elim_tac ctxt THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac ctxt) (Thm.assume A RS elim) |> Drule.export_without_context_open; fun induction_rules raw_induct = let val dummy = writeln " Proving the induction rule..."; (*** Prove the main induction rule ***) val pred_name = "P"; (*name for predicate variables*) (*Used to make induction rules; ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops prem is a premise of an intr rule*) - fun add_induct_prem ind_alist (prem as Const (\<^const_name>\Trueprop\, _) $ - (Const (\<^const_name>\mem\, _) $ t $ X), iprems) = + fun add_induct_prem ind_alist (prem as \<^Const_>\Trueprop for \\<^Const_>\mem for t X\\\, iprems) = (case AList.lookup (op aconv) ind_alist X of SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems | NONE => (*possibly membership in M(rec_tm), for M monotone*) let fun mk_sb (rec_tm,pred) = (rec_tm, \<^const>\Collect\ $ rec_tm $ pred) in subst_free (map mk_sb ind_alist) prem :: iprems end) | add_induct_prem ind_alist (prem,iprems) = prem :: iprems; (*Make a premise of the induction rule.*) fun induct_prem ind_alist intr = let val xs = subtract (op =) rec_params (Misc_Legacy.term_frees intr) val iprems = List.foldr (add_induct_prem ind_alist) [] (Logic.strip_imp_prems intr) val (t,X) = Ind_Syntax.rule_concl intr val (SOME pred) = AList.lookup (op aconv) ind_alist X val concl = FOLogic.mk_Trueprop (pred $ t) in fold_rev Logic.all xs (Logic.list_implies (iprems,concl)) end handle Bind => error"Recursion term not found in conclusion"; (*Minimizes backtracking by delivering the correct premise to each goal. Intro rules with extra Vars in premises still cause some backtracking *) fun ind_tac _ [] 0 = all_tac | ind_tac ctxt (prem::prems) i = DEPTH_SOLVE_1 (ares_tac ctxt [prem, @{thm refl}] i) THEN ind_tac ctxt prems (i-1); val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT); val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms; val dummy = if ! Ind_Syntax.trace then writeln (cat_lines (["ind_prems:"] @ map (Syntax.string_of_term ctxt4) ind_prems @ ["raw_induct:", Thm.string_of_thm ctxt4 raw_induct])) else (); (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules. If the premises get simplified, then the proofs could fail.*) val min_ss = (empty_simpset ctxt4 |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)) setSolver (mk_solver "minimal" (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) ORELSE' assume_tac ctxt ORELSE' eresolve_tac ctxt @{thms FalseE})); val quant_induct = Goal.prove_global thy4 [] ind_prems (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred))) (fn {context = ctxt, prems} => EVERY [rewrite_goals_tac ctxt part_rec_defs, resolve_tac ctxt [@{thm impI} RS @{thm allI}] 1, DETERM (eresolve_tac ctxt [raw_induct] 1), (*Push Part inside Collect*) full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1, (*This CollectE and disjE separates out the introduction rules*) REPEAT (FIRSTGOAL (eresolve_tac ctxt [@{thm CollectE}, @{thm disjE}])), (*Now break down the individual cases. No disjE here in case some premise involves disjunction.*) REPEAT (FIRSTGOAL (eresolve_tac ctxt [@{thm CollectE}, @{thm exE}, @{thm conjE}] ORELSE' (bound_hyp_subst_tac ctxt))), ind_tac ctxt (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]); val dummy = if ! Ind_Syntax.trace then writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt4 quant_induct) else (); (*** Prove the simultaneous induction rule ***) (*Make distinct predicates for each inductive set*) (*The components of the element type, several if it is a product*) val elem_type = CP.pseudo_type dom_sum; val elem_factors = CP.factors elem_type; val elem_frees = mk_frees "za" elem_factors; val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees; (*Given a recursive set and its domain, return the "fsplit" predicate and a conclusion for the simultaneous induction rule. NOTE. This will not work for mutually recursive predicates. Previously a summand 'domt' was also an argument, but this required the domain of mutual recursion to invariably be a disjoint sum.*) fun mk_predpair rec_tm = let val rec_name = (#1 o dest_Const o head_of) rec_tm val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name, elem_factors ---> FOLogic.oT) val qconcl = List.foldr FOLogic.mk_all (FOLogic.imp $ (\<^const>\mem\ $ elem_tuple $ rec_tm) $ (list_comb (pfree, elem_frees))) elem_frees in (CP.ap_split elem_type FOLogic.oT pfree, qconcl) end; val (preds,qconcls) = split_list (map mk_predpair rec_tms); (*Used to form simultaneous induction lemma*) fun mk_rec_imp (rec_tm,pred) = FOLogic.imp $ (\<^const>\mem\ $ Bound 0 $ rec_tm) $ (pred $ Bound 0); (*To instantiate the main induction rule*) val induct_concl = FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, Abs("z", Ind_Syntax.iT, Balanced_Tree.make FOLogic.mk_conj (ListPair.map mk_rec_imp (rec_tms, preds))))) and mutual_induct_concl = FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls); val dummy = if !Ind_Syntax.trace then (writeln ("induct_concl = " ^ Syntax.string_of_term ctxt4 induct_concl); writeln ("mutual_induct_concl = " ^ Syntax.string_of_term ctxt4 mutual_induct_concl)) else (); fun lemma_tac ctxt = FIRST' [eresolve_tac ctxt [@{thm asm_rl}, @{thm conjE}, @{thm PartE}, @{thm mp}], resolve_tac ctxt [@{thm allI}, @{thm impI}, @{thm conjI}, @{thm Part_eqI}], dresolve_tac ctxt [@{thm spec}, @{thm mp}, Pr.fsplitD]]; val need_mutual = length rec_names > 1; val lemma = (*makes the link between the two induction rules*) if need_mutual then (writeln " Proving the mutual induction rule..."; Goal.prove_global thy4 [] [] (Logic.mk_implies (induct_concl, mutual_induct_concl)) (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt part_rec_defs, REPEAT (rewrite_goals_tac ctxt [Pr.split_eq] THEN lemma_tac ctxt 1)])) else (writeln " [ No mutual induction rule needed ]"; @{thm TrueI}); val dummy = if ! Ind_Syntax.trace then writeln ("lemma: " ^ Thm.string_of_thm ctxt4 lemma) else (); (*Mutual induction follows by freeness of Inl/Inr.*) (*Simplification largely reduces the mutual induction rule to the standard rule*) val mut_ss = min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff]; val all_defs = con_defs @ part_rec_defs; (*Removes Collects caused by M-operators in the intro rules. It is very hard to simplify list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))}) where t==Part(tf,Inl) and f==Part(tf,Inr) to list({v: tf. P_t(v)}). Instead the following rules extract the relevant conjunct. *) val cmonos = [@{thm subset_refl} RS @{thm Collect_mono}] RL monos RLN (2,[@{thm rev_subsetD}]); (*Minimizes backtracking by delivering the correct premise to each goal*) fun mutual_ind_tac _ [] 0 = all_tac | mutual_ind_tac ctxt (prem::prems) i = DETERM (SELECT_GOAL ( (*Simplify the assumptions and goal by unfolding Part and using freeness of the Sum constructors; proves all but one conjunct by contradiction*) rewrite_goals_tac ctxt all_defs THEN simp_tac (mut_ss addsimps [@{thm Part_iff}]) 1 THEN IF_UNSOLVED (*simp_tac may have finished it off!*) ((*simplify assumptions*) (*some risk of excessive simplification here -- might have to identify the bare minimum set of rewrites*) full_simp_tac (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1 THEN (*unpackage and use "prem" in the corresponding place*) REPEAT (resolve_tac ctxt @{thms impI} 1) THEN resolve_tac ctxt [rewrite_rule ctxt all_defs prem] 1 THEN (*prem must not be REPEATed below: could loop!*) DEPTH_SOLVE (FIRSTGOAL (ares_tac ctxt [@{thm impI}] ORELSE' eresolve_tac ctxt (@{thm conjE} :: @{thm mp} :: cmonos)))) ) i) THEN mutual_ind_tac ctxt prems (i-1); val mutual_induct_fsplit = if need_mutual then Goal.prove_global thy4 [] (map (induct_prem (rec_tms~~preds)) intr_tms) mutual_induct_concl (fn {context = ctxt, prems} => EVERY [resolve_tac ctxt [quant_induct RS lemma] 1, mutual_ind_tac ctxt (rev prems) (length prems)]) else @{thm TrueI}; (** Uncurrying the predicate in the ordinary induction rule **) (*instantiate the variable to a tuple, if it is non-trivial, in order to allow the predicate to be "opened up". The name "x.1" comes from the "RS spec" !*) val inst = case elem_frees of [_] => I | _ => Drule.instantiate_normalize (TVars.empty, Vars.make [(\<^var>\?x1::i\, Thm.global_cterm_of thy4 elem_tuple)]); (*strip quantifier and the implication*) val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp})); - val Const (\<^const_name>\Trueprop\, _) $ (pred_var $ _) = Thm.concl_of induct0 + val \<^Const_>\Trueprop for \pred_var $ _\\ = Thm.concl_of induct0 val induct0 = CP.split_rule_var ctxt4 (pred_var, elem_type-->FOLogic.oT, induct0) |> Drule.export_without_context and mutual_induct = CP.remove_split ctxt4 mutual_induct_fsplit val ([induct, mutual_induct], thy5) = thy4 |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct0), [case_names, Induct.induct_pred big_rec_name]), ((Binding.name "mutual_induct", mutual_induct), [case_names])]; in ((induct, mutual_induct), thy5) end; (*of induction_rules*) val raw_induct = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.induct) val ((induct, mutual_induct), thy5) = if not coind then induction_rules raw_induct else thy4 |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])] |> apfst (hd #> pair @{thm TrueI}); val (([cases], [defs]), thy6) = thy5 |> IndCases.declare big_rec_name make_cases |> Global_Theory.add_thms [((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])] ||>> (Global_Theory.add_thmss o map Thm.no_attributes) [(Binding.name "defs", big_rec_def :: part_rec_defs)]; val (named_intrs, thy7) = thy6 |> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs) ~~ map #2 intr_specs) ||> Sign.parent_path; in (thy7, {defs = defs, bnd_mono = bnd_mono, dom_subset = dom_subset, intrs = named_intrs, elim = cases, induct = induct, mutual_induct = mutual_induct}) end; (*source version*) fun add_inductive (srec_tms, sdom_sum) intr_srcs (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy = let val ctxt = Proof_Context.init_global thy; val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT) #> Syntax.check_terms ctxt; val intr_atts = map (map (Attrib.attribute_cmd ctxt) o snd) intr_srcs; val sintrs = map fst intr_srcs ~~ intr_atts; val rec_tms = read_terms srec_tms; val dom_sum = singleton read_terms sdom_sum; val intr_tms = Syntax.read_props ctxt (map (snd o fst) sintrs); val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs; val monos = Attrib.eval_thms ctxt raw_monos; val con_defs = Attrib.eval_thms ctxt raw_con_defs; val type_intrs = Attrib.eval_thms ctxt raw_type_intrs; val type_elims = Attrib.eval_thms ctxt raw_type_elims; in thy |> add_inductive_i true (rec_tms, dom_sum) intr_specs (monos, con_defs, type_intrs, type_elims) end; (* outer syntax *) fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) = #1 o add_inductive doms (map (fn ((x, y), z) => ((x, z), y)) intrs) (monos, con_defs, type_intrs, type_elims); val ind_decl = (\<^keyword>\domains\ |-- Parse.!!! (Parse.enum1 "+" Parse.term -- ((\<^keyword>\\\ || \<^keyword>\<=\) |-- Parse.term))) -- (\<^keyword>\intros\ |-- Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) -- Scan.optional (\<^keyword>\monos\ |-- Parse.!!! Parse.thms1) [] -- Scan.optional (\<^keyword>\con_defs\ |-- Parse.!!! Parse.thms1) [] -- Scan.optional (\<^keyword>\type_intros\ |-- Parse.!!! Parse.thms1) [] -- Scan.optional (\<^keyword>\type_elims\ |-- Parse.!!! Parse.thms1) [] >> (Toplevel.theory o mk_ind); val _ = Outer_Syntax.command (if coind then \<^command_keyword>\coinductive\ else \<^command_keyword>\inductive\) ("define " ^ co_prefix ^ "inductive sets") ind_decl; end; diff --git a/src/ZF/Tools/primrec_package.ML b/src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML +++ b/src/ZF/Tools/primrec_package.ML @@ -1,204 +1,203 @@ (* Title: ZF/Tools/primrec_package.ML Author: Norbert Voelker, FernUni Hagen Author: Stefan Berghofer, TU Muenchen Author: Lawrence C Paulson, Cambridge University Computer Laboratory Package for defining functions on datatypes by primitive recursion. *) signature PRIMREC_PACKAGE = sig val primrec: ((binding * string) * Token.src list) list -> theory -> thm list * theory val primrec_i: ((binding * term) * attribute list) list -> theory -> thm list * theory end; structure PrimrecPackage : PRIMREC_PACKAGE = struct exception RecError of string; (*Remove outer Trueprop and equality sign*) val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop; fun primrec_err s = error ("Primrec definition error:\n" ^ s); fun primrec_eq_err sign s eq = primrec_err (s ^ "\nin equation\n" ^ Syntax.string_of_term_global sign eq); (* preprocessing of equations *) (*rec_fn_opt records equations already noted for this function*) fun process_eqn thy (eq, rec_fn_opt) = let val (lhs, rhs) = if null (Term.add_vars eq []) then dest_eqn eq handle TERM _ => raise RecError "not a proper equation" else raise RecError "illegal schematic variable(s)"; val (recfun, args) = strip_comb lhs; val (fname, ftype) = dest_Const recfun handle TERM _ => raise RecError "function is not declared as constant in theory"; val (ls_frees, rest) = chop_prefix is_Free args; val (middle, rs_frees) = chop_suffix is_Free rest; val (constr, cargs_frees) = if null middle then raise RecError "constructor missing" else strip_comb (hd middle); val (cname, _) = dest_Const constr handle TERM _ => raise RecError "ill-formed constructor"; val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname) handle Option.Option => raise RecError "cannot determine datatype associated with function" val (ls, cargs, rs) = (map dest_Free ls_frees, map dest_Free cargs_frees, map dest_Free rs_frees) handle TERM _ => raise RecError "illegal argument in pattern"; val lfrees = ls @ rs @ cargs; (*Constructor, frees to left of pattern, pattern variables, frees to right of pattern, rhs of equation, full original equation. *) val new_eqn = (cname, (rhs, cargs, eq)) in if has_duplicates (op =) lfrees then raise RecError "repeated variable name in pattern" else if not (subset (op =) (Term.add_frees rhs [], lfrees)) then raise RecError "extra variables on rhs" else if length middle > 1 then raise RecError "more than one non-variable in pattern" else case rec_fn_opt of NONE => SOME (fname, ftype, ls, rs, con_info, [new_eqn]) | SOME (fname', _, ls', rs', con_info': constructor_info, eqns) => if AList.defined (op =) eqns cname then raise RecError "constructor already occurred as pattern" else if (ls <> ls') orelse (rs <> rs') then raise RecError "non-recursive arguments are inconsistent" else if #big_rec_name con_info <> #big_rec_name con_info' then raise RecError ("Mixed datatypes for function " ^ fname) else if fname <> fname' then raise RecError ("inconsistent functions for datatype " ^ #big_rec_name con_info) else SOME (fname, ftype, ls, rs, con_info, new_eqn::eqns) end handle RecError s => primrec_eq_err thy s eq; (*Instantiates a recursor equation with constructor arguments*) fun inst_recursor ((_ $ constr, rhs), cargs') = subst_atomic (#2 (strip_comb constr) ~~ map Free cargs') rhs; (*Convert a list of recursion equations into a recursor call*) fun process_fun thy (fname, ftype, ls, rs, con_info: constructor_info, eqns) = let val fconst = Const(fname, ftype) val fabs = list_comb (fconst, map Free ls @ [Bound 0] @ map Free rs) and {big_rec_name, constructors, rec_rewrites, ...} = con_info (*Replace X_rec(args,t) by fname(ls,t,rs) *) fun use_fabs (_ $ t) = subst_bound (t, fabs) | use_fabs t = t val cnames = map (#1 o dest_Const) constructors and recursor_pairs = map (dest_eqn o Thm.concl_of) rec_rewrites fun absterm (Free x, body) = absfree x body | absterm (t, body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body)) (*Translate rec equations into function arguments suitable for recursor. Missing cases are replaced by 0 and all cases are put into order.*) fun add_case ((cname, recursor_pair), cases) = let val (rhs, recursor_rhs, eq) = case AList.lookup (op =) eqns cname of NONE => (warning ("no equation for constructor " ^ cname ^ "\nin definition of function " ^ fname); - (Const (\<^const_name>\zero\, Ind_Syntax.iT), - #2 recursor_pair, Const (\<^const_name>\zero\, Ind_Syntax.iT))) + (\<^Const>\zero\, #2 recursor_pair, \<^Const>\zero\)) | SOME (rhs, cargs', eq) => (rhs, inst_recursor (recursor_pair, cargs'), eq) val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs)) val abs = List.foldr absterm rhs allowed_terms in if !Ind_Syntax.trace then writeln ("recursor_rhs = " ^ Syntax.string_of_term_global thy recursor_rhs ^ "\nabs = " ^ Syntax.string_of_term_global thy abs) else(); if Logic.occs (fconst, abs) then primrec_eq_err thy ("illegal recursive occurrences of " ^ fname) eq else abs :: cases end val recursor = head_of (#1 (hd recursor_pairs)) (** make definition **) (*the recursive argument*) val rec_arg = Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name), Ind_Syntax.iT) val def_tm = Logic.mk_equals (subst_bound (rec_arg, fabs), list_comb (recursor, List.foldr add_case [] (cnames ~~ recursor_pairs)) $ rec_arg) in if !Ind_Syntax.trace then writeln ("primrec def:\n" ^ Syntax.string_of_term_global thy def_tm) else(); (Long_Name.base_name fname ^ "_" ^ Long_Name.base_name big_rec_name ^ "_def", def_tm) end; (* prepare functions needed for definitions *) fun primrec_i args thy = let val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args); val SOME (fname, ftype, ls, rs, con_info, eqns) = List.foldr (process_eqn thy) NONE eqn_terms; val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns); val ([def_thm], thy1) = thy |> Sign.add_path (Long_Name.base_name fname) |> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)]; val rewrites = def_thm :: map (mk_meta_eq o Thm.transfer thy1) (#rec_rewrites con_info) val eqn_thms0 = eqn_terms |> map (fn t => Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac ctxt @{thms refl} 1])); in thy1 |> Global_Theory.add_thms ((eqn_names ~~ eqn_thms0) ~~ eqn_atts) |-> (fn eqn_thms => Global_Theory.add_thmss [((Binding.name "simps", eqn_thms), [Simplifier.simp_add])]) |>> the_single ||> Sign.parent_path end; fun primrec args thy = primrec_i (map (fn ((name, s), srcs) => ((name, Syntax.read_prop_global thy s), map (Attrib.attribute_cmd_global thy) srcs)) args) thy; (* outer syntax *) val _ = Outer_Syntax.command \<^command_keyword>\primrec\ "define primitive recursive functions on datatypes" (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop) >> (Toplevel.theory o (#2 oo (primrec o map (fn ((x, y), z) => ((x, z), y)))))); end; diff --git a/src/ZF/Tools/typechk.ML b/src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML +++ b/src/ZF/Tools/typechk.ML @@ -1,132 +1,131 @@ (* Title: ZF/Tools/typechk.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge Automated type checking (cf. CTT). *) signature TYPE_CHECK = sig val print_tcset: Proof.context -> unit val TC_add: attribute val TC_del: attribute val typecheck_tac: Proof.context -> tactic val type_solver_tac: Proof.context -> thm list -> int -> tactic val type_solver: solver end; structure TypeCheck: TYPE_CHECK = struct (* datatype tcset *) datatype tcset = TC of {rules: thm list, (*the type-checking rules*) net: thm Net.net}; (*discrimination net of the same rules*) fun add_rule ctxt th (tcs as TC {rules, net}) = if member Thm.eq_thm_prop rules th then (warning ("Ignoring duplicate type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs) else TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net}; fun del_rule ctxt th (tcs as TC {rules, net}) = if member Thm.eq_thm_prop rules th then TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net, rules = remove Thm.eq_thm_prop th rules} else (warning ("No such type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs); (* generic data *) structure Data = Generic_Data ( type T = tcset; val empty = TC {rules = [], net = Net.empty}; val extend = I; fun merge (TC {rules, net}, TC {rules = rules', net = net'}) = TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')}; ); val TC_add = Thm.declaration_attribute (fn thm => fn context => Data.map (add_rule (Context.proof_of context) (Thm.trim_context thm)) context); val TC_del = Thm.declaration_attribute (fn thm => fn context => Data.map (del_rule (Context.proof_of context) thm) context); val tcset_of = Data.get o Context.Proof; fun print_tcset ctxt = let val TC {rules, ...} = tcset_of ctxt in Pretty.writeln (Pretty.big_list "type-checking rules:" (map (Thm.pretty_thm_item ctxt) rules)) end; (* tactics *) (*resolution using a net rather than rules*) fun net_res_tac ctxt maxr net = SUBGOAL (fn (prem, i) => let val rls = Net.unify_term net (Logic.strip_assums_concl prem) in if length rls <= maxr then resolve_tac ctxt rls i else no_tac end); -fun is_rigid_elem (Const(\<^const_name>\Trueprop\,_) $ (Const(\<^const_name>\mem\,_) $ a $ _)) = - not (is_Var (head_of a)) +fun is_rigid_elem \<^Const_>\Trueprop for \\<^Const_>\mem for a _\\\ = not (is_Var (head_of a)) | is_rigid_elem _ = false; (*Try solving a:A by assumption provided a is rigid!*) fun test_assume_tac ctxt = SUBGOAL(fn (prem,i) => if is_rigid_elem (Logic.strip_assums_concl prem) then assume_tac ctxt i else eq_assume_tac i); (*Type checking solves a:?A (a rigid, ?A maybe flexible). match_tac is too strict; would refuse to instantiate ?A*) fun typecheck_step_tac ctxt = let val TC {net, ...} = tcset_of ctxt in FIRSTGOAL (test_assume_tac ctxt ORELSE' net_res_tac ctxt 3 net) end; fun typecheck_tac ctxt = REPEAT (typecheck_step_tac ctxt); (*Compile a term-net for speed*) val basic_net = Tactic.build_net @{thms TrueI refl reflexive iff_refl ballI allI conjI impI}; (*Instantiates variables in typing conditions. drawback: does not simplify conjunctions*) fun type_solver_tac ctxt hyps = SELECT_GOAL (DEPTH_SOLVE (eresolve_tac ctxt @{thms FalseE} 1 ORELSE resolve_from_net_tac ctxt basic_net 1 ORELSE (ares_tac ctxt hyps 1 APPEND typecheck_step_tac ctxt))); val type_solver = Simplifier.mk_solver "ZF typecheck" (fn ctxt => type_solver_tac ctxt (Simplifier.prems_of ctxt)); val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt setSolver type_solver)); (* concrete syntax *) val _ = Theory.setup (Attrib.setup \<^binding>\TC\ (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #> Method.setup \<^binding>\typecheck\ (Method.sections [Args.add -- Args.colon >> K (Method.modifier TC_add \<^here>), Args.del -- Args.colon >> K (Method.modifier TC_del \<^here>)] >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))) "ZF type-checking"); val _ = Outer_Syntax.command \<^command_keyword>\print_tcset\ "print context of ZF typecheck" (Scan.succeed (Toplevel.keep (print_tcset o Toplevel.context_of))); end; diff --git a/src/ZF/arith_data.ML b/src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML +++ b/src/ZF/arith_data.ML @@ -1,283 +1,283 @@ (* Title: ZF/arith_data.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Arithmetic simplification: cancellation of common terms *) signature ARITH_DATA = sig (*the main outcome*) val nat_cancel: simproc list (*tools for use in similar applications*) val gen_trans_tac: Proof.context -> thm -> thm option -> tactic val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option val simplify_meta_eq: thm list -> Proof.context -> thm -> thm (*debugging*) structure EqCancelNumeralsData : CANCEL_NUMERALS_DATA structure LessCancelNumeralsData : CANCEL_NUMERALS_DATA structure DiffCancelNumeralsData : CANCEL_NUMERALS_DATA end; structure ArithData: ARITH_DATA = struct val iT = Ind_Syntax.iT; -val zero = Const(\<^const_name>\zero\, iT); -val succ = Const(\<^const_name>\succ\, iT --> iT); +val zero = \<^Const>\zero\; +val succ = \<^Const>\succ\; fun mk_succ t = succ $ t; val one = mk_succ zero; val mk_plus = FOLogic.mk_binop \<^const_name>\Arith.add\; (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) fun mk_sum [] = zero | mk_sum [t,u] = mk_plus (t, u) | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); (*this version ALWAYS includes a trailing zero*) fun long_mk_sum [] = zero | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); val dest_plus = FOLogic.dest_bin \<^const_name>\Arith.add\ iT; (* dest_sum *) -fun dest_sum (Const(\<^const_name>\zero\,_)) = [] - | dest_sum (Const(\<^const_name>\succ\,_) $ t) = one :: dest_sum t - | dest_sum (Const(\<^const_name>\Arith.add\,_) $ t $ u) = dest_sum t @ dest_sum u +fun dest_sum \<^Const_>\zero\ = [] + | dest_sum \<^Const_>\succ for t\ = one :: dest_sum t + | dest_sum \<^Const_>\Arith.add for t u\ = dest_sum t @ dest_sum u | dest_sum tm = [tm]; (*Apply the given rewrite (if present) just once*) fun gen_trans_tac _ _ NONE = all_tac | gen_trans_tac ctxt th2 (SOME th) = ALLGOALS (resolve_tac ctxt [th RS th2]); (*Use <-> or = depending on the type of t*) fun mk_eq_iff(t,u) = if fastype_of t = iT then FOLogic.mk_eq(t,u) else FOLogic.mk_iff(t,u); (*We remove equality assumptions because they confuse the simplifier and because only type-checking assumptions are necessary.*) fun is_eq_thm th = can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th)); fun add_chyps chyps ct = Drule.list_implies (map Thm.cprop_of chyps, ct); fun prove_conv name tacs ctxt prems (t,u) = if t aconv u then NONE else let val prems' = filter_out is_eq_thm prems val goal = Logic.list_implies (map Thm.prop_of prems', FOLogic.mk_Trueprop (mk_eq_iff (t, u))); in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs))) handle ERROR msg => (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE) end; (*** Use CancelNumerals simproc without binary numerals, just for cancellation ***) val mk_times = FOLogic.mk_binop \<^const_name>\Arith.mult\; fun mk_prod [] = one | mk_prod [t] = t | mk_prod (t :: ts) = if t = one then mk_prod ts else mk_times (t, mk_prod ts); val dest_times = FOLogic.dest_bin \<^const_name>\Arith.mult\ iT; fun dest_prod t = let val (t,u) = dest_times t in dest_prod t @ dest_prod u end handle TERM _ => [t]; (*Dummy version: the only arguments are 0 and 1*) fun mk_coeff (0, t) = zero | mk_coeff (1, t) = t | mk_coeff _ = raise TERM("mk_coeff", []); (*Dummy version: the "coefficient" is always 1. In the result, the factors are sorted terms*) fun dest_coeff t = (1, mk_prod (sort Term_Ord.term_ord (dest_prod t))); (*Find first coefficient-term THAT MATCHES u*) fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) | find_first_coeff past u (t::terms) = let val (n,u') = dest_coeff t in if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end handle TERM _ => find_first_coeff (t::past) u terms; (*Simplify #1*n and n*#1 to n*) val add_0s = [@{thm add_0_natify}, @{thm add_0_right_natify}]; val add_succs = [@{thm add_succ}, @{thm add_succ_right}]; val mult_1s = [@{thm mult_1_natify}, @{thm mult_1_right_natify}]; val tc_rules = [@{thm natify_in_nat}, @{thm add_type}, @{thm diff_type}, @{thm mult_type}]; val natifys = [@{thm natify_0}, @{thm natify_ident}, @{thm add_natify1}, @{thm add_natify2}, @{thm diff_natify1}, @{thm diff_natify2}]; (*Final simplification: cancel + and **) fun simplify_meta_eq rules ctxt = let val ctxt' = put_simpset FOL_ss ctxt delsimps @{thms iff_simps} (*these could erase the whole rule!*) addsimps rules |> fold Simplifier.add_eqcong [@{thm eq_cong2}, @{thm iff_cong2}] in mk_meta_eq o simplify ctxt' end; val final_rules = add_0s @ mult_1s @ [@{thm mult_0}, @{thm mult_0_right}]; structure CancelNumeralsCommon = struct val mk_sum = (fn T:typ => mk_sum) val dest_sum = dest_sum val mk_coeff = mk_coeff val dest_coeff = dest_coeff val find_first_coeff = find_first_coeff [] val norm_ss1 = simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ add_succs @ mult_1s @ @{thms add_ac}) val norm_ss2 = simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ mult_1s @ @{thms add_ac} @ @{thms mult_ac} @ tc_rules @ natifys) fun norm_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) val numeral_simp_ss = simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ tc_rules @ natifys) fun numeral_simp_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = simplify_meta_eq final_rules end; (** The functor argumnets are declared as separate structures so that they can be exported to ease debugging. **) structure EqCancelNumeralsData = struct open CancelNumeralsCommon val prove_conv = prove_conv "nateq_cancel_numerals" val mk_bal = FOLogic.mk_eq val dest_bal = FOLogic.dest_eq val bal_add1 = @{thm eq_add_iff [THEN iff_trans]} val bal_add2 = @{thm eq_add_iff [THEN iff_trans]} fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans} end; structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData); structure LessCancelNumeralsData = struct open CancelNumeralsCommon val prove_conv = prove_conv "natless_cancel_numerals" val mk_bal = FOLogic.mk_binrel \<^const_name>\Ordinal.lt\ val dest_bal = FOLogic.dest_bin \<^const_name>\Ordinal.lt\ iT val bal_add1 = @{thm less_add_iff [THEN iff_trans]} val bal_add2 = @{thm less_add_iff [THEN iff_trans]} fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans} end; structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData); structure DiffCancelNumeralsData = struct open CancelNumeralsCommon val prove_conv = prove_conv "natdiff_cancel_numerals" val mk_bal = FOLogic.mk_binop \<^const_name>\Arith.diff\ val dest_bal = FOLogic.dest_bin \<^const_name>\Arith.diff\ iT val bal_add1 = @{thm diff_add_eq [THEN trans]} val bal_add2 = @{thm diff_add_eq [THEN trans]} fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans} end; structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData); val nat_cancel = [Simplifier.make_simproc \<^context> "nateq_cancel_numerals" {lhss = [\<^term>\l #+ m = n\, \<^term>\l = m #+ n\, \<^term>\l #* m = n\, \<^term>\l = m #* n\, \<^term>\succ(m) = n\, \<^term>\m = succ(n)\], proc = K EqCancelNumerals.proc}, Simplifier.make_simproc \<^context> "natless_cancel_numerals" {lhss = [\<^term>\l #+ m < n\, \<^term>\l < m #+ n\, \<^term>\l #* m < n\, \<^term>\l < m #* n\, \<^term>\succ(m) < n\, \<^term>\m < succ(n)\], proc = K LessCancelNumerals.proc}, Simplifier.make_simproc \<^context> "natdiff_cancel_numerals" {lhss = [\<^term>\(l #+ m) #- n\, \<^term>\l #- (m #+ n)\, \<^term>\(l #* m) #- n\, \<^term>\l #- (m #* n)\, \<^term>\succ(m) #- n\, \<^term>\m #- succ(n)\], proc = K DiffCancelNumerals.proc}]; end; val _ = Theory.setup (Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs ArithData.nat_cancel)); (*examples: print_depth 22; set timing; set simp_trace; fun test s = (Goal s; by (Asm_simp_tac 1)); test "x #+ y = x #+ z"; test "y #+ x = x #+ z"; test "x #+ y #+ z = x #+ z"; test "y #+ (z #+ x) = z #+ x"; test "x #+ y #+ z = (z #+ y) #+ (x #+ w)"; test "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)"; test "x #+ succ(y) = x #+ z"; test "x #+ succ(y) = succ(z #+ x)"; test "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)"; test "(x #+ y) #- (x #+ z) = w"; test "(y #+ x) #- (x #+ z) = dd"; test "(x #+ y #+ z) #- (x #+ z) = dd"; test "(y #+ (z #+ x)) #- (z #+ x) = dd"; test "(x #+ y #+ z) #- ((z #+ y) #+ (x #+ w)) = dd"; test "(x#*y #+ z) #- ((z #+ y) #+ (y#*x #+ w)) = dd"; (*BAD occurrence of natify*) test "(x #+ succ(y)) #- (x #+ z) = dd"; test "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2"; test "(x #+ succ(y)) #- (succ(z #+ x)) = dd"; test "(succ(x) #+ succ(y) #+ z) #- (succ(z #+ y) #+ succ(x #+ w)) = dd"; (*use of typing information*) test "x : nat ==> x #+ y = x"; test "x : nat --> x #+ y = x"; test "x : nat ==> x #+ y < x"; test "x : nat ==> x < y#+x"; test "x : nat ==> x le succ(x)"; (*fails: no typing information isn't visible*) test "x #+ y = x"; test "x #+ y < x #+ z"; test "y #+ x < x #+ z"; test "x #+ y #+ z < x #+ z"; test "y #+ z #+ x < x #+ z"; test "y #+ (z #+ x) < z #+ x"; test "x #+ y #+ z < (z #+ y) #+ (x #+ w)"; test "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)"; test "x #+ succ(y) < x #+ z"; test "x #+ succ(y) < succ(z #+ x)"; test "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)"; test "x #+ succ(y) le succ(z #+ x)"; *) diff --git a/src/ZF/ind_syntax.ML b/src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML +++ b/src/ZF/ind_syntax.ML @@ -1,122 +1,121 @@ (* Title: ZF/ind_syntax.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Abstract Syntax functions for Inductive Definitions. *) structure Ind_Syntax = struct (*Print tracing messages during processing of "inductive" theory sections*) val trace = Unsynchronized.ref false; fun traceIt msg thy t = if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t) else t; (** Abstract syntax definitions for ZF **) -val iT = Type(\<^type_name>\i\, []); +val iT = \<^Type>\i\; (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) fun mk_all_imp (A,P) = FOLogic.all_const iT $ Abs("v", iT, FOLogic.imp $ (\<^const>\mem\ $ Bound 0 $ A) $ Term.betapply(P, Bound 0)); fun mk_Collect (a, D, t) = \<^const>\Collect\ $ D $ absfree (a, iT) t; (*simple error-checking in the premises of an inductive definition*) -fun chk_prem rec_hd (Const (\<^const_name>\conj\, _) $ _ $ _) = +fun chk_prem rec_hd \<^Const_>\conj for _ _\ = error"Premises may not be conjuctive" - | chk_prem rec_hd (Const (\<^const_name>\mem\, _) $ t $ X) = + | chk_prem rec_hd \<^Const_>\mem for t X\ = (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ()) | chk_prem rec_hd t = (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ()); (*Return the conclusion of a rule, of the form t:X*) fun rule_concl rl = - let val Const (\<^const_name>\Trueprop\, _) $ (Const (\<^const_name>\mem\, _) $ t $ X) = - Logic.strip_imp_concl rl + let val \<^Const_>\Trueprop for \\<^Const_>\mem for t X\\\ = Logic.strip_imp_concl rl in (t,X) end; (*As above, but return error message if bad*) fun rule_concl_msg sign rl = rule_concl rl handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ Syntax.string_of_term_global sign rl); (*For deriving cases rules. CollectD2 discards the domain, which is redundant; read_instantiate replaces a propositional variable by a formula variable*) val equals_CollectD = Rule_Insts.read_instantiate \<^context> [((("W", 0), Position.none), "Q")] ["Q"] (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2})); (** For datatype definitions **) (*Constructor name, type, mixfix info; internal name from mixfix, datatype sets, full premises*) type constructor_spec = (string * typ * mixfix) * string * term list * term list; -fun dest_mem (Const (\<^const_name>\mem\, _) $ x $ A) = (x, A) +fun dest_mem \<^Const_>\mem for x A\ = (x, A) | dest_mem _ = error "Constructor specifications must have the form x:A"; (*read a constructor specification*) fun read_construct ctxt (id: string, sprems, syn: mixfix) = let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems |> Syntax.check_terms ctxt val args = map (#1 o dest_mem) prems val T = (map (#2 o dest_Free) args) ---> iT handle TERM _ => error "Bad variable in constructor specification" in ((id,T,syn), id, args, prems) end; val read_constructs = map o map o read_construct; (*convert constructor specifications into introduction rules*) fun mk_intr_tms sg (rec_tm, constructs) = let fun mk_intr ((id,T,syn), name, args, prems) = Logic.list_implies (map FOLogic.mk_Trueprop prems, FOLogic.mk_Trueprop (\<^const>\mem\ $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm)) in map mk_intr constructs end; fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg); fun mk_Un (t1, t2) = \<^const>\Un\ $ t1 $ t2; (*Make a datatype's domain: form the union of its set parameters*) fun union_params (rec_tm, cs) = let val (_,args) = strip_comb rec_tm fun is_ind arg = (type_of arg = iT) in case filter is_ind (args @ cs) of [] => \<^const>\zero\ | u_args => Balanced_Tree.make mk_Un u_args end; (*Includes rules for succ and Pair since they are common constructions*) val elim_rls = [@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0}, @{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject}, make_elim @{thm succ_inject}, @{thm refl_thin}, @{thm conjE}, @{thm exE}, @{thm disjE}]; (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*) fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) | tryres (th, []) = raise THM("tryres", 0, [th]); fun gen_make_elim elim_rls rl = Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl])); (*Turns iff rules into safe elimination rules*) fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]); end; diff --git a/src/ZF/int_arith.ML b/src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML +++ b/src/ZF/int_arith.ML @@ -1,327 +1,327 @@ (* Title: ZF/int_arith.ML Author: Larry Paulson Simprocs for linear arithmetic. *) signature INT_NUMERAL_SIMPROCS = sig val cancel_numerals: simproc list val combine_numerals: simproc val combine_numerals_prod: simproc end structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS = struct (* abstract syntax operations *) fun mk_bit 0 = \<^term>\0\ | mk_bit 1 = \<^term>\succ(0)\ | mk_bit _ = raise TERM ("mk_bit", []); fun dest_bit \<^term>\0\ = 0 | dest_bit \<^term>\succ(0)\ = 1 | dest_bit t = raise TERM ("dest_bit", [t]); fun mk_bin i = let fun term_of [] = \<^term>\Pls\ | term_of [~1] = \<^term>\Min\ | term_of (b :: bs) = \<^term>\Bit\ $ term_of bs $ mk_bit b; in term_of (Numeral_Syntax.make_binary i) end; fun dest_bin tm = let fun bin_of \<^term>\Pls\ = [] | bin_of \<^term>\Min\ = [~1] | bin_of (\<^term>\Bit\ $ bs $ b) = dest_bit b :: bin_of bs | bin_of _ = raise TERM ("dest_bin", [tm]); in Numeral_Syntax.dest_binary (bin_of tm) end; (*Utilities*) fun mk_numeral i = \<^const>\integ_of\ $ mk_bin i; -fun dest_numeral (Const(\<^const_name>\integ_of\, _) $ w) = dest_bin w +fun dest_numeral \<^Const_>\integ_of for w\ = dest_bin w | dest_numeral t = raise TERM ("dest_numeral", [t]); fun find_first_numeral past (t::terms) = ((dest_numeral t, rev past @ terms) handle TERM _ => find_first_numeral (t::past) terms) | find_first_numeral past [] = raise TERM("find_first_numeral", []); val zero = mk_numeral 0; val mk_plus = FOLogic.mk_binop \<^const_name>\zadd\; (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) fun mk_sum [] = zero | mk_sum [t,u] = mk_plus (t, u) | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); (*this version ALWAYS includes a trailing zero*) fun long_mk_sum [] = zero | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); (*decompose additions AND subtractions as a sum*) -fun dest_summing (pos, Const (\<^const_name>\zadd\, _) $ t $ u, ts) = +fun dest_summing (pos, \<^Const_>\zadd for t u\, ts) = dest_summing (pos, t, dest_summing (pos, u, ts)) - | dest_summing (pos, Const (\<^const_name>\zdiff\, _) $ t $ u, ts) = + | dest_summing (pos, \<^Const_>\zdiff for t u\, ts) = dest_summing (pos, t, dest_summing (not pos, u, ts)) | dest_summing (pos, t, ts) = if pos then t::ts else \<^const>\zminus\ $ t :: ts; fun dest_sum t = dest_summing (true, t, []); val one = mk_numeral 1; val mk_times = FOLogic.mk_binop \<^const_name>\zmult\; fun mk_prod [] = one | mk_prod [t] = t | mk_prod (t :: ts) = if t = one then mk_prod ts else mk_times (t, mk_prod ts); val dest_times = FOLogic.dest_bin \<^const_name>\zmult\ \<^typ>\i\; fun dest_prod t = let val (t,u) = dest_times t in dest_prod t @ dest_prod u end handle TERM _ => [t]; (*DON'T do the obvious simplifications; that would create special cases*) fun mk_coeff (k, t) = mk_times (mk_numeral k, t); (*Express t as a product of (possibly) a numeral with other sorted terms*) -fun dest_coeff sign (Const (\<^const_name>\zminus\, _) $ t) = dest_coeff (~sign) t +fun dest_coeff sign \<^Const_>\zminus for t\ = dest_coeff (~sign) t | dest_coeff sign t = let val ts = sort Term_Ord.term_ord (dest_prod t) val (n, ts') = find_first_numeral [] ts handle TERM _ => (1, ts) in (sign*n, mk_prod ts') end; (*Find first coefficient-term THAT MATCHES u*) fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) | find_first_coeff past u (t::terms) = let val (n,u') = dest_coeff 1 t in if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end handle TERM _ => find_first_coeff (t::past) u terms; (*Simplify #1*n and n*#1 to n*) val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}]; val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify}, @{thm zmult_minus1}, @{thm zmult_minus1_right}]; val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int}, @{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @ @{thms bin.intros}; val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2}, @{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2}, @{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}]; (*To perform binary arithmetic*) val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps}; (*To evaluate binary negations of coefficients*) val zminus_simps = @{thms NCons_simps} @ [@{thm integ_of_minus} RS @{thm sym}, @{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min}, @{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}]; (*To let us treat subtraction as addition*) val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}]; (*push the unary minus down*) val int_minus_mult_eq_1_to_2 = @{lemma "$- w $* z = w $* $- z" by simp}; (*to extract again any uncancelled minuses*) val int_minus_from_mult_simps = [@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}]; (*combine unary minus with numeric literals, however nested within a product*) val int_mult_minus_simps = [@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2]; structure CancelNumeralsCommon = struct val mk_sum = (fn _ : typ => mk_sum) val dest_sum = dest_sum val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 val find_first_coeff = find_first_coeff [] fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm iff_trans} val norm_ss1 = simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}) val norm_ss2 = simpset_of (put_simpset ZF_ss \<^context> addsimps bin_simps @ int_mult_minus_simps @ intifys) val norm_ss3 = simpset_of (put_simpset ZF_ss \<^context> addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys) fun norm_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ bin_simps @ tc_rules @ intifys) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) THEN ALLGOALS (asm_simp_tac ctxt) val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) end; structure EqCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = ArithData.prove_conv "inteq_cancel_numerals" val mk_bal = FOLogic.mk_eq val dest_bal = FOLogic.dest_eq val bal_add1 = @{thm eq_add_iff1} RS @{thm iff_trans} val bal_add2 = @{thm eq_add_iff2} RS @{thm iff_trans} ); structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = ArithData.prove_conv "intless_cancel_numerals" val mk_bal = FOLogic.mk_binrel \<^const_name>\zless\ val dest_bal = FOLogic.dest_bin \<^const_name>\zless\ \<^typ>\i\ val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans} val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans} ); structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = ArithData.prove_conv "intle_cancel_numerals" val mk_bal = FOLogic.mk_binrel \<^const_name>\zle\ val dest_bal = FOLogic.dest_bin \<^const_name>\zle\ \<^typ>\i\ val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans} val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans} ); val cancel_numerals = [Simplifier.make_simproc \<^context> "inteq_cancel_numerals" {lhss = [\<^term>\l $+ m = n\, \<^term>\l = m $+ n\, \<^term>\l $- m = n\, \<^term>\l = m $- n\, \<^term>\l $* m = n\, \<^term>\l = m $* n\], proc = K EqCancelNumerals.proc}, Simplifier.make_simproc \<^context> "intless_cancel_numerals" {lhss = [\<^term>\l $+ m $< n\, \<^term>\l $< m $+ n\, \<^term>\l $- m $< n\, \<^term>\l $< m $- n\, \<^term>\l $* m $< n\, \<^term>\l $< m $* n\], proc = K LessCancelNumerals.proc}, Simplifier.make_simproc \<^context> "intle_cancel_numerals" {lhss = [\<^term>\l $+ m $\ n\, \<^term>\l $\ m $+ n\, \<^term>\l $- m $\ n\, \<^term>\l $\ m $- n\, \<^term>\l $* m $\ n\, \<^term>\l $\ m $* n\], proc = K LeCancelNumerals.proc}]; (*version without the hyps argument*) fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg []; structure CombineNumeralsData = struct type coeff = int val iszero = (fn x => x = 0) val add = op + val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *) val dest_sum = dest_sum val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans} val prove_conv = prove_conv_nohyps "int_combine_numerals" fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans} val norm_ss1 = simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys) val norm_ss2 = simpset_of (put_simpset ZF_ss \<^context> addsimps bin_simps @ int_mult_minus_simps @ intifys) val norm_ss3 = simpset_of (put_simpset ZF_ss \<^context> addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys) fun norm_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ bin_simps @ tc_rules @ intifys) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); val combine_numerals = Simplifier.make_simproc \<^context> "int_combine_numerals" {lhss = [\<^term>\i $+ j\, \<^term>\i $- j\], proc = K CombineNumerals.proc}; (** Constant folding for integer multiplication **) (*The trick is to regard products as sums, e.g. #3 $* x $* #4 as the "sum" of #3, x, #4; the literals are then multiplied*) structure CombineNumeralsProdData = struct type coeff = int val iszero = (fn x => x = 0) val add = op * val mk_sum = (fn _ : typ => mk_prod) val dest_sum = dest_prod fun mk_coeff(k,t) = if t = one then mk_numeral k else raise TERM("mk_coeff", []) fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*) val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans} val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans} val norm_ss1 = simpset_of (put_simpset ZF_ss \<^context> addsimps mult_1s @ diff_simps @ zminus_simps) val norm_ss2 = simpset_of (put_simpset ZF_ss \<^context> addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @ bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys) fun norm_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) val numeral_simp_ss = simpset_of (put_simpset ZF_ss \<^context> addsimps bin_simps @ tc_rules @ intifys) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s); end; structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); val combine_numerals_prod = Simplifier.make_simproc \<^context> "int_combine_numerals_prod" {lhss = [\<^term>\i $* j\], proc = K CombineNumeralsProd.proc}; end; val _ = Theory.setup (Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs (Int_Numeral_Simprocs.cancel_numerals @ [Int_Numeral_Simprocs.combine_numerals, Int_Numeral_Simprocs.combine_numerals_prod]))); diff --git a/src/ZF/simpdata.ML b/src/ZF/simpdata.ML --- a/src/ZF/simpdata.ML +++ b/src/ZF/simpdata.ML @@ -1,45 +1,45 @@ (* Title: ZF/simpdata.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Rewriting for ZF set theory: specialized extraction of rewrites from theorems. *) (*** New version of mk_rew_rules ***) (*Should False yield False<->True, or should it solve goals some other way?*) (*Analyse a theorem to atomic rewrite rules*) fun atomize (conn_pairs, mem_pairs) th = let fun tryrules pairs t = case head_of t of Const(a,_) => (case AList.lookup (op =) pairs a of SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls) | NONE => [th]) | _ => [th] in case Thm.concl_of th of - Const(\<^const_name>\Trueprop\,_) $ P => + \<^Const_>\Trueprop for P\ => (case P of - Const(\<^const_name>\mem\,_) $ a $ b => tryrules mem_pairs b - | Const(\<^const_name>\True\,_) => [] - | Const(\<^const_name>\False\,_) => [] + \<^Const_>\mem for a b\ => tryrules mem_pairs b + | \<^Const_>\True\ => [] + | \<^Const_>\False\ => [] | A => tryrules conn_pairs A) | _ => [th] end; (*Analyse a rigid formula*) val ZF_conn_pairs = [(\<^const_name>\Ball\, [@{thm bspec}]), (\<^const_name>\All\, [@{thm spec}]), (\<^const_name>\imp\, [@{thm mp}]), (\<^const_name>\conj\, [@{thm conjunct1}, @{thm conjunct2}])]; (*Analyse a:b, where b is rigid*) val ZF_mem_pairs = [(\<^const_name>\Collect\, [@{thm CollectD1}, @{thm CollectD2}]), (\<^const_name>\Diff\, [@{thm DiffD1}, @{thm DiffD2}]), (\<^const_name>\Int\, [@{thm IntD1}, @{thm IntD2}])]; val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);