# HG changeset patch # User krauss # Date 1158141950 -7200 # Node ID 36a59e5d003909cbe7fa6ab921689a433b3c8fad # Parent 05072ae0d4351678d539ebd0c37c28727671b94e Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts. diff -r 05072ae0d435 -r 36a59e5d0039 etc/isar-keywords.el --- a/etc/isar-keywords.el Wed Sep 13 00:38:38 2006 +0200 +++ b/etc/isar-keywords.el Wed Sep 13 12:05:50 2006 +0200 @@ -46,12 +46,10 @@ "code_const" "code_constname" "code_gen" - "code_generate" "code_instance" "code_library" "code_module" "code_purge" - "code_serialize" "code_simtype" "code_type" "code_typename" @@ -89,6 +87,7 @@ "fixrec" "from" "full_prf" + "fun" "function" "global" "guess" @@ -393,12 +392,10 @@ "code_const" "code_constname" "code_gen" - "code_generate" "code_instance" "code_library" "code_module" "code_purge" - "code_serialize" "code_type" "code_typename" "coinductive" @@ -417,6 +414,7 @@ "finalconsts" "fixpat" "fixrec" + "fun" "global" "hide" "inductive" diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Datatype.thy Wed Sep 13 12:05:50 2006 +0200 @@ -233,27 +233,27 @@ lemmas [code] = imp_conv_disj -lemma [code fun]: +lemma [code func]: "(\ True) = False" by (rule HOL.simp_thms) -lemma [code fun]: +lemma [code func]: "(\ False) = True" by (rule HOL.simp_thms) -lemma [code fun]: +lemma [code func]: shows "(False \ x) = False" and "(True \ x) = x" and "(x \ False) = False" and "(x \ True) = x" by simp_all -lemma [code fun]: +lemma [code func]: shows "(False \ x) = x" and "(True \ x) = True" and "(x \ False) = x" and "(x \ True) = True" by simp_all declare - if_True [code fun] - if_False [code fun] + if_True [code func] + if_False [code func] fst_conv [code] snd_conv [code] diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/FunDef.thy Wed Sep 13 12:05:50 2006 +0200 @@ -11,6 +11,7 @@ ("Tools/function_package/sum_tools.ML") ("Tools/function_package/fundef_common.ML") ("Tools/function_package/fundef_lib.ML") +("Tools/function_package/inductive_wrap.ML") ("Tools/function_package/context_tree.ML") ("Tools/function_package/fundef_prep.ML") ("Tools/function_package/fundef_proof.ML") @@ -23,20 +24,20 @@ begin lemma fundef_ex1_existence: -assumes f_def: "\x. f x \ THE y. (x,y)\G" +assumes f_def: "f \ \x. THE y. (x,y)\G" assumes ex1: "\!y. (x,y)\G" shows "(x, f x)\G" by (simp only:f_def, rule theI', rule ex1) lemma fundef_ex1_uniqueness: -assumes f_def: "\x. f x \ THE y. (x,y)\G" +assumes f_def: "f \ \x. THE y. (x,y)\G" assumes ex1: "\!y. (x,y)\G" assumes elm: "(x, h x)\G" shows "h x = f x" by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm) lemma fundef_ex1_iff: -assumes f_def: "\x. f x \ THE y. (x,y)\G" +assumes f_def: "f \ \x. THE y. (x,y)\G" assumes ex1: "\!y. (x,y)\G" shows "((x, y)\G) = (f x = y)" apply (auto simp:ex1 f_def the1_equality) @@ -71,6 +72,7 @@ use "Tools/function_package/sum_tools.ML" use "Tools/function_package/fundef_common.ML" use "Tools/function_package/fundef_lib.ML" +use "Tools/function_package/inductive_wrap.ML" use "Tools/function_package/context_tree.ML" use "Tools/function_package/fundef_prep.ML" use "Tools/function_package/fundef_proof.ML" diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Induct/QuoNestedDataType.thy --- a/src/HOL/Induct/QuoNestedDataType.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Sep 13 12:05:50 2006 +0200 @@ -351,7 +351,7 @@ subsection{*Injectivity of @{term FnCall}*} definition - fun :: "exp \ nat" + "fun" :: "exp \ nat" "fun X = contents (\U \ Rep_Exp X. {freefun U})" lemma fun_respects: "(%U. {freefun U}) respects exprel" diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Integ/IntArith.thy --- a/src/HOL/Integ/IntArith.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Integ/IntArith.thy Wed Sep 13 12:05:50 2006 +0200 @@ -376,23 +376,23 @@ "Numeral.B1" "IntDef.b1" lemma - Numeral_Pls_refl [code fun]: "Numeral.Pls = Numeral.Pls" .. + Numeral_Pls_refl [code func]: "Numeral.Pls = Numeral.Pls" .. lemma - Numeral_Min_refl [code fun]: "Numeral.Min = Numeral.Min" .. + Numeral_Min_refl [code func]: "Numeral.Min = Numeral.Min" .. lemma - Numeral_Bit_refl [code fun]: "Numeral.Bit = Numeral.Bit" .. + Numeral_Bit_refl [code func]: "Numeral.Bit = Numeral.Bit" .. -lemma zero_is_num_zero [code fun, code inline]: +lemma zero_is_num_zero [code func, code inline]: "(0::int) = Numeral.Pls" unfolding Pls_def .. -lemma one_is_num_one [code fun, code inline]: +lemma one_is_num_one [code func, code inline]: "(1::int) = Numeral.Pls BIT bit.B1" unfolding Pls_def Bit_def by simp -lemma number_of_is_id [code fun, code inline]: +lemma number_of_is_id [code func, code inline]: "number_of (k::int) = k" unfolding int_number_of_def by simp diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Isar_examples/ExprCompiler.thy --- a/src/HOL/Isar_examples/ExprCompiler.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Wed Sep 13 12:05:50 2006 +0200 @@ -173,14 +173,14 @@ case (Load adr) from Cons show ?case by simp -- {* same as above *} next - case (Apply fun) - have "exec ((Apply fun # xs) @ ys) s env = - exec (Apply fun # xs @ ys) s env" by simp + case (Apply fn) + have "exec ((Apply fn # xs) @ ys) s env = + exec (Apply fn # xs @ ys) s env" by simp also have "... = - exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env" by simp + exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp also from Cons have "... = - exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env" . - also have "... = exec ys (exec (Apply fun # xs) s env) env" by simp + exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" . + also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp finally show ?case . qed qed @@ -199,19 +199,19 @@ case (Constant val s) show ?case by simp -- {* same as above *} next - case (Binop fun e1 e2 s) - have "exec (compile (Binop fun e1 e2)) s env = - exec (compile e2 @ compile e1 @ [Apply fun]) s env" by simp - also have "... = exec [Apply fun] + case (Binop fn e1 e2 s) + have "exec (compile (Binop fn e1 e2)) s env = + exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp + also have "... = exec [Apply fn] (exec (compile e1) (exec (compile e2) s env) env) env" by (simp only: exec_append) also have "exec (compile e2) s env = eval e2 env # s" by fact also have "exec (compile e1) ... env = eval e1 env # ..." by fact - also have "exec [Apply fun] ... env = - fun (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp - also have "... = fun (eval e1 env) (eval e2 env) # s" by simp - also have "fun (eval e1 env) (eval e2 env) = - eval (Binop fun e1 e2) env" + also have "exec [Apply fn] ... env = + fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp + also have "... = fn (eval e1 env) (eval e2 env) # s" by simp + also have "fn (eval e1 env) (eval e2 env) = + eval (Binop fn e1 e2) env" by simp finally show ?case . qed diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Lattice/Lattice.thy --- a/src/HOL/Lattice/Lattice.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Lattice/Lattice.thy Wed Sep 13 12:05:50 2006 +0200 @@ -519,7 +519,7 @@ qed qed -instance fun :: (type, lattice) lattice +instance "fun" :: (type, lattice) lattice proof fix f g :: "'a \ 'b::lattice" show "\inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \ show \ .."} does not work!? unification incompleteness!? *) diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Lattice/Orders.thy --- a/src/HOL/Lattice/Orders.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Lattice/Orders.thy Wed Sep 13 12:05:50 2006 +0200 @@ -249,7 +249,7 @@ orders need \emph{not} be linear in general. *} -instance fun :: (type, leq) leq .. +instance "fun" :: (type, leq) leq .. defs (overloaded) leq_fun_def: "f \ g \ \x. f x \ g x" @@ -260,7 +260,7 @@ lemma leq_funD [dest?]: "f \ g \ f x \ g x" by (unfold leq_fun_def) blast -instance fun :: (type, quasi_order) quasi_order +instance "fun" :: (type, quasi_order) quasi_order proof fix f g h :: "'a \ 'b::quasi_order" show "f \ f" @@ -276,7 +276,7 @@ qed qed -instance fun :: (type, partial_order) partial_order +instance "fun" :: (type, partial_order) partial_order proof fix f g :: "'a \ 'b::partial_order" assume fg: "f \ g" and gf: "g \ f" diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Library/EfficientNat.thy --- a/src/HOL/Library/EfficientNat.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Library/EfficientNat.thy Wed Sep 13 12:05:50 2006 +0200 @@ -112,23 +112,23 @@ lemma [code]: "(m < n) = (int m < int n)" by simp -lemma [code fun, code inline]: "m + n = nat_plus m n" +lemma [code func, code inline]: "m + n = nat_plus m n" unfolding nat_plus_def by arith -lemma [code fun, code inline]: "m - n = nat_minus m n" +lemma [code func, code inline]: "m - n = nat_minus m n" unfolding nat_minus_def by arith -lemma [code fun, code inline]: "m * n = nat_mult m n" +lemma [code func, code inline]: "m * n = nat_mult m n" unfolding nat_mult_def by (simp add: zmult_int) -lemma [code fun, code inline]: "m div n = nat_div m n" +lemma [code func, code inline]: "m div n = nat_div m n" unfolding nat_div_def div_def [symmetric] zdiv_int [symmetric] by simp -lemma [code fun, code inline]: "m mod n = nat_mod m n" +lemma [code func, code inline]: "m mod n = nat_mod m n" unfolding nat_mod_def mod_def [symmetric] zmod_int [symmetric] by simp -lemma [code fun, code inline]: "(m < n) = nat_less m n" +lemma [code func, code inline]: "(m < n) = nat_less m n" unfolding nat_less_def by simp -lemma [code fun, code inline]: "(m <= n) = nat_less_equal m n" +lemma [code func, code inline]: "(m <= n) = nat_less_equal m n" unfolding nat_less_equal_def by simp -lemma [code fun, code inline]: "(m = n) = nat_eq m n" +lemma [code func, code inline]: "(m = n) = nat_eq m n" unfolding nat_eq_def by simp -lemma [code fun]: +lemma [code func]: "int_aux i n = (if nat_eq n 0 then i else int_aux (i + 1) (nat_minus n 1))" unfolding nat_eq_def nat_minus_def int_aux_def by simp diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Library/ExecutableSet.thy --- a/src/HOL/Library/ExecutableSet.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Library/ExecutableSet.thy Wed Sep 13 12:05:50 2006 +0200 @@ -84,51 +84,55 @@ subsection {* Derived definitions *} -consts - unionl :: "'a list \ 'a list \ 'a list" - intersect :: "'a list \ 'a list \ 'a list" - subtract :: "'a list \ 'a list \ 'a list" - map_distinct :: "('a \ 'b) \ 'a list \ 'b list" - unions :: "'a list list \ 'a list" - intersects :: "'a list list \ 'a list" -function +function unionl :: "'a list \ 'a list \ 'a list" +where "unionl [] ys = ys" - "unionl xs ys = foldr insertl xs ys" - by pat_completeness auto +| "unionl xs ys = foldr insertl xs ys" +by pat_completeness auto termination unionl by (auto_term "{}") lemmas unionl_def = unionl.simps(2) +declare unionl.simps[code] -function +function intersect :: "'a list \ 'a list \ 'a list" +where "intersect [] ys = []" - "intersect xs [] = []" - "intersect xs ys = filter (member xs) ys" - by pat_completeness simp_all +| "intersect xs [] = []" +| "intersect xs ys = filter (member xs) ys" + by pat_completeness auto termination intersect by (auto_term "{}") lemmas intersect_def = intersect.simps(3) +declare intersect.simps[code] -function +function subtract :: "'a list \ 'a list \ 'a list" +where "subtract [] ys = ys" - "subtract xs [] = []" - "subtract xs ys = foldr remove1 xs ys" - by pat_completeness simp_all +| "subtract xs [] = []" +| "subtract xs ys = foldr remove1 xs ys" + by pat_completeness auto termination subtract by (auto_term "{}") lemmas subtract_def = subtract.simps(3) +declare subtract.simps[code] -function +function map_distinct :: "('a \ 'b) \ 'a list \ 'b list" +where "map_distinct f [] = []" - "map_distinct f xs = foldr (insertl o f) xs []" - by pat_completeness simp_all +| "map_distinct f xs = foldr (insertl o f) xs []" + by pat_completeness auto termination map_distinct by (auto_term "{}") lemmas map_distinct_def = map_distinct.simps(2) +declare map_distinct.simps[code] -function +function unions :: "'a list list \ 'a list" +where "unions [] = []" "unions xs = foldr unionl xs []" - by pat_completeness simp_all + by pat_completeness auto termination unions by (auto_term "{}") lemmas unions_def = unions.simps(2) +declare unions.simps[code] +consts intersects :: "'a list list \ 'a list" primrec "intersects (x#xs) = foldr intersect xs x" @@ -156,7 +160,8 @@ lemma iso_union: "set (unionl xs ys) = set xs \ set ys" - unfolding unionl_def by (induct xs arbitrary: ys) (simp_all add: iso_insert) + unfolding unionl_def + by (induct xs arbitrary: ys) (simp_all add: iso_insert) lemma iso_intersect: "set (intersect xs ys) = set xs \ set ys" diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Library/SetsAndFunctions.thy --- a/src/HOL/Library/SetsAndFunctions.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Library/SetsAndFunctions.thy Wed Sep 13 12:05:50 2006 +0200 @@ -18,33 +18,33 @@ subsection {* Basic definitions *} instance set :: (plus) plus .. -instance fun :: (type, plus) plus .. +instance "fun" :: (type, plus) plus .. defs (overloaded) func_plus: "f + g == (%x. f x + g x)" set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}" instance set :: (times) times .. -instance fun :: (type, times) times .. +instance "fun" :: (type, times) times .. defs (overloaded) func_times: "f * g == (%x. f x * g x)" set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}" -instance fun :: (type, minus) minus .. +instance "fun" :: (type, minus) minus .. defs (overloaded) func_minus: "- f == (%x. - f x)" func_diff: "f - g == %x. f x - g x" -instance fun :: (type, zero) zero .. +instance "fun" :: (type, zero) zero .. instance set :: (zero) zero .. defs (overloaded) func_zero: "0::(('a::type) => ('b::zero)) == %x. 0" set_zero: "0::('a::zero)set == {0}" -instance fun :: (type, one) one .. +instance "fun" :: (type, one) one .. instance set :: (one) one .. defs (overloaded) @@ -62,29 +62,29 @@ elt_set_eq :: "'a => 'a set => bool" (infix "=o" 50) "x =o A == x : A" -instance fun :: (type,semigroup_add)semigroup_add +instance "fun" :: (type,semigroup_add)semigroup_add by default (auto simp add: func_plus add_assoc) -instance fun :: (type,comm_monoid_add)comm_monoid_add +instance "fun" :: (type,comm_monoid_add)comm_monoid_add by default (auto simp add: func_zero func_plus add_ac) -instance fun :: (type,ab_group_add)ab_group_add +instance "fun" :: (type,ab_group_add)ab_group_add apply default apply (simp add: func_minus func_plus func_zero) apply (simp add: func_minus func_plus func_diff diff_minus) done -instance fun :: (type,semigroup_mult)semigroup_mult +instance "fun" :: (type,semigroup_mult)semigroup_mult apply default apply (auto simp add: func_times mult_assoc) done -instance fun :: (type,comm_monoid_mult)comm_monoid_mult +instance "fun" :: (type,comm_monoid_mult)comm_monoid_mult apply default apply (auto simp add: func_one func_times mult_ac) done -instance fun :: (type,comm_ring_1)comm_ring_1 +instance "fun" :: (type,comm_ring_1)comm_ring_1 apply default apply (auto simp add: func_plus func_times func_minus func_diff ext func_one func_zero ring_eq_simps) diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/context_tree.ML Wed Sep 13 12:05:50 2006 +0200 @@ -15,8 +15,11 @@ val cong_deps : thm -> int IntGraph.T val add_congs : thm list - val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> - term -> Proof.context -> term -> FundefCommon.ctx_tree + val mk_tree: (thm * FundefCommon.depgraph) list -> + (string * typ) -> Proof.context -> term -> FundefCommon.ctx_tree + + val inst_tree: theory -> term -> term -> FundefCommon.ctx_tree + -> FundefCommon.ctx_tree val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list @@ -32,7 +35,7 @@ (((string * typ) list * thm list) * thm) list * 'b) -> FundefCommon.ctx_tree -> 'b -> 'b - val rewrite_by_tree : theory -> 'a -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list + val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list end structure FundefCtxTree : FUNDEF_CTXTREE = @@ -79,35 +82,61 @@ (ctx', fixes, assumes, rhs_of term) end -fun find_cong_rule thy ctx ((r,dep)::rs) t = +fun find_cong_rule ctx ((r,dep)::rs) t = (let val (c, subs) = (meta_rhs_of (concl_of r), prems_of r) - val subst = Pattern.match thy (c, t) (Vartab.empty, Vartab.empty) + val subst = Pattern.match (ProofContext.theory_of ctx) (c, t) (Vartab.empty, Vartab.empty) val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs in (r, dep, branches) end - handle Pattern.MATCH => find_cong_rule thy ctx rs t) - | find_cong_rule thy _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!" + handle Pattern.MATCH => find_cong_rule ctx rs t) + | find_cong_rule _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!" -fun matchcall f (a $ b) = if a = f then SOME b else NONE - | matchcall f _ = NONE +fun matchcall fvar (a $ b) = if a = Free fvar then SOME b else NONE + | matchcall fvar _ = NONE + +fun mk_tree congs fvar ctx t = + case matchcall fvar t of + SOME arg => RCall (t, mk_tree congs fvar ctx arg) + | NONE => + if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t + else + let val (r, dep, branches) = find_cong_rule ctx congs t in + Cong (t, r, dep, + map (fn (ctx', fixes, assumes, st) => + (fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes, + mk_tree congs fvar ctx' st)) branches) + end + -fun mk_tree thy congs f ctx t = - case matchcall f t of - SOME arg => RCall (t, mk_tree thy congs f ctx arg) - | NONE => - if not (exists_Const (curry op = (dest_Const f)) t) then Leaf t - else - let val (r, dep, branches) = find_cong_rule thy ctx congs t in - Cong (t, r, dep, map (fn (ctx', fixes, assumes, st) => - (fixes, map (assume o cterm_of thy) assumes, mk_tree thy congs f ctx' st)) branches) - end - - +fun inst_tree thy fvar f tr = + let + val cfvar = cterm_of thy fvar + val cf = cterm_of thy f + + fun inst_term t = + subst_bound(f, abstract_over (fvar, t)) + + val inst_thm = forall_elim cf o forall_intr cfvar + + fun inst_tree_aux (Leaf t) = Leaf t + | inst_tree_aux (Cong (t, crule, deps, branches)) = + Cong (inst_term t, inst_thm crule, deps, map inst_branch branches) + | inst_tree_aux (RCall (t, str)) = + RCall (inst_term t, inst_tree_aux str) + and inst_branch (fxs, assms, str) = + (fxs, map (assume o cterm_of thy o inst_term o prop_of) assms, inst_tree_aux str) + in + inst_tree_aux tr + end + + + +(* FIXME: remove *) fun add_context_varnames (Leaf _) = I | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (curry op ins_string o fst) fs o add_context_varnames st) sub | add_context_varnames (RCall (_,st)) = add_context_varnames st @@ -185,7 +214,7 @@ fun is_refl thm = let val (l,r) = Logic.dest_equals (prop_of thm) in l = r end -fun rewrite_by_tree thy f h ih x tr = +fun rewrite_by_tree thy h ih x tr = let fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x) | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) = diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Wed Sep 13 12:05:50 2006 +0200 @@ -12,6 +12,8 @@ (* Theory Dependencies *) val acc_const_name = "Accessible_Part.acc" +fun mk_acc domT R = + Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R type depgraph = int IntGraph.T @@ -25,17 +27,20 @@ type glrs = (term list * term list * term * term) list -(* A record containing all the relevant symbols and types needed during the proof. - This is set up at the beginning and does not change. *) -datatype naming_context = - Names of { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ, - G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term, - D: term, Pbool:term, - glrs: (term list * term list * term * term) list, - glrs': (term list * term list * term * term) list, - f_def: thm, - ctx: Proof.context - } +datatype globals = + Globals of { + fvar: term, + domT: typ, + ranT: typ, + h: term, + y: term, + x: term, + z: term, + a:term, + P: term, + D: term, + Pbool:term +} datatype rec_call_info = @@ -46,70 +51,91 @@ rcarg: term, (* The recursive argument *) llRI: thm, - Gh: thm, - Gh': thm + h_assum: term } - + + +datatype clause_context = + ClauseContext of + { + ctxt : Proof.context, + + qs : term list, + gs : term list, + lhs: term, + rhs: term, + + cqs: cterm list, + ags: thm list, + case_hyp : thm + } + + +fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = + ClauseContext { ctxt = ProofContext.transfer thy ctxt, + qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } + + datatype clause_info = ClauseInfo of { no: int, + qglr : ((string * typ) list * term list * term * term), + cdata : clause_context, tree: ctx_tree, - case_hyp: thm, - - qs: term list, - gs: term list, - lhs: term, - rhs: term, - - cqs: cterm list, - ags: thm list, - - cqs': cterm list, - ags': thm list, - lhs': term, - rhs': term, - lGI: thm, - RCs: rec_call_info list, - - ordcqs': cterm list + RCs: rec_call_info list } -type qgar = (string * typ) list * term list * term list * term + + + +type qgar = string * (string * typ) list * term list * term list * term + +fun name_of_fqgar (f, _, _, _, _) = f datatype mutual_part = MutualPart of { - f_name: string, - const: string * typ, + fvar : string * typ, cargTs: typ list, pthA: SumTools.sum_path, pthR: SumTools.sum_path, - qgars: qgar list, - f_def: thm + f_def: term, + + f: term option, + f_defthm : thm option } datatype mutual_info = Mutual of { - name: string, - sum_const: string * typ, + defname: string, + fsum_var : string * typ, + ST: typ, RST: typ, streeA: SumTools.sum_tree, streeR: SumTools.sum_tree, + parts: mutual_part list, - qglrss: (term list * term list * term * term) list list + fqgars: qgar list, + qglrs: ((string * typ) list * term list * term * term) list, + + fsum : term option } datatype prep_result = Prep of { - names: naming_context, + globals: globals, + f: term, + G: term, + R: term, + goal: term, goalI: thm, values: thm list, @@ -138,10 +164,10 @@ FundefMResult of { f: term, - G : term, - R : term, + G: term, + R: term, - psimps : thm list list, + psimps : thm list, subset_pinducts : thm list, simple_pinducts : thm list, cases : thm, @@ -150,10 +176,10 @@ } -type fundef_spec = ((string * attribute list) * term list) list list +type fundef_spec = ((string * typ) * mixfix) list *((string * Attrib.src list) * term list) list list type result_with_names = fundef_mresult * mutual_info * fundef_spec -structure FundefData = TheoryDataFun +structure FundefData = GenericDataFun (struct val name = "HOL/function_def/data"; type T = string * result_with_names Symtab.table @@ -204,6 +230,7 @@ val mk_prod = HOLogic.mk_prod val mk_mem = HOLogic.mk_mem val mk_eq = HOLogic.mk_eq +val eq_const = HOLogic.eq_const val Trueprop = HOLogic.mk_Trueprop val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Wed Sep 13 12:05:50 2006 +0200 @@ -10,6 +10,7 @@ sig val pat_complete_tac: int -> tactic + val pat_completeness : method val setup : theory -> theory end @@ -160,8 +161,48 @@ handle COMPLETENESS => Seq.empty +val pat_completeness = Method.SIMPLE_METHOD (pat_complete_tac 1) + +val by_pat_completeness_simp = + Proof.global_terminal_proof + (Method.Basic (K pat_completeness), + SOME (Method.Source (Args.src (("simp_all", []), Position.none)))) + val setup = - Method.add_methods [("pat_completeness", Method.no_args (Method.SIMPLE_METHOD (pat_complete_tac 1)), "Completeness prover for datatype patterns")] + Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")] + + + + + + +local structure P = OuterParse and K = OuterKeyword in + + +fun local_theory_to_proof f = + Toplevel.theory_to_proof (f o LocalTheory.init NONE) + +fun or_list1 s = P.enum1 "|" s +val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" +val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false)) +val statements_ow = or_list1 statement_ow +val funP = + OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl + ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow) + >> (fn ((target, fixes), statements) => + Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements true + #> by_pat_completeness_simp))); + +val _ = OuterSyntax.add_parsers [funP]; end + + + + + + + + +end \ No newline at end of file diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Wed Sep 13 12:05:50 2006 +0200 @@ -7,14 +7,12 @@ *) +fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *) + fun mk_forall (var as Free (v,T)) t = all T $ Abs (v,T, abstract_over (var,t)) | mk_forall v _ = let val _ = print v in sys_error "mk_forall" end -(* Builds a quantification with a new name for the variable. *) -fun mk_forall_rename (v as Free (_,T),newname) t = - all T $ Abs (newname, T, abstract_over (v, t)) - | mk_forall_rename (v, _) _ = let val _ = print v in sys_error "mk_forall_rename" end (* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *) fun tupled_lambda vars t = @@ -75,10 +73,18 @@ | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs | map3 _ _ _ _ = raise Library.UnequalLengths; +fun map4 _ [] [] [] [] = [] + | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us + | map4 _ _ _ _ _ = raise Library.UnequalLengths; + fun map6 _ [] [] [] [] [] [] = [] | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths; +fun map7 _ [] [] [] [] [] [] [] = [] + | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs + | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths; + (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) @@ -88,3 +94,36 @@ fun the_single [x] = x | the_single _ = sys_error "the_single" + + +(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *) +fun replace_frees assoc = + map_aterms (fn c as Free (n, _) => (case AList.lookup (op =) assoc n of + NONE => c + | SOME t => t) + | t => t) + + + +fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b)) + | rename_bound n _ = raise Match + +fun mk_forall_rename (n, v) = + rename_bound n o mk_forall v + +fun forall_intr_rename (n, cv) thm = + let + val allthm = forall_intr cv thm + val reflx = prop_of allthm + |> rename_bound n + |> cterm_of (theory_of_thm thm) + |> reflexive + in + equal_elim reflx allthm + end + + +(* Returns the frees in a term in canonical order, excluding the fixes from the context *) +fun frees_in_term ctxt t = + rev (fold_aterms (fn Free (v as (x, _)) => + if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t []) diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Sep 13 12:05:50 2006 +0200 @@ -1,4 +1,3 @@ - (* Title: HOL/Tools/function_package/fundef_package.ML ID: $Id$ Author: Alexander Krauss, TU Muenchen @@ -10,7 +9,17 @@ signature FUNDEF_PACKAGE = sig - val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *) + val add_fundef : (string * string option * mixfix) list + -> ((bstring * Attrib.src list) * string list) list list + -> bool + -> local_theory + -> Proof.state + + val add_fundef_i: (string * typ option * mixfix) list + -> ((bstring * Attrib.src list) * term list) list list + -> bool + -> local_theory + -> Proof.state val cong_add: attribute val cong_del: attribute @@ -20,167 +29,136 @@ end -structure FundefPackage : FUNDEF_PACKAGE = +structure FundefPackage = struct open FundefCommon -fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy = - let - val psimpss = Library.unflat (map snd spec_part) psimps - val (names, attss) = split_list (map fst spec_part) +fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *) + let val (xs, ys) = split_list ps + in xs ~~ f ys end - val thy = thy |> Theory.add_path f_name +fun restore_spec_structure reps spec = + (burrow o burrow_snd o burrow o K) reps spec - val thy = thy |> Theory.add_path label - val spsimpss = map (map standard) psimpss (* FIXME *) - val add_list = (names ~~ spsimpss) ~~ attss - val (_, thy) = PureThy.add_thmss add_list thy - val thy = thy |> Theory.parent_path - - val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy - val thy = thy |> Theory.parent_path +fun with_local_path path f lthy = + let + val restore = Theory.restore_naming (ProofContext.theory_of lthy) in - thy + lthy + |> LocalTheory.theory (Theory.add_path path) + |> f + |> LocalTheory.theory restore end - - - - - -fun fundef_afterqed congs mutual_info name data spec [[result]] thy = +fun add_simps label moreatts mutual_info fixes psimps spec lthy = let - val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result - val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data - val Mutual {parts, ...} = mutual_info + val fnames = map (fst o fst) fixes + val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps - val Prep {names = Names {acc_R=accR, ...}, ...} = data - val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR) - val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy - - val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy - - val casenames = flat (map (map (fst o fst)) spec) - - val thy = thy |> Theory.add_path name - val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy - val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy - val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy - val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy - val thy = thy |> Theory.parent_path + fun add_for_f fname psimps = + with_local_path fname + (LocalTheory.note ((label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd) in - add_fundef_data name (fundef_data, mutual_info, spec) thy - end - -fun gen_add_fundef prep_att eqns_attss (preprocess : bool) thy = - let - fun prep_eqns neqs = - neqs - |> map (apsnd (Sign.read_prop thy)) - |> map (apfst (apsnd (apfst (map (prep_att thy))))) - |> FundefSplit.split_some_equations (ProofContext.init thy) - - val spec = map prep_eqns eqns_attss - val t_eqnss = map (flat o map snd) spec - - val congs = get_fundef_congs (Context.Theory thy) - - val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy - val Prep {goal, goalI, ...} = data - in - thy |> ProofContext.init - |> Proof.theorem_i PureThy.internalK NONE - (ProofContext.theory o fundef_afterqed congs mutual_info name data spec) NONE ("", []) - [(("", []), [(goal, [])])] - |> Proof.refine (Method.primitive_text (fn _ => goalI)) - |> Seq.hd + lthy + |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd + |> fold2 add_for_f fnames psimps_by_f end -fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy = +fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy = + let + val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result + val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data + in + lthy + |> add_simps "psimps" [] mutual_info fixes psimps spec + |> with_local_path defname + (LocalTheory.note (("domintros", []), domintros) #> snd + #> LocalTheory.note (("termination", []), [termination]) #> snd + #> LocalTheory.note (("cases", []), [cases]) #> snd + #> LocalTheory.note (("pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) #> snd) + |> LocalTheory.theory (Context.theory_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec)))) + end (* FIXME: Add cases for induct and cases thm *) + + + +fun prep_with_flags prep fixspec eqnss_flags global_flag lthy = let - val totality = hd (hd thmss) + val eqnss = map (map (apsnd (map fst))) eqnss_flags + val flags = map (map (map (fn (_, f) => global_flag orelse f) o snd)) eqnss_flags + + val ((fixes, _), ctxt') = prep fixspec [] lthy + val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss + |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *) + |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags + |> (burrow o burrow_snd o burrow) + (FundefSplit.split_some_equations lthy) + |> map (map (apsnd flat)) + in + ((fixes, spec), ctxt') + end + - val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec) - = the (get_fundef_data name thy) +fun gen_add_fundef prep_spec fixspec eqnss_flags preprocess lthy = + let + val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags preprocess lthy + val t_eqns = spec + |> flat |> map snd |> flat (* flatten external structure *) + + val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = + FundefMutual.prepare_fundef_mutual fixes t_eqns lthy + + val afterqed = fundef_afterqed fixes spec mutual_info name prep_result + in + lthy + |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])] + |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd + end + + +fun total_termination_afterqed defname data [[totality]] lthy = + let + val (FundefMResult {psimps, simple_pinducts, ... }, mutual_info, (fixes, stmts)) = data val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) - val tsimps = map (map remove_domain_condition) psimps + val tsimps = map remove_domain_condition psimps val tinduct = map remove_domain_condition simple_pinducts - val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps) - val allatts = if has_guards then [] else [RecfunCodegen.add NONE] - - val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy - - val thy = Theory.add_path name thy - - val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy - val thy = Theory.parent_path thy + (* FIXME: How to generate code from (possibly) local contexts + val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps + val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)] + *) in - thy - end - -(* -fun mk_partial_rules name D_name D domT idomT thmss thy = - let - val [subs, dcl] = (hd thmss) - - val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... } - = the (Symtab.lookup (FundefData.get thy) name) - - val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] - [SOME (cterm_of thy D)] - subsetD) - - val D_simps = map (curry op RS D_implies_dom) f_simps - - val D_induct = subset_induct - |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)] - |> curry op COMP subs - |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT))) - |> forall_intr (cterm_of thy (Var (("x",0), idomT)))) - - val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy - val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2 - in - thy3 - end -*) - - -fun fundef_setup_termination_proof name NONE thy = - let - val name = if name = "" then get_last_fundef thy else name - val data = the (get_fundef_data name thy) - handle Option.Option => raise ERROR ("No such function definition: " ^ name) - - val (res as FundefMResult {termination, ...}, mutual, _) = data - val goal = FundefTermination.mk_total_termination_goal data - in - thy |> ProofContext.init - |> ProofContext.note_thmss_i [(("termination", - [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd - |> Proof.theorem_i PureThy.internalK NONE - (ProofContext.theory o total_termination_afterqed name mutual) NONE ("", []) - [(("", []), [(goal, [])])] - end - | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy = - let - val name = if name = "" then get_last_fundef thy else name - val data = the (get_fundef_data name thy) - val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom - in - thy |> ProofContext.init - |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", []) - [(("", []), [(subs, []), (dcl, [])])] + lthy + |> add_simps "simps" [] mutual_info fixes tsimps stmts + |> with_local_path defname + (LocalTheory.note (("induct", [Attrib.internal (InductAttrib.induct_set "")]), tinduct) #> snd) end -val add_fundef = gen_add_fundef Attrib.attribute +fun fundef_setup_termination_proof name_opt lthy = + let + val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt + val data = the (get_fundef_data name (Context.Proof lthy)) + handle Option.Option => raise ERROR ("No such function definition: " ^ name) + + val (res as FundefMResult {termination, ...}, _, _) = data + val goal = FundefTermination.mk_total_termination_goal data + in + lthy + |> ProofContext.note_thmss_i [(("termination", + [ContextRules.intro_query NONE]), [(ProofContext.export_standard lthy lthy [termination], [])])] |> snd + |> Proof.theorem_i PureThy.internalK NONE + (total_termination_afterqed name data) NONE ("", []) + [(("", []), [(goal, [])])] + end + + +val add_fundef = gen_add_fundef Specification.read_specification +val add_fundef_i = gen_add_fundef Specification.cert_specification @@ -206,39 +184,34 @@ -val star = Scan.one (fn t => (OuterLex.val_of t = "*")); +fun or_list1 s = P.enum1 "|" s + +val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false + +val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" +val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false)) +val statements_ow = or_list1 statement_ow -val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME)) - >> (fn x => (map_filter I x, exists is_none x))) - --| P.$$$ "]"; - -val opt_attribs_with_star = Scan.optional attribs_with_star ([], false); - -val opt_thm_name_star = - Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ ":") ("", ([], false)); - - -val function_decl = - Scan.repeat1 (opt_thm_name_star -- P.prop); +fun local_theory_to_proof f = + Toplevel.theory_to_proof (f o LocalTheory.init NONE) val functionP = OuterSyntax.command "function" "define general recursive functions" K.thy_goal - (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) -- - P.and_list1 function_decl) >> (fn (prepr, eqnss) => - Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr))); + ((opt_sequential -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow) + >> (fn (((sequential, target), fixes), statements) => + Toplevel.print o local_theory_to_proof (add_fundef fixes statements sequential))); + val terminationP = OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal - ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")")) - >> (fn (name,dom) => - Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom))); + (Scan.option P.name + >> (fn name => Toplevel.print o local_theory_to_proof (fundef_setup_termination_proof name))); -val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; val _ = OuterSyntax.add_parsers [functionP]; val _ = OuterSyntax.add_parsers [terminationP]; - +val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; (* currently unused *) end; diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Wed Sep 13 12:05:50 2006 +0200 @@ -9,12 +9,15 @@ signature FUNDEF_PREP = sig - val prepare_fundef : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list - -> FundefCommon.prep_result * theory + val prepare_fundef : string (* defname *) + -> (string * typ * mixfix) (* defined symbol *) + -> ((string * typ) list * term list * term * term) list (* specification *) + -> local_theory + -> FundefCommon.prep_result * term * local_theory end -structure FundefPrep (*: FUNDEF_PREP*) = +structure FundefPrep : FUNDEF_PREP = struct @@ -34,26 +37,6 @@ -fun split_list3 [] = ([],[],[]) - | split_list3 ((x,y,z)::xyzs) = - let - val (xs, ys, zs) = split_list3 xyzs - in - (x::xs,y::ys,z::zs) - end - - -fun build_tree thy f congs ctx (qs, gs, lhs, rhs) = - let - (* FIXME: Save precomputed dependencies in a theory data slot *) - val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) - - val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx - in - FundefCtxTree.mk_tree thy congs_deps f ctx' rhs - end - - fun find_calls tree = let fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs) @@ -64,205 +47,97 @@ -(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *) -fun mk_primed_vars thy glrs = +(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *) +(* Takes bound form of qglrs tuples *) +fun mk_compat_impl domT ranT fvar f ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = let - val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs [] - - fun rename_vars (qs,gs,lhs,rhs) = - let - val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs - val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') [] - in - (qs', map rename_vars gs, rename_vars lhs, rename_vars rhs) - end + val shift = incr_boundvars (length qs') in - map rename_vars glrs + (implies $ Trueprop (eq_const domT $ shift lhs $ lhs') + $ Trueprop (eq_const ranT $ shift rhs $ rhs')) + |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') + |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs') + |> curry abstract_over fvar + |> curry subst_bound f end +fun mk_compat_proof_obligations domT ranT fvar f glrs = + map (mk_compat_impl domT ranT fvar f) (unordered_pairs glrs) -(* Chooses fresh free names, declares G and R, defines f and returns a record - with all the information *) -fun setup_context f glrs defname thy = +fun mk_completeness globals clauses qglrs = let - val Const (f_fullname, fT) = f - val fname = Sign.base_name f_fullname - - val domT = domain_type fT - val ranT = range_type fT - - val GT = mk_relT (domT, ranT) - val RT = mk_relT (domT, domT) - val G_name = defname ^ "_graph" - val R_name = defname ^ "_rel" - - val gfixes = [("h_fd", domT --> ranT), - ("y_fd", ranT), - ("x_fd", domT), - ("z_fd", domT), - ("a_fd", domT), - ("D_fd", HOLogic.mk_setT domT), - ("P_fd", domT --> boolT), - ("Pb_fd", boolT), - ("f_fd", fT)] - - val (fxnames, ctx) = (ProofContext.init thy) - |> ProofContext.add_fixes_i (map (fn (n,T) => (n, SOME T, NoSyn)) gfixes) - - val [h, y, x, z, a, D, P, Pbool, fvar] = map (fn (n,(_,T)) => Free (n, T)) (fxnames ~~ gfixes) - - val Free (fvarname, _) = fvar - - val glrs' = mk_primed_vars thy glrs + val Globals {x, Pbool, ...} = globals - val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy - - val G = Const (Sign.full_name thy G_name, GT) - val R = Const (Sign.full_name thy R_name, RT) - val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R - - val f_eq = Logic.mk_equals (f $ x, - Const ("The", (ranT --> boolT) --> ranT) $ - Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G)) - - val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy - in - (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy) - end - - - - - -(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *) -fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = - (implies $ Trueprop (mk_eq (lhs, lhs')) - $ Trueprop (mk_eq (rhs, rhs'))) - |> fold_rev (curry Logic.mk_implies) (gs @ gs') - |> fold_rev mk_forall (qs @ qs') - -(* all proof obligations *) -fun mk_compat_proof_obligations glrs glrs' = - map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (unordered_pairs (glrs ~~ glrs')) - - -fun mk_completeness names glrs = - let - val Names {domT, x, Pbool, ...} = names - - fun mk_case (qs, gs, lhs, _) = Trueprop Pbool + fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = Trueprop Pbool |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs))) |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev mk_forall qs + |> fold_rev mk_forall_rename (map fst oqs ~~ qs) in Trueprop Pbool - |> fold_rev (curry Logic.mk_implies o mk_case) glrs - |> mk_forall_rename (x, "x") - |> mk_forall_rename (Pbool, "P") + |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) + |> mk_forall_rename ("x", x) + |> mk_forall_rename ("P", Pbool) end -fun inductive_def_wrap defs (thy, const) = +fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = let - val qdefs = map dest_all_all defs + val (qs, ctxt') = Variable.invent_fixes (map fst pre_qs) ctxt + |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs - val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) = - InductivePackage.add_inductive_i true (*verbose*) - false (*add_consts*) - "" (* no altname *) - false (* no coind *) - false (* elims, please *) - false (* induction thm please *) - [const] (* the constant *) - (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *) - [] (* no special monos *) - thy + val thy = ProofContext.theory_of ctxt' -(* It would be nice if this worked... But this is actually HO-Unification... *) -(* fun inst (qs, intr) intr_gen = - Goal.init (cterm_of thy intr) - |> curry op COMP intr_gen - |> Goal.finish - |> fold_rev (forall_intr o cterm_of thy) qs*) + fun inst t = subst_bounds (rev qs, t) + val gs = map inst pre_gs + val lhs = inst pre_lhs + val rhs = inst pre_rhs + + val cqs = map (cterm_of thy) qs + val ags = map (assume o cterm_of thy) gs + + val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) + in + ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, + cqs = cqs, ags = ags, case_hyp = case_hyp } + end + - fun inst (qs, intr) intr_gen = - intr_gen - |> Thm.freezeT - |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs - - val intrs = map2 inst qdefs intrs_gen - val elim = elim_gen - |> Thm.freezeT - |> forall_intr_vars (* FIXME *) - in - (intrs, (thy, const, elim)) - end - - +(* lowlevel term function *) +fun abstract_over_list vs body = + let + exception SAME; + fun abs lev v tm = + if v aconv tm then Bound lev + else + (case tm of + Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t) + | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u) + | _ => raise SAME); + in + fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body + end -(* - * "!!qs xs. CS ==> G => (r, lhs) : R" - *) -fun mk_RIntro R (qs, gs, lhs, rhs) (rcfix, rcassm, rcarg) = - mk_relmem (rcarg, lhs) R - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev (mk_forall o Free) rcfix - |> fold_rev mk_forall qs - - -fun mk_GIntro thy f_const f_var G (qs, gs, lhs, rhs) RCs = +fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = let - fun mk_h_assm (rcfix, rcassm, rcarg) = - mk_relmem (rcarg, f_var $ rcarg) G - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm - |> fold_rev (mk_forall o Free) rcfix - in - mk_relmem (lhs, rhs) G - |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs - |> fold_rev (curry Logic.mk_implies) gs - |> Pattern.rewrite_term thy [(f_const, f_var)] [] - |> fold_rev mk_forall (f_var :: qs) - end - - + val Globals {h, fvar, x, ...} = globals -fun mk_clause_info thy names no (qs,gs,lhs,rhs) tree RCs GIntro_thm RIntro_thms = - let - val Names {G, h, f, fvar, x, ...} = names - - val cqs = map (cterm_of thy) qs - val ags = map (assume o cterm_of thy) gs + val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata + val cert = Thm.cterm_of (ProofContext.theory_of ctxt) - val used = [] (* XXX *) - (* FIXME: What is the relationship between this and mk_primed_vars? *) - val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs - val cqs' = map (cterm_of thy) qs' - - val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') [] - val ags' = map (assume o cterm_of thy o rename_vars) gs - val lhs' = rename_vars lhs - val rhs' = rename_vars rhs - + (* Instantiate the GIntro thm with "f" and import into the clause context. *) val lGI = GIntro_thm - |> forall_elim (cterm_of thy f) + |> forall_elim (cert f) |> fold forall_elim cqs |> fold implies_elim_swp ags - (* FIXME: Can be removed when inductive-package behaves nicely. *) - val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) []) - (term_frees (snd (dest_all_all (prop_of GIntro_thm)))) - fun mk_call_info (rcfix, rcassm, rcarg) RI = let - val crcfix = map (cterm_of thy o Free) rcfix - val llRI = RI |> fold forall_elim cqs - |> fold forall_elim crcfix + |> fold (forall_elim o cert o Free) rcfix |> fold implies_elim_swp ags |> fold implies_elim_swp rcassm @@ -270,27 +145,23 @@ mk_relmem (rcarg, h $ rcarg) G |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |> fold_rev (mk_forall o Free) rcfix - |> Pattern.rewrite_term thy [(f, h)] [] - - val Gh = assume (cterm_of thy h_assum) - val Gh' = assume (cterm_of thy (rename_vars h_assum)) + |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] + |> abstract_over_list (rev qs) in - RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI} + RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} end - val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) - val RC_infos = map2 mk_call_info RCs RIntro_thms in ClauseInfo { no=no, - qs=qs, gs=gs, lhs=lhs, rhs=rhs, - cqs=cqs, ags=ags, - cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', - lGI=lGI, RCs=RC_infos, - tree=tree, case_hyp = case_hyp, - ordcqs'=ordcqs' + cdata=cdata, + qglr=qglr, + + lGI=lGI, + RCs=RC_infos, + tree=tree } end @@ -298,10 +169,7 @@ -(* Copied from fundef_proof.ML: *) -(***********************************************) -(* Compat thms are stored in normal form (with vars) *) (* replace this by a table later*) fun store_compat_thms 0 thms = [] @@ -312,72 +180,63 @@ (thms1 :: store_compat_thms (n - 1) thms2) end - -(* needs i <= j *) +(* expects i <= j *) fun lookup_compat_thm i j cts = nth (nth cts (i - 1)) (j - i) -(***********************************************) - -(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *) +(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) (* if j < i, then turn around *) -fun get_compat_thm thy cts clausei clausej = +fun get_compat_thm thy cts i j ctxi ctxj = let - val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei - val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej + val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi + val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj - val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj'))) + val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj))) in if j < i then let val compat = lookup_compat_thm j i cts in - compat (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *) - |> fold forall_elim (qsj' @ qsi) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *) - |> fold implies_elim_swp gsj' - |> fold implies_elim_swp gsi - |> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *) + compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) + |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) + |> fold implies_elim_swp agsj + |> fold implies_elim_swp agsi + |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) end else let val compat = lookup_compat_thm i j cts in - compat (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *) - |> fold forall_elim (qsi @ qsj') (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *) - |> fold implies_elim_swp gsi - |> fold implies_elim_swp gsj' - |> implies_elim_swp (assume lhsi_eq_lhsj') - |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *) + compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) + |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) + |> fold implies_elim_swp agsi + |> fold implies_elim_swp agsj + |> implies_elim_swp (assume lhsi_eq_lhsj) + |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) end end -(* Generates the replacement lemma with primed variables. A problem here is that one should not do -the complete requantification at the end to replace the variables. One should find a way to be more efficient -here. *) -fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = + +(* Generates the replacement lemma in fully quantified form. *) +fun mk_replacement_lemma thy h ih_elim clause = let - val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names - val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause + val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs - val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs - val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs + val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *) - val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree + val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree val replace_lemma = (eql RS meta_eq_to_obj_eq) |> implies_intr (cprop_of case_hyp) |> fold_rev (implies_intr o cprop_of) h_assums |> fold_rev (implies_intr o cprop_of) ags |> fold_rev forall_intr cqs - |> fold forall_elim cqs' - |> fold implies_elim_swp ags' - |> fold implies_elim_swp h_assums' in replace_lemma end @@ -385,15 +244,30 @@ -fun mk_uniqueness_clause thy names compat_store clausei clausej RLj = +fun pr (s:string) x = + let val _ = print s + in + x + end + + +fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj = let - val Names {f, h, y, ...} = names - val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei - val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej + val Globals {h, y, x, fvar, ...} = globals + val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei + val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej + + val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} + = mk_clause_context x ctxti cdescj - val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj' - val compat = get_compat_thm thy compat_store clausei clausej - val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj + val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' + val compat = get_compat_thm thy compat_store i j cctxi cctxj + val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj + + val RLj_import = + RLj |> fold forall_elim cqsj' + |> fold implies_elim_swp agsj' + |> fold implies_elim_swp Ghsj' val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h)))) val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) @@ -401,7 +275,7 @@ val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h))))) in (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) - |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) + |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) |> implies_intr (cprop_of y_eq_rhsj'h) @@ -409,17 +283,18 @@ |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) |> implies_elim_swp eq_pairs |> fold_rev (implies_intr o cprop_of) Ghsj' - |> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) + |> fold_rev (implies_intr o cprop_of) agsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) |> implies_intr (cprop_of eq_pairs) - |> fold_rev forall_intr ordcqs'j + |> fold_rev forall_intr (cterm_of thy h :: cqsj') end -fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = +fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = let - val Names {x, y, G, fvar, f, ranT, ...} = names - val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei + val Globals {x, y, ranT, fvar, ...} = globals + val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei + val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro @@ -427,14 +302,13 @@ |> fold_rev (implies_intr o cprop_of) CCas |> fold_rev (forall_intr o cterm_of thy o Free) RIvs - val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*) - |> fold (curry op COMP o prep_RC) RCs + val existence = fold (curry op COMP o prep_RC) RCs lGI val a = cterm_of thy (mk_prod (lhs, y)) - val P = cterm_of thy (mk_eq (y, rhs)) + val P = cterm_of thy (mk_eq (y, rhsC)) val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G)))) - val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas + val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas val uniqueness = G_cases |> forall_elim a @@ -447,7 +321,7 @@ val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *) val exactly_one = - ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)] + ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |> curry (op COMP) existence |> curry (op COMP) uniqueness |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) @@ -457,7 +331,6 @@ val function_value = existence - |> fold_rev (implies_intr o cprop_of) ags |> implies_intr ihyp |> implies_intr (cprop_of case_hyp) |> forall_intr (cterm_of thy x) @@ -470,19 +343,13 @@ -fun prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim = +fun prove_stuff thy congs globals G f R clauses complete compat compat_store G_elim f_def = let - val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names - - val f_def_fr = Thm.freezeT f_def + val Globals {h, domT, ranT, x, ...} = globals - val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] - [SOME (cterm_of thy f), SOME (cterm_of thy G)]) - #> curry op COMP (forall_intr_vars f_def_fr) - - val inst_ex1_ex = instantiate_and_def ex1_implies_ex - val inst_ex1_un = instantiate_and_def ex1_implies_un - val inst_ex1_iff = instantiate_and_def ex1_implies_iff + val inst_ex1_ex = f_def RS ex1_implies_ex + val inst_ex1_un = f_def RS ex1_implies_un + val inst_ex1_iff = f_def RS ex1_implies_iff (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) val ihyp = all domT $ Abs ("z", domT, @@ -496,17 +363,18 @@ val ih_elim = ihyp_thm RS inst_ex1_un val _ = Output.debug "Proving Replacement lemmas..." - val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses + val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses val _ = Output.debug "Proving cases for unique existence..." - val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) + val (ex1s, values) = + split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *) val graph_is_function = complete |> forall_elim_vars 0 |> fold (curry op COMP) ex1s |> implies_intr (ihyp) - |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R)))) + |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, mk_acc domT R)))) |> forall_intr (cterm_of thy x) |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it) @@ -523,47 +391,152 @@ end +fun define_graph Gname fvar domT ranT clauses RCss lthy = + let + val GT = mk_relT (domT, ranT) + val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)])) + + fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = + let + fun mk_h_assm (rcfix, rcassm, rcarg) = + mk_relmem (rcarg, fvar $ rcarg) Gvar + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (mk_forall o Free) rcfix + in + mk_relmem (lhs, rhs) Gvar + |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev mk_forall (fvar :: qs) + end + + val G_intros = map2 mk_GIntro clauses RCss + + val (GIntro_thms, (G, G_elim, lthy)) = + FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy) + in + ((G, GIntro_thms, G_elim), lthy) + end -(* - * This is the first step in a function definition. - * - * Defines the function, the graph and the termination relation, synthesizes completeness - * and comatibility conditions and returns everything. - *) -fun prepare_fundef thy congs defname f qglrs used = +fun define_function fdefname (fname, mixfix) domT ranT G lthy = + let + val f_def = + Abs ("x", domT, Const ("The", (ranT --> boolT) --> ranT) $ + Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)) + + val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy + in + ((f, f_defthm), lthy) + end + + +fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy = let - val (names, thy) = setup_context f qglrs defname thy - val Names {G, R, ctx, glrs', fvar, ...} = names + + val RT = mk_relT (domT, domT) + val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)])) + + fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = + mk_relmem (rcarg, lhs) Rvar + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev (mk_forall o Free) rcfix + |> fold_rev mk_forall_rename (map fst oqs ~~ qs) + (* "!!qs xs. CS ==> G => (r, lhs) : R" *) + + val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss + + val (RIntro_thmss, (R, R_elim, lthy)) = + fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy) + in + ((R, RIntro_thmss, R_elim), lthy) + end - val n = length qglrs - val trees = map (build_tree thy f congs ctx) qglrs +fun fix_globals domT ranT fvar ctxt = + let + val ([h, y, x, z, a, D, P, Pbool],ctxt') = + Variable.invent_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt + in + (Globals {h = Free (h, domT --> ranT), + y = Free (y, ranT), + x = Free (x, domT), + z = Free (z, domT), + a = Free (a, domT), + D = Free (D, HOLogic.mk_setT domT), + P = Free (P, domT --> boolT), + Pbool = Free (Pbool, boolT), + fvar = fvar, + domT = domT, + ranT = ranT + }, + ctxt') + end + + + +fun inst_RC thy fvar f (rcfix, rcassm, rcarg) = + let + fun inst_term t = + subst_bound(f, abstract_over (fvar, t)) + in + (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg) + end + + + +fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs lthy = + let + val fvar = Free (fname, fT) + val domT = domain_type fT + val ranT = range_type fT + + val congs = get_fundef_congs (Context.Proof lthy) + val (globals, ctxt') = fix_globals domT ranT fvar lthy + + val Globals { x, ... } = globals + + val clauses = map (mk_clause_context x ctxt') abstract_qglrs + + val n = length abstract_qglrs + + val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *) + + fun build_tree (ClauseContext { ctxt, rhs, ...}) = + FundefCtxTree.mk_tree congs_deps (fname, fT) ctxt rhs + + val trees = map build_tree clauses val RCss = map find_calls trees - val complete = mk_completeness names qglrs - |> cterm_of thy - |> assume + val ((G, GIntro_thms, G_elim), lthy) = define_graph (defname ^ "_graph") fvar domT ranT clauses RCss lthy + val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G lthy + + val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss + val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees - val compat = mk_compat_proof_obligations qglrs glrs' - |> map (assume o cterm_of thy) + val ((R, RIntro_thmss, R_elim), lthy) = + define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss lthy - val compat_store = compat - |> store_compat_thms n + val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", fastype_of (mk_acc domT R)), mk_acc domT R) + val lthy = Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)] lthy - val R_intross = map2 (fn qglr => map (mk_RIntro R qglr)) qglrs RCss - val G_intros = map2 (mk_GIntro thy f fvar G) qglrs RCss + val newthy = ProofContext.theory_of lthy + val clauses = map (transfer_clause_ctx newthy) clauses - val (GIntro_thms, (thy, _, G_elim)) = inductive_def_wrap G_intros (thy, G) - val (RIntro_thmss, (thy, _, R_elim)) = fold_burrow inductive_def_wrap R_intross (thy, R) + val cert = cterm_of (ProofContext.theory_of lthy) + + val xclauses = map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms RIntro_thmss - val clauses = map6 (mk_clause_info thy names) (1 upto n) qglrs trees RCss GIntro_thms RIntro_thmss + val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume + val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume) + + val compat_store = store_compat_thms n compat - val (goal, goalI, ex1_iff, values) = prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim + val (goal, goalI, ex1_iff, values) = prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim f_defthm in - (Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim}, - thy) + (Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f, + lthy) end diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/fundef_proof.ML --- a/src/HOL/Tools/function_package/fundef_proof.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_proof.ML Wed Sep 13 12:05:50 2006 +0200 @@ -28,25 +28,22 @@ val wf_induct_rule = thm "wf_induct_rule"; val Pair_inject = thm "Product_Type.Pair_inject"; -val acc_induct_rule = thm "acc_induct_rule" (* from: Accessible_Part *) -val acc_downward = thm "acc_downward" -val accI = thm "accI" +val acc_induct_rule = thm "Accessible_Part.acc_induct_rule" +val acc_downward = thm "Accessible_Part.acc_downward" +val accI = thm "Accessible_Part.accI" -val ex1_implies_ex = thm "fundef_ex1_existence" (* from: Fundef.thy *) -val ex1_implies_un = thm "fundef_ex1_uniqueness" -val ex1_implies_iff = thm "fundef_ex1_iff" -val acc_subset_induct = thm "acc_subset_induct" +val acc_subset_induct = thm "Accessible_Part.acc_subset_induct" val conjunctionD1 = thm "conjunctionD1" val conjunctionD2 = thm "conjunctionD2" - -fun mk_psimp thy names f_iff graph_is_function clause valthm = +fun mk_psimp thy globals R f_iff graph_is_function clause valthm = let - val Names {R, acc_R, domT, z, ...} = names - val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause - val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *) + val Globals {domT, z, ...} = globals + + val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause + val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, mk_acc domT R))) (* "lhs : acc R" *) val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *) in ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward)) @@ -56,14 +53,16 @@ |> (fn it => it COMP valthm) |> implies_intr lhs_acc |> asm_simplify (HOL_basic_ss addsimps [f_iff]) + |> fold_rev (implies_intr o cprop_of) ags + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end - -fun mk_partial_induct_rule thy names complete_thm clauses = +fun mk_partial_induct_rule thy globals R complete_thm clauses = let - val Names {domT, R, acc_R, x, z, a, P, D, ...} = names + val Globals {domT, x, z, a, P, D, ...} = globals + val acc_R = mk_acc domT R val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D)))) val a_D = cterm_of thy (Trueprop (mk_mem (a, D))) @@ -88,7 +87,8 @@ fun prove_case clause = let - val ClauseInfo {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause + val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs, + qglr = (oqs, _, _, _), ...} = clause val replace_x_ss = HOL_basic_ss addsimps [case_hyp] val lhs_D = simplify replace_x_ss x_D (* lhs : D *) @@ -106,7 +106,7 @@ |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |> fold_rev (curry Logic.mk_implies) gs |> curry Logic.mk_implies (Trueprop (mk_mem (lhs, D))) - |> fold_rev mk_forall qs + |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> cterm_of thy val P_lhs = assume step @@ -130,10 +130,10 @@ val istep = complete_thm |> forall_elim_vars 0 - |> fold (curry op COMP) cases (* P x *) - |> implies_intr ihyp - |> implies_intr (cprop_of x_D) - |> forall_intr (cterm_of thy x) + |> fold (curry op COMP) cases (* P x *) + |> implies_intr ihyp + |> implies_intr (cprop_of x_D) + |> forall_intr (cterm_of thy x) val subset_induct_rule = acc_subset_induct @@ -166,189 +166,13 @@ -(***********************************************) -(* Compat thms are stored in normal form (with vars) *) - -(* replace this by a table later*) -fun store_compat_thms 0 cts = [] - | store_compat_thms n cts = +(* Does this work with Guards??? *) +fun mk_domain_intro thy globals R R_cases clause = let - val (cts1, cts2) = chop n cts - in - (cts1 :: store_compat_thms (n - 1) cts2) - end - - -(* needs i <= j *) -fun lookup_compat_thm i j cts = - nth (nth cts (i - 1)) (j - i) -(***********************************************) - - -(* recover the order of Vars *) -fun get_var_order thy clauses = - map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (unordered_pairs clauses) - - -(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *) -(* if j < i, then turn around *) -fun get_compat_thm thy cts clausei clausej = - let - val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei - val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej - - val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj'))) - in if j < i then - let - val (var_ord, compat) = lookup_compat_thm j i cts - in - compat (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *) - |> instantiate ([],(var_ord ~~ (qsj' @ qsi))) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *) - |> fold implies_elim_swp gsj' - |> fold implies_elim_swp gsi - |> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *) - end - else - let - val (var_ord, compat) = lookup_compat_thm i j cts - in - compat (* "?Gsi => ?Gsj' => ?lhsi = ?lhsj' ==> ?rhsi = ?rhsj'" *) - |> instantiate ([], (var_ord ~~ (qsi @ qsj'))) (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *) - |> fold implies_elim_swp gsi - |> fold implies_elim_swp gsj' - |> implies_elim_swp (assume lhsi_eq_lhsj') - |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *) - end - end - - - - - - - -(* Generates the replacement lemma with primed variables. A problem here is that one should not do -the complete requantification at the end to replace the variables. One should find a way to be more efficient -here. *) -fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = - let - val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names - val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause - - val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim - - val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs - val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs - val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs - - val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *) - - val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree - - val replace_lemma = (eql RS meta_eq_to_obj_eq) - |> implies_intr (cprop_of case_hyp) - |> fold_rev (implies_intr o cprop_of) h_assums - |> fold_rev (implies_intr o cprop_of) ags - |> fold_rev forall_intr cqs - |> fold forall_elim cqs' - |> fold implies_elim_swp ags' - |> fold implies_elim_swp h_assums' - in - replace_lemma - end - - - - -fun mk_uniqueness_clause thy names compat_store clausei clausej RLj = - let - val Names {f, h, y, ...} = names - val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei - val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej - - val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj' - val compat = get_compat_thm thy compat_store clausei clausej - val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj - - val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h)))) - val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) - - val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h))))) - in - (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) - |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) - |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) - |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) - |> implies_intr (cprop_of y_eq_rhsj'h) - |> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *) - |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) - |> implies_elim_swp eq_pairs - |> fold_rev (implies_intr o cprop_of) Ghsj' - |> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) - |> implies_intr (cprop_of eq_pairs) - |> fold_rev forall_intr ordcqs'j - end - - - -fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = - let - val Names {x, y, G, fvar, f, ranT, ...} = names - val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei - - val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro - - fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) - |> fold_rev (implies_intr o cprop_of) CCas - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs - - val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)]) - |> fold (curry op COMP o prep_RC) RCs - - - val a = cterm_of thy (mk_prod (lhs, y)) - val P = cterm_of thy (mk_eq (y, rhs)) - val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G)))) - - val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas - - val uniqueness = G_cases - |> instantiate' [] [SOME a, SOME P] - |> implies_elim_swp a_in_G - |> fold implies_elim_swp unique_clauses - |> implies_intr (cprop_of a_in_G) - |> forall_intr (cterm_of thy y) - - val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *) - - val exactly_one = - ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)] - |> curry (op COMP) existence - |> curry (op COMP) uniqueness - |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) - |> implies_intr (cprop_of case_hyp) - |> fold_rev (implies_intr o cprop_of) ags - |> fold_rev forall_intr cqs - val function_value = - existence - |> fold_rev (implies_intr o cprop_of) ags - |> implies_intr ihyp - |> implies_intr (cprop_of case_hyp) - |> forall_intr (cterm_of thy x) - |> forall_elim (cterm_of thy lhs) - |> curry (op RS) refl - in - (exactly_one, function_value) - end - - - -(* Does this work with Guards??? *) -fun mk_domain_intro thy names R_cases clause = - let - val Names {z, R, acc_R, ...} = names - val ClauseInfo {qs, gs, lhs, rhs, ...} = clause - val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R))) + val Globals {z, domT, ...} = globals + val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, + qglr = (oqs, _, _, _), ...} = clause + val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs, mk_acc domT R))) |> fold_rev (curry Logic.mk_implies) gs |> cterm_of thy in @@ -357,15 +181,17 @@ |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the |> (SINGLE (CLASIMPSET auto_tac)) |> the |> Goal.conclude + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end -fun mk_nest_term_case thy names R' ihyp clause = +fun mk_nest_term_case thy globals R' ihyp clause = let - val Names {x, z, ...} = names - val ClauseInfo {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause + val Globals {x, z, ...} = globals + val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree, + qglr=(oqs, _, _, _), ...} = clause val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp @@ -377,7 +203,7 @@ |> fold_rev (curry Logic.mk_implies o prop_of) used |> FundefCtxTree.export_term (fixes, map prop_of assumes) |> fold_rev (curry Logic.mk_implies o prop_of) ags - |> fold_rev mk_forall qs + |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> cterm_of thy val thm = assume hyp @@ -398,16 +224,10 @@ val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs)))) - val z_acc' = (z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject)) - |> FundefCtxTree.export_thm thy ([], (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes)) - - val occvars = fold (OrdList.insert Term.term_ord) (term_frees (prop_of z_acc')) [] - val ordvars = fold (OrdList.insert Term.term_ord) (map Free fixes @ qs) [] (* FIXME... remove when inductive behaves nice *) - |> OrdList.inter Term.term_ord occvars - - val ethm = z_acc' - |> FundefCtxTree.export_thm thy (map dest_Free ordvars, []) - + val ethm = (z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject)) + |> FundefCtxTree.export_thm thy (fixes, + (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes)) + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) val sub' = sub @ [(([],[]), acc)] in @@ -419,11 +239,10 @@ end -fun mk_nest_term_rule thy names clauses = +fun mk_nest_term_rule thy globals R R_cases clauses = let - val Names { R, acc_R, domT, x, z, ... } = names - - val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) + val Globals { domT, x, z, ... } = globals + val acc_R = mk_acc domT R val R' = Free ("R", fastype_of R) @@ -439,13 +258,12 @@ val ihyp_a = assume ihyp |> forall_elim_vars 0 val z_ltR_x = cterm_of thy (mk_relmem (z, x) R) (* "(z, x) : R" *) - val z_acc = cterm_of thy (mk_mem (z, acc_R)) - val (hyps,cases) = fold (mk_nest_term_case thy names R' ihyp_a) clauses ([],[]) + val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[]) in - R_elim - |> Thm.freezeT - |> instantiate' [] [SOME (cterm_of thy (mk_prod (z,x))), SOME z_acc] + R_cases + |> forall_elim (cterm_of thy (mk_prod (z,x))) + |> forall_elim (cterm_of thy (mk_mem (z, acc_R))) |> curry op COMP (assume z_ltR_x) |> fold_rev (curry op COMP) cases |> implies_intr z_ltR_x @@ -465,8 +283,7 @@ fun mk_partial_rules thy data provedgoal = let - val Prep {names, clauses, values, R_cases, ex1_iff, ...} = data - val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names + val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data val _ = print "Closing Derivation" @@ -486,16 +303,16 @@ val f_iff = (graph_is_function RS ex1_iff) val _ = Output.debug "Proving simplification rules" - val psimps = map2 (mk_psimp thy names f_iff graph_is_function) clauses values + val psimps = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values val _ = Output.debug "Proving partial induction rule" - val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses + val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses val _ = Output.debug "Proving nested termination rule" - val total_intro = mk_nest_term_rule thy names clauses + val total_intro = mk_nest_term_rule thy globals R R_cases clauses val _ = Output.debug "Proving domain introduction rules" - val dom_intros = map (mk_domain_intro thy names R_cases) clauses + val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses in FundefResult {f=f, G=G, R=R, completeness=complete_thm, psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro, diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/inductive_wrap.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML Wed Sep 13 12:05:50 2006 +0200 @@ -0,0 +1,110 @@ +(* Title: HOL/Tools/function_package/inductive_wrap.ML + ID: $Id$ + Author: Alexander Krauss, TU Muenchen + + +This is a wrapper around the inductive package which corrects some of its +slightly annoying behaviours and makes the whole business more controllable. + +Specifically: + +- Following newer Isar conventions, declaration and definition are done in one step + +- The specification is expected in fully quantified form. This allows the client to + control the variable order. The variables will appear in the result in the same order. + This is especially relevant for the elimination rule, where the order usually *does* matter. + + +All this will probably become obsolete in the near future, when the new "predicate" package +is in place. + +*) + +signature FUNDEF_INDUCTIVE_WRAP = +sig + val inductive_def : term list + -> ((bstring * typ) * mixfix) * local_theory + -> thm list * (term * thm * local_theory) +end + +structure FundefInductiveWrap = +struct + + +fun inst_forall (Free (n,_)) (_ $ Abs (_, T, b)) = subst_bound (Free (n, T), b) + | inst_forall t1 t2 = sys_error ((Sign.string_of_term (the_context ()) t1)) + +fun permute_bounds_in_premises thy [] impl = impl + | permute_bounds_in_premises thy ((oldvs, newvs) :: perms) impl = + let + val (prem, concl) = dest_implies (cprop_of impl) + + val newprem = term_of prem + |> fold inst_forall oldvs + |> fold_rev mk_forall newvs + |> cterm_of thy + in + assume newprem + |> fold (forall_elim o cterm_of thy) newvs + |> fold_rev (forall_intr o cterm_of thy) oldvs + |> implies_elim impl + |> permute_bounds_in_premises thy perms + |> implies_intr newprem + end + + +fun inductive_def defs (((R, T), mixfix), lthy) = + let + fun wrap1 thy = + let + val thy = Sign.add_consts_i [(R, T, mixfix)] thy + val RC = Const (Sign.full_name thy R, T) + + val cdefs = map (Pattern.rewrite_term thy [(Free (R, T), RC)] []) defs + val qdefs = map dest_all_all cdefs + + val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) = + InductivePackage.add_inductive_i true (*verbose*) + false (* dont add_consts *) + "" (* no altname *) + false (* no coind *) + false (* elims, please *) + false (* induction thm please *) + [RC] (* the constant *) + (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *) + [] (* no special monos *) + thy + + val perms = map (fn (qs, t) => ((term_frees t) inter qs, qs)) qdefs + + fun inst (qs, _) intr_gen = + intr_gen + |> Thm.freezeT + |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs + + + val a = cterm_of thy (Free ("a0123", HOLogic.dest_setT T)) (* Let's just hope there are no clashes :-} *) + val P = cterm_of thy (Free ("P0123", HOLogic.boolT)) + + val intrs = map2 inst qdefs intrs_gen + + val elim = elim_gen + |> Thm.freezeT + |> forall_intr_vars (* FIXME... *) + |> forall_elim a + |> forall_elim P + |> permute_bounds_in_premises thy (([],[]) :: perms) + |> forall_intr P + |> forall_intr a + in + ((RC, (intrs, elim)), thy) + end + + val ((RC, (intrs, elim)), lthy) = LocalTheory.theory_result wrap1 lthy + in + (intrs, (RC, elim, lthy)) + end + + +end + diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Wed Sep 13 12:05:50 2006 +0200 @@ -10,12 +10,17 @@ signature FUNDEF_MUTUAL = sig - val prepare_fundef_mutual : thm list -> term list list -> theory -> - (FundefCommon.mutual_info * string * (FundefCommon.prep_result * theory)) + val prepare_fundef_mutual : ((string * typ) * mixfix) list + -> term list + -> local_theory + -> ((FundefCommon.mutual_info * string * FundefCommon.prep_result) * local_theory) - val mk_partial_rules_mutual : theory -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> + val mk_partial_rules_mutual : Proof.context -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> FundefCommon.fundef_mresult + + val sort_by_function : FundefCommon.mutual_info -> string list -> 'a list -> 'a list list + end @@ -24,46 +29,83 @@ open FundefCommon +(* Theory dependencies *) +val sum_case_rules = thms "Datatype.sum.cases" +val split_apply = thm "Product_Type.split" + -fun check_const (Const C) = C - | check_const _ = raise ERROR "Head symbol of every left hand side must be a constant." (* FIXME: Output the equation here *) +fun mutual_induct_Pnames n = + if n < 5 then fst (chop n ["P","Q","R","S"]) + else map (fn i => "P" ^ string_of_int i) (1 upto n) + + +fun check_head fs t = + if (case t of + (Free (n, _)) => n mem fs + | _ => false) + then dest_Free t + else raise ERROR "Head symbol of every left hand side must be the new function." (* FIXME: Output the equation here *) +fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) + | open_all_all t = ([], t) -fun split_def geq = +(* Builds a curried clause description in abstracted form *) +fun split_def fnames geq = let - val gs = Logic.strip_imp_prems geq - val eq = Logic.strip_imp_concl geq - val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) - val (fc, args) = strip_comb f_args - val f = check_const fc - - val qs = fold_rev Term.add_frees args [] - - val rhs_new_vars = (Term.add_frees rhs []) \\ qs - val _ = if null rhs_new_vars then () - else raise ERROR "Variables occur on right hand side only: " (* FIXME: Output vars here *) + val (qs, imp) = open_all_all geq + + val gs = Logic.strip_imp_prems imp + val eq = Logic.strip_imp_concl imp + + val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) + val (fc, args) = strip_comb f_args + val f as (fname, _) = check_head fnames fc + + val add_bvs = fold_aterms (fn Bound i => insert (op =) i | _ => I) + val rhs_only = (add_bvs rhs [] \\ fold add_bvs args []) + |> map (fst o nth (rev qs)) + val _ = if null rhs_only then () + else raise ERROR "Variables occur on right hand side only." (* FIXME: Output vars *) in - ((f, length args), (qs, gs, args, rhs)) + ((f, length args), (fname, qs, gs, args, rhs)) end +fun get_part fname = + the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname) -fun analyze_eqs thy eqss = +(* FIXME *) +fun mk_prod_abs e (t1, t2) = + let + val bTs = rev (map snd e) + val T1 = fastype_of1 (bTs, t1) + val T2 = fastype_of1 (bTs, t2) + in + HOLogic.pair_const T1 T2 $ t1 $ t2 + end; + + +fun analyze_eqs ctxt fnames eqs = let + (* FIXME: Add check for number of arguments fun all_equal ((x as ((n:string,T), k:int))::xs) = if forall (fn ((n',_),k') => n = n' andalso k = k') xs then x else raise ERROR ("All equations in a block must describe the same " - ^ "constant and have the same number of arguments.") + ^ "function and have the same number of arguments.") + *) - val def_infoss = map (split_list o map split_def) eqss - val (consts, qgarss) = split_list (map (fn (Cis, eqs) => (all_equal Cis, eqs)) def_infoss) + val (consts, fqgars) = split_list (map (split_def fnames) eqs) - val cnames = map (fst o fst) consts - val check_rcs = exists_Const (fn (n,_) => if n mem cnames - then raise ERROR "Recursive Calls not allowed in premises." else false) - val _ = forall (forall (fn (_, gs, _, _) => forall check_rcs gs)) qgarss + val different_consts = distinct (eq_fst (eq_fst eq_str)) consts + val cnames = map (fst o fst) different_consts + + val check_rcs = exists_subterm (fn Free (n, _) => if n mem cnames + then raise ERROR "Recursive Calls not allowed in premises." else false + | _ => false) + + val _ = forall (fn (_, _, gs, _, _) => forall check_rcs gs) fqgars fun curried_types ((_,T), k) = let @@ -72,61 +114,87 @@ (caTs, uaTs ---> body_type T) end - val (caTss, resultTs) = split_list (map curried_types consts) + val (caTss, resultTs) = split_list (map curried_types different_consts) val argTs = map (foldr1 HOLogic.mk_prodT) caTss - val (RST,streeR, pthsR) = SumTools.mk_tree resultTs + val (RST,streeR, pthsR) = SumTools.mk_tree_distinct resultTs val (ST, streeA, pthsA) = SumTools.mk_tree argTs val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name cnames) - val sfun_xname = def_name ^ "_sum" - val sfun_type = ST --> RST + val fsum_type = ST --> RST - val thy = Sign.add_consts_i [(sfun_xname, sfun_type, NoSyn)] thy (* Add the sum function *) - val sfun = Const (Sign.full_name thy sfun_xname, sfun_type) + val ([fsum_var_name], _) = Variable.add_fixes [ def_name ^ "_sum" ] ctxt + val fsum_var = (fsum_var_name, fsum_type) - fun define (((((n, T), _), caTs), (pthA, pthR)), qgars) (thy, rews) = + fun define (fvar as (n, T), _) caTs pthA pthR = let - val fxname = Sign.base_name n - val f = Const (n, T) - val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs + val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs (* FIXME: Bind xs properly *) - val f_exp = SumTools.mk_proj streeR pthR (sfun $ SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod vars)) - val def = Logic.mk_equals (list_comb (f, vars), f_exp) - - val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy - val rews' = (f, fold_rev lambda vars f_exp) :: rews + val f_exp = SumTools.mk_proj streeR pthR (Free fsum_var $ SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod vars)) + val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) + + val rew = (n, fold_rev lambda vars f_exp) in - (MutualPart {f_name=fxname, const=(n, T),cargTs=caTs,pthA=pthA,pthR=pthR,qgars=qgars,f_def=f_def}, (thy, rews')) + (MutualPart {fvar=fvar,cargTs=caTs,pthA=pthA,pthR=pthR,f_def=def,f=NONE,f_defthm=NONE}, rew) end - val (parts, (thy, rews)) = fold_map define (((consts ~~ caTss)~~ (pthsA ~~ pthsR)) ~~ qgarss) (thy, []) + val (parts, rews) = split_list (map4 define different_consts caTss pthsA pthsR) - fun mk_qglrss (MutualPart {qgars, pthA, pthR, ...}) = - let - fun convert_eqs (qs, gs, args, rhs) = - (map Free qs, gs, SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod args), - SumTools.mk_inj streeR pthR (Pattern.rewrite_term thy rews [] rhs)) - in - map convert_eqs qgars - end - - val qglrss = map mk_qglrss parts + fun convert_eqs (f, qs, gs, args, rhs) = + let + val MutualPart {pthA, pthR, ...} = get_part f parts + in + (qs, gs, SumTools.mk_inj streeA pthA (foldr1 (mk_prod_abs qs) args), + SumTools.mk_inj streeR pthR (replace_frees rews rhs) + |> Envir.norm_term (Envir.empty 0)) + end + + val qglrs = map convert_eqs fqgars in - (Mutual {name=def_name,sum_const=dest_Const sfun, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts, qglrss=qglrss}, thy) + Mutual {defname=def_name,fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, + parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} end -fun prepare_fundef_mutual congs eqss thy = +fun define_projections fixes mutual fsum lthy = + let + fun def ((MutualPart {fvar=(fname, fT), cargTs, pthA, pthR, f_def, ...}), (_, mixfix)) lthy = + let + val ((f, (_, f_defthm)), lthy') = LocalTheory.def ((fname, mixfix), + ((fname ^ "_def", []), Term.subst_bound (fsum, f_def))) + lthy + in + (MutualPart {fvar=(fname, fT), cargTs=cargTs, pthA=pthA, pthR=pthR, f_def=f_def, + f=SOME f, f_defthm=SOME f_defthm }, + lthy') + end + + val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual + val (parts', lthy') = fold_map def (parts ~~ fixes) lthy + in + (Mutual { defname=defname, fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts', + fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, + lthy') + end + + + + + + +fun prepare_fundef_mutual fixes eqss lthy = let - val (mutual, thy) = analyze_eqs thy eqss - val Mutual {name, sum_const, qglrss, ...} = mutual - val global_glrs = flat qglrss - val used = fold (fn (qs, _, _, _) => fold (curry op ins_string o fst o dest_Free) qs) global_glrs [] + val mutual = analyze_eqs lthy (map (fst o fst) fixes) eqss + val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual + + val (prep_result, fsum, lthy') = + FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs lthy + + val (mutual', lthy'') = define_projections fixes mutual fsum lthy' in - (mutual, name, FundefPrep.prepare_fundef thy congs name (Const sum_const) global_glrs used) + ((mutual', defname, prep_result), lthy'') end @@ -140,48 +208,76 @@ transitive (symmetric lhs_conv) (transitive thm rhs_conv) end - - - -fun map_mutual2 f (Mutual {parts, ...}) = - map2 (fn (p as MutualPart {qgars, ...}) => map2 (f p) qgars) parts - +fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm -fun recover_mutual_psimp thy RST streeR all_f_defs (MutualPart {f_def, pthR, ...}) (_,_,args,_) sum_psimp = +fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = let - val conds = cprems_of sum_psimp (* dom-condition and guards *) - val plain_eq = sum_psimp - |> fold (implies_elim_swp o assume) conds + val thy = ProofContext.theory_of ctxt - val x = Free ("x", RST) + val oqnames = map fst pre_qs + val (qs, ctxt') = Variable.invent_fixes oqnames ctxt + |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs - val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (Thm.freezeT f_def) (* FIXME: freezeT *) + fun inst t = subst_bounds (rev qs, t) + val gs = map inst pre_gs + val args = map inst pre_args + val rhs = inst pre_rhs + + val cqs = map (cterm_of thy) qs + val ags = map (assume o cterm_of thy) gs + + val import = fold forall_elim cqs + #> fold implies_elim_swp ags + + val export = fold_rev (implies_intr o cprop_of) ags + #> fold_rev forall_intr_rename (oqnames ~~ cqs) in - reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x))) (* PR(x) == PR(x) *) - |> (fn it => combination it (plain_eq RS eq_reflection)) - |> beta_norm_eq (* PR(S(I(as))) == PR(IR(...)) *) - |> transitive f_def_inst (* f ... == PR(IR(...)) *) - |> simplify (HOL_basic_ss addsimps [SumTools.projl_inl, SumTools.projr_inr]) (* f ... == ... *) - |> simplify (HOL_basic_ss addsimps all_f_defs) (* f ... == ... *) - |> (fn it => it RS meta_eq_to_obj_eq) - |> fold_rev implies_intr conds + F (f, qs, gs, args, rhs) import export end +fun recover_mutual_psimp thy RST streeR all_f_defs parts (f, _, _, args, _) import (export : thm -> thm) sum_psimp_eq = + let + val (MutualPart {f_defthm=SOME f_def, pthR, ...}) = get_part f parts + val psimp = import sum_psimp_eq + val (simp, restore_cond) = case cprems_of psimp of + [] => (psimp, I) + | [cond] => (implies_elim psimp (assume cond), implies_intr cond) + | _ => sys_error "Too many conditions" + + val x = Free ("x", RST) + + val f_def_inst = fold (fn arg => fn thm => combination thm (reflexive (cterm_of thy arg))) args (Thm.freezeT f_def) (* FIXME *) + |> beta_reduce + in + reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x))) (* PR(x) == PR(x) *) + |> (fn it => combination it (simp RS eq_reflection)) + |> beta_norm_eq (* PR(S(I(as))) == PR(IR(...)) *) + |> transitive f_def_inst (* f ... == PR(IR(...)) *) + |> simplify (HOL_basic_ss addsimps [SumTools.projl_inl, SumTools.projr_inr]) (* f ... == ... *) + |> simplify (HOL_basic_ss addsimps all_f_defs) (* f ... == ... *) + |> (fn it => it RS meta_eq_to_obj_eq) + |> restore_cond + |> export + end -fun mutual_induct_Pnames n = - if n < 5 then fst (chop n ["P","Q","R","S"]) - else map (fn i => "P" ^ string_of_int i) (1 upto n) - - -val sum_case_rules = thms "Datatype.sum.cases" -val split_apply = thm "Product_Type.split" +(* FIXME HACK *) +fun mk_applied_form ctxt caTs thm = + let + val thy = ProofContext.theory_of ctxt + val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) + in + fold (fn x => fn thm => combination thm (reflexive x)) xs thm + |> beta_reduce + |> fold_rev forall_intr xs + |> forall_elim_vars 0 + end + - -fun mutual_induct_rules thy induct all_f_defs (Mutual {qglrss, RST, parts, streeA, ...}) = +fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) = let fun mk_P (MutualPart {cargTs, ...}) Pname = let @@ -210,29 +306,53 @@ end in - map (mk_proj induct_inst) parts + map (mk_proj induct_inst) parts end - + -fun mk_partial_rules_mutual thy (m as Mutual {qglrss, RST, parts, streeR, ...}) data result = +fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result = let - val result = FundefProof.mk_partial_rules thy data result - val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result - - val sum_psimps = Library.unflat qglrss psimps + val thy = ProofContext.theory_of lthy + + val result = FundefProof.mk_partial_rules thy data prep_result + val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result + + val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} => + mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def))) + parts + |> print + + fun mk_mpsimp fqgar sum_psimp = + in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp + + val mpsimps = map2 mk_mpsimp fqgars psimps + + val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m + val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro + in + FundefMResult { f=f, G=G, R=R, + psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts, + cases=completeness, termination=termination, domintros=dom_intros } + end - val all_f_defs = map (fn MutualPart {f_def, ...} => symmetric f_def) parts - val mpsimps = map_mutual2 (recover_mutual_psimp thy RST streeR all_f_defs) m sum_psimps - val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m - val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro - in - FundefMResult { f=f, G=G, R=R, - psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts, - cases=completeness, termination=termination, domintros=dom_intros} - end + + +(* puts an object in the "right bucket" *) +fun store_grouped P x [] = [] + | store_grouped P x ((l, xs)::bs) = + if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs) + +fun sort_by_function (Mutual {fqgars, ...}) names xs = + fold_rev (store_grouped (eq_str o apfst fst)) (* fill *) + (map name_of_fqgar fqgars ~~ xs) (* the name-thm pairs *) + (map (rpair []) names) (* in the empty buckets labeled with names *) + + |> map (snd #> map snd) (* and remove the labels afterwards *) + + end diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/pattern_split.ML --- a/src/HOL/Tools/function_package/pattern_split.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/pattern_split.ML Wed Sep 13 12:05:50 2006 +0200 @@ -12,8 +12,10 @@ signature FUNDEF_SPLIT = sig val split_some_equations : - Proof.context -> (('a * ('b * bool)) * term) list -> (('a * 'b) * term list) list + Proof.context -> (bool * term) list -> term list list + val split_all_equations : + Proof.context -> term list -> term list list end structure FundefSplit : FUNDEF_SPLIT = @@ -51,7 +53,7 @@ val (vs', t) = saturate ctx vs constr val substs = pattern_subtract_subst ctx vs' t t' in - map (cons (v, t)) substs + map (fn (vs, subst) => (vs, (v,t)::subst)) substs end in flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T)) @@ -63,24 +65,29 @@ in if C = C' then flat (map2 (pattern_subtract_subst ctx vs) ps qs) - else [[]] + else [(vs, [])] end -fun pattern_subtract_parallel ctx vs ps qs = - flat (map2 (pattern_subtract_subst ctx vs) ps qs) - - -(* ps - qs *) +(* p - q *) fun pattern_subtract ctx eq2 eq1 = let - val _ $ (_ $ lhs1 $ _) = eq1 - val _ $ (_ $ lhs2 $ _) = eq2 + + val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1 + val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2 val thy = ProofContext.theory_of ctx - val vs = term_frees eq1 + + val substs = pattern_subtract_subst ctx vs lhs1 lhs2 + + fun instantiate (vs', sigma) = + let + val t = Pattern.rewrite_term thy sigma [] feq1 + in + fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t + end in - map (fn sigma => Pattern.rewrite_term thy sigma [] eq1) (pattern_subtract_subst ctx vs lhs1 lhs2) + map instantiate substs end @@ -94,24 +101,21 @@ -fun split_all_equations ctx eqns = - let - fun split_aux prev [] = [] - | split_aux prev (e::es) = pattern_subtract_many ctx prev [e] @ split_aux (e::prev) es - in - split_aux [] eqns -end - - fun split_some_equations ctx eqns = let fun split_aux prev [] = [] - | split_aux prev (((n, (att, true)), eq) :: es) = ((n, att), pattern_subtract_many ctx prev [eq]) - :: split_aux (eq :: prev) es - | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq]) - :: split_aux (eq :: prev) es + | split_aux prev ((true, eq) :: es) = pattern_subtract_many ctx prev [eq] + :: split_aux (eq :: prev) es + | split_aux prev ((false, eq) :: es) = [eq] + :: split_aux (eq :: prev) es in split_aux [] eqns end +fun split_all_equations ctx = + split_some_equations ctx o map (pair true) + + + + end diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/sum_tools.ML --- a/src/HOL/Tools/function_package/sum_tools.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/sum_tools.ML Wed Sep 13 12:05:50 2006 +0200 @@ -17,6 +17,7 @@ val projr_inr: thm val mk_tree : typ list -> typ * sum_tree * sum_path list + val mk_tree_distinct : typ list -> typ * sum_tree * sum_path list val mk_proj: sum_tree -> sum_path -> term -> term val mk_inj: sum_tree -> sum_path -> term -> term @@ -37,12 +38,9 @@ val projl_inl = thm "FunDef.lproj_inl" val projr_inr = thm "FunDef.rproj_inr" - - fun mk_sumT LT RT = Type ("+", [LT, RT]) fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r - datatype sum_tree = Leaf of typ | Branch of (typ * (typ * sum_tree) * (typ * sum_tree)) @@ -72,6 +70,23 @@ end +fun mk_tree_distinct Ts = + let + fun insert_once T Ts = + let + val i = find_index_eq T Ts + in + if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts) + end + + val (idxs, dist_Ts) = fold_map insert_once Ts [] + + val (ST, tree, pths) = mk_tree dist_Ts + in + (ST, tree, map (nth pths) idxs) + end + + fun mk_inj (Leaf _) [] t = t | mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t = Const (inlN, LT --> ST) $ mk_inj tr pth t diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/termination.ML --- a/src/HOL/Tools/function_package/termination.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/Tools/function_package/termination.ML Wed Sep 13 12:05:50 2006 +0200 @@ -25,7 +25,7 @@ val domT = domain_type (fastype_of f) val x = Free ("x", domT) in - Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R)) + Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R)) end fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom = diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/W0/W0.thy --- a/src/HOL/W0/W0.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/W0/W0.thy Wed Sep 13 12:05:50 2006 +0200 @@ -57,7 +57,7 @@ instance "typ" :: type_struct .. instance list :: (type_struct) type_struct .. -instance fun :: (type, type_struct) type_struct .. +instance "fun" :: (type, type_struct) type_struct .. subsection {* Substitutions *} diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/ex/CodeCollections.thy --- a/src/HOL/ex/CodeCollections.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/ex/CodeCollections.thy Wed Sep 13 12:05:50 2006 +0200 @@ -5,7 +5,7 @@ header {* Collection classes as examples for code generation *} theory CodeCollections -imports CodeOperationalEquality +imports "../FundefDebug" CodeOperationalEquality begin section {* Collection classes as examples for code generation *} @@ -66,16 +66,16 @@ max :: "'a::ordered \ 'a \ 'a" "max x y = (if x <<= y then y else x)" -consts - abs_sorted :: "('a \ 'a \ bool) \ 'a list \ bool" - -function +fun abs_sorted :: "('a \ 'a \ bool) \ 'a list \ bool" +where "abs_sorted cmp [] = True" - "abs_sorted cmp [x] = True" - "abs_sorted cmp (x#y#xs) = (cmp x y \ abs_sorted cmp (y#xs))" -by pat_completeness simp_all +| "abs_sorted cmp [x] = True" +| "abs_sorted cmp (x#y#xs) = (cmp x y \ abs_sorted cmp (y#xs))" + termination by (auto_term "measure (length o snd)") +thm abs_sorted.simps + abbreviation (in ordered) "sorted \ abs_sorted le" @@ -90,7 +90,8 @@ next case (Cons x' xs) from this(5) have "sorted (x # x' # xs)" . - then show "sorted (x' # xs)" by auto + then show "sorted (x' # xs)" + by auto qed instance bool :: ordered @@ -109,14 +110,13 @@ "u <<= v == True" by default (simp_all add: ordered_unit_def) -consts - le_option' :: "'a::ordered option \ 'a option \ bool" -function +fun le_option' :: "'a::ordered option \ 'a option \ bool" +where "le_option' None y = True" - "le_option' (Some x) None = False" - "le_option' (Some x) (Some y) = x <<= y" - by pat_completeness simp_all +| "le_option' (Some x) None = False" +| "le_option' (Some x) (Some y) = x <<= y" + termination by (auto_term "{}") instance (ordered) option :: ordered @@ -144,12 +144,9 @@ "Some v <<= Some w = v <<= w" unfolding ordered_option_def le_option'.simps by rule+ -consts - le_pair' :: "'a::ordered \ 'b::ordered \ 'a \ 'b \ bool" - -function +fun le_pair' :: "'a::ordered \ 'b::ordered \ 'a \ 'b \ bool" +where "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \ x1 = x2 \ y1 <<= y2)" - by pat_completeness simp_all termination by (auto_term "{}") instance (ordered, ordered) * :: ordered @@ -164,14 +161,14 @@ "(x1, y1) <<= (x2, y2) = (x1 << x2 \ x1 = x2 \ y1 <<= y2)" unfolding "ordered_*_def" le_pair'.simps .. -(* consts - le_list' :: "'a::ordered list \ 'a list \ bool" +(* -function +fun le_list' :: "'a::ordered list \ 'a list \ bool" +where "le_list' [] ys = True" - "le_list' (x#xs) [] = False" - "le_list' (x#xs) (y#ys) = (x << y \ x = y \ le_list' xs ys)" - by pat_completeness simp_all +| "le_list' (x#xs) [] = False" +| "le_list' (x#xs) (y#ys) = (x << y \ x = y \ le_list' xs ys)" + termination by (auto_term "measure (length o fst)") instance (ordered) list :: ordered @@ -213,14 +210,13 @@ shows no_smaller: "a = inf" using prem inf by (rule order_antisym) -consts - abs_max_of :: "('a \ 'a \ bool) \ 'a \ 'a list \ 'a" ML {* set quick_and_dirty *} -function +function abs_max_of :: "('a \ 'a \ bool) \ 'a \ 'a list \ 'a" +where "abs_max_of cmp inff [] = inff" - "abs_max_of cmp inff [x] = x" - "abs_max_of cmp inff (x#xs) = +| "abs_max_of cmp inff [x] = x" +| "abs_max_of cmp inff (x#xs) = ordered.max cmp x (abs_max_of cmp inff xs)" apply pat_completeness sorry diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/ex/CodeOperationalEquality.thy --- a/src/HOL/ex/CodeOperationalEquality.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/ex/CodeOperationalEquality.thy Wed Sep 13 12:05:50 2006 +0200 @@ -113,7 +113,7 @@ instance int :: eq .. -lemma [code fun]: +lemma [code func]: "eq k l = eq_integer k l" unfolding eq_integer_def eq_def .. diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/ex/Fundefs.thy --- a/src/HOL/ex/Fundefs.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/ex/Fundefs.thy Wed Sep 13 12:05:50 2006 +0200 @@ -6,26 +6,31 @@ *) theory Fundefs -imports Main +imports Main "../FundefDebug" begin + section {* Very basic *} -consts fib :: "nat \ nat" -function +ML "trace_simp := false" + +fun fib :: "nat \ nat" +where "fib 0 = 1" - "fib (Suc 0) = 1" - "fib (Suc (Suc n)) = fib n + fib (Suc n)" -by pat_completeness -- {* shows that the patterns are complete *} - auto -- {* shows that the patterns are compatible *} +| "fib (Suc 0) = 1" +| "fib (Suc (Suc n)) = fib n + fib (Suc n)" + text {* we get partial simp and induction rules: *} thm fib.psimps -thm pinduct +thm fib.pinduct text {* There is also a cases rule to distinguish cases along the definition *} thm fib.cases +thm fib.domintros + + text {* Now termination: *} termination fib by (auto_term "less_than") @@ -36,34 +41,30 @@ section {* Currying *} -consts add :: "nat \ nat \ nat" -function +fun add :: "nat \ nat \ nat" +where "add 0 y = y" - "add (Suc x) y = Suc (add x y)" -thm add_rel.cases - -by pat_completeness auto +| "add (Suc x) y = Suc (add x y)" termination by (auto_term "measure fst") +thm add.simps thm add.induct -- {* Note the curried induction predicate *} section {* Nested recursion *} -consts nz :: "nat \ nat" -function +fun nz :: "nat \ nat" +where "nz 0 = 0" - "nz (Suc x) = nz (nz x)" -by pat_completeness auto +| "nz (Suc x) = nz (nz x)" + lemma nz_is_zero: -- {* A lemma we need to prove termination *} assumes trm: "x \ nz_dom" shows "nz x = 0" using trm -apply induct -apply auto -done +by induct auto termination nz apply (auto_term "less_than") -- {* Oops, it left us something to prove *} @@ -74,10 +75,10 @@ text {* Here comes McCarthy's 91-function *} -consts f91 :: "nat => nat" -function +fun f91 :: "nat => nat" +where "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))" -by pat_completeness auto + (* Prove a lemma before attempting a termination proof *) lemma f91_estimate: @@ -85,7 +86,6 @@ shows "n < f91 n + 11" using trm by induct auto -(* Now go for termination *) termination proof let ?R = "measure (%x. 101 - x)" @@ -109,15 +109,16 @@ no automatic splitting takes place. But the following definition of gcd is ok, although patterns overlap: *} -consts gcd2 :: "nat \ nat \ nat" -function +fun gcd2 :: "nat \ nat \ nat" +where "gcd2 x 0 = x" - "gcd2 0 y = y" - "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) - else gcd2 (x - y) (Suc y))" -by pat_completeness auto +| "gcd2 0 y = y" +| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) + else gcd2 (x - y) (Suc y))" + + termination - by (auto_term "measure (\(x,y). x + y)") + by (auto_term "(measure (%x. x)) <*lex*> (measure (%x. x))") thm gcd2.simps thm gcd2.induct @@ -127,8 +128,8 @@ text {* We can reformulate the above example using guarded patterns *} -consts gcd3 :: "nat \ nat \ nat" -function +function gcd3 :: "nat \ nat \ nat" +where "gcd3 x 0 = x" "gcd3 0 y = y" "x < y \ gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" @@ -136,6 +137,7 @@ apply (case_tac x, case_tac a, auto) apply (case_tac ba, auto) done + termination by (auto_term "measure (\(x,y). x + y)") @@ -143,10 +145,10 @@ thm gcd3.induct +text {* General patterns allow even strange definitions: *} -text {* General patterns allow even strange definitions: *} -consts ev :: "nat \ bool" -function +function ev :: "nat \ bool" +where "ev (2 * n) = True" "ev (2 * n + 1) = False" proof - -- {* completeness is more difficult here \dots *} @@ -166,7 +168,7 @@ with divmod have "x = 2 * (x div 2) + 1" by simp with c2 show "P" . qed -qed presburger+ -- {* solve compatibility with presburger *} +qed presburger+ -- {* solve compatibility with presburger *} termination by (auto_term "{}") thm ev.simps @@ -176,18 +178,12 @@ section {* Mutual Recursion *} - -consts - evn :: "nat \ bool" - od :: "nat \ bool" - -function +fun evn od :: "nat \ bool" +where "evn 0 = True" - "evn (Suc n) = od n" -and - "od 0 = False" - "od (Suc n) = evn n" - by pat_completeness auto +| "od 0 = False" +| "evn (Suc n) = od n" +| "od (Suc n) = evn n" thm evn.psimps thm od.psimps diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/ex/Higher_Order_Logic.thy --- a/src/HOL/ex/Higher_Order_Logic.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/ex/Higher_Order_Logic.thy Wed Sep 13 12:05:50 2006 +0200 @@ -25,7 +25,7 @@ typedecl o arities o :: type - fun :: (type, type) type + "fun" :: (type, type) type subsubsection {* Basic logical connectives *} diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/ex/NormalForm.thy --- a/src/HOL/ex/NormalForm.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/ex/NormalForm.thy Wed Sep 13 12:05:50 2006 +0200 @@ -9,7 +9,7 @@ begin lemma "p \ True" by normalization -declare disj_assoc [code fun] +declare disj_assoc [code func] normal_form "(P | Q) | R" lemma "0 + (n::nat) = n" by normalization diff -r 05072ae0d435 -r 36a59e5d0039 src/HOLCF/Ffun.thy --- a/src/HOLCF/Ffun.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOLCF/Ffun.thy Wed Sep 13 12:05:50 2006 +0200 @@ -15,7 +15,7 @@ subsection {* Full function space is a partial order *} -instance fun :: (type, sq_ord) sq_ord .. +instance "fun" :: (type, sq_ord) sq_ord .. defs (overloaded) less_fun_def: "(op \) \ (\f g. \x. f x \ g x)" @@ -36,7 +36,7 @@ apply (erule spec) done -instance fun :: (type, po) po +instance "fun" :: (type, po) po by intro_classes (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+ @@ -90,7 +90,7 @@ "chain (S::nat \ 'a::type \ 'b::cpo) \ \x. range S <<| x" by (rule exI, erule lub_fun) -instance fun :: (type, cpo) cpo +instance "fun" :: (type, cpo) cpo by intro_classes (rule cpo_fun) subsection {* Full function space is pointed *} @@ -103,7 +103,7 @@ apply (rule minimal_fun [THEN allI]) done -instance fun :: (type, pcpo) pcpo +instance "fun" :: (type, pcpo) pcpo by intro_classes (rule least_fun) text {* for compatibility with old HOLCF-Version *} diff -r 05072ae0d435 -r 36a59e5d0039 src/Pure/Tools/codegen_theorems.ML --- a/src/Pure/Tools/codegen_theorems.ML Wed Sep 13 00:38:38 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Wed Sep 13 12:05:50 2006 +0200 @@ -918,7 +918,7 @@ (Context.map_theory o f); in val _ = map (Context.add_setup o add_simple_attribute) [ - ("fun", add_fun), + ("func", add_fun), ("nofun", del_fun), ("unfold", (fn thm => Codegen.add_unfold thm #> add_unfold thm)), ("inline", add_unfold),