# HG changeset patch
# User krauss
# Date 1154362062 -7200
# Node ID 3abe7dae681e934b6e41ea438cec974b0949ba49
# Parent  c40070317ab81e6a19400a04004f801edd4d0f2e
Function package can now do automatic splits of overlapping datatype patterns

diff -r c40070317ab8 -r 3abe7dae681e src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Mon Jul 31 18:05:40 2006 +0200
+++ b/src/HOL/FunDef.thy	Mon Jul 31 18:07:42 2006 +0200
@@ -9,6 +9,7 @@
 ("Tools/function_package/fundef_proof.ML")
 ("Tools/function_package/termination.ML")
 ("Tools/function_package/mutual.ML")
+("Tools/function_package/pattern_split.ML")
 ("Tools/function_package/fundef_package.ML")
 ("Tools/function_package/fundef_datatype.ML")
 ("Tools/function_package/auto_term.ML")
@@ -71,6 +72,7 @@
 use "Tools/function_package/fundef_proof.ML"
 use "Tools/function_package/termination.ML"
 use "Tools/function_package/mutual.ML"
+use "Tools/function_package/pattern_split.ML"
 use "Tools/function_package/fundef_package.ML"
 
 setup FundefPackage.setup
diff -r c40070317ab8 -r 3abe7dae681e src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Jul 31 18:05:40 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Jul 31 18:07:42 2006 +0200
@@ -150,7 +150,8 @@
      }
 
 
-type result_with_names = fundef_mresult * mutual_info * string list list * attribute list list list
+type fundef_spec = ((string * attribute list) * term list) list list
+type result_with_names = fundef_mresult * mutual_info * fundef_spec
 
 structure FundefData = TheoryDataFun
 (struct
diff -r c40070317ab8 -r 3abe7dae681e src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 31 18:05:40 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 31 18:07:42 2006 +0200
@@ -1,3 +1,4 @@
+
 (*  Title:      HOL/Tools/function_package/fundef_package.ML
     ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
@@ -9,7 +10,7 @@
 
 signature FUNDEF_PACKAGE = 
 sig
-    val add_fundef : ((bstring * Attrib.src list) * string) list list -> theory -> Proof.state (* Need an _i variant *)
+    val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
 
     val cong_add: attribute
     val cong_del: attribute
@@ -27,17 +28,20 @@
 val True_implies = thm "True_implies"
 
 
-fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) (names, attss) thy =
+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) 
+
       val thy = thy |> Theory.add_path f_name 
                 
       val thy = thy |> Theory.add_path label
-      val spsimps = map standard psimps
-      val add_list = (names ~~ spsimps) ~~ attss
-      val (_, thy) = PureThy.add_thms add_list thy
+      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, spsimps), Simplifier.simp_add :: moreatts)] thy
+      val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
       val thy = thy |> Theory.parent_path
     in
       thy
@@ -48,7 +52,7 @@
 
 
 
-fun fundef_afterqed congs mutual_info name data names atts [[result]] thy =
+fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
     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
@@ -58,44 +62,43 @@
 	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) (names ~~ atts) 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 (flat names)])] thy
+	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 (flat names), InductAttrib.induct_set ""])] 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
     in
-	add_fundef_data name (fundef_data, mutual_info, names, atts) thy
+      add_fundef_data name (fundef_data, mutual_info, spec) thy
     end
 
-fun gen_add_fundef prep_att eqns_attss thy =
+fun gen_add_fundef prep_att eqns_attss preprocess thy =
     let
-	fun split eqns_atts =
-	    let 
-		val (natts, eqns) = split_list eqns_atts
-		val (names, raw_atts) = split_list natts
-		val atts = map (map (prep_att thy)) raw_atts
-	    in
-		((names, atts), eqns)
-	    end
-
+      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 (natts, eqns) = split_list (map split_list eqns_attss)
-	val (names, raw_atts) = split_list (map split_list natts)
-
-	val atts = map (map (map (prep_att thy))) raw_atts
+(*
+ val t_eqns = if preprocess then map (FundefSplit.split_all_equations (ProofContext.init thy)) t_eqns
+              else t_eqns
+*)
 
-	val congs = get_fundef_congs (Context.Theory thy)
+      val congs = get_fundef_congs (Context.Theory thy)
 
-	val t_eqns = map (map (Sign.read_prop thy)) eqns
-
-	val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
-	val Prep {goal, goalI, ...} = data
+      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 (fundef_afterqed congs mutual_info name data names atts) NONE ("", [])
+	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data spec) NONE ("", [])
 	    [(("", []), [(goal, [])])]
             |> Proof.refine (Method.primitive_text (fn _ => goalI))
             |> Seq.hd
@@ -106,7 +109,7 @@
     let
 	val totality = hd (hd thmss)
 
-	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, names, atts)
+	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
 	  = the (get_fundef_data name thy)
 
 	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
@@ -117,7 +120,7 @@
         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) (names ~~ atts) thy
+        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
 
 	val thy = Theory.add_path name thy
 		  
@@ -161,7 +164,7 @@
 	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 (res as FundefMResult {termination, ...}, mutual, _) = data
 	val goal = FundefTermination.mk_total_termination_goal data
     in
 	thy |> ProofContext.init
@@ -206,13 +209,29 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+
+
+val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
+
+
+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);
+
+fun opt_thm_name_star s =
+  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ s) ("", ([], false));
+
+
 val function_decl =
-    Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
+    Scan.repeat1 (opt_thm_name_star ":" -- P.prop);
 
 val functionP =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
-    (P.and_list1 function_decl >> (fn eqnss =>
-      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss)));
+  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "pre" -- P.$$$ ")") >> K true) false) --    
+  P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
+                                    Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
 
 val terminationP =
   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
diff -r c40070317ab8 -r 3abe7dae681e src/HOL/Tools/function_package/pattern_split.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Mon Jul 31 18:07:42 2006 +0200
@@ -0,0 +1,133 @@
+(*  Title:      HOL/Tools/function_package/fundef_package.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+
+Automatic splitting of overlapping constructor patterns. This is a preprocessing step which 
+turns a specification with overlaps into an overlap-free specification.
+
+*)
+
+signature FUNDEF_SPLIT = 
+sig
+  val split_some_equations : ProofContext.context -> (('a * ('b * bool)) * Term.term) list 
+                             -> (('a * 'b) * Term.term list) list
+
+end
+
+structure FundefSplit : FUNDEF_SPLIT = 
+struct
+
+
+(* We use proof context for the variable management *)
+(* FIXME: no __ *)
+
+fun new_var ctx vs T = 
+    let 
+      val [v] = Variable.variant_frees ctx vs [("v", T)]
+    in
+      (Free v :: vs, Free v)
+    end
+
+fun saturate ctx vs t =
+    fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t))
+         (binder_types (fastype_of t)) (vs, t)
+
+
+(* This is copied from "fundef_datatype.ML" *)
+fun inst_constrs_of thy (T as Type (name, _)) =
+	map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+	    (the (DatatypePackage.get_datatype_constrs thy name))
+  | inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
+
+
+
+fun pattern_subtract_subst ctx vs _ (Free v2) = []
+  | pattern_subtract_subst ctx vs (v as (Free (_, T))) t' =
+    let 
+      fun foo constr = 
+          let 
+            val (vs', t) = saturate ctx vs constr
+            val substs = pattern_subtract_subst ctx vs' t t'
+          in
+            map (cons (v, t)) substs
+          end
+    in
+      flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
+    end
+  | pattern_subtract_subst ctx vs t t' =
+    let
+      val (C, ps) = strip_comb t
+      val (C', qs) = strip_comb t'
+    in
+      if C = C'
+      then flat (map2 (pattern_subtract_subst ctx vs) ps qs)
+      else [[]]
+    end
+
+fun pattern_subtract_parallel ctx vs ps qs =
+    flat (map2 (pattern_subtract_subst ctx vs) ps qs)
+
+
+
+(* ps - qs *)
+fun pattern_subtract ctx eq2 eq1 =
+    let
+      val _ $ (_ $ lhs1 $ _) = eq1
+      val _ $ (_ $ lhs2 $ _) = eq2
+
+      val thy = ProofContext.theory_of ctx
+      val vs = term_frees eq1
+    in
+      map (fn sigma => Pattern.rewrite_term thy sigma [] eq1) (pattern_subtract_subst ctx vs lhs1 lhs2)
+    end
+
+
+(* ps - p' *)
+fun pattern_subtract_from_many ctx p'=
+    flat o map (pattern_subtract ctx p')
+
+(* in reverse order *)
+fun pattern_subtract_many ctx ps' =
+    fold_rev (pattern_subtract_from_many ctx) ps'
+
+
+
+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 prevs [] = []
+        | 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
+    in
+      split_aux [] eqns
+    end
+
+
+
+
+
+
+end
+
+
+
+
+
+
+
+
+
+
diff -r c40070317ab8 -r 3abe7dae681e src/HOL/Tools/function_package/termination.ML
--- a/src/HOL/Tools/function_package/termination.ML	Mon Jul 31 18:05:40 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML	Mon Jul 31 18:07:42 2006 +0200
@@ -20,7 +20,7 @@
 open FundefCommon
 open FundefAbbrev
 
-fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _, _) =
+fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
     let
 	val domT = domain_type (fastype_of f)
 	val x = Free ("x", domT)
@@ -28,7 +28,7 @@
 	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 =
+fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
     let
 	val domT = domain_type (fastype_of f)
 	val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
diff -r c40070317ab8 -r 3abe7dae681e src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Mon Jul 31 18:05:40 2006 +0200
+++ b/src/HOL/ex/Fundefs.thy	Mon Jul 31 18:07:42 2006 +0200
@@ -92,13 +92,11 @@
   show "wf ?R" ..
 
   fix n::nat assume "~ 100 < n" (* Inner call *)
-  thus "(n + 11, n) : ?R"
-    by simp arith
+  thus "(n + 11, n) : ?R" by simp 
 
   assume inner_trm: "n + 11 : f91_dom" (* Outer call *)
   with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
-  with `~ 100 < n` show "(f91 (n + 11), n) : ?R"
-    by simp arith
+  with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp 
 qed
 
 
@@ -108,7 +106,7 @@
 subsection {* Overlapping patterns *}
 
 text {* Currently, patterns must always be compatible with each other, since
-no automatich splitting takes place. But the following definition of
+no automatic splitting takes place. But the following definition of
 gcd is ok, although patterns overlap: *}
 
 consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"