--- 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)
--- 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
--- 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
--- 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
--- 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 \<noteq> x"
have "elim [(v, Var x)] v"
@@ -328,13 +328,13 @@
by auto
from nonocc have "\<not> [(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 \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
hence not_in_M: "v \<notin> vars_of M" by simp
from nonocc have "\<not> [(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 \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
hence not_in_N: "v \<notin> vars_of N" by simp
--- 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)