src/HOL/Tools/function_package/fundef_prep.ML
author haftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 19818 5c5c1208a3fa
parent 19781 c62720b20e9a
child 19876 11d447d5d68c
permissions -rw-r--r--
adding case theorems for code generator
krauss@19564
     1
(*  Title:      HOL/Tools/function_package/fundef_prep.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
Preparation step: makes auxiliary definitions and generates
krauss@19564
     7
proof obligations.
krauss@19564
     8
*)
krauss@19564
     9
krauss@19564
    10
signature FUNDEF_PREP =
krauss@19564
    11
sig
krauss@19773
    12
    val prepare_fundef : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
krauss@19773
    13
			 -> FundefCommon.prep_result * theory
krauss@19770
    14
krauss@19564
    15
end
krauss@19564
    16
krauss@19564
    17
krauss@19564
    18
krauss@19564
    19
krauss@19564
    20
krauss@19564
    21
structure FundefPrep : FUNDEF_PREP =
krauss@19564
    22
struct
krauss@19564
    23
krauss@19564
    24
krauss@19564
    25
open FundefCommon
krauss@19564
    26
open FundefAbbrev 
krauss@19564
    27
krauss@19564
    28
krauss@19564
    29
krauss@19564
    30
krauss@19564
    31
fun split_list3 [] = ([],[],[])
krauss@19564
    32
  | split_list3 ((x,y,z)::xyzs) = 
krauss@19564
    33
    let
krauss@19564
    34
	val (xs, ys, zs) = split_list3 xyzs
krauss@19564
    35
    in
krauss@19564
    36
	(x::xs,y::ys,z::zs)
krauss@19564
    37
    end
krauss@19564
    38
krauss@19564
    39
krauss@19564
    40
fun build_tree thy f congs (qs, gs, lhs, rhs) =
krauss@19564
    41
    let
krauss@19564
    42
	(* FIXME: Save precomputed dependencies in a theory data slot *)
krauss@19564
    43
	val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
krauss@19564
    44
    in
krauss@19564
    45
	FundefCtxTree.mk_tree thy congs_deps f rhs
krauss@19564
    46
    end
krauss@19564
    47
krauss@19564
    48
krauss@19564
    49
(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
krauss@19564
    50
fun mk_primed_vars thy glrs =
krauss@19564
    51
    let
krauss@19564
    52
	val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
krauss@19564
    53
krauss@19564
    54
	fun rename_vars (qs,gs,lhs,rhs) =
krauss@19564
    55
	    let
krauss@19564
    56
		val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
krauss@19564
    57
		val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
krauss@19564
    58
	    in
krauss@19564
    59
		(qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
krauss@19564
    60
	    end
krauss@19564
    61
    in
krauss@19564
    62
	map rename_vars glrs
krauss@19564
    63
    end
krauss@19564
    64
krauss@19564
    65
krauss@19564
    66
fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
krauss@19564
    67
    let
krauss@19583
    68
	val Names {domT, G, R, h, f, fvar, used, x, ...} = names
krauss@19564
    69
				 
krauss@19564
    70
	val zv = Var (("z",0), domT) (* for generating h_assums *)
krauss@19564
    71
	val xv = Var (("x",0), domT)
krauss@19564
    72
	val rw_RI_to_h_assum = (mk_mem (mk_prod (zv, xv), R),
krauss@19564
    73
				mk_mem (mk_prod (zv, h $ zv), G))
krauss@19564
    74
	val rw_f_to_h = (f, h)
krauss@19564
    75
			
krauss@19564
    76
	val cqs = map (cterm_of thy) qs
krauss@19564
    77
		  
krauss@19564
    78
	val vqs = map free_to_var qs
krauss@19564
    79
	val cvqs = map (cterm_of thy) vqs
krauss@19564
    80
krauss@19564
    81
	val ags = map (assume o cterm_of thy) gs
krauss@19564
    82
		  
krauss@19564
    83
	val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
krauss@19564
    84
	val cqs' = map (cterm_of thy) qs'
krauss@19564
    85
krauss@19564
    86
	val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
krauss@19564
    87
	val ags' = map (assume o cterm_of thy o rename_vars) gs
krauss@19564
    88
	val lhs' = rename_vars lhs
krauss@19564
    89
	val rhs' = rename_vars rhs
krauss@19564
    90
krauss@19564
    91
	val localize = instantiate ([], cvqs ~~ cqs) 
krauss@19564
    92
					   #> fold implies_elim_swp ags
krauss@19564
    93
krauss@19564
    94
	val GI = freezeT GI
krauss@19564
    95
	val lGI = localize GI
krauss@19564
    96
krauss@19564
    97
	val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI))
krauss@19564
    98
			  
krauss@19564
    99
	fun mk_call_info (RIvs, RI) =
krauss@19564
   100
	    let
krauss@19564
   101
		fun mk_var0 (v,T) = Var ((v,0),T)
krauss@19564
   102
krauss@19564
   103
		val RI = freezeT RI
krauss@19564
   104
		val lRI = localize RI
krauss@19564
   105
		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
krauss@19770
   106
		val plRI = prop_of lRI
krauss@19770
   107
		val GmAs = Logic.strip_imp_prems plRI
krauss@19770
   108
		val rcarg = case Logic.strip_imp_concl plRI of
krauss@19770
   109
				trueprop $ (memb $ (pair $ rcarg $ _) $ R) => rcarg
krauss@19770
   110
			      | _ => raise Match
krauss@19564
   111
			  
krauss@19564
   112
		val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq)
krauss@19564
   113
		val Gh = assume (cterm_of thy Gh_term)
krauss@19564
   114
		val Gh' = assume (cterm_of thy (rename_vars Gh_term))
krauss@19564
   115
	    in
krauss@19770
   116
		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh', GmAs=GmAs, rcarg=rcarg}
krauss@19564
   117
	    end
krauss@19564
   118
krauss@19564
   119
	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
krauss@19564
   120
    in
krauss@19583
   121
	ClauseInfo
krauss@19583
   122
	    {
krauss@19583
   123
	     no=no,
krauss@19583
   124
	     qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
krauss@19583
   125
	     cqs=cqs, cvqs=cvqs, ags=ags,		 
krauss@19583
   126
	     cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
krauss@19583
   127
	     GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
krauss@19583
   128
	     tree=tree, case_hyp = case_hyp
krauss@19583
   129
	    }
krauss@19564
   130
    end
krauss@19564
   131
krauss@19564
   132
krauss@19564
   133
krauss@19564
   134
krauss@19564
   135
(* Chooses fresh free names, declares G and R, defines f and returns a record
krauss@19564
   136
   with all the information *)  
krauss@19770
   137
fun setup_context (f, glrs, used) defname congs thy =
krauss@19564
   138
    let
krauss@19564
   139
	val trees = map (build_tree thy f congs) glrs
krauss@19564
   140
	val allused = fold FundefCtxTree.add_context_varnames trees used
krauss@19564
   141
krauss@19781
   142
	val Const (f_fullname, fT) = f
krauss@19781
   143
	val fname = Sign.base_name f_fullname
krauss@19564
   144
krauss@19564
   145
	val domT = domain_type fT 
krauss@19564
   146
	val ranT = range_type fT
krauss@19564
   147
krauss@19564
   148
	val h = Free (variant allused "h", domT --> ranT)
krauss@19564
   149
	val y = Free (variant allused "y", ranT)
krauss@19564
   150
	val x = Free (variant allused "x", domT)
krauss@19564
   151
	val z = Free (variant allused "z", domT)
krauss@19564
   152
	val a = Free (variant allused "a", domT)
krauss@19564
   153
	val D = Free (variant allused "D", HOLogic.mk_setT domT)
krauss@19564
   154
	val P = Free (variant allused "P", domT --> boolT)
krauss@19564
   155
	val Pbool = Free (variant allused "P", boolT)
krauss@19564
   156
	val fvarname = variant allused "f"
krauss@19564
   157
	val fvar = Free (fvarname, domT --> ranT)
krauss@19564
   158
krauss@19564
   159
	val GT = mk_relT (domT, ranT)
krauss@19564
   160
	val RT = mk_relT (domT, domT)
krauss@19770
   161
	val G_name = defname ^ "_graph"
krauss@19770
   162
	val R_name = defname ^ "_rel"
krauss@19564
   163
krauss@19564
   164
	val glrs' = mk_primed_vars thy glrs
krauss@19564
   165
krauss@19564
   166
	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
krauss@19564
   167
krauss@19781
   168
	val G = Const (Sign.full_name thy G_name, GT)
krauss@19781
   169
	val R = Const (Sign.full_name thy R_name, RT)
krauss@19564
   170
	val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
krauss@19564
   171
krauss@19564
   172
	val f_eq = Logic.mk_equals (f $ x, 
krauss@19564
   173
				    Const ("The", (ranT --> boolT) --> ranT) $
krauss@19564
   174
					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
krauss@19564
   175
krauss@19781
   176
	val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
krauss@19564
   177
    in
krauss@19583
   178
	(Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy)
krauss@19564
   179
    end
krauss@19564
   180
krauss@19564
   181
krauss@19564
   182
(* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
krauss@19564
   183
fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
krauss@19564
   184
    (implies $ Trueprop (mk_eq (lhs, lhs'))
krauss@19564
   185
	     $ Trueprop (mk_eq (rhs, rhs')))
krauss@19564
   186
	|> fold_rev (curry Logic.mk_implies) (gs @ gs')
krauss@19564
   187
krauss@19564
   188
krauss@19564
   189
(* all proof obligations *)
krauss@19564
   190
fun mk_compat_proof_obligations glrs glrs' =
krauss@19564
   191
    map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (upairs (glrs ~~ glrs'))
krauss@19564
   192
krauss@19564
   193
krauss@19564
   194
fun extract_Ris thy congs f R tree (qs, gs, lhs, rhs) =
krauss@19564
   195
    let
krauss@19564
   196
	fun add_Ri2 (fixes,assumes) (_ $ arg) _ (_, x) = ([], (FundefCtxTree.export_term (fixes, map prop_of assumes) (mk_relmem (arg, lhs) R)) :: x)
krauss@19564
   197
	  | add_Ri2 _ _ _ _ = raise Match
krauss@19564
   198
krauss@19564
   199
	val preRis = rev (FundefCtxTree.traverse_tree add_Ri2 tree [])
krauss@19564
   200
	val (vRis, preRis_unq) = split_list (map dest_all_all preRis)
krauss@19564
   201
krauss@19564
   202
	val Ris = map (fold_rev (curry Logic.mk_implies) gs) preRis_unq
krauss@19564
   203
    in
krauss@19564
   204
	(map (map dest_Free) vRis, preRis, Ris)
krauss@19564
   205
    end
krauss@19564
   206
krauss@19564
   207
fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
krauss@19564
   208
    let
krauss@19583
   209
	val Names { domT, R, G, f, fvar, h, y, Pbool, ... } = names
krauss@19564
   210
krauss@19564
   211
	val z = Var (("z",0), domT)
krauss@19564
   212
	val x = Var (("x",0), domT)
krauss@19564
   213
krauss@19564
   214
	val rew1 = (mk_mem (mk_prod (z, x), R),
krauss@19564
   215
		    mk_mem (mk_prod (z, fvar $ z), G))
krauss@19564
   216
	val rew2 = (f, fvar)
krauss@19564
   217
krauss@19564
   218
	val prems = map (Pattern.rewrite_term thy [rew1, rew2] []) Ris
krauss@19564
   219
	val rhs' = Pattern.rewrite_term thy [rew2] [] rhs 
krauss@19564
   220
    in
krauss@19564
   221
	mk_relmem (lhs, rhs') G
krauss@19564
   222
		  |> fold_rev (curry Logic.mk_implies) prems
krauss@19564
   223
		  |> fold_rev (curry Logic.mk_implies) gs
krauss@19564
   224
    end
krauss@19564
   225
krauss@19564
   226
fun mk_completeness names glrs =
krauss@19564
   227
    let
krauss@19583
   228
	val Names {domT, x, Pbool, ...} = names
krauss@19564
   229
krauss@19564
   230
	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
krauss@19564
   231
						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
krauss@19564
   232
						|> fold_rev (curry Logic.mk_implies) gs
krauss@19564
   233
						|> fold_rev mk_forall qs
krauss@19564
   234
    in
krauss@19564
   235
	Trueprop Pbool
krauss@19564
   236
		 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
krauss@19564
   237
    end
krauss@19564
   238
krauss@19564
   239
krauss@19564
   240
fun extract_conditions thy names trees congs =
krauss@19564
   241
    let
krauss@19781
   242
	val Names {f, R, glrs, glrs', ...} = names
krauss@19564
   243
krauss@19564
   244
	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
krauss@19564
   245
	val Gis = map2 (mk_GIntro thy names) glrs preRiss
krauss@19564
   246
	val complete = mk_completeness names glrs
krauss@19564
   247
	val compat = mk_compat_proof_obligations glrs glrs'
krauss@19564
   248
    in
krauss@19564
   249
	{G_intros = Gis, vRiss = vRiss, R_intross = Riss, complete = complete, compat = compat}
krauss@19564
   250
    end
krauss@19564
   251
krauss@19564
   252
krauss@19564
   253
fun inductive_def defs (thy, const) =
krauss@19564
   254
    let
krauss@19564
   255
 	val (thy, {intrs, elims = [elim], ...}) = 
krauss@19564
   256
	    InductivePackage.add_inductive_i true (*verbose*)
krauss@19564
   257
					     false (*add_consts*)
krauss@19564
   258
					     "" (* no altname *)
krauss@19564
   259
					     false (* no coind *)
krauss@19564
   260
					     false (* elims, please *)
krauss@19564
   261
					     false (* induction thm please *)
krauss@19564
   262
					     [const] (* the constant *)
krauss@19564
   263
					     (map (fn t=>(("", t),[])) defs) (* the intros *)
krauss@19564
   264
					     [] (* no special monos *)
krauss@19564
   265
					     thy
krauss@19564
   266
    in
krauss@19564
   267
	(intrs, (thy, elim))
krauss@19564
   268
    end
krauss@19564
   269
krauss@19564
   270
krauss@19564
   271
krauss@19564
   272
(*
krauss@19564
   273
 * This is the first step in a function definition.
krauss@19564
   274
 *
krauss@19564
   275
 * Defines the function, the graph and the termination relation, synthesizes completeness
krauss@19564
   276
 * and comatibility conditions and returns everything.
krauss@19564
   277
 *)
krauss@19773
   278
fun prepare_fundef thy congs defname f glrs used =
krauss@19770
   279
    let
krauss@19770
   280
	val (names, thy) = setup_context (f, glrs, used) defname congs thy
krauss@19770
   281
	val Names {G, R, glrs, trees, ...} = names
krauss@19770
   282
krauss@19770
   283
	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
krauss@19770
   284
krauss@19770
   285
	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
krauss@19770
   286
	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
krauss@19770
   287
krauss@19770
   288
	val n = length glrs
krauss@19770
   289
	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
krauss@19770
   290
    in
krauss@19770
   291
	(Prep {names = names, complete=complete, compat=compat, clauses = clauses},
krauss@19770
   292
	 thy) 
krauss@19770
   293
    end
krauss@19770
   294
krauss@19770
   295
krauss@19770
   296
krauss@19770
   297
krauss@19564
   298
end