src/HOL/Tools/function_package/fundef_package.ML
changeset 20270 3abe7dae681e
parent 19938 241a7777a3ff
child 20285 23f5cd23c1e1
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 31 18:05:40 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 31 18:07:42 2006 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  (*  Title:      HOL/Tools/function_package/fundef_package.ML
     1.6      ID:         $Id$
     1.7      Author:     Alexander Krauss, TU Muenchen
     1.8 @@ -9,7 +10,7 @@
     1.9  
    1.10  signature FUNDEF_PACKAGE = 
    1.11  sig
    1.12 -    val add_fundef : ((bstring * Attrib.src list) * string) list list -> theory -> Proof.state (* Need an _i variant *)
    1.13 +    val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
    1.14  
    1.15      val cong_add: attribute
    1.16      val cong_del: attribute
    1.17 @@ -27,17 +28,20 @@
    1.18  val True_implies = thm "True_implies"
    1.19  
    1.20  
    1.21 -fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) (names, attss) thy =
    1.22 +fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
    1.23      let 
    1.24 +      val psimpss = Library.unflat (map snd spec_part) psimps
    1.25 +      val (names, attss) = split_list (map fst spec_part) 
    1.26 +
    1.27        val thy = thy |> Theory.add_path f_name 
    1.28                  
    1.29        val thy = thy |> Theory.add_path label
    1.30 -      val spsimps = map standard psimps
    1.31 -      val add_list = (names ~~ spsimps) ~~ attss
    1.32 -      val (_, thy) = PureThy.add_thms add_list thy
    1.33 +      val spsimpss = map (map standard) psimpss (* FIXME *)
    1.34 +      val add_list = (names ~~ spsimpss) ~~ attss
    1.35 +      val (_, thy) = PureThy.add_thmss add_list thy
    1.36        val thy = thy |> Theory.parent_path
    1.37                  
    1.38 -      val (_, thy) = PureThy.add_thmss [((label, spsimps), Simplifier.simp_add :: moreatts)] thy
    1.39 +      val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
    1.40        val thy = thy |> Theory.parent_path
    1.41      in
    1.42        thy
    1.43 @@ -48,7 +52,7 @@
    1.44  
    1.45  
    1.46  
    1.47 -fun fundef_afterqed congs mutual_info name data names atts [[result]] thy =
    1.48 +fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
    1.49      let
    1.50  	val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
    1.51  	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.52 @@ -58,44 +62,43 @@
    1.53  	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    1.54  	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    1.55  
    1.56 -        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy
    1.57 +        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy
    1.58 +
    1.59 +        val casenames = flat (map (map (fst o fst)) spec)
    1.60  
    1.61  	val thy = thy |> Theory.add_path name
    1.62 -	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names (flat names)])] thy
    1.63 +	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
    1.64  	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    1.65  	val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
    1.66 -	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy
    1.67 +	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
    1.68  	val thy = thy |> Theory.parent_path
    1.69      in
    1.70 -	add_fundef_data name (fundef_data, mutual_info, names, atts) thy
    1.71 +      add_fundef_data name (fundef_data, mutual_info, spec) thy
    1.72      end
    1.73  
    1.74 -fun gen_add_fundef prep_att eqns_attss thy =
    1.75 +fun gen_add_fundef prep_att eqns_attss preprocess thy =
    1.76      let
    1.77 -	fun split eqns_atts =
    1.78 -	    let 
    1.79 -		val (natts, eqns) = split_list eqns_atts
    1.80 -		val (names, raw_atts) = split_list natts
    1.81 -		val atts = map (map (prep_att thy)) raw_atts
    1.82 -	    in
    1.83 -		((names, atts), eqns)
    1.84 -	    end
    1.85 -
    1.86 +      fun prep_eqns neqs =
    1.87 +          neqs
    1.88 +            |> map (apsnd (Sign.read_prop thy))    
    1.89 +            |> map (apfst (apsnd (apfst (map (prep_att thy)))))
    1.90 +            |> FundefSplit.split_some_equations (ProofContext.init thy)
    1.91 +      
    1.92 +      val spec = map prep_eqns eqns_attss
    1.93 +      val t_eqnss = map (flat o map snd) spec
    1.94  
    1.95 -	val (natts, eqns) = split_list (map split_list eqns_attss)
    1.96 -	val (names, raw_atts) = split_list (map split_list natts)
    1.97 -
    1.98 -	val atts = map (map (map (prep_att thy))) raw_atts
    1.99 +(*
   1.100 + val t_eqns = if preprocess then map (FundefSplit.split_all_equations (ProofContext.init thy)) t_eqns
   1.101 +              else t_eqns
   1.102 +*)
   1.103  
   1.104 -	val congs = get_fundef_congs (Context.Theory thy)
   1.105 +      val congs = get_fundef_congs (Context.Theory thy)
   1.106  
   1.107 -	val t_eqns = map (map (Sign.read_prop thy)) eqns
   1.108 -
   1.109 -	val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
   1.110 -	val Prep {goal, goalI, ...} = data
   1.111 +      val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
   1.112 +      val Prep {goal, goalI, ...} = data
   1.113      in
   1.114  	thy |> ProofContext.init
   1.115 -	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data names atts) NONE ("", [])
   1.116 +	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data spec) NONE ("", [])
   1.117  	    [(("", []), [(goal, [])])]
   1.118              |> Proof.refine (Method.primitive_text (fn _ => goalI))
   1.119              |> Seq.hd
   1.120 @@ -106,7 +109,7 @@
   1.121      let
   1.122  	val totality = hd (hd thmss)
   1.123  
   1.124 -	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, names, atts)
   1.125 +	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
   1.126  	  = the (get_fundef_data name thy)
   1.127  
   1.128  	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
   1.129 @@ -117,7 +120,7 @@
   1.130          val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
   1.131          val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
   1.132  
   1.133 -        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) (names ~~ atts) thy
   1.134 +        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
   1.135  
   1.136  	val thy = Theory.add_path name thy
   1.137  		  
   1.138 @@ -161,7 +164,7 @@
   1.139  	val data = the (get_fundef_data name thy)
   1.140                     handle Option.Option => raise ERROR ("No such function definition: " ^ name)
   1.141  
   1.142 -	val (res as FundefMResult {termination, ...}, mutual, _, _) = data
   1.143 +	val (res as FundefMResult {termination, ...}, mutual, _) = data
   1.144  	val goal = FundefTermination.mk_total_termination_goal data
   1.145      in
   1.146  	thy |> ProofContext.init
   1.147 @@ -206,13 +209,29 @@
   1.148  
   1.149  local structure P = OuterParse and K = OuterKeyword in
   1.150  
   1.151 +
   1.152 +
   1.153 +val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
   1.154 +
   1.155 +
   1.156 +val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME)) 
   1.157 +                                               >> (fn x => (map_filter I x, exists is_none x)))
   1.158 +                              --| P.$$$ "]";
   1.159 +
   1.160 +val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
   1.161 +
   1.162 +fun opt_thm_name_star s =
   1.163 +  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ s) ("", ([], false));
   1.164 +
   1.165 +
   1.166  val function_decl =
   1.167 -    Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   1.168 +    Scan.repeat1 (opt_thm_name_star ":" -- P.prop);
   1.169  
   1.170  val functionP =
   1.171    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   1.172 -    (P.and_list1 function_decl >> (fn eqnss =>
   1.173 -      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss)));
   1.174 +  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "pre" -- P.$$$ ")") >> K true) false) --    
   1.175 +  P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
   1.176 +                                    Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
   1.177  
   1.178  val terminationP =
   1.179    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal