src/HOL/Tools/function_package/fundef_prep.ML
author krauss
Fri May 05 17:17:21 2006 +0200 (2006-05-05)
changeset 19564 d3e2f532459a
child 19583 c5fa77b03442
permissions -rw-r--r--
First usable version of the new function definition package (HOL/function_packake/...).
Moved Accessible_Part.thy from Library to Main.
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@19564
    90
	val {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@19564
   133
		{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@19564
   138
	{
krauss@19564
   139
	 no=no,
krauss@19564
   140
	 qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
krauss@19564
   141
	 cqs=cqs, cvqs=cvqs, ags=ags,		 
krauss@19564
   142
	 cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
krauss@19564
   143
	 GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
krauss@19564
   144
	 tree=tree, case_hyp = case_hyp
krauss@19564
   145
	}
krauss@19564
   146
    end
krauss@19564
   147
krauss@19564
   148
krauss@19564
   149
krauss@19564
   150
krauss@19564
   151
(* Chooses fresh free names, declares G and R, defines f and returns a record
krauss@19564
   152
   with all the information *)  
krauss@19564
   153
fun setup_context (f, glrs, used) fname congs thy =
krauss@19564
   154
    let
krauss@19564
   155
	val trees = map (build_tree thy f congs) glrs
krauss@19564
   156
	val allused = fold FundefCtxTree.add_context_varnames trees used
krauss@19564
   157
krauss@19564
   158
	val Const (f_proper_name, fT) = f
krauss@19564
   159
	val fxname = Sign.extern_const thy f_proper_name
krauss@19564
   160
krauss@19564
   161
	val domT = domain_type fT 
krauss@19564
   162
	val ranT = range_type fT
krauss@19564
   163
krauss@19564
   164
	val h = Free (variant allused "h", domT --> ranT)
krauss@19564
   165
	val y = Free (variant allused "y", ranT)
krauss@19564
   166
	val x = Free (variant allused "x", domT)
krauss@19564
   167
	val z = Free (variant allused "z", domT)
krauss@19564
   168
	val a = Free (variant allused "a", domT)
krauss@19564
   169
	val D = Free (variant allused "D", HOLogic.mk_setT domT)
krauss@19564
   170
	val P = Free (variant allused "P", domT --> boolT)
krauss@19564
   171
	val Pbool = Free (variant allused "P", boolT)
krauss@19564
   172
	val fvarname = variant allused "f"
krauss@19564
   173
	val fvar = Free (fvarname, domT --> ranT)
krauss@19564
   174
krauss@19564
   175
	val GT = mk_relT (domT, ranT)
krauss@19564
   176
	val RT = mk_relT (domT, domT)
krauss@19564
   177
	val G_name = fname ^ "_graph"
krauss@19564
   178
	val R_name = fname ^ "_rel"
krauss@19564
   179
krauss@19564
   180
	val glrs' = mk_primed_vars thy glrs
krauss@19564
   181
krauss@19564
   182
	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
krauss@19564
   183
krauss@19564
   184
	val G = Const (Sign.intern_const thy G_name, GT)
krauss@19564
   185
	val R = Const (Sign.intern_const thy R_name, RT)
krauss@19564
   186
	val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
krauss@19564
   187
krauss@19564
   188
	val f_eq = Logic.mk_equals (f $ x, 
krauss@19564
   189
				    Const ("The", (ranT --> boolT) --> ranT) $
krauss@19564
   190
					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
krauss@19564
   191
krauss@19564
   192
	val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
krauss@19564
   193
    in
krauss@19564
   194
	({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
   195
    end
krauss@19564
   196
krauss@19564
   197
krauss@19564
   198
(* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
krauss@19564
   199
fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
krauss@19564
   200
    (implies $ Trueprop (mk_eq (lhs, lhs'))
krauss@19564
   201
	     $ Trueprop (mk_eq (rhs, rhs')))
krauss@19564
   202
	|> fold_rev (curry Logic.mk_implies) (gs @ gs')
krauss@19564
   203
krauss@19564
   204
krauss@19564
   205
(* all proof obligations *)
krauss@19564
   206
fun mk_compat_proof_obligations glrs glrs' =
krauss@19564
   207
    map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (upairs (glrs ~~ glrs'))
krauss@19564
   208
krauss@19564
   209
krauss@19564
   210
fun extract_Ris thy congs f R tree (qs, gs, lhs, rhs) =
krauss@19564
   211
    let
krauss@19564
   212
	fun add_Ri2 (fixes,assumes) (_ $ arg) _ (_, x) = ([], (FundefCtxTree.export_term (fixes, map prop_of assumes) (mk_relmem (arg, lhs) R)) :: x)
krauss@19564
   213
	  | add_Ri2 _ _ _ _ = raise Match
krauss@19564
   214
krauss@19564
   215
	val preRis = rev (FundefCtxTree.traverse_tree add_Ri2 tree [])
krauss@19564
   216
	val (vRis, preRis_unq) = split_list (map dest_all_all preRis)
krauss@19564
   217
krauss@19564
   218
	val Ris = map (fold_rev (curry Logic.mk_implies) gs) preRis_unq
krauss@19564
   219
    in
krauss@19564
   220
	(map (map dest_Free) vRis, preRis, Ris)
krauss@19564
   221
    end
krauss@19564
   222
krauss@19564
   223
fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
krauss@19564
   224
    let
krauss@19564
   225
	val { domT, R, G, f, fvar, h, y, Pbool, ... } = names
krauss@19564
   226
krauss@19564
   227
	val z = Var (("z",0), domT)
krauss@19564
   228
	val x = Var (("x",0), domT)
krauss@19564
   229
krauss@19564
   230
	val rew1 = (mk_mem (mk_prod (z, x), R),
krauss@19564
   231
		    mk_mem (mk_prod (z, fvar $ z), G))
krauss@19564
   232
	val rew2 = (f, fvar)
krauss@19564
   233
krauss@19564
   234
	val prems = map (Pattern.rewrite_term thy [rew1, rew2] []) Ris
krauss@19564
   235
	val rhs' = Pattern.rewrite_term thy [rew2] [] rhs 
krauss@19564
   236
    in
krauss@19564
   237
	mk_relmem (lhs, rhs') G
krauss@19564
   238
		  |> fold_rev (curry Logic.mk_implies) prems
krauss@19564
   239
		  |> fold_rev (curry Logic.mk_implies) gs
krauss@19564
   240
    end
krauss@19564
   241
krauss@19564
   242
fun mk_completeness names glrs =
krauss@19564
   243
    let
krauss@19564
   244
	val {domT, x, Pbool, ...} = names
krauss@19564
   245
krauss@19564
   246
	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
krauss@19564
   247
						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
krauss@19564
   248
						|> fold_rev (curry Logic.mk_implies) gs
krauss@19564
   249
						|> fold_rev mk_forall qs
krauss@19564
   250
    in
krauss@19564
   251
	Trueprop Pbool
krauss@19564
   252
		 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
krauss@19564
   253
    end
krauss@19564
   254
krauss@19564
   255
krauss@19564
   256
fun extract_conditions thy names trees congs =
krauss@19564
   257
    let
krauss@19564
   258
	val {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
krauss@19564
   259
krauss@19564
   260
	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
krauss@19564
   261
	val Gis = map2 (mk_GIntro thy names) glrs preRiss
krauss@19564
   262
	val complete = mk_completeness names glrs
krauss@19564
   263
	val compat = mk_compat_proof_obligations glrs glrs'
krauss@19564
   264
    in
krauss@19564
   265
	{G_intros = Gis, vRiss = vRiss, R_intross = Riss, complete = complete, compat = compat}
krauss@19564
   266
    end
krauss@19564
   267
krauss@19564
   268
krauss@19564
   269
fun inductive_def defs (thy, const) =
krauss@19564
   270
    let
krauss@19564
   271
 	val (thy, {intrs, elims = [elim], ...}) = 
krauss@19564
   272
	    InductivePackage.add_inductive_i true (*verbose*)
krauss@19564
   273
					     false (*add_consts*)
krauss@19564
   274
					     "" (* no altname *)
krauss@19564
   275
					     false (* no coind *)
krauss@19564
   276
					     false (* elims, please *)
krauss@19564
   277
					     false (* induction thm please *)
krauss@19564
   278
					     [const] (* the constant *)
krauss@19564
   279
					     (map (fn t=>(("", t),[])) defs) (* the intros *)
krauss@19564
   280
					     [] (* no special monos *)
krauss@19564
   281
					     thy
krauss@19564
   282
    in
krauss@19564
   283
	(intrs, (thy, elim))
krauss@19564
   284
    end
krauss@19564
   285
krauss@19564
   286
krauss@19564
   287
krauss@19564
   288
(*
krauss@19564
   289
 * This is the first step in a function definition.
krauss@19564
   290
 *
krauss@19564
   291
 * Defines the function, the graph and the termination relation, synthesizes completeness
krauss@19564
   292
 * and comatibility conditions and returns everything.
krauss@19564
   293
 *)
krauss@19564
   294
fun prepare_fundef congs eqs fname thy =
krauss@19564
   295
    let
krauss@19564
   296
	val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
krauss@19564
   297
	val {G, R, glrs, trees, ...} = names
krauss@19564
   298
krauss@19564
   299
	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
krauss@19564
   300
krauss@19564
   301
	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
krauss@19564
   302
	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
krauss@19564
   303
krauss@19564
   304
	val n = length glrs
krauss@19564
   305
	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
   306
    in
krauss@19564
   307
	({names = names, complete=complete, compat=compat, clauses = clauses},
krauss@19564
   308
	 thy) 
krauss@19564
   309
    end
krauss@19564
   310
krauss@19564
   311
krauss@19564
   312
krauss@19564
   313
krauss@19564
   314
fun prepare_fundef_curried congs eqs thy =
krauss@19564
   315
    let
krauss@19564
   316
	val lhs1 = hd eqs
krauss@19564
   317
		   |> dest_implies_list |> snd
krauss@19564
   318
		   |> HOLogic.dest_Trueprop
krauss@19564
   319
		   |> HOLogic.dest_eq |> fst
krauss@19564
   320
krauss@19564
   321
	val (f, args) = strip_comb lhs1
krauss@19564
   322
	val Const(fname, fT) = f
krauss@19564
   323
	val fxname = Sign.extern_const thy fname
krauss@19564
   324
    in
krauss@19564
   325
	if (length args < 2)
krauss@19564
   326
	then (NONE, fxname, (prepare_fundef congs eqs fxname thy))
krauss@19564
   327
	else
krauss@19564
   328
	    let
krauss@19564
   329
		val (caTs, uaTs) = chop (length args) (binder_types fT)
krauss@19564
   330
		val newtype = foldr1 HOLogic.mk_prodT caTs --> (uaTs ---> body_type fT)
krauss@19564
   331
		val gxname = fxname ^ "_tupled"
krauss@19564
   332
			     
krauss@19564
   333
    		val thy = Sign.add_consts_i [(gxname, newtype, NoSyn)] thy
krauss@19564
   334
		val gc = Const (Sign.intern_const thy gxname, newtype)
krauss@19564
   335
			 
krauss@19564
   336
		val vars = map2 (fn i => fn T => Free ("x"^(string_of_int i), T))
krauss@19564
   337
				(1 upto (length caTs)) caTs
krauss@19564
   338
krauss@19564
   339
		val f_lambda = fold_rev lambda vars (gc $ foldr1 HOLogic.mk_prod vars)
krauss@19564
   340
			       
krauss@19564
   341
		val def = Logic.mk_equals (fold (curry ((op $) o Library.swap)) vars f,
krauss@19564
   342
					   gc $ foldr1 HOLogic.mk_prod vars)
krauss@19564
   343
			  
krauss@19564
   344
		val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
krauss@19564
   345
				      
krauss@19564
   346
		val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def]
krauss@19564
   347
		val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs
krauss@19564
   348
	    in
krauss@19564
   349
		(SOME {curry_ss = g_to_f_ss, argTs = caTs}, fxname, prepare_fundef congs eqs_tupled fxname thy)
krauss@19564
   350
	    end
krauss@19564
   351
    end
krauss@19564
   352
krauss@19564
   353
krauss@19564
   354
krauss@19564
   355
end