src/HOL/Tools/function_package/fundef_common.ML
author haftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 19818 5c5c1208a3fa
parent 19781 c62720b20e9a
child 19922 984ae977f7aa
permissions -rw-r--r--
adding case theorems for code generator
     1 (*  Title:      HOL/Tools/function_package/fundef_common.ML
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 
     5 A package for general recursive function definitions. 
     6 Common type definitions and other infrastructure.
     7 *)
     8 
     9 structure FundefCommon =
    10 struct
    11 
    12 (* Theory Dependencies *)
    13 val acc_const_name = "Accessible_Part.acc"
    14 
    15 
    16 
    17 type depgraph = int IntGraph.T
    18 
    19 
    20 datatype ctx_tree 
    21   = Leaf of term
    22   | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
    23   | RCall of (term * ctx_tree)
    24 
    25 type glrs = (term list * term list * term * term) list
    26 
    27 
    28 (* A record containing all the relevant symbols and types needed during the proof.
    29    This is set up at the beginning and does not change. *)
    30 datatype naming_context =
    31    Names of { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
    32        G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term, 
    33        D: term, Pbool:term,
    34        glrs: (term list * term list * term * term) list,
    35        glrs': (term list * term list * term * term) list,
    36        f_def: thm,
    37        used: string list,
    38        trees: ctx_tree list
    39      }
    40 
    41 
    42 datatype rec_call_info = 
    43   RCInfo of
    44   {
    45    RI: thm, 
    46    RIvs: (string * typ) list,
    47    lRI: thm, 
    48    lRIq: thm, 
    49    Gh: thm, 
    50    Gh': thm,
    51    GmAs: term list,
    52    rcarg: term
    53   } 
    54      
    55 datatype clause_info =
    56   ClauseInfo of 
    57      {
    58       no: int,
    59 
    60       qs: term list, 
    61       gs: term list,
    62       lhs: term,
    63       rhs: term,
    64 
    65       cqs: cterm list,
    66       cvqs: cterm list,
    67       ags: thm list,
    68       
    69       cqs': cterm list, 
    70       ags': thm list,
    71       lhs': term,
    72       rhs': term,
    73       ordcqs': cterm list, 
    74 
    75       GI: thm,
    76       lGI: thm,
    77       RCs: rec_call_info list,
    78 
    79       tree: ctx_tree,
    80       case_hyp: thm
    81      }
    82 
    83 type inj_proj = ((term -> term) * (term -> term))
    84 
    85 type qgar = (string * typ) list * term list * term list * term
    86 
    87 datatype mutual_part =
    88   MutualPart of 
    89 	 {
    90           f_name: string,
    91 	  const: string * typ,
    92 	  cargTs: typ list,
    93 	  pthA: SumTools.sum_path,
    94 	  pthR: SumTools.sum_path,
    95 	  qgars: qgar list,
    96 	  f_def: thm
    97 	 }
    98 	 
    99 
   100 datatype mutual_info =
   101   Mutual of 
   102 	 { 
   103 	  name: string, 
   104 	  sum_const: string * typ,
   105 	  ST: typ,
   106 	  RST: typ,
   107 	  streeA: SumTools.sum_tree,
   108 	  streeR: SumTools.sum_tree,
   109 	  parts: mutual_part list,
   110 	  qglrss: (term list * term list * term * term) list list
   111 	 }
   112 
   113 
   114 datatype prep_result =
   115   Prep of
   116      {
   117       names: naming_context, 
   118       complete : term,
   119       compat : term list,
   120       clauses: clause_info list
   121      }
   122 
   123 datatype fundef_result =
   124   FundefResult of
   125      {
   126       f: term,
   127       G : term,
   128       R : term,
   129       completeness : thm,
   130       compatibility : thm list,
   131 
   132       psimps : thm list, 
   133       subset_pinduct : thm, 
   134       simple_pinduct : thm, 
   135       total_intro : thm,
   136       dom_intros : thm list
   137      }
   138 
   139 datatype fundef_mresult =
   140   FundefMResult of
   141      {
   142       f: term,
   143       G : term,
   144       R : term,
   145 
   146       psimps : thm list list, 
   147       subset_pinducts : thm list, 
   148       simple_pinducts : thm list, 
   149       cases : thm,
   150       termination : thm,
   151       domintros : thm list
   152      }
   153 
   154 
   155 type result_with_names = fundef_mresult * mutual_info * string list list * attribute list list list
   156 
   157 structure FundefData = TheoryDataFun
   158 (struct
   159   val name = "HOL/function_def/data";
   160   type T = string * result_with_names Symtab.table
   161 
   162   val empty = ("", Symtab.empty);
   163   val copy = I;
   164   val extend = I;
   165   fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (K true) (tab1, tab2))
   166 
   167   fun print _ _ = ();
   168 end);
   169 
   170 
   171 structure FundefCongs = GenericDataFun
   172 (struct
   173     val name = "HOL/function_def/congs"
   174     type T = thm list
   175     val empty = []
   176     val extend = I
   177     fun merge _ (l1, l2) = l1 @ l2
   178     fun print  _ _ = ()
   179 end);
   180 
   181 
   182 fun add_fundef_data name fundef_data =
   183     FundefData.map (fn (_,tab) => (name, Symtab.update_new (name, fundef_data) tab))
   184 
   185 fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name
   186 
   187 fun get_last_fundef thy = fst (FundefData.get thy)
   188 
   189 val map_fundef_congs = FundefCongs.map 
   190 val get_fundef_congs = FundefCongs.get
   191 
   192 end
   193 
   194 
   195 
   196 (* Common Abbreviations *)
   197 
   198 structure FundefAbbrev =
   199 struct
   200 
   201 fun implies_elim_swp x y = implies_elim y x
   202 
   203 (* Some HOL things frequently used *)
   204 val boolT = HOLogic.boolT
   205 val mk_prod = HOLogic.mk_prod
   206 val mk_mem = HOLogic.mk_mem
   207 val mk_eq = HOLogic.mk_eq
   208 val Trueprop = HOLogic.mk_Trueprop
   209 
   210 val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
   211 fun mk_relmem (x,y) R = Trueprop (mk_mem (mk_prod (x, y), R))
   212 
   213 fun mk_subset T A B = 
   214     let val sT = HOLogic.mk_setT T
   215     in Const ("Orderings.less_eq", sT --> sT --> boolT) $ A $ B end
   216 
   217 
   218 (* with explicit types: Needed with loose bounds *)
   219 fun mk_relmemT xT yT (x,y) R = 
   220     let 
   221 	val pT = HOLogic.mk_prodT (xT, yT)
   222 	val RT = HOLogic.mk_setT pT
   223     in
   224 	Const ("op :", [pT, RT] ---> boolT)
   225 	      $ (HOLogic.pair_const xT yT $ x $ y)
   226 	      $ R
   227     end
   228 
   229 fun free_to_var (Free (v,T)) = Var ((v,0),T)
   230   | free_to_var _ = raise Match
   231 
   232 fun var_to_free (Var ((v,_),T)) = Free (v,T)
   233   | var_to_free _ = raise Match
   234 
   235 
   236 end