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