Function package can now do automatic splits of overlapping datatype patterns
authorkrauss
Mon Jul 31 18:07:42 2006 +0200 (2006-07-31)
changeset 202703abe7dae681e
parent 20269 c40070317ab8
child 20271 e76e77e0d615
Function package can now do automatic splits of overlapping datatype patterns
src/HOL/FunDef.thy
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/pattern_split.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/ex/Fundefs.thy
     1.1 --- a/src/HOL/FunDef.thy	Mon Jul 31 18:05:40 2006 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Mon Jul 31 18:07:42 2006 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  ("Tools/function_package/fundef_proof.ML")
     1.5  ("Tools/function_package/termination.ML")
     1.6  ("Tools/function_package/mutual.ML")
     1.7 +("Tools/function_package/pattern_split.ML")
     1.8  ("Tools/function_package/fundef_package.ML")
     1.9  ("Tools/function_package/fundef_datatype.ML")
    1.10  ("Tools/function_package/auto_term.ML")
    1.11 @@ -71,6 +72,7 @@
    1.12  use "Tools/function_package/fundef_proof.ML"
    1.13  use "Tools/function_package/termination.ML"
    1.14  use "Tools/function_package/mutual.ML"
    1.15 +use "Tools/function_package/pattern_split.ML"
    1.16  use "Tools/function_package/fundef_package.ML"
    1.17  
    1.18  setup FundefPackage.setup
     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Jul 31 18:05:40 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Jul 31 18:07:42 2006 +0200
     2.3 @@ -150,7 +150,8 @@
     2.4       }
     2.5  
     2.6  
     2.7 -type result_with_names = fundef_mresult * mutual_info * string list list * attribute list list list
     2.8 +type fundef_spec = ((string * attribute list) * term list) list list
     2.9 +type result_with_names = fundef_mresult * mutual_info * fundef_spec
    2.10  
    2.11  structure FundefData = TheoryDataFun
    2.12  (struct
     3.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 31 18:05:40 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 31 18:07:42 2006 +0200
     3.3 @@ -1,3 +1,4 @@
     3.4 +
     3.5  (*  Title:      HOL/Tools/function_package/fundef_package.ML
     3.6      ID:         $Id$
     3.7      Author:     Alexander Krauss, TU Muenchen
     3.8 @@ -9,7 +10,7 @@
     3.9  
    3.10  signature FUNDEF_PACKAGE = 
    3.11  sig
    3.12 -    val add_fundef : ((bstring * Attrib.src list) * string) list list -> theory -> Proof.state (* Need an _i variant *)
    3.13 +    val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
    3.14  
    3.15      val cong_add: attribute
    3.16      val cong_del: attribute
    3.17 @@ -27,17 +28,20 @@
    3.18  val True_implies = thm "True_implies"
    3.19  
    3.20  
    3.21 -fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) (names, attss) thy =
    3.22 +fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
    3.23      let 
    3.24 +      val psimpss = Library.unflat (map snd spec_part) psimps
    3.25 +      val (names, attss) = split_list (map fst spec_part) 
    3.26 +
    3.27        val thy = thy |> Theory.add_path f_name 
    3.28                  
    3.29        val thy = thy |> Theory.add_path label
    3.30 -      val spsimps = map standard psimps
    3.31 -      val add_list = (names ~~ spsimps) ~~ attss
    3.32 -      val (_, thy) = PureThy.add_thms add_list thy
    3.33 +      val spsimpss = map (map standard) psimpss (* FIXME *)
    3.34 +      val add_list = (names ~~ spsimpss) ~~ attss
    3.35 +      val (_, thy) = PureThy.add_thmss add_list thy
    3.36        val thy = thy |> Theory.parent_path
    3.37                  
    3.38 -      val (_, thy) = PureThy.add_thmss [((label, spsimps), Simplifier.simp_add :: moreatts)] thy
    3.39 +      val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
    3.40        val thy = thy |> Theory.parent_path
    3.41      in
    3.42        thy
    3.43 @@ -48,7 +52,7 @@
    3.44  
    3.45  
    3.46  
    3.47 -fun fundef_afterqed congs mutual_info name data names atts [[result]] thy =
    3.48 +fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
    3.49      let
    3.50  	val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
    3.51  	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    3.52 @@ -58,44 +62,43 @@
    3.53  	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    3.54  	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    3.55  
    3.56 -        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy
    3.57 +        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy
    3.58 +
    3.59 +        val casenames = flat (map (map (fst o fst)) spec)
    3.60  
    3.61  	val thy = thy |> Theory.add_path name
    3.62 -	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names (flat names)])] thy
    3.63 +	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
    3.64  	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    3.65  	val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
    3.66 -	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy
    3.67 +	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
    3.68  	val thy = thy |> Theory.parent_path
    3.69      in
    3.70 -	add_fundef_data name (fundef_data, mutual_info, names, atts) thy
    3.71 +      add_fundef_data name (fundef_data, mutual_info, spec) thy
    3.72      end
    3.73  
    3.74 -fun gen_add_fundef prep_att eqns_attss thy =
    3.75 +fun gen_add_fundef prep_att eqns_attss preprocess thy =
    3.76      let
    3.77 -	fun split eqns_atts =
    3.78 -	    let 
    3.79 -		val (natts, eqns) = split_list eqns_atts
    3.80 -		val (names, raw_atts) = split_list natts
    3.81 -		val atts = map (map (prep_att thy)) raw_atts
    3.82 -	    in
    3.83 -		((names, atts), eqns)
    3.84 -	    end
    3.85 -
    3.86 +      fun prep_eqns neqs =
    3.87 +          neqs
    3.88 +            |> map (apsnd (Sign.read_prop thy))    
    3.89 +            |> map (apfst (apsnd (apfst (map (prep_att thy)))))
    3.90 +            |> FundefSplit.split_some_equations (ProofContext.init thy)
    3.91 +      
    3.92 +      val spec = map prep_eqns eqns_attss
    3.93 +      val t_eqnss = map (flat o map snd) spec
    3.94  
    3.95 -	val (natts, eqns) = split_list (map split_list eqns_attss)
    3.96 -	val (names, raw_atts) = split_list (map split_list natts)
    3.97 -
    3.98 -	val atts = map (map (map (prep_att thy))) raw_atts
    3.99 +(*
   3.100 + val t_eqns = if preprocess then map (FundefSplit.split_all_equations (ProofContext.init thy)) t_eqns
   3.101 +              else t_eqns
   3.102 +*)
   3.103  
   3.104 -	val congs = get_fundef_congs (Context.Theory thy)
   3.105 +      val congs = get_fundef_congs (Context.Theory thy)
   3.106  
   3.107 -	val t_eqns = map (map (Sign.read_prop thy)) eqns
   3.108 -
   3.109 -	val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
   3.110 -	val Prep {goal, goalI, ...} = data
   3.111 +      val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
   3.112 +      val Prep {goal, goalI, ...} = data
   3.113      in
   3.114  	thy |> ProofContext.init
   3.115 -	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data names atts) NONE ("", [])
   3.116 +	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data spec) NONE ("", [])
   3.117  	    [(("", []), [(goal, [])])]
   3.118              |> Proof.refine (Method.primitive_text (fn _ => goalI))
   3.119              |> Seq.hd
   3.120 @@ -106,7 +109,7 @@
   3.121      let
   3.122  	val totality = hd (hd thmss)
   3.123  
   3.124 -	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, names, atts)
   3.125 +	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
   3.126  	  = the (get_fundef_data name thy)
   3.127  
   3.128  	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
   3.129 @@ -117,7 +120,7 @@
   3.130          val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
   3.131          val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
   3.132  
   3.133 -        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) (names ~~ atts) thy
   3.134 +        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
   3.135  
   3.136  	val thy = Theory.add_path name thy
   3.137  		  
   3.138 @@ -161,7 +164,7 @@
   3.139  	val data = the (get_fundef_data name thy)
   3.140                     handle Option.Option => raise ERROR ("No such function definition: " ^ name)
   3.141  
   3.142 -	val (res as FundefMResult {termination, ...}, mutual, _, _) = data
   3.143 +	val (res as FundefMResult {termination, ...}, mutual, _) = data
   3.144  	val goal = FundefTermination.mk_total_termination_goal data
   3.145      in
   3.146  	thy |> ProofContext.init
   3.147 @@ -206,13 +209,29 @@
   3.148  
   3.149  local structure P = OuterParse and K = OuterKeyword in
   3.150  
   3.151 +
   3.152 +
   3.153 +val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
   3.154 +
   3.155 +
   3.156 +val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME)) 
   3.157 +                                               >> (fn x => (map_filter I x, exists is_none x)))
   3.158 +                              --| P.$$$ "]";
   3.159 +
   3.160 +val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
   3.161 +
   3.162 +fun opt_thm_name_star s =
   3.163 +  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ s) ("", ([], false));
   3.164 +
   3.165 +
   3.166  val function_decl =
   3.167 -    Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   3.168 +    Scan.repeat1 (opt_thm_name_star ":" -- P.prop);
   3.169  
   3.170  val functionP =
   3.171    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   3.172 -    (P.and_list1 function_decl >> (fn eqnss =>
   3.173 -      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss)));
   3.174 +  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "pre" -- P.$$$ ")") >> K true) false) --    
   3.175 +  P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
   3.176 +                                    Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
   3.177  
   3.178  val terminationP =
   3.179    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Mon Jul 31 18:07:42 2006 +0200
     4.3 @@ -0,0 +1,133 @@
     4.4 +(*  Title:      HOL/Tools/function_package/fundef_package.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Alexander Krauss, TU Muenchen
     4.7 +
     4.8 +A package for general recursive function definitions. 
     4.9 +
    4.10 +Automatic splitting of overlapping constructor patterns. This is a preprocessing step which 
    4.11 +turns a specification with overlaps into an overlap-free specification.
    4.12 +
    4.13 +*)
    4.14 +
    4.15 +signature FUNDEF_SPLIT = 
    4.16 +sig
    4.17 +  val split_some_equations : ProofContext.context -> (('a * ('b * bool)) * Term.term) list 
    4.18 +                             -> (('a * 'b) * Term.term list) list
    4.19 +
    4.20 +end
    4.21 +
    4.22 +structure FundefSplit : FUNDEF_SPLIT = 
    4.23 +struct
    4.24 +
    4.25 +
    4.26 +(* We use proof context for the variable management *)
    4.27 +(* FIXME: no __ *)
    4.28 +
    4.29 +fun new_var ctx vs T = 
    4.30 +    let 
    4.31 +      val [v] = Variable.variant_frees ctx vs [("v", T)]
    4.32 +    in
    4.33 +      (Free v :: vs, Free v)
    4.34 +    end
    4.35 +
    4.36 +fun saturate ctx vs t =
    4.37 +    fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t))
    4.38 +         (binder_types (fastype_of t)) (vs, t)
    4.39 +
    4.40 +
    4.41 +(* This is copied from "fundef_datatype.ML" *)
    4.42 +fun inst_constrs_of thy (T as Type (name, _)) =
    4.43 +	map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    4.44 +	    (the (DatatypePackage.get_datatype_constrs thy name))
    4.45 +  | inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
    4.46 +
    4.47 +
    4.48 +
    4.49 +fun pattern_subtract_subst ctx vs _ (Free v2) = []
    4.50 +  | pattern_subtract_subst ctx vs (v as (Free (_, T))) t' =
    4.51 +    let 
    4.52 +      fun foo constr = 
    4.53 +          let 
    4.54 +            val (vs', t) = saturate ctx vs constr
    4.55 +            val substs = pattern_subtract_subst ctx vs' t t'
    4.56 +          in
    4.57 +            map (cons (v, t)) substs
    4.58 +          end
    4.59 +    in
    4.60 +      flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
    4.61 +    end
    4.62 +  | pattern_subtract_subst ctx vs t t' =
    4.63 +    let
    4.64 +      val (C, ps) = strip_comb t
    4.65 +      val (C', qs) = strip_comb t'
    4.66 +    in
    4.67 +      if C = C'
    4.68 +      then flat (map2 (pattern_subtract_subst ctx vs) ps qs)
    4.69 +      else [[]]
    4.70 +    end
    4.71 +
    4.72 +fun pattern_subtract_parallel ctx vs ps qs =
    4.73 +    flat (map2 (pattern_subtract_subst ctx vs) ps qs)
    4.74 +
    4.75 +
    4.76 +
    4.77 +(* ps - qs *)
    4.78 +fun pattern_subtract ctx eq2 eq1 =
    4.79 +    let
    4.80 +      val _ $ (_ $ lhs1 $ _) = eq1
    4.81 +      val _ $ (_ $ lhs2 $ _) = eq2
    4.82 +
    4.83 +      val thy = ProofContext.theory_of ctx
    4.84 +      val vs = term_frees eq1
    4.85 +    in
    4.86 +      map (fn sigma => Pattern.rewrite_term thy sigma [] eq1) (pattern_subtract_subst ctx vs lhs1 lhs2)
    4.87 +    end
    4.88 +
    4.89 +
    4.90 +(* ps - p' *)
    4.91 +fun pattern_subtract_from_many ctx p'=
    4.92 +    flat o map (pattern_subtract ctx p')
    4.93 +
    4.94 +(* in reverse order *)
    4.95 +fun pattern_subtract_many ctx ps' =
    4.96 +    fold_rev (pattern_subtract_from_many ctx) ps'
    4.97 +
    4.98 +
    4.99 +
   4.100 +fun split_all_equations ctx eqns =
   4.101 +    let 
   4.102 +      fun split_aux prev [] = []
   4.103 +        | split_aux prev (e::es) = pattern_subtract_many ctx prev [e] @ split_aux (e::prev) es
   4.104 +    in
   4.105 +      split_aux [] eqns
   4.106 +end
   4.107 +
   4.108 +
   4.109 +
   4.110 +fun split_some_equations ctx eqns =
   4.111 +    let
   4.112 +      fun split_aux prevs [] = []
   4.113 +        | split_aux prev (((n, (att, true)), eq) :: es) = ((n, att), pattern_subtract_many ctx prev [eq])
   4.114 +                                                          :: split_aux (eq :: prev) es
   4.115 +        | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq]) 
   4.116 +                                                                :: split_aux (eq :: prev) es
   4.117 +    in
   4.118 +      split_aux [] eqns
   4.119 +    end
   4.120 +
   4.121 +
   4.122 +
   4.123 +
   4.124 +
   4.125 +
   4.126 +end
   4.127 +
   4.128 +
   4.129 +
   4.130 +
   4.131 +
   4.132 +
   4.133 +
   4.134 +
   4.135 +
   4.136 +
     5.1 --- a/src/HOL/Tools/function_package/termination.ML	Mon Jul 31 18:05:40 2006 +0200
     5.2 +++ b/src/HOL/Tools/function_package/termination.ML	Mon Jul 31 18:07:42 2006 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4  open FundefCommon
     5.5  open FundefAbbrev
     5.6  
     5.7 -fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _, _) =
     5.8 +fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
     5.9      let
    5.10  	val domT = domain_type (fastype_of f)
    5.11  	val x = Free ("x", domT)
    5.12 @@ -28,7 +28,7 @@
    5.13  	Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
    5.14      end
    5.15  
    5.16 -fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom =
    5.17 +fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
    5.18      let
    5.19  	val domT = domain_type (fastype_of f)
    5.20  	val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
     6.1 --- a/src/HOL/ex/Fundefs.thy	Mon Jul 31 18:05:40 2006 +0200
     6.2 +++ b/src/HOL/ex/Fundefs.thy	Mon Jul 31 18:07:42 2006 +0200
     6.3 @@ -92,13 +92,11 @@
     6.4    show "wf ?R" ..
     6.5  
     6.6    fix n::nat assume "~ 100 < n" (* Inner call *)
     6.7 -  thus "(n + 11, n) : ?R"
     6.8 -    by simp arith
     6.9 +  thus "(n + 11, n) : ?R" by simp 
    6.10  
    6.11    assume inner_trm: "n + 11 : f91_dom" (* Outer call *)
    6.12    with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
    6.13 -  with `~ 100 < n` show "(f91 (n + 11), n) : ?R"
    6.14 -    by simp arith
    6.15 +  with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp 
    6.16  qed
    6.17  
    6.18  
    6.19 @@ -108,7 +106,7 @@
    6.20  subsection {* Overlapping patterns *}
    6.21  
    6.22  text {* Currently, patterns must always be compatible with each other, since
    6.23 -no automatich splitting takes place. But the following definition of
    6.24 +no automatic splitting takes place. But the following definition of
    6.25  gcd is ok, although patterns overlap: *}
    6.26  
    6.27  consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"