src/HOL/Tools/function_package/fundef_prep.ML
author krauss
Sun May 07 00:00:13 2006 +0200 (2006-05-07)
changeset 19583 c5fa77b03442
parent 19564 d3e2f532459a
child 19770 be5c23ebe1eb
permissions -rw-r--r--
function-package: Changed record usage to make sml/nj happy...
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@19564
    12
    val prepare_fundef_curried : thm list -> term list -> theory
krauss@19564
    13
				 -> FundefCommon.curry_info option * xstring * (FundefCommon.prep_result * theory)
krauss@19564
    14
end
krauss@19564
    15
krauss@19564
    16
krauss@19564
    17
krauss@19564
    18
krauss@19564
    19
krauss@19564
    20
structure FundefPrep : FUNDEF_PREP =
krauss@19564
    21
struct
krauss@19564
    22
krauss@19564
    23
krauss@19564
    24
open FundefCommon
krauss@19564
    25
open FundefAbbrev 
krauss@19564
    26
krauss@19564
    27
krauss@19564
    28
krauss@19564
    29
krauss@19564
    30
fun split_list3 [] = ([],[],[])
krauss@19564
    31
  | split_list3 ((x,y,z)::xyzs) = 
krauss@19564
    32
    let
krauss@19564
    33
	val (xs, ys, zs) = split_list3 xyzs
krauss@19564
    34
    in
krauss@19564
    35
	(x::xs,y::ys,z::zs)
krauss@19564
    36
    end
krauss@19564
    37
krauss@19564
    38
krauss@19564
    39
fun build_tree thy f congs (qs, gs, lhs, rhs) =
krauss@19564
    40
    let
krauss@19564
    41
	(* FIXME: Save precomputed dependencies in a theory data slot *)
krauss@19564
    42
	val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
krauss@19564
    43
    in
krauss@19564
    44
	FundefCtxTree.mk_tree thy congs_deps f rhs
krauss@19564
    45
    end
krauss@19564
    46
krauss@19564
    47
krauss@19564
    48
fun analyze_eqs eqs =
krauss@19564
    49
    let
krauss@19564
    50
	fun dest_geq geq = 
krauss@19564
    51
	    let
krauss@19564
    52
		val qs = add_term_frees (geq, [])
krauss@19564
    53
	    in
krauss@19564
    54
		case dest_implies_list geq of
krauss@19564
    55
		    (gs, Const ("Trueprop", _) $ (Const ("op =", _) $ (f $ lhs) $ rhs)) => 
krauss@19564
    56
		    (f, (qs, gs, lhs, rhs))
krauss@19564
    57
		  | _ => raise ERROR "Not a guarded equation"
krauss@19564
    58
	    end
krauss@19564
    59
			       
krauss@19564
    60
	val (fs, glrs) = split_list (map dest_geq eqs)
krauss@19564
    61
			 
krauss@19564
    62
	val f = (hd fs) (* should be equal and a constant... check! *)
krauss@19564
    63
krauss@19564
    64
	val used = fold (curry add_term_names) eqs [] (* all names in the eqs *)
krauss@19564
    65
		   (* Must check for recursive calls in guards and new vars in rhss *)
krauss@19564
    66
    in
krauss@19564
    67
	(f, glrs, used)
krauss@19564
    68
    end
krauss@19564
    69
krauss@19564
    70
krauss@19564
    71
(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
krauss@19564
    72
fun mk_primed_vars thy glrs =
krauss@19564
    73
    let
krauss@19564
    74
	val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
krauss@19564
    75
krauss@19564
    76
	fun rename_vars (qs,gs,lhs,rhs) =
krauss@19564
    77
	    let
krauss@19564
    78
		val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
krauss@19564
    79
		val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
krauss@19564
    80
	    in
krauss@19564
    81
		(qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
krauss@19564
    82
	    end
krauss@19564
    83
    in
krauss@19564
    84
	map rename_vars glrs
krauss@19564
    85
    end
krauss@19564
    86
krauss@19564
    87
krauss@19564
    88
fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
krauss@19564
    89
    let
krauss@19583
    90
	val Names {domT, G, R, h, f, fvar, used, x, ...} = names
krauss@19564
    91
				 
krauss@19564
    92
	val zv = Var (("z",0), domT) (* for generating h_assums *)
krauss@19564
    93
	val xv = Var (("x",0), domT)
krauss@19564
    94
	val rw_RI_to_h_assum = (mk_mem (mk_prod (zv, xv), R),
krauss@19564
    95
				mk_mem (mk_prod (zv, h $ zv), G))
krauss@19564
    96
	val rw_f_to_h = (f, h)
krauss@19564
    97
			
krauss@19564
    98
	val cqs = map (cterm_of thy) qs
krauss@19564
    99
		  
krauss@19564
   100
	val vqs = map free_to_var qs
krauss@19564
   101
	val cvqs = map (cterm_of thy) vqs
krauss@19564
   102
krauss@19564
   103
	val ags = map (assume o cterm_of thy) gs
krauss@19564
   104
		  
krauss@19564
   105
	val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
krauss@19564
   106
	val cqs' = map (cterm_of thy) qs'
krauss@19564
   107
krauss@19564
   108
	val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
krauss@19564
   109
	val ags' = map (assume o cterm_of thy o rename_vars) gs
krauss@19564
   110
	val lhs' = rename_vars lhs
krauss@19564
   111
	val rhs' = rename_vars rhs
krauss@19564
   112
krauss@19564
   113
	val localize = instantiate ([], cvqs ~~ cqs) 
krauss@19564
   114
					   #> fold implies_elim_swp ags
krauss@19564
   115
krauss@19564
   116
	val GI = freezeT GI
krauss@19564
   117
	val lGI = localize GI
krauss@19564
   118
krauss@19564
   119
	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
   120
			  
krauss@19564
   121
	fun mk_call_info (RIvs, RI) =
krauss@19564
   122
	    let
krauss@19564
   123
		fun mk_var0 (v,T) = Var ((v,0),T)
krauss@19564
   124
krauss@19564
   125
		val RI = freezeT RI
krauss@19564
   126
		val lRI = localize RI
krauss@19564
   127
		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
krauss@19564
   128
			  
krauss@19564
   129
		val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq)
krauss@19564
   130
		val Gh = assume (cterm_of thy Gh_term)
krauss@19564
   131
		val Gh' = assume (cterm_of thy (rename_vars Gh_term))
krauss@19564
   132
	    in
krauss@19583
   133
		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
krauss@19564
   134
	    end
krauss@19564
   135
krauss@19564
   136
	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
krauss@19564
   137
    in
krauss@19583
   138
	ClauseInfo
krauss@19583
   139
	    {
krauss@19583
   140
	     no=no,
krauss@19583
   141
	     qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
krauss@19583
   142
	     cqs=cqs, cvqs=cvqs, ags=ags,		 
krauss@19583
   143
	     cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
krauss@19583
   144
	     GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
krauss@19583
   145
	     tree=tree, case_hyp = case_hyp
krauss@19583
   146
	    }
krauss@19564
   147
    end
krauss@19564
   148
krauss@19564
   149
krauss@19564
   150
krauss@19564
   151
krauss@19564
   152
(* Chooses fresh free names, declares G and R, defines f and returns a record
krauss@19564
   153
   with all the information *)  
krauss@19564
   154
fun setup_context (f, glrs, used) fname congs thy =
krauss@19564
   155
    let
krauss@19564
   156
	val trees = map (build_tree thy f congs) glrs
krauss@19564
   157
	val allused = fold FundefCtxTree.add_context_varnames trees used
krauss@19564
   158
krauss@19564
   159
	val Const (f_proper_name, fT) = f
krauss@19564
   160
	val fxname = Sign.extern_const thy f_proper_name
krauss@19564
   161
krauss@19564
   162
	val domT = domain_type fT 
krauss@19564
   163
	val ranT = range_type fT
krauss@19564
   164
krauss@19564
   165
	val h = Free (variant allused "h", domT --> ranT)
krauss@19564
   166
	val y = Free (variant allused "y", ranT)
krauss@19564
   167
	val x = Free (variant allused "x", domT)
krauss@19564
   168
	val z = Free (variant allused "z", domT)
krauss@19564
   169
	val a = Free (variant allused "a", domT)
krauss@19564
   170
	val D = Free (variant allused "D", HOLogic.mk_setT domT)
krauss@19564
   171
	val P = Free (variant allused "P", domT --> boolT)
krauss@19564
   172
	val Pbool = Free (variant allused "P", boolT)
krauss@19564
   173
	val fvarname = variant allused "f"
krauss@19564
   174
	val fvar = Free (fvarname, domT --> ranT)
krauss@19564
   175
krauss@19564
   176
	val GT = mk_relT (domT, ranT)
krauss@19564
   177
	val RT = mk_relT (domT, domT)
krauss@19564
   178
	val G_name = fname ^ "_graph"
krauss@19564
   179
	val R_name = fname ^ "_rel"
krauss@19564
   180
krauss@19564
   181
	val glrs' = mk_primed_vars thy glrs
krauss@19564
   182
krauss@19564
   183
	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
krauss@19564
   184
krauss@19564
   185
	val G = Const (Sign.intern_const thy G_name, GT)
krauss@19564
   186
	val R = Const (Sign.intern_const thy R_name, RT)
krauss@19564
   187
	val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
krauss@19564
   188
krauss@19564
   189
	val f_eq = Logic.mk_equals (f $ x, 
krauss@19564
   190
				    Const ("The", (ranT --> boolT) --> ranT) $
krauss@19564
   191
					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
krauss@19564
   192
krauss@19564
   193
	val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
krauss@19564
   194
    in
krauss@19583
   195
	(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
   196
    end
krauss@19564
   197
krauss@19564
   198
krauss@19564
   199
(* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
krauss@19564
   200
fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
krauss@19564
   201
    (implies $ Trueprop (mk_eq (lhs, lhs'))
krauss@19564
   202
	     $ Trueprop (mk_eq (rhs, rhs')))
krauss@19564
   203
	|> fold_rev (curry Logic.mk_implies) (gs @ gs')
krauss@19564
   204
krauss@19564
   205
krauss@19564
   206
(* all proof obligations *)
krauss@19564
   207
fun mk_compat_proof_obligations glrs glrs' =
krauss@19564
   208
    map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (upairs (glrs ~~ glrs'))
krauss@19564
   209
krauss@19564
   210
krauss@19564
   211
fun extract_Ris thy congs f R tree (qs, gs, lhs, rhs) =
krauss@19564
   212
    let
krauss@19564
   213
	fun add_Ri2 (fixes,assumes) (_ $ arg) _ (_, x) = ([], (FundefCtxTree.export_term (fixes, map prop_of assumes) (mk_relmem (arg, lhs) R)) :: x)
krauss@19564
   214
	  | add_Ri2 _ _ _ _ = raise Match
krauss@19564
   215
krauss@19564
   216
	val preRis = rev (FundefCtxTree.traverse_tree add_Ri2 tree [])
krauss@19564
   217
	val (vRis, preRis_unq) = split_list (map dest_all_all preRis)
krauss@19564
   218
krauss@19564
   219
	val Ris = map (fold_rev (curry Logic.mk_implies) gs) preRis_unq
krauss@19564
   220
    in
krauss@19564
   221
	(map (map dest_Free) vRis, preRis, Ris)
krauss@19564
   222
    end
krauss@19564
   223
krauss@19564
   224
fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
krauss@19564
   225
    let
krauss@19583
   226
	val Names { domT, R, G, f, fvar, h, y, Pbool, ... } = names
krauss@19564
   227
krauss@19564
   228
	val z = Var (("z",0), domT)
krauss@19564
   229
	val x = Var (("x",0), domT)
krauss@19564
   230
krauss@19564
   231
	val rew1 = (mk_mem (mk_prod (z, x), R),
krauss@19564
   232
		    mk_mem (mk_prod (z, fvar $ z), G))
krauss@19564
   233
	val rew2 = (f, fvar)
krauss@19564
   234
krauss@19564
   235
	val prems = map (Pattern.rewrite_term thy [rew1, rew2] []) Ris
krauss@19564
   236
	val rhs' = Pattern.rewrite_term thy [rew2] [] rhs 
krauss@19564
   237
    in
krauss@19564
   238
	mk_relmem (lhs, rhs') G
krauss@19564
   239
		  |> fold_rev (curry Logic.mk_implies) prems
krauss@19564
   240
		  |> fold_rev (curry Logic.mk_implies) gs
krauss@19564
   241
    end
krauss@19564
   242
krauss@19564
   243
fun mk_completeness names glrs =
krauss@19564
   244
    let
krauss@19583
   245
	val Names {domT, x, Pbool, ...} = names
krauss@19564
   246
krauss@19564
   247
	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
krauss@19564
   248
						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
krauss@19564
   249
						|> fold_rev (curry Logic.mk_implies) gs
krauss@19564
   250
						|> fold_rev mk_forall qs
krauss@19564
   251
    in
krauss@19564
   252
	Trueprop Pbool
krauss@19564
   253
		 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
krauss@19564
   254
    end
krauss@19564
   255
krauss@19564
   256
krauss@19564
   257
fun extract_conditions thy names trees congs =
krauss@19564
   258
    let
krauss@19583
   259
	val Names {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
krauss@19564
   260
krauss@19564
   261
	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
krauss@19564
   262
	val Gis = map2 (mk_GIntro thy names) glrs preRiss
krauss@19564
   263
	val complete = mk_completeness names glrs
krauss@19564
   264
	val compat = mk_compat_proof_obligations glrs glrs'
krauss@19564
   265
    in
krauss@19564
   266
	{G_intros = Gis, vRiss = vRiss, R_intross = Riss, complete = complete, compat = compat}
krauss@19564
   267
    end
krauss@19564
   268
krauss@19564
   269
krauss@19564
   270
fun inductive_def defs (thy, const) =
krauss@19564
   271
    let
krauss@19564
   272
 	val (thy, {intrs, elims = [elim], ...}) = 
krauss@19564
   273
	    InductivePackage.add_inductive_i true (*verbose*)
krauss@19564
   274
					     false (*add_consts*)
krauss@19564
   275
					     "" (* no altname *)
krauss@19564
   276
					     false (* no coind *)
krauss@19564
   277
					     false (* elims, please *)
krauss@19564
   278
					     false (* induction thm please *)
krauss@19564
   279
					     [const] (* the constant *)
krauss@19564
   280
					     (map (fn t=>(("", t),[])) defs) (* the intros *)
krauss@19564
   281
					     [] (* no special monos *)
krauss@19564
   282
					     thy
krauss@19564
   283
    in
krauss@19564
   284
	(intrs, (thy, elim))
krauss@19564
   285
    end
krauss@19564
   286
krauss@19564
   287
krauss@19564
   288
krauss@19564
   289
(*
krauss@19564
   290
 * This is the first step in a function definition.
krauss@19564
   291
 *
krauss@19564
   292
 * Defines the function, the graph and the termination relation, synthesizes completeness
krauss@19564
   293
 * and comatibility conditions and returns everything.
krauss@19564
   294
 *)
krauss@19564
   295
fun prepare_fundef congs eqs fname thy =
krauss@19564
   296
    let
krauss@19564
   297
	val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
krauss@19583
   298
	val Names {G, R, glrs, trees, ...} = names
krauss@19564
   299
krauss@19564
   300
	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
krauss@19564
   301
krauss@19564
   302
	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
krauss@19564
   303
	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
krauss@19564
   304
krauss@19564
   305
	val n = length glrs
krauss@19564
   306
	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
krauss@19564
   307
    in
krauss@19583
   308
	(Prep {names = names, complete=complete, compat=compat, clauses = clauses},
krauss@19564
   309
	 thy) 
krauss@19564
   310
    end
krauss@19564
   311
krauss@19564
   312
krauss@19564
   313
krauss@19564
   314
krauss@19564
   315
fun prepare_fundef_curried congs eqs thy =
krauss@19564
   316
    let
krauss@19564
   317
	val lhs1 = hd eqs
krauss@19564
   318
		   |> dest_implies_list |> snd
krauss@19564
   319
		   |> HOLogic.dest_Trueprop
krauss@19564
   320
		   |> HOLogic.dest_eq |> fst
krauss@19564
   321
krauss@19564
   322
	val (f, args) = strip_comb lhs1
krauss@19564
   323
	val Const(fname, fT) = f
krauss@19564
   324
	val fxname = Sign.extern_const thy fname
krauss@19564
   325
    in
krauss@19564
   326
	if (length args < 2)
krauss@19564
   327
	then (NONE, fxname, (prepare_fundef congs eqs fxname thy))
krauss@19564
   328
	else
krauss@19564
   329
	    let
krauss@19564
   330
		val (caTs, uaTs) = chop (length args) (binder_types fT)
krauss@19564
   331
		val newtype = foldr1 HOLogic.mk_prodT caTs --> (uaTs ---> body_type fT)
krauss@19564
   332
		val gxname = fxname ^ "_tupled"
krauss@19564
   333
			     
krauss@19564
   334
    		val thy = Sign.add_consts_i [(gxname, newtype, NoSyn)] thy
krauss@19564
   335
		val gc = Const (Sign.intern_const thy gxname, newtype)
krauss@19564
   336
			 
krauss@19564
   337
		val vars = map2 (fn i => fn T => Free ("x"^(string_of_int i), T))
krauss@19564
   338
				(1 upto (length caTs)) caTs
krauss@19564
   339
krauss@19564
   340
		val f_lambda = fold_rev lambda vars (gc $ foldr1 HOLogic.mk_prod vars)
krauss@19564
   341
			       
krauss@19564
   342
		val def = Logic.mk_equals (fold (curry ((op $) o Library.swap)) vars f,
krauss@19564
   343
					   gc $ foldr1 HOLogic.mk_prod vars)
krauss@19564
   344
			  
krauss@19564
   345
		val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
krauss@19564
   346
				      
krauss@19564
   347
		val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def]
krauss@19564
   348
		val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs
krauss@19564
   349
	    in
krauss@19583
   350
		(SOME (Curry {curry_ss = g_to_f_ss, argTs = caTs}), fxname, prepare_fundef congs eqs_tupled fxname thy)
krauss@19564
   351
	    end
krauss@19564
   352
    end
krauss@19564
   353
krauss@19564
   354
krauss@19564
   355
krauss@19564
   356
end