isabelle: src/HOL/Tools/function_package/inductive

20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	1	(* Title: HOL/Tools/function_package/inductive_wrap.ML
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	2	ID: $Id$
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	3	Author: Alexander Krauss, TU Muenchen
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	4
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	5
21237 b803f9870e97 untabified krauss parents: 21105 diff changeset	6	A wrapper around the inductive package, restoring the quantifiers in
b803f9870e97 untabified krauss parents: 21105 diff changeset	7	the introduction and elimination rules.
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	8	*)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	9
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	10	signature FUNDEF_INDUCTIVE_WRAP =
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	11	sig
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	12	val inductive_def : term list
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	13	-> ((bstring * typ) * mixfix) * local_theory
22166 0a50d4db234a * Preliminary implementation of tail recursion krauss parents: 21365 diff changeset	14	-> thm list * (term * thm * thm * local_theory)
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	15	end
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	16
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	17	structure FundefInductiveWrap =
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	18	struct
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	19
21051 c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	20	open FundefLib
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	21
22619 166b4c3b41c0 tuned krauss parents: 22612 diff changeset	22	fun requantify ctxt lfix orig_def thm =
21051 c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	23	let
22619 166b4c3b41c0 tuned krauss parents: 22612 diff changeset	24	val (qs, t) = dest_all_all orig_def
21105 9e812f9f3a97 Removed debugging output krauss parents: 21051 diff changeset	25	val thy = theory_of_thm thm
21051 c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	26	val frees = frees_in_term ctxt t
21237 b803f9870e97 untabified krauss parents: 21105 diff changeset	27	\|> remove (op =) lfix
21051 c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	28	val vars = Term.add_vars (prop_of thm) [] \|> rev
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	29
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	30	val varmap = frees ~~ vars
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	31	in
21051 c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	32	fold_rev (fn Free (n, T) =>
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	33	forall_intr_rename (n, cterm_of thy (Var (the_default (("",0), T) (AList.lookup (op =) varmap (n, T))))))
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	34	qs
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	35	thm
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	36	end
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	37
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	38
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	39
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	40	fun inductive_def defs (((R, T), mixfix), lthy) =
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	41	let
22166 0a50d4db234a * Preliminary implementation of tail recursion krauss parents: 21365 diff changeset	42	val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
22619 166b4c3b41c0 tuned krauss parents: 22612 diff changeset	43	InductivePackage.add_inductive_i (! Toplevel.debug) (verbose)
21051 c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	44	"" (* no altname *)
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	45	false (* no coind *)
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	46	false (* elims, please *)
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	47	false (* induction thm please *)
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	48	[(R, SOME T, NoSyn)] (* the relation *)
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	49	[] (* no parameters *)
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	50	(map (fn t => (("", []), t)) defs) (* the intros *)
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	51	[] (* no special monos *)
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	52	lthy
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	53
22619 166b4c3b41c0 tuned krauss parents: 22612 diff changeset	54	val intrs = map2 (requantify lthy (R, T)) defs intrs_gen
21051 c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	55
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	56	val elim = elim_gen
c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	57	\|> forall_intr_vars (* FIXME... *)
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	58
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	59	in
22612 1f017e6a0395 removed obsolete workarounds krauss parents: 22166 diff changeset	60	(intrs, (Rdef, elim, induct, lthy))
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	61	end
21051 c49467a9c1e1 Switched function package to use the new package for inductive predicates. krauss parents: 21025 diff changeset	62
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: diff changeset	63	end

author	krauss
	Tue, 10 Apr 2007 18:09:58 +0200
changeset 22623	5fcee5b319a2
parent 22619	166b4c3b41c0
child 24746	6d42be359d57
permissions	-rw-r--r--