some interface cleanup
authorkrauss
Mon Jul 16 21:22:43 2007 +0200 (2007-07-16)
changeset 238192040846d1bbe
parent 23818 cfe8d4bf749a
child 23820 8290cd33c4d5
some interface cleanup
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/mutual.ML
     1.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Mon Jul 16 21:17:12 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Mon Jul 16 21:22:43 2007 +0200
     1.3 @@ -9,19 +9,19 @@
     1.4  
     1.5  signature FUNDEF_CTXTREE =
     1.6  sig
     1.7 +    type depgraph
     1.8      type ctx_tree
     1.9  
    1.10      (* FIXME: This interface is a mess and needs to be cleaned up! *)
    1.11      val cong_deps : thm -> int IntGraph.T
    1.12      val add_congs : thm list
    1.13  
    1.14 -    val mk_tree: (thm * FundefCommon.depgraph) list ->
    1.15 -                 (string * typ) -> term -> Proof.context -> term -> FundefCommon.ctx_tree
    1.16 +    val mk_tree: (thm * depgraph) list ->
    1.17 +                 (string * typ) -> term -> Proof.context -> term -> ctx_tree
    1.18  
    1.19 -    val inst_tree: theory -> term -> term -> FundefCommon.ctx_tree
    1.20 -                   -> FundefCommon.ctx_tree
    1.21 +    val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree
    1.22  
    1.23 -    val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
    1.24 +    val add_context_varnames : ctx_tree -> string list -> string list
    1.25  
    1.26      val export_term : (string * typ) list * term list -> term -> term
    1.27      val export_thm : theory -> (string * typ) list * term list -> thm -> thm
    1.28 @@ -33,9 +33,9 @@
    1.29     (((string * typ) list * thm list) * thm) list ->
    1.30     (((string * typ) list * thm list) * thm) list * 'b ->
    1.31     (((string * typ) list * thm list) * thm) list * 'b)
    1.32 -   -> FundefCommon.ctx_tree -> 'b -> 'b
    1.33 +   -> ctx_tree -> 'b -> 'b
    1.34  
    1.35 -    val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list
    1.36 +    val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> ctx_tree -> thm * (thm * thm) list
    1.37  end
    1.38  
    1.39  structure FundefCtxTree : FUNDEF_CTXTREE =
    1.40 @@ -44,6 +44,13 @@
    1.41  open FundefCommon
    1.42  open FundefLib
    1.43  
    1.44 +type depgraph = int IntGraph.T
    1.45 +
    1.46 +datatype ctx_tree 
    1.47 +  = Leaf of term
    1.48 +  | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
    1.49 +  | RCall of (term * ctx_tree)
    1.50 +
    1.51  
    1.52  (* Maps "Trueprop A = B" to "A" *)
    1.53  val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
    1.54 @@ -160,7 +167,7 @@
    1.55  
    1.56  fun import_thm thy (fixes, athms) =
    1.57      fold (forall_elim o cterm_of thy o Free) fixes
    1.58 - #> fold implies_elim_swp athms
    1.59 + #> fold (flip implies_elim) athms
    1.60  
    1.61  fun assume_in_ctxt thy (fixes, athms) prop =
    1.62      let
     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Jul 16 21:17:12 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Jul 16 21:22:43 2007 +0200
     2.3 @@ -26,14 +26,6 @@
     2.4  val rel_name = suffix "_rel"
     2.5  val dom_name = suffix "_dom"
     2.6  
     2.7 -type depgraph = int IntGraph.T
     2.8 -
     2.9 -datatype ctx_tree 
    2.10 -  = Leaf of term
    2.11 -  | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
    2.12 -  | RCall of (term * ctx_tree)
    2.13 -
    2.14 -
    2.15  
    2.16  datatype fundef_result =
    2.17    FundefResult of
    2.18 @@ -58,6 +50,7 @@
    2.19       {
    2.20        defname : string,
    2.21  
    2.22 +      (* contains no logical entities: invariant under morphisms *)
    2.23        add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
    2.24  
    2.25        fs : term list,
    2.26 @@ -73,7 +66,7 @@
    2.27        val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    2.28        val name = Morphism.name phi
    2.29      in
    2.30 -      FundefCtxData { add_simps = add_simps (* contains no logical entities *), 
    2.31 +      FundefCtxData { add_simps = add_simps,
    2.32                        fs = map term fs, R = term R, psimps = fact psimps, 
    2.33                        pinducts = fact pinducts, termination = thm termination,
    2.34                        defname = name defname }
    2.35 @@ -154,7 +147,6 @@
    2.36      FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
    2.37      #> store_termination_rule termination
    2.38  
    2.39 -
    2.40  (* Configuration management *)
    2.41  datatype fundef_opt 
    2.42    = Sequential
    2.43 @@ -186,6 +178,10 @@
    2.44  
    2.45  fun target_of (FundefConfig {target, ...}) = target
    2.46  
    2.47 +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", 
    2.48 +                                    target=NONE, domintros=false, tailrec=false }
    2.49 +
    2.50 +
    2.51  (* Common operations on equations *)
    2.52  
    2.53  fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
    2.54 @@ -248,7 +244,7 @@
    2.55              val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    2.56                                                          ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
    2.57                                      
    2.58 -            val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs 
    2.59 +            val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames | _ => false)) gs 
    2.60                      orelse error (input_error "Recursive Calls not allowed in premises")
    2.61            in
    2.62              fqgar
    2.63 @@ -265,14 +261,23 @@
    2.64  
    2.65  type fixes = ((string * typ) * mixfix) list
    2.66  type 'a spec = ((bstring * Attrib.src list) * 'a list) list
    2.67 -type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec))
    2.68 +type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec 
    2.69 +               -> (term list * (thm list -> thm spec) * (thm list -> thm list list))
    2.70 +
    2.71 +val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
    2.72  
    2.73  fun empty_preproc check _ _ ctxt fixes spec =
    2.74      let 
    2.75        val (nas,tss) = split_list spec
    2.76        val _ = check ctxt fixes (flat tss)
    2.77 +      val ts = flat tss
    2.78 +      val fnames = map (fst o fst) fixes
    2.79 +      val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
    2.80 +
    2.81 +      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
    2.82 +                        |> map (map snd)
    2.83      in
    2.84 -      (flat tss, curry op ~~ nas o Library.unflat tss)
    2.85 +      (ts, curry op ~~ nas o Library.unflat tss, sort)
    2.86      end
    2.87  
    2.88  structure Preprocessor = GenericDataFun
    2.89 @@ -313,44 +318,11 @@
    2.90  
    2.91    val flags_statements = statements_ow
    2.92                           >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
    2.93 -
    2.94 -  fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements)
    2.95  in
    2.96    fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements)
    2.97 -                                  
    2.98  end
    2.99  
   2.100  
   2.101 -
   2.102 -
   2.103 -
   2.104 -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", 
   2.105 -                                    target=NONE, domintros=false, tailrec=false }
   2.106 -
   2.107 -
   2.108  end
   2.109  end
   2.110  
   2.111 -(* Common Abbreviations *)
   2.112 -
   2.113 -structure FundefAbbrev =
   2.114 -struct
   2.115 -
   2.116 -fun implies_elim_swp x y = implies_elim y x
   2.117 -
   2.118 -(* HOL abbreviations *)
   2.119 -val boolT = HOLogic.boolT
   2.120 -val mk_prod = HOLogic.mk_prod
   2.121 -val mk_eq = HOLogic.mk_eq
   2.122 -val eq_const = HOLogic.eq_const
   2.123 -val Trueprop = HOLogic.mk_Trueprop
   2.124 -val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
   2.125 -
   2.126 -fun free_to_var (Free (v,T)) = Var ((v,0),T)
   2.127 -  | free_to_var _ = raise Match
   2.128 -
   2.129 -fun var_to_free (Var ((v,_),T)) = Free (v,T)
   2.130 -  | var_to_free _ = raise Match
   2.131 -
   2.132 -
   2.133 -end
     3.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Mon Jul 16 21:17:12 2007 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Mon Jul 16 21:22:43 2007 +0200
     3.3 @@ -24,10 +24,11 @@
     3.4  structure FundefCore : FUNDEF_CORE =
     3.5  struct
     3.6  
     3.7 +val boolT = HOLogic.boolT
     3.8 +val mk_eq = HOLogic.mk_eq
     3.9  
    3.10  open FundefLib
    3.11  open FundefCommon
    3.12 -open FundefAbbrev
    3.13  
    3.14  datatype globals =
    3.15     Globals of { 
    3.16 @@ -85,7 +86,7 @@
    3.17        qglr : ((string * typ) list * term list * term * term),
    3.18        cdata : clause_context,
    3.19  
    3.20 -      tree: ctx_tree,
    3.21 +      tree: FundefCtxTree.ctx_tree,
    3.22        lGI: thm,
    3.23        RCs: rec_call_info list
    3.24       }
    3.25 @@ -125,8 +126,8 @@
    3.26            let
    3.27              val shift = incr_boundvars (length qs')
    3.28            in
    3.29 -            (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
    3.30 -                     $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
    3.31 +            (implies $ HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs')
    3.32 +                     $ HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
    3.33                |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
    3.34                |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
    3.35                |> curry abstract_over fvar
    3.36 @@ -140,12 +141,12 @@
    3.37  fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
    3.38      let
    3.39          fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
    3.40 -            Trueprop Pbool
    3.41 -                     |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
    3.42 +            HOLogic.mk_Trueprop Pbool
    3.43 +                     |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
    3.44                       |> fold_rev (curry Logic.mk_implies) gs
    3.45                       |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
    3.46      in
    3.47 -        Trueprop Pbool
    3.48 +        HOLogic.mk_Trueprop Pbool
    3.49                   |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
    3.50                   |> mk_forall_rename ("x", x)
    3.51                   |> mk_forall_rename ("P", Pbool)
    3.52 @@ -168,7 +169,7 @@
    3.53        val cqs = map (cterm_of thy) qs
    3.54        val ags = map (assume o cterm_of thy) gs
    3.55                    
    3.56 -      val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
    3.57 +      val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
    3.58      in
    3.59        ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, 
    3.60                        cqs = cqs, ags = ags, case_hyp = case_hyp }
    3.61 @@ -203,18 +204,18 @@
    3.62          val lGI = GIntro_thm
    3.63                      |> forall_elim (cert f)
    3.64                      |> fold forall_elim cqs
    3.65 -                    |> fold implies_elim_swp ags
    3.66 +                    |> fold (flip implies_elim) ags
    3.67  
    3.68          fun mk_call_info (rcfix, rcassm, rcarg) RI =
    3.69              let
    3.70                  val llRI = RI
    3.71                               |> fold forall_elim cqs
    3.72                               |> fold (forall_elim o cert o Free) rcfix
    3.73 -                             |> fold implies_elim_swp ags
    3.74 -                             |> fold implies_elim_swp rcassm
    3.75 +                             |> fold (flip implies_elim) ags
    3.76 +                             |> fold (flip implies_elim) rcassm
    3.77  
    3.78                  val h_assum =
    3.79 -                    Trueprop (G $ rcarg $ (h $ rcarg))
    3.80 +                    HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
    3.81                                |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
    3.82                                |> fold_rev (mk_forall o Free) rcfix
    3.83                                |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
    3.84 @@ -263,16 +264,16 @@
    3.85        val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
    3.86        val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
    3.87            
    3.88 -      val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
    3.89 +      val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
    3.90      in if j < i then
    3.91           let
    3.92             val compat = lookup_compat_thm j i cts
    3.93           in
    3.94             compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
    3.95                  |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
    3.96 -                |> fold implies_elim_swp agsj
    3.97 -                |> fold implies_elim_swp agsi
    3.98 -                |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
    3.99 +                |> fold (flip implies_elim) agsj
   3.100 +                |> fold (flip implies_elim) agsi
   3.101 +                |> flip implies_elim ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
   3.102           end
   3.103         else
   3.104           let
   3.105 @@ -280,9 +281,9 @@
   3.106           in
   3.107                 compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   3.108                   |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   3.109 -                 |> fold implies_elim_swp agsi
   3.110 -                 |> fold implies_elim_swp agsj
   3.111 -                 |> implies_elim_swp (assume lhsi_eq_lhsj)
   3.112 +                 |> fold (flip implies_elim) agsi
   3.113 +                 |> fold (flip implies_elim) agsj
   3.114 +                 |> flip implies_elim (assume lhsi_eq_lhsj)
   3.115                   |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
   3.116           end
   3.117      end
   3.118 @@ -330,11 +331,11 @@
   3.119  
   3.120          val RLj_import = 
   3.121              RLj |> fold forall_elim cqsj'
   3.122 -                |> fold implies_elim_swp agsj'
   3.123 -                |> fold implies_elim_swp Ghsj'
   3.124 +                |> fold (flip implies_elim) agsj'
   3.125 +                |> fold (flip implies_elim) Ghsj'
   3.126  
   3.127 -        val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
   3.128 -        val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
   3.129 +        val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
   3.130 +        val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
   3.131      in
   3.132          (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   3.133          |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   3.134 @@ -364,7 +365,7 @@
   3.135          val existence = fold (curry op COMP o prep_RC) RCs lGI
   3.136  
   3.137          val P = cterm_of thy (mk_eq (y, rhsC))
   3.138 -        val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
   3.139 +        val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
   3.140  
   3.141          val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
   3.142  
   3.143 @@ -372,8 +373,8 @@
   3.144                             |> forall_elim (cterm_of thy lhs)
   3.145                             |> forall_elim (cterm_of thy y)
   3.146                             |> forall_elim P
   3.147 -                           |> implies_elim_swp G_lhs_y
   3.148 -                           |> fold implies_elim_swp unique_clauses
   3.149 +                           |> flip implies_elim G_lhs_y
   3.150 +                           |> fold (flip implies_elim) unique_clauses
   3.151                             |> implies_intr (cprop_of G_lhs_y)
   3.152                             |> forall_intr (cterm_of thy y)
   3.153  
   3.154 @@ -409,8 +410,8 @@
   3.155  
   3.156          (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   3.157          val ihyp = all domT $ Abs ("z", domT,
   3.158 -                                   implies $ Trueprop (R $ Bound 0 $ x)
   3.159 -                                           $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   3.160 +                                   implies $ HOLogic.mk_Trueprop (R $ Bound 0 $ x)
   3.161 +                                           $ HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   3.162                                                               Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
   3.163                         |> cterm_of thy
   3.164  
   3.165 @@ -430,7 +431,7 @@
   3.166                                    |> forall_elim_vars 0
   3.167                                    |> fold (curry op COMP) ex1s
   3.168                                    |> implies_intr (ihyp)
   3.169 -                                  |> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x)))
   3.170 +                                  |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
   3.171                                    |> forall_intr (cterm_of thy x)
   3.172                                    |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   3.173                                    |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
   3.174 @@ -453,11 +454,11 @@
   3.175        fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
   3.176            let
   3.177              fun mk_h_assm (rcfix, rcassm, rcarg) =
   3.178 -                Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
   3.179 +                HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
   3.180                            |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   3.181                            |> fold_rev (mk_forall o Free) rcfix
   3.182            in
   3.183 -            Trueprop (Gvar $ lhs $ rhs)
   3.184 +            HOLogic.mk_Trueprop (Gvar $ lhs $ rhs)
   3.185                        |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
   3.186                        |> fold_rev (curry Logic.mk_implies) gs
   3.187                        |> fold_rev mk_forall (fvar :: qs)
   3.188 @@ -494,7 +495,7 @@
   3.189        val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
   3.190  
   3.191        fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
   3.192 -          Trueprop (Rvar $ rcarg $ lhs)
   3.193 +          HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs)
   3.194                      |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   3.195                      |> fold_rev (curry Logic.mk_implies) gs
   3.196                      |> fold_rev (mk_forall o Free) rcfix
   3.197 @@ -551,8 +552,8 @@
   3.198    
   3.199        fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
   3.200            let
   3.201 -            val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
   3.202 -            val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
   3.203 +            val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
   3.204 +            val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
   3.205            in
   3.206              ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
   3.207                |> (fn it => it COMP graph_is_function)
   3.208 @@ -580,23 +581,23 @@
   3.209        val Globals {domT, x, z, a, P, D, ...} = globals
   3.210        val acc_R = mk_acc domT R
   3.211                    
   3.212 -      val x_D = assume (cterm_of thy (Trueprop (D $ x)))
   3.213 -      val a_D = cterm_of thy (Trueprop (D $ a))
   3.214 +      val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
   3.215 +      val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
   3.216                  
   3.217 -      val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
   3.218 +      val D_subset = cterm_of thy (mk_forall x (implies $ HOLogic.mk_Trueprop (D $ x) $ HOLogic.mk_Trueprop (acc_R $ x)))
   3.219                       
   3.220        val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
   3.221                      mk_forall x
   3.222 -                    (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
   3.223 -                                                    Logic.mk_implies (Trueprop (R $ z $ x),
   3.224 -                                                                      Trueprop (D $ z)))))
   3.225 +                    (mk_forall z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
   3.226 +                                                    Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
   3.227 +                                                                      HOLogic.mk_Trueprop (D $ z)))))
   3.228                      |> cterm_of thy
   3.229                      
   3.230                      
   3.231    (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   3.232        val ihyp = all domT $ Abs ("z", domT, 
   3.233 -               implies $ Trueprop (R $ Bound 0 $ x)
   3.234 -             $ Trueprop (P $ Bound 0))
   3.235 +               implies $ HOLogic.mk_Trueprop (R $ Bound 0 $ x)
   3.236 +             $ HOLogic.mk_Trueprop (P $ Bound 0))
   3.237             |> cterm_of thy
   3.238  
   3.239        val aihyp = assume ihyp
   3.240 @@ -612,26 +613,26 @@
   3.241            
   3.242      fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
   3.243          sih |> forall_elim (cterm_of thy rcarg)
   3.244 -            |> implies_elim_swp llRI
   3.245 +            |> flip implies_elim llRI
   3.246              |> fold_rev (implies_intr o cprop_of) CCas
   3.247              |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   3.248          
   3.249      val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   3.250                   
   3.251 -    val step = Trueprop (P $ lhs)
   3.252 +    val step = HOLogic.mk_Trueprop (P $ lhs)
   3.253              |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   3.254              |> fold_rev (curry Logic.mk_implies) gs
   3.255 -            |> curry Logic.mk_implies (Trueprop (D $ lhs))
   3.256 +            |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
   3.257              |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   3.258              |> cterm_of thy
   3.259           
   3.260      val P_lhs = assume step
   3.261             |> fold forall_elim cqs
   3.262 -           |> implies_elim_swp lhs_D 
   3.263 -           |> fold implies_elim_swp ags
   3.264 -           |> fold implies_elim_swp P_recs
   3.265 +           |> flip implies_elim lhs_D 
   3.266 +           |> fold (flip implies_elim) ags
   3.267 +           |> fold (flip implies_elim) P_recs
   3.268            
   3.269 -    val res = cterm_of thy (Trueprop (P $ x))
   3.270 +    val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
   3.271             |> Simplifier.rewrite replace_x_ss
   3.272             |> symmetric (* P lhs == P x *)
   3.273             |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
   3.274 @@ -687,7 +688,7 @@
   3.275      let
   3.276        val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
   3.277                        qglr = (oqs, _, _, _), ...} = clause
   3.278 -      val goal = Trueprop (mk_acc domT R $ lhs)
   3.279 +      val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
   3.280                            |> fold_rev (curry Logic.mk_implies) gs
   3.281                            |> cterm_of thy
   3.282      in
   3.283 @@ -719,7 +720,7 @@
   3.284            let
   3.285              val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
   3.286                         
   3.287 -            val hyp = Trueprop (R' $ arg $ lhs)
   3.288 +            val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
   3.289                        |> fold_rev (curry Logic.mk_implies o prop_of) used
   3.290                        |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
   3.291                        |> fold_rev (curry Logic.mk_implies o prop_of) ags
   3.292 @@ -728,13 +729,13 @@
   3.293                        
   3.294              val thm = assume hyp
   3.295                        |> fold forall_elim cqs
   3.296 -                      |> fold implies_elim_swp ags
   3.297 +                      |> fold (flip implies_elim) ags
   3.298                        |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
   3.299 -                      |> fold implies_elim_swp used
   3.300 +                      |> fold (flip implies_elim) used
   3.301                        
   3.302              val acc = thm COMP ih_case
   3.303                        
   3.304 -            val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
   3.305 +            val z_eq_arg = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (z, arg)))
   3.306                             
   3.307              val arg_eq_z = (assume z_eq_arg) RS sym
   3.308                             
   3.309 @@ -742,8 +743,8 @@
   3.310                          |> implies_intr (cprop_of case_hyp)
   3.311                          |> implies_intr z_eq_arg
   3.312  
   3.313 -            val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
   3.314 -            val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   3.315 +            val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
   3.316 +            val x_eq_lhs = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   3.317                             
   3.318              val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
   3.319                           |> FundefCtxTree.export_thm thy (fixes, 
   3.320 @@ -767,20 +768,20 @@
   3.321                    
   3.322        val R' = Free ("R", fastype_of R)
   3.323                 
   3.324 -      val Rrel = Free ("R", mk_relT (domT, domT))
   3.325 -      val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
   3.326 +      val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
   3.327 +      val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
   3.328                      
   3.329 -      val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   3.330 +      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   3.331                            
   3.332        (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   3.333        val ihyp = all domT $ Abs ("z", domT, 
   3.334 -                                 implies $ Trueprop (R' $ Bound 0 $ x)
   3.335 -                                         $ Trueprop (acc_R $ Bound 0))
   3.336 +                                 implies $ HOLogic.mk_Trueprop (R' $ Bound 0 $ x)
   3.337 +                                         $ HOLogic.mk_Trueprop (acc_R $ Bound 0))
   3.338                       |> cterm_of thy
   3.339  
   3.340        val ihyp_a = assume ihyp |> forall_elim_vars 0
   3.341                     
   3.342 -      val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 
   3.343 +      val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) 
   3.344                    
   3.345        val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
   3.346      in
   3.347 @@ -842,14 +843,15 @@
   3.348                          
   3.349              val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
   3.350              val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
   3.351 +            fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
   3.352            in
   3.353              Goal.prove ctxt [] [] trsimp
   3.354                         (fn _ =>  
   3.355                             rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
   3.356                                  THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
   3.357 -                                THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1))
   3.358 +                                THEN (SIMPSET' simp_default_tac 1)
   3.359                                  THEN (etac not_acc_down 1)
   3.360 -                                THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 1)
   3.361 +                                THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' simp_default_tac)) 1)
   3.362                |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   3.363            end
   3.364      in
     4.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jul 16 21:17:12 2007 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jul 16 21:22:43 2007 +0200
     4.3 @@ -249,13 +249,21 @@
     4.4                             |> tap (check_defs ctxt fixes) (* Standard checks *)
     4.5                             |> tap (map (check_pats ctxt))    (* More checks for sequential mode *)
     4.6                             |> curry op ~~ flags'
     4.7 -                           |> add_catchall fixes   (* Completion: still disabled *)
     4.8 +                           |> add_catchall fixes   (* Completion *)
     4.9                             |> FundefSplit.split_some_equations ctxt
    4.10  
    4.11            fun restore_spec thms =
    4.12                nas ~~ Library.take (length nas, Library.unflat spliteqs thms)
    4.13 +              
    4.14 +          val spliteqs' = flat (Library.take (length nas, spliteqs))
    4.15 +          val fnames = map (fst o fst) fixes
    4.16 +          val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
    4.17 +
    4.18 +          fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
    4.19 +                                       |> map (map snd)
    4.20 +
    4.21          in
    4.22 -          (flat spliteqs, restore_spec)
    4.23 +          (flat spliteqs, restore_spec, sort)
    4.24          end
    4.25        else
    4.26          FundefCommon.empty_preproc check_defs config flags ctxt fixes spec
     5.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jul 16 21:17:12 2007 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jul 16 21:22:43 2007 +0200
     5.3 @@ -73,8 +73,6 @@
     5.4      (ctx, [], t)
     5.5  
     5.6  
     5.7 -fun implies_elim_swp a b = implies_elim b a
     5.8 -
     5.9  fun map3 _ [] [] [] = []
    5.10    | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
    5.11    | map3 _ _ _ _ = raise Library.UnequalLengths;
     6.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 16 21:17:12 2007 +0200
     6.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 16 21:22:43 2007 +0200
     6.3 @@ -44,20 +44,20 @@
     6.4  
     6.5  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
     6.6  
     6.7 -fun add_simps fixes post sort label moreatts simps lthy =
     6.8 +fun add_simps fnames post sort label moreatts simps lthy =
     6.9      let
    6.10 -      val fnames = map (fst o fst) fixes
    6.11 +      val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
    6.12 +      val spec = post simps
    6.13 +                   |> map (apfst (apsnd (append atts)))
    6.14  
    6.15        val (saved_spec_simps, lthy) =
    6.16 -        fold_map note_theorem (post simps) lthy
    6.17 +        fold_map note_theorem spec lthy
    6.18 +
    6.19        val saved_simps = flat (map snd saved_spec_simps)
    6.20 -
    6.21        val simps_by_f = sort saved_simps
    6.22  
    6.23        fun add_for_f fname simps =
    6.24 -        note_theorem
    6.25 -          ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts),
    6.26 -            simps) #> snd
    6.27 +        note_theorem ((NameSpace.qualified fname label, []), simps) #> snd
    6.28      in
    6.29        (saved_simps,
    6.30         fold2 add_for_f fnames simps_by_f lthy)
    6.31 @@ -68,8 +68,9 @@
    6.32        val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    6.33            cont (Goal.close_result proof)
    6.34  
    6.35 +      val fnames = map (fst o fst) fixes
    6.36        val qualify = NameSpace.qualified defname
    6.37 -      val addsmps = add_simps fixes post sort_cont
    6.38 +      val addsmps = add_simps fnames post sort_cont
    6.39  
    6.40        val (((psimps', pinducts'), (_, [termination'])), lthy) =
    6.41            lthy
    6.42 @@ -107,11 +108,11 @@
    6.43  fun gen_add_fundef prep fixspec eqnss config flags lthy =
    6.44      let
    6.45        val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy
    6.46 -      val (eqs, post) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    6.47 +      val (eqs, post, sort_cont) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    6.48  
    6.49        val defname = mk_defname fixes
    6.50  
    6.51 -      val ((goalstate, cont, sort_cont), lthy) =
    6.52 +      val ((goalstate, cont), lthy) =
    6.53            FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
    6.54  
    6.55        val afterqed = fundef_afterqed config fixes post defname cont sort_cont
    6.56 @@ -190,6 +191,7 @@
    6.57      DatatypeHooks.add case_cong_hook
    6.58      #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
    6.59  
    6.60 +
    6.61  (* ad-hoc method to convert elimination-style goals to existential statements *)
    6.62  
    6.63  fun insert_int_goal thy subg st =
     7.1 --- a/src/HOL/Tools/function_package/mutual.ML	Mon Jul 16 21:17:12 2007 +0200
     7.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Mon Jul 16 21:22:43 2007 +0200
     7.3 @@ -16,7 +16,6 @@
     7.4                                -> local_theory
     7.5                                -> ((thm (* goalstate *)
     7.6                                     * (thm -> FundefCommon.fundef_result) (* proof continuation *)
     7.7 -                                   * (thm list -> thm list list)         (* sorting continuation *)
     7.8                                    ) * local_theory)
     7.9  
    7.10  end
    7.11 @@ -332,19 +331,6 @@
    7.12                       trsimps=mtrsimps}
    7.13      end
    7.14        
    7.15 -(* puts an object in the "right bucket" *)
    7.16 -fun store_grouped P x [] = []
    7.17 -  | store_grouped P x ((l, xs)::bs) =
    7.18 -    if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs)
    7.19 -                                           
    7.20 -fun sort_by_function (Mutual {fqgars, ...}) names xs =
    7.21 -    fold_rev (store_grouped (op = o apfst fst))  (* fill *)
    7.22 -             (map name_of_fqgar (Library.take (length xs, fqgars)) ~~ xs)      (* the name-thm pairs *)
    7.23 -             (map (rpair []) names)                (* in the empty buckets labeled with names *)
    7.24 -             
    7.25 -             |> map (snd #> map snd)                     (* and remove the labels afterwards *)
    7.26 -
    7.27 -
    7.28  fun prepare_fundef_mutual config defname fixes eqss lthy =
    7.29      let
    7.30        val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
    7.31 @@ -356,9 +342,8 @@
    7.32        val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
    7.33  
    7.34        val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
    7.35 -      val sort_cont = sort_by_function mutual' (map (fst o fst) fixes)
    7.36      in
    7.37 -      ((goalstate, mutual_cont, sort_cont), lthy'')
    7.38 +      ((goalstate, mutual_cont), lthy'')
    7.39      end
    7.40  
    7.41