src/HOL/Tools/Function/function_common.ML
changeset 34232 36a2a3029fd3
parent 34231 da4d7d40f2f9
child 36521 73ed9f18fdd3
     1.1 --- a/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4 -(*  Title:      HOL/Tools/Function/fundef_common.ML
     1.5 +(*  Title:      HOL/Tools/Function/function_common.ML
     1.6      Author:     Alexander Krauss, TU Muenchen
     1.7  
     1.8 -A package for general recursive function definitions. 
     1.9 +A package for general recursive function definitions.
    1.10  Common definitions and other infrastructure.
    1.11  *)
    1.12  
    1.13 @@ -21,8 +21,7 @@
    1.14    pinducts: thm list,
    1.15    simps : thm list option,
    1.16    inducts : thm list option,
    1.17 -  termination: thm
    1.18 - }  
    1.19 +  termination: thm}
    1.20  
    1.21  end
    1.22  
    1.23 @@ -42,8 +41,7 @@
    1.24    pinducts: thm list,
    1.25    simps : thm list option,
    1.26    inducts : thm list option,
    1.27 -  termination: thm
    1.28 - }  
    1.29 +  termination: thm}
    1.30  
    1.31  end
    1.32  
    1.33 @@ -62,7 +60,7 @@
    1.34  
    1.35  val acc_const_name = @{const_name accp}
    1.36  fun mk_acc domT R =
    1.37 -    Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
    1.38 +  Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
    1.39  
    1.40  val function_name = suffix "C"
    1.41  val graph_name = suffix "_graph"
    1.42 @@ -86,21 +84,18 @@
    1.43  
    1.44  (* Function definition result data *)
    1.45  
    1.46 -datatype function_result =
    1.47 -  FunctionResult of
    1.48 -     {
    1.49 -      fs: term list,
    1.50 -      G: term,
    1.51 -      R: term,
    1.52 +datatype function_result = FunctionResult of
    1.53 + {fs: term list,
    1.54 +  G: term,
    1.55 +  R: term,
    1.56  
    1.57 -      psimps : thm list, 
    1.58 -      trsimps : thm list option, 
    1.59 +  psimps : thm list,
    1.60 +  trsimps : thm list option,
    1.61  
    1.62 -      simple_pinducts : thm list, 
    1.63 -      cases : thm,
    1.64 -      termination : thm,
    1.65 -      domintros : thm list option
    1.66 -     }
    1.67 +  simple_pinducts : thm list,
    1.68 +  cases : thm,
    1.69 +  termination : thm,
    1.70 +  domintros : thm list option}
    1.71  
    1.72  fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
    1.73    simps, inducts, termination, defname, is_partial} : info) phi =
    1.74 @@ -109,7 +104,7 @@
    1.75        val name = Binding.name_of o Morphism.binding phi o Binding.name
    1.76      in
    1.77        { add_simps = add_simps, case_names = case_names,
    1.78 -        fs = map term fs, R = term R, psimps = fact psimps, 
    1.79 +        fs = map term fs, R = term R, psimps = fact psimps,
    1.80          pinducts = fact pinducts, simps = Option.map fact simps,
    1.81          inducts = Option.map fact inducts, termination = thm termination,
    1.82          defname = name defname, is_partial=is_partial }
    1.83 @@ -121,57 +116,56 @@
    1.84    val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
    1.85    val extend = I;
    1.86    fun merge tabs : T = Item_Net.merge tabs;
    1.87 -);
    1.88 +)
    1.89  
    1.90  val get_function = FunctionData.get o Context.Proof;
    1.91  
    1.92  
    1.93 -(* Generally useful?? *)
    1.94 -fun lift_morphism thy f = 
    1.95 -    let 
    1.96 -      val term = Drule.term_rule thy f
    1.97 -    in
    1.98 -      Morphism.thm_morphism f $> Morphism.term_morphism term 
    1.99 -       $> Morphism.typ_morphism (Logic.type_map term)
   1.100 -    end
   1.101 +fun lift_morphism thy f =
   1.102 +  let
   1.103 +    val term = Drule.term_rule thy f
   1.104 +  in
   1.105 +    Morphism.thm_morphism f $> Morphism.term_morphism term
   1.106 +    $> Morphism.typ_morphism (Logic.type_map term)
   1.107 +  end
   1.108  
   1.109  fun import_function_data t ctxt =
   1.110 -    let
   1.111 -      val thy = ProofContext.theory_of ctxt
   1.112 -      val ct = cterm_of thy t
   1.113 -      val inst_morph = lift_morphism thy o Thm.instantiate 
   1.114 +  let
   1.115 +    val thy = ProofContext.theory_of ctxt
   1.116 +    val ct = cterm_of thy t
   1.117 +    val inst_morph = lift_morphism thy o Thm.instantiate
   1.118  
   1.119 -      fun match (trm, data) = 
   1.120 -          SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
   1.121 -          handle Pattern.MATCH => NONE
   1.122 -    in 
   1.123 -      get_first match (Item_Net.retrieve (get_function ctxt) t)
   1.124 -    end
   1.125 +    fun match (trm, data) =
   1.126 +      SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
   1.127 +      handle Pattern.MATCH => NONE
   1.128 +  in
   1.129 +    get_first match (Item_Net.retrieve (get_function ctxt) t)
   1.130 +  end
   1.131  
   1.132  fun import_last_function ctxt =
   1.133 -    case Item_Net.content (get_function ctxt) of
   1.134 -      [] => NONE
   1.135 -    | (t, data) :: _ =>
   1.136 -      let 
   1.137 -        val ([t'], ctxt') = Variable.import_terms true [t] ctxt
   1.138 -      in
   1.139 -        import_function_data t' ctxt'
   1.140 -      end
   1.141 +  case Item_Net.content (get_function ctxt) of
   1.142 +    [] => NONE
   1.143 +  | (t, data) :: _ =>
   1.144 +    let
   1.145 +      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
   1.146 +    in
   1.147 +      import_function_data t' ctxt'
   1.148 +    end
   1.149  
   1.150  val all_function_data = Item_Net.content o get_function
   1.151  
   1.152  fun add_function_data (data : info as {fs, termination, ...}) =
   1.153 -    FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
   1.154 -    #> store_termination_rule termination
   1.155 +  FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
   1.156 +  #> store_termination_rule termination
   1.157  
   1.158  
   1.159  (* Simp rules for termination proofs *)
   1.160  
   1.161  structure Termination_Simps = Named_Thms
   1.162  (
   1.163 -  val name = "termination_simp" 
   1.164 +  val name = "termination_simp"
   1.165    val description = "Simplification rule for termination proofs"
   1.166 -);
   1.167 +)
   1.168  
   1.169  
   1.170  (* Default Termination Prover *)
   1.171 @@ -182,29 +176,26 @@
   1.172    val empty = (fn _ => error "Termination prover not configured")
   1.173    val extend = I
   1.174    fun merge (a, b) = b  (* FIXME ? *)
   1.175 -);
   1.176 +)
   1.177  
   1.178  val set_termination_prover = TerminationProver.put
   1.179  val get_termination_prover = TerminationProver.get o Context.Proof
   1.180  
   1.181  
   1.182  (* Configuration management *)
   1.183 -datatype function_opt 
   1.184 +datatype function_opt
   1.185    = Sequential
   1.186    | Default of string
   1.187    | DomIntros
   1.188    | No_Partials
   1.189    | Tailrec
   1.190  
   1.191 -datatype function_config
   1.192 -  = FunctionConfig of
   1.193 -   {
   1.194 -    sequential: bool,
   1.195 -    default: string,
   1.196 -    domintros: bool,
   1.197 -    partials: bool,
   1.198 -    tailrec: bool
   1.199 -   }
   1.200 +datatype function_config = FunctionConfig of
   1.201 + {sequential: bool,
   1.202 +  default: string,
   1.203 +  domintros: bool,
   1.204 +  partials: bool,
   1.205 +  tailrec: bool}
   1.206  
   1.207  fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
   1.208      FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec}
   1.209 @@ -225,97 +216,94 @@
   1.210  (* Analyzing function equations *)
   1.211  
   1.212  fun split_def ctxt geq =
   1.213 -    let
   1.214 -      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
   1.215 -      val qs = Term.strip_qnt_vars "all" geq
   1.216 -      val imp = Term.strip_qnt_body "all" geq
   1.217 -      val (gs, eq) = Logic.strip_horn imp
   1.218 +  let
   1.219 +    fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
   1.220 +    val qs = Term.strip_qnt_vars "all" geq
   1.221 +    val imp = Term.strip_qnt_body "all" geq
   1.222 +    val (gs, eq) = Logic.strip_horn imp
   1.223  
   1.224 -      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
   1.225 -          handle TERM _ => error (input_error "Not an equation")
   1.226 +    val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
   1.227 +      handle TERM _ => error (input_error "Not an equation")
   1.228  
   1.229 -      val (head, args) = strip_comb f_args
   1.230 +    val (head, args) = strip_comb f_args
   1.231  
   1.232 -      val fname = fst (dest_Free head)
   1.233 -          handle TERM _ => error (input_error "Head symbol must not be a bound variable")
   1.234 -    in
   1.235 -      (fname, qs, gs, args, rhs)
   1.236 -    end
   1.237 +    val fname = fst (dest_Free head)
   1.238 +      handle TERM _ => error (input_error "Head symbol must not be a bound variable")
   1.239 +  in
   1.240 +    (fname, qs, gs, args, rhs)
   1.241 +  end
   1.242  
   1.243  (* Check for all sorts of errors in the input *)
   1.244  fun check_defs ctxt fixes eqs =
   1.245 -    let
   1.246 -      val fnames = map (fst o fst) fixes
   1.247 -                                
   1.248 -      fun check geq = 
   1.249 -          let
   1.250 -            fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
   1.251 -                                  
   1.252 -            val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
   1.253 -                                 
   1.254 -            val _ = fname mem fnames 
   1.255 -                    orelse input_error 
   1.256 -                             ("Head symbol of left hand side must be " 
   1.257 -                              ^ plural "" "one out of " fnames ^ commas_quote fnames)
   1.258 -                                            
   1.259 -            val _ = length args > 0 orelse input_error "Function has no arguments:"
   1.260 +  let
   1.261 +    val fnames = map (fst o fst) fixes
   1.262 +
   1.263 +    fun check geq =
   1.264 +      let
   1.265 +        fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
   1.266  
   1.267 -            fun add_bvs t is = add_loose_bnos (t, 0, is)
   1.268 +        val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
   1.269 +
   1.270 +        val _ = fname mem fnames
   1.271 +          orelse input_error ("Head symbol of left hand side must be " ^
   1.272 +            plural "" "one out of " fnames ^ commas_quote fnames)
   1.273 +
   1.274 +        val _ = length args > 0 orelse input_error "Function has no arguments:"
   1.275 +
   1.276 +        fun add_bvs t is = add_loose_bnos (t, 0, is)
   1.277              val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
   1.278                          |> map (fst o nth (rev qs))
   1.279 -                      
   1.280 -            val _ = null rvs orelse input_error 
   1.281 -                        ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
   1.282 -                         ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
   1.283 -                                    
   1.284 -            val _ = forall (not o Term.exists_subterm 
   1.285 -                             (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
   1.286 -                    orelse input_error "Defined function may not occur in premises or arguments"
   1.287 +
   1.288 +        val _ = null rvs orelse input_error
   1.289 +          ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
   1.290 +           " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
   1.291 +
   1.292 +        val _ = forall (not o Term.exists_subterm
   1.293 +          (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
   1.294 +          orelse input_error "Defined function may not occur in premises or arguments"
   1.295  
   1.296 -            val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
   1.297 -            val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
   1.298 -            val _ = null funvars
   1.299 -                    orelse (warning (cat_lines 
   1.300 -                    ["Bound variable" ^ plural " " "s " funvars 
   1.301 -                     ^ commas_quote (map fst funvars) ^  
   1.302 -                     " occur" ^ plural "s" "" funvars ^ " in function position.",  
   1.303 -                     "Misspelled constructor???"]); true)
   1.304 -          in
   1.305 -            (fname, length args)
   1.306 -          end
   1.307 +        val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
   1.308 +        val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
   1.309 +        val _ = null funvars orelse (warning (cat_lines
   1.310 +          ["Bound variable" ^ plural " " "s " funvars ^
   1.311 +          commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
   1.312 +          " in function position.", "Misspelled constructor???"]); true)
   1.313 +      in
   1.314 +        (fname, length args)
   1.315 +      end
   1.316  
   1.317 -      val grouped_args = AList.group (op =) (map check eqs)
   1.318 -      val _ = grouped_args
   1.319 -        |> map (fn (fname, ars) =>
   1.320 -             length (distinct (op =) ars) = 1
   1.321 -             orelse error ("Function " ^ quote fname ^
   1.322 -                           " has different numbers of arguments in different equations"))
   1.323 +    val grouped_args = AList.group (op =) (map check eqs)
   1.324 +    val _ = grouped_args
   1.325 +      |> map (fn (fname, ars) =>
   1.326 +        length (distinct (op =) ars) = 1
   1.327 +        orelse error ("Function " ^ quote fname ^
   1.328 +          " has different numbers of arguments in different equations"))
   1.329  
   1.330 -      val not_defined = subtract (op =) (map fst grouped_args) fnames
   1.331 -      val _ = null not_defined
   1.332 -        orelse error ("No defining equations for function" ^
   1.333 -          plural " " "s " not_defined ^ commas_quote not_defined)
   1.334 +    val not_defined = subtract (op =) (map fst grouped_args) fnames
   1.335 +    val _ = null not_defined
   1.336 +      orelse error ("No defining equations for function" ^
   1.337 +        plural " " "s " not_defined ^ commas_quote not_defined)
   1.338  
   1.339 -      fun check_sorts ((fname, fT), _) =
   1.340 -          Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
   1.341 -          orelse error (cat_lines 
   1.342 -          ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
   1.343 -           setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
   1.344 +    fun check_sorts ((fname, fT), _) =
   1.345 +      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
   1.346 +      orelse error (cat_lines
   1.347 +      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
   1.348 +       setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
   1.349  
   1.350 -      val _ = map check_sorts fixes
   1.351 -    in
   1.352 -      ()
   1.353 -    end
   1.354 +    val _ = map check_sorts fixes
   1.355 +  in
   1.356 +    ()
   1.357 +  end
   1.358  
   1.359  (* Preprocessors *)
   1.360  
   1.361  type fixes = ((string * typ) * mixfix) list
   1.362  type 'a spec = (Attrib.binding * 'a list) list
   1.363 -type preproc = function_config -> Proof.context -> fixes -> term spec 
   1.364 -               -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
   1.365 +type preproc = function_config -> Proof.context -> fixes -> term spec ->
   1.366 +  (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
   1.367  
   1.368 -val fname_of = fst o dest_Free o fst o strip_comb o fst 
   1.369 - o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
   1.370 +val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o
   1.371 +  HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
   1.372  
   1.373  fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
   1.374    | mk_case_names _ n 0 = []
   1.375 @@ -323,22 +311,21 @@
   1.376    | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
   1.377  
   1.378  fun empty_preproc check _ ctxt fixes spec =
   1.379 -    let 
   1.380 -      val (bnds, tss) = split_list spec
   1.381 -      val ts = flat tss
   1.382 -      val _ = check ctxt fixes ts
   1.383 -      val fnames = map (fst o fst) fixes
   1.384 -      val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
   1.385 +  let
   1.386 +    val (bnds, tss) = split_list spec
   1.387 +    val ts = flat tss
   1.388 +    val _ = check ctxt fixes ts
   1.389 +    val fnames = map (fst o fst) fixes
   1.390 +    val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
   1.391  
   1.392 -      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
   1.393 -                                   (indices ~~ xs)
   1.394 -                        |> map (map snd)
   1.395 +    fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
   1.396 +      (indices ~~ xs) |> map (map snd)
   1.397  
   1.398 -      (* using theorem names for case name currently disabled *)
   1.399 -      val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
   1.400 -    in
   1.401 -      (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
   1.402 -    end
   1.403 +    (* using theorem names for case name currently disabled *)
   1.404 +    val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
   1.405 +  in
   1.406 +    (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
   1.407 +  end
   1.408  
   1.409  structure Preprocessor = Generic_Data
   1.410  (
   1.411 @@ -346,32 +333,31 @@
   1.412    val empty : T = empty_preproc check_defs
   1.413    val extend = I
   1.414    fun merge (a, _) = a
   1.415 -);
   1.416 +)
   1.417  
   1.418  val get_preproc = Preprocessor.get o Context.Proof
   1.419  val set_preproc = Preprocessor.map o K
   1.420  
   1.421  
   1.422  
   1.423 -local 
   1.424 +local
   1.425    structure P = OuterParse and K = OuterKeyword
   1.426  
   1.427 -  val option_parser = 
   1.428 -      P.group "option" ((P.reserved "sequential" >> K Sequential)
   1.429 -                    || ((P.reserved "default" |-- P.term) >> Default)
   1.430 -                    || (P.reserved "domintros" >> K DomIntros)
   1.431 -                    || (P.reserved "no_partials" >> K No_Partials)
   1.432 -                    || (P.reserved "tailrec" >> K Tailrec))
   1.433 +  val option_parser = P.group "option"
   1.434 +    ((P.reserved "sequential" >> K Sequential)
   1.435 +     || ((P.reserved "default" |-- P.term) >> Default)
   1.436 +     || (P.reserved "domintros" >> K DomIntros)
   1.437 +     || (P.reserved "no_partials" >> K No_Partials)
   1.438 +     || (P.reserved "tailrec" >> K Tailrec))
   1.439  
   1.440 -  fun config_parser default = 
   1.441 -      (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
   1.442 -        >> (fn opts => fold apply_opt opts default)
   1.443 +  fun config_parser default =
   1.444 +    (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
   1.445 +     >> (fn opts => fold apply_opt opts default)
   1.446  in
   1.447 -  fun function_parser default_cfg = 
   1.448 +  fun function_parser default_cfg =
   1.449        config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
   1.450  end
   1.451  
   1.452  
   1.453  end
   1.454  end
   1.455 -