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