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