1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 06 08:21:14 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 06 09:28:24 2006 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4  	val tsimps = map (map remove_domain_condition) psimps
     1.5  	val tinduct = map remove_domain_condition simple_pinducts
     1.6  
     1.7 -        val thy = fold2 (add_simps "simps" [RecfunCodegen.add NONE]) (parts ~~ tsimps) (names ~~ atts) thy
     1.8 +        val thy = fold2 (add_simps "simps" [(*RecfunCodegen.add NONE*)]) (parts ~~ tsimps) (names ~~ atts) thy
     1.9  
    1.10  	val thy = Theory.add_path name thy
    1.11  		  

     2.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Tue Jun 06 08:21:14 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Tue Jun 06 09:28:24 2006 +0200
     2.3 @@ -347,7 +347,9 @@
     2.4      let
     2.5  	val Names {z, R, acc_R, ...} = names
     2.6  	val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
     2.7 -	val goal = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
     2.8 +	val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
     2.9 +                     |> fold_rev (curry Logic.mk_implies) gs
    2.10 +                     |> cterm_of thy
    2.11      in
    2.12  	Goal.init goal 
    2.13  		  |> (SINGLE (resolve_tac [accI] 1)) |> the

     3.1 --- a/src/HOL/Tools/function_package/mutual.ML	Tue Jun 06 08:21:14 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Tue Jun 06 09:28:24 2006 +0200
     3.3 @@ -150,11 +150,13 @@
     3.4  
     3.5  fun recover_mutual_psimp thy RST streeR all_f_defs (MutualPart {f_def, pthR, ...}) (_,_,args,_) sum_psimp =
     3.6      let
     3.7 -	val [accCond] = cprems_of sum_psimp
     3.8 -	val plain_eq = implies_elim sum_psimp (assume accCond)
     3.9 +	val conds = cprems_of sum_psimp (* dom-condition and guards *)
    3.10 +	val plain_eq = sum_psimp
    3.11 +                         |> fold (implies_elim_swp o assume) conds
    3.12 +
    3.13  	val x = Free ("x", RST)
    3.14  
    3.15 -	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) f_def
    3.16 +	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (freezeT f_def) (* FIXME: freezeT *)
    3.17      in
    3.18  	reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x)))  (*  PR(x) == PR(x) *)
    3.19  		  |> (fn it => combination it (plain_eq RS eq_reflection))
    3.20 @@ -163,7 +165,7 @@
    3.21  		  |> simplify (HOL_basic_ss addsimps [SumTools.projl_inl, SumTools.projr_inr]) (*  f ... == ... *)
    3.22  		  |> simplify (HOL_basic_ss addsimps all_f_defs) (*  f ... == ... *)
    3.23  		  |> (fn it => it RS meta_eq_to_obj_eq)
    3.24 -		  |> implies_intr accCond
    3.25 +		  |> fold_rev implies_intr conds
    3.26      end
    3.27  
    3.28  

     4.1 --- a/src/HOL/ex/Fundefs.thy	Tue Jun 06 08:21:14 2006 +0200
     4.2 +++ b/src/HOL/ex/Fundefs.thy	Tue Jun 06 09:28:24 2006 +0200
     4.3 @@ -105,6 +105,8 @@
     4.4  
     4.5  section {* More general patterns *}
     4.6  
     4.7 +subsection {* Overlapping patterns *}
     4.8 +
     4.9  text {* Currently, patterns must always be compatible with each other, since
    4.10  no automatich splitting takes place. But the following definition of
    4.11  gcd is ok, although patterns overlap: *}
    4.12 @@ -123,6 +125,27 @@
    4.13  thm gcd2.induct
    4.14  
    4.15  
    4.16 +subsection {* Guards *}
    4.17 +
    4.18 +text {* We can reformulate the above example using guarded patterns *}
    4.19 +
    4.20 +consts gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    4.21 +function
    4.22 +  "gcd3 x 0 = x"
    4.23 +  "gcd3 0 y = y"
    4.24 +  "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
    4.25 +  "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
    4.26 +  apply (cases xa, case_tac a, auto)
    4.27 +  apply (case_tac b, auto)
    4.28 +  done
    4.29 +termination 
    4.30 +  by (auto_term "measure (\<lambda>(x,y). x + y)")
    4.31 +
    4.32 +thm gcd3.simps
    4.33 +thm gcd3.induct
    4.34 +
    4.35 +
    4.36 +
    4.37  text {* General patterns allow even strange definitions: *}
    4.38  consts ev :: "nat \<Rightarrow> bool"
    4.39  function