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