Major update to function package, including new syntax and the (only theoretical)
ability to handle local contexts.
--- 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"
--- 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]:
"(\<not> True) = False" by (rule HOL.simp_thms)
-lemma [code fun]:
+lemma [code func]:
"(\<not> False) = True" by (rule HOL.simp_thms)
-lemma [code fun]:
+lemma [code func]:
shows "(False \<and> x) = False"
and "(True \<and> x) = x"
and "(x \<and> False) = False"
and "(x \<and> True) = x" by simp_all
-lemma [code fun]:
+lemma [code func]:
shows "(False \<or> x) = x"
and "(True \<or> x) = True"
and "(x \<or> False) = x"
and "(x \<or> 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]
--- 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: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
+assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
assumes ex1: "\<exists>!y. (x,y)\<in>G"
shows "(x, f x)\<in>G"
by (simp only:f_def, rule theI', rule ex1)
lemma fundef_ex1_uniqueness:
-assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
+assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
assumes ex1: "\<exists>!y. (x,y)\<in>G"
assumes elm: "(x, h x)\<in>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: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
+assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
assumes ex1: "\<exists>!y. (x,y)\<in>G"
shows "((x, y)\<in>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"
--- 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 \<Rightarrow> nat"
+ "fun" :: "exp \<Rightarrow> nat"
"fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
lemma fun_respects: "(%U. {freefun U}) respects exprel"
--- 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
--- 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
--- 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 \<Rightarrow> 'b::lattice"
show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
--- 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 \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
@@ -260,7 +260,7 @@
lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> 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 \<Rightarrow> 'b::quasi_order"
show "f \<sqsubseteq> 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 \<Rightarrow> 'b::partial_order"
assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
--- 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
--- 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 \<Rightarrow> 'a list \<Rightarrow> 'a list"
- intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
- subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
- map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
- unions :: "'a list list \<Rightarrow> 'a list"
- intersects :: "'a list list \<Rightarrow> 'a list"
-function
+function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> 'a list"
primrec
"intersects (x#xs) = foldr intersect xs x"
@@ -156,7 +160,8 @@
lemma iso_union:
"set (unionl xs ys) = set xs \<union> 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 \<inter> set ys"
--- 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)
--- 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)) =
--- 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
--- 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
--- 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 [])
--- 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;
--- 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
--- 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,
--- /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
+
--- 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
--- 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
--- 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
--- 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 =
--- 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 *}
--- 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 \<Rightarrow> 'a \<Rightarrow> 'a"
"max x y = (if x <<= y then y else x)"
-consts
- abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
-
-function
+fun abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+where
"abs_sorted cmp [] = True"
- "abs_sorted cmp [x] = True"
- "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
-by pat_completeness simp_all
+| "abs_sorted cmp [x] = True"
+| "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
+
termination by (auto_term "measure (length o snd)")
+thm abs_sorted.simps
+
abbreviation (in ordered)
"sorted \<equiv> 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 \<Rightarrow> 'a option \<Rightarrow> bool"
-function
+fun le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> 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 \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-
-function
+fun le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+where
"le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> 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 \<or> x1 = x2 \<and> y1 <<= y2)"
unfolding "ordered_*_def" le_pair'.simps ..
-(* consts
- le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool"
+(*
-function
+fun le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool"
+where
"le_list' [] ys = True"
- "le_list' (x#xs) [] = False"
- "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)"
- by pat_completeness simp_all
+| "le_list' (x#xs) [] = False"
+| "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> 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 \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a"
ML {* set quick_and_dirty *}
-function
+function abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> '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
--- 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 ..
--- 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 \<Rightarrow> nat"
-function
+ML "trace_simp := false"
+
+fun fib :: "nat \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> nat"
-function
+fun add :: "nat \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> nat"
-function
+fun nz :: "nat \<Rightarrow> 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 \<in> 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 \<Rightarrow> nat \<Rightarrow> nat"
-function
+fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> 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 (\<lambda>(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 \<Rightarrow> nat \<Rightarrow> nat"
-function
+function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
"gcd3 x 0 = x"
"gcd3 0 y = y"
"x < y \<Longrightarrow> 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 (\<lambda>(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 \<Rightarrow> bool"
-function
+function ev :: "nat \<Rightarrow> 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 \<Rightarrow> bool"
- od :: "nat \<Rightarrow> bool"
-
-function
+fun evn od :: "nat \<Rightarrow> 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
--- 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 *}
--- 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 \<longrightarrow> 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
--- 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 \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> 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 \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>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 *}
--- 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),