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