--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Jun 06 08:21:14 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Jun 06 09:28:24 2006 +0200
@@ -116,7 +116,7 @@
val tsimps = map (map remove_domain_condition) psimps
val tinduct = map remove_domain_condition simple_pinducts
- val thy = fold2 (add_simps "simps" [RecfunCodegen.add NONE]) (parts ~~ tsimps) (names ~~ atts) thy
+ val thy = fold2 (add_simps "simps" [(*RecfunCodegen.add NONE*)]) (parts ~~ tsimps) (names ~~ atts) thy
val thy = Theory.add_path name thy
--- a/src/HOL/Tools/function_package/fundef_proof.ML Tue Jun 06 08:21:14 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_proof.ML Tue Jun 06 09:28:24 2006 +0200
@@ -347,7 +347,9 @@
let
val Names {z, R, acc_R, ...} = names
val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
- val goal = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
+ val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> cterm_of thy
in
Goal.init goal
|> (SINGLE (resolve_tac [accI] 1)) |> the
--- a/src/HOL/Tools/function_package/mutual.ML Tue Jun 06 08:21:14 2006 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML Tue Jun 06 09:28:24 2006 +0200
@@ -150,11 +150,13 @@
fun recover_mutual_psimp thy RST streeR all_f_defs (MutualPart {f_def, pthR, ...}) (_,_,args,_) sum_psimp =
let
- val [accCond] = cprems_of sum_psimp
- val plain_eq = implies_elim sum_psimp (assume accCond)
+ val conds = cprems_of sum_psimp (* dom-condition and guards *)
+ val plain_eq = sum_psimp
+ |> fold (implies_elim_swp o assume) conds
+
val x = Free ("x", RST)
- val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) f_def
+ val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (freezeT f_def) (* FIXME: freezeT *)
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))
@@ -163,7 +165,7 @@
|> 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)
- |> implies_intr accCond
+ |> fold_rev implies_intr conds
end
--- a/src/HOL/ex/Fundefs.thy Tue Jun 06 08:21:14 2006 +0200
+++ b/src/HOL/ex/Fundefs.thy Tue Jun 06 09:28:24 2006 +0200
@@ -105,6 +105,8 @@
section {* More general patterns *}
+subsection {* Overlapping patterns *}
+
text {* Currently, patterns must always be compatible with each other, since
no automatich splitting takes place. But the following definition of
gcd is ok, although patterns overlap: *}
@@ -123,6 +125,27 @@
thm gcd2.induct
+subsection {* Guards *}
+
+text {* We can reformulate the above example using guarded patterns *}
+
+consts gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+function
+ "gcd3 x 0 = x"
+ "gcd3 0 y = y"
+ "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
+ "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
+ apply (cases xa, case_tac a, auto)
+ apply (case_tac b, auto)
+ done
+termination
+ by (auto_term "measure (\<lambda>(x,y). x + y)")
+
+thm gcd3.simps
+thm gcd3.induct
+
+
+
text {* General patterns allow even strange definitions: *}
consts ev :: "nat \<Rightarrow> bool"
function