# HG changeset patch # User huffman # Date 1240358568 25200 # Node ID fbdefa2196fa50f300c3e34cc15470cdda579efd # Parent 811ab0923a62c47138f32e67499f294822dd371e# Parent bd4f255837e51acbb023419bc8b88af30667d53d merged diff -r 811ab0923a62 -r fbdefa2196fa src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Tue Apr 21 17:01:45 2009 -0700 +++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Apr 21 17:02:48 2009 -0700 @@ -215,21 +215,6 @@ (fname, qs, gs, args, rhs) end -exception ArgumentCount of string - -fun mk_arities fqgars = - let fun f (fname, _, _, args, _) arities = - let val k = length args - in - case Symtab.lookup arities fname of - NONE => Symtab.update (fname, k) arities - | SOME i => (if i = k then arities else raise ArgumentCount fname) - end - in - fold f fqgars Symtab.empty - end - - (* Check for all sorts of errors in the input *) fun check_defs ctxt fixes eqs = let @@ -269,13 +254,14 @@ " occur" ^ plural "s" "" funvars ^ " in function position.", "Misspelled constructor???"]); true) in - fqgar + (fname, length args) end - - val _ = mk_arities (map check eqs) - handle ArgumentCount fname => - error ("Function " ^ quote fname ^ - " has different numbers of arguments in different equations") + + val _ = AList.group (op =) (map check eqs) + |> map (fn (fname, ars) => + length (distinct (op =) ars) = 1 + orelse error ("Function " ^ quote fname ^ + " has different numbers of arguments in different equations")) fun check_sorts ((fname, fT), _) = Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) diff -r 811ab0923a62 -r fbdefa2196fa src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Tue Apr 21 17:01:45 2009 -0700 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Tue Apr 21 17:02:48 2009 -0700 @@ -215,11 +215,11 @@ #> Proof.global_future_terminal_proof (Method.Basic (method, Position.none), NONE) int -fun mk_catchall fixes arities = +fun mk_catchall fixes arity_of = let fun mk_eqn ((fname, fT), _) = let - val n = the (Symtab.lookup arities fname) + val n = arity_of fname val (argTs, rT) = chop n (binder_types fT) |> apsnd (fn Ts => Ts ---> body_type fT) @@ -235,7 +235,12 @@ end fun add_catchall ctxt fixes spec = - spec @ mk_catchall fixes (mk_arities (map (split_def ctxt) spec)) + let val fqgars = map (split_def ctxt) spec + val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars + |> AList.lookup (op =) #> the + in + spec @ mk_catchall fixes arity_of + end fun warn_if_redundant ctxt origs tss = let diff -r 811ab0923a62 -r fbdefa2196fa src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Apr 21 17:01:45 2009 -0700 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Apr 21 17:02:48 2009 -0700 @@ -67,40 +67,6 @@ fold2 add_for_f fnames simps_by_f lthy) end -fun fundef_afterqed do_print fixes post defname cont sort_cont cnames [[proof]] lthy = - let - val FundefResult {fs, R, psimps, trsimps, simple_pinducts, termination, domintros, cases, ...} = - cont (Thm.close_derivation proof) - - val fnames = map (fst o fst) fixes - val qualify = Long_Name.qualify defname - val addsmps = add_simps fnames post sort_cont - - val (((psimps', pinducts'), (_, [termination'])), lthy) = - lthy - |> addsmps (Binding.qualify false "partial") "psimps" - psimp_attribs psimps - ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps - ||>> note_theorem ((qualify "pinduct", - [Attrib.internal (K (RuleCases.case_names cnames)), - Attrib.internal (K (RuleCases.consumes 1)), - Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) - ||>> note_theorem ((qualify "termination", []), [termination]) - ||> (snd o note_theorem ((qualify "cases", - [Attrib.internal (K (RuleCases.case_names cnames))]), [cases])) - ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros - - val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', - pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname } - val _ = - if not do_print then () - else Specification.print_consts lthy (K false) (map fst fixes) - in - lthy - |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata) - end - - fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy = let val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) @@ -114,7 +80,40 @@ val ((goalstate, cont), lthy) = FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy - val afterqed = fundef_afterqed is_external fixes post defname cont sort_cont cnames + fun afterqed [[proof]] lthy = + let + val FundefResult {fs, R, psimps, trsimps, simple_pinducts, termination, + domintros, cases, ...} = + cont (Thm.close_derivation proof) + + val fnames = map (fst o fst) fixes + val qualify = Long_Name.qualify defname + val addsmps = add_simps fnames post sort_cont + + val (((psimps', pinducts'), (_, [termination'])), lthy) = + lthy + |> addsmps (Binding.qualify false "partial") "psimps" + psimp_attribs psimps + ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps + ||>> note_theorem ((qualify "pinduct", + [Attrib.internal (K (RuleCases.case_names cnames)), + Attrib.internal (K (RuleCases.consumes 1)), + Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) + ||>> note_theorem ((qualify "termination", []), [termination]) + ||> (snd o note_theorem ((qualify "cases", + [Attrib.internal (K (RuleCases.case_names cnames))]), [cases])) + ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros + + val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', + pinducts=snd pinducts', termination=termination', + fs=fs, R=R, defname=defname } + val _ = + if not is_external then () + else Specification.print_consts lthy (K false) (map fst fixes) + in + lthy + |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata) + end in lthy |> is_external ? LocalTheory.set_group (serial_string ()) @@ -125,25 +124,6 @@ val add_fundef = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) val add_fundef_cmd = gen_add_fundef true Specification.read_spec "_::type" - -fun total_termination_afterqed data [[totality]] lthy = - let - val FundefCtxData { add_simps, case_names, psimps, pinducts, defname, ... } = data - - val totality = Thm.close_derivation totality - - val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) - - val tsimps = map remove_domain_condition psimps - val tinduct = map remove_domain_condition pinducts - - val qualify = Long_Name.qualify defname; - in - lthy - |> add_simps I "simps" simp_attribs tsimps |> snd - |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd - end - fun gen_termination_proof prep_term raw_term_opt lthy = let val term_opt = Option.map (prep_term lthy) raw_term_opt @@ -153,17 +133,37 @@ error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) | NONE => (import_last_fundef lthy handle Option.Option => error "Not a function")) - val FundefCtxData {termination, R, ...} = data + val FundefCtxData { termination, R, add_simps, case_names, psimps, + pinducts, defname, ...} = data val domT = domain_type (fastype_of R) - val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) + val goal = HOLogic.mk_Trueprop + (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) + fun afterqed [[totality]] lthy = + let + val totality = Thm.close_derivation totality + val remove_domain_condition = + full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) + val tsimps = map remove_domain_condition psimps + val tinduct = map remove_domain_condition pinducts + val qualify = Long_Name.qualify defname; + in + lthy + |> add_simps I "simps" simp_attribs tsimps |> snd + |> note_theorem + ((qualify "induct", + [Attrib.internal (K (RuleCases.case_names case_names))]), + tinduct) |> snd + end in lthy - |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd - |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd - |> ProofContext.note_thmss "" - [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]), - [([Goal.norm_result termination], [])])] |> snd - |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]] + |> ProofContext.note_thmss "" + [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd + |> ProofContext.note_thmss "" + [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd + |> ProofContext.note_thmss "" + [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]), + [([Goal.norm_result termination], [])])] |> snd + |> Proof.theorem_i NONE afterqed [[(goal, [])]] end val termination_proof = gen_termination_proof Syntax.check_term; @@ -198,8 +198,9 @@ (* setup *) val setup = - Attrib.setup @{binding fundef_cong} (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del) - "declaration of congruence rule for function definitions" + Attrib.setup @{binding fundef_cong} + (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del) + "declaration of congruence rule for function definitions" #> setup_case_cong #> FundefRelation.setup #> FundefCommon.TerminationSimps.setup diff -r 811ab0923a62 -r fbdefa2196fa src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Tue Apr 21 17:01:45 2009 -0700 +++ b/src/HOL/Tools/function_package/mutual.ML Tue Apr 21 17:02:48 2009 -0700 @@ -87,12 +87,12 @@ val num = length fs val fnames = map fst fs val fqgars = map (split_def ctxt) eqs - val arities = mk_arities fqgars + val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars + |> AList.lookup (op =) #> the fun curried_types (fname, fT) = let - val k = the_default 1 (Symtab.lookup arities fname) - val (caTs, uaTs) = chop k (binder_types fT) + val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) in (caTs, uaTs ---> body_type fT) end diff -r 811ab0923a62 -r fbdefa2196fa src/HOL/ex/Unification.thy --- a/src/HOL/ex/Unification.thy Tue Apr 21 17:01:45 2009 -0700 +++ b/src/HOL/ex/Unification.thy Tue Apr 21 17:02:48 2009 -0700 @@ -277,7 +277,7 @@ by (induct t) simp_all qed -lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])" +lemma var_same: "([(v, t)] =\<^sub>s []) = (t = Var v)" proof assume t_v: "t = Var v" thus "[(v, t)] =\<^sub>s []" @@ -307,7 +307,7 @@ proof cases assume "v = x" thus ?thesis - by (simp add:var_same[symmetric]) + by (simp add:var_same) next assume neq: "v \ x" have "elim [(v, Var x)] v" @@ -328,13 +328,13 @@ by auto from nonocc have "\ [(v,M)] =\<^sub>s []" - by (simp add:var_same[symmetric]) + by (simp add:var_same) with ih1 have "elim [(v, M)] v" by blast hence "v \ vars_of (Var v \ [(v,M)])" .. hence not_in_M: "v \ vars_of M" by simp from nonocc have "\ [(v,N)] =\<^sub>s []" - by (simp add:var_same[symmetric]) + by (simp add:var_same) with ih2 have "elim [(v, N)] v" by blast hence "v \ vars_of (Var v \ [(v,N)])" .. hence not_in_N: "v \ vars_of N" by simp diff -r 811ab0923a62 -r fbdefa2196fa src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Tue Apr 21 17:01:45 2009 -0700 +++ b/src/Pure/meta_simplifier.ML Tue Apr 21 17:02:48 2009 -0700 @@ -16,7 +16,6 @@ val trace_simp_depth_limit: int ref type rrule val eq_rrule: rrule * rrule -> bool - type cong type simpset type proc type solver @@ -87,7 +86,7 @@ bounds: int * ((string * typ) * string) list, depth: int * bool ref, context: Proof.context option} * - {congs: (string * cong) list * string list, + {congs: (string * thm) list * string list, procs: proc Net.net, mk_rews: {mk: thm -> thm list, @@ -161,10 +160,7 @@ (* congruences *) -type cong = {thm: thm, lhs: cterm}; - -fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) = - Thm.eq_thm_prop (thm1, thm2); +val eq_cong = Thm.eq_thm_prop (* simplification sets, procedures, and solvers *) @@ -201,7 +197,7 @@ bounds: int * ((string * typ) * string) list, depth: int * bool ref, context: Proof.context option} * - {congs: (string * cong) list * string list, + {congs: (string * thm) list * string list, procs: proc Net.net, mk_rews: mk_rews, termless: term * term -> bool, @@ -570,7 +566,7 @@ val _ = if AList.defined (op =) xs a then warning ("Overwriting congruence rule for " ^ quote a) else (); - val xs' = AList.update (op =) (a, {lhs = lhs, thm = thm}) xs; + val xs' = AList.update (op =) (a, thm) xs; val weak' = if is_full_cong thm then weak else a :: weak; in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); @@ -584,7 +580,7 @@ raise SIMPLIFIER ("Congruence must start with a constant", thm); val (xs, _) = congs; val xs' = filter_out (fn (x : string, _) => x = a) xs; - val weak' = xs' |> map_filter (fn (a, {thm, ...}: cong) => + val weak' = xs' |> map_filter (fn (a, thm) => if is_full_cong thm then NONE else SOME a); in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); @@ -810,7 +806,7 @@ |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id)) |> partition_eq (eq_snd eq_procid) |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), - congs = map (fn (name, {thm, ...}) => (name, thm)) (#1 congs), + congs = #1 congs, weak_congs = #2 congs, loopers = map fst loop_tacs, unsafe_solvers = map solver_name (#1 solvers), @@ -980,7 +976,7 @@ (* conversion to apply a congruence rule to a term *) -fun congc prover ss maxt {thm=cong,lhs=lhs} t = +fun congc prover ss maxt cong t = let val rthm = Thm.incr_indexes (maxt + 1) cong; val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm))); val insts = Thm.match (rlhs, t)