# HG changeset patch
# User krauss
# Date 1149578904 -7200
# Node ID 48c4632e2c2841fed8a02e1b348376626d8aae6c
# Parent  c62720b20e9afe3e5659919fa3f59f1235b3116e
HOL/Tools/function_package: imporoved handling of guards, added an example

diff -r c62720b20e9a -r 48c4632e2c28 src/HOL/Tools/function_package/fundef_package.ML
--- 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
 		  
diff -r c62720b20e9a -r 48c4632e2c28 src/HOL/Tools/function_package/fundef_proof.ML
--- 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
diff -r c62720b20e9a -r 48c4632e2c28 src/HOL/Tools/function_package/mutual.ML
--- 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
 
 
diff -r c62720b20e9a -r 48c4632e2c28 src/HOL/ex/Fundefs.thy
--- 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