src/HOL/Tools/function_package/fundef_prep.ML
author krauss
Tue Jun 06 08:21:14 2006 +0200 (2006-06-06)
changeset 19781 c62720b20e9a
parent 19773 ebc3b67fbd2c
child 19876 11d447d5d68c
permissions -rw-r--r--
HOL/Tools/function_package: More cleanup
     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 : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
    13 			 -> FundefCommon.prep_result * theory
    14 
    15 end
    16 
    17 
    18 
    19 
    20 
    21 structure FundefPrep : FUNDEF_PREP =
    22 struct
    23 
    24 
    25 open FundefCommon
    26 open FundefAbbrev 
    27 
    28 
    29 
    30 
    31 fun split_list3 [] = ([],[],[])
    32   | split_list3 ((x,y,z)::xyzs) = 
    33     let
    34 	val (xs, ys, zs) = split_list3 xyzs
    35     in
    36 	(x::xs,y::ys,z::zs)
    37     end
    38 
    39 
    40 fun build_tree thy f congs (qs, gs, lhs, rhs) =
    41     let
    42 	(* FIXME: Save precomputed dependencies in a theory data slot *)
    43 	val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
    44     in
    45 	FundefCtxTree.mk_tree thy congs_deps f rhs
    46     end
    47 
    48 
    49 (* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
    50 fun mk_primed_vars thy glrs =
    51     let
    52 	val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
    53 
    54 	fun rename_vars (qs,gs,lhs,rhs) =
    55 	    let
    56 		val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
    57 		val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
    58 	    in
    59 		(qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
    60 	    end
    61     in
    62 	map rename_vars glrs
    63     end
    64 
    65 
    66 fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
    67     let
    68 	val Names {domT, G, R, h, f, fvar, used, x, ...} = names
    69 				 
    70 	val zv = Var (("z",0), domT) (* for generating h_assums *)
    71 	val xv = Var (("x",0), domT)
    72 	val rw_RI_to_h_assum = (mk_mem (mk_prod (zv, xv), R),
    73 				mk_mem (mk_prod (zv, h $ zv), G))
    74 	val rw_f_to_h = (f, h)
    75 			
    76 	val cqs = map (cterm_of thy) qs
    77 		  
    78 	val vqs = map free_to_var qs
    79 	val cvqs = map (cterm_of thy) vqs
    80 
    81 	val ags = map (assume o cterm_of thy) gs
    82 		  
    83 	val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
    84 	val cqs' = map (cterm_of thy) qs'
    85 
    86 	val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
    87 	val ags' = map (assume o cterm_of thy o rename_vars) gs
    88 	val lhs' = rename_vars lhs
    89 	val rhs' = rename_vars rhs
    90 
    91 	val localize = instantiate ([], cvqs ~~ cqs) 
    92 					   #> fold implies_elim_swp ags
    93 
    94 	val GI = freezeT GI
    95 	val lGI = localize GI
    96 
    97 	val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI))
    98 			  
    99 	fun mk_call_info (RIvs, RI) =
   100 	    let
   101 		fun mk_var0 (v,T) = Var ((v,0),T)
   102 
   103 		val RI = freezeT RI
   104 		val lRI = localize RI
   105 		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
   106 		val plRI = prop_of lRI
   107 		val GmAs = Logic.strip_imp_prems plRI
   108 		val rcarg = case Logic.strip_imp_concl plRI of
   109 				trueprop $ (memb $ (pair $ rcarg $ _) $ R) => rcarg
   110 			      | _ => raise Match
   111 			  
   112 		val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq)
   113 		val Gh = assume (cterm_of thy Gh_term)
   114 		val Gh' = assume (cterm_of thy (rename_vars Gh_term))
   115 	    in
   116 		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh', GmAs=GmAs, rcarg=rcarg}
   117 	    end
   118 
   119 	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   120     in
   121 	ClauseInfo
   122 	    {
   123 	     no=no,
   124 	     qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
   125 	     cqs=cqs, cvqs=cvqs, ags=ags,		 
   126 	     cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
   127 	     GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
   128 	     tree=tree, case_hyp = case_hyp
   129 	    }
   130     end
   131 
   132 
   133 
   134 
   135 (* Chooses fresh free names, declares G and R, defines f and returns a record
   136    with all the information *)  
   137 fun setup_context (f, glrs, used) defname congs thy =
   138     let
   139 	val trees = map (build_tree thy f congs) glrs
   140 	val allused = fold FundefCtxTree.add_context_varnames trees used
   141 
   142 	val Const (f_fullname, fT) = f
   143 	val fname = Sign.base_name f_fullname
   144 
   145 	val domT = domain_type fT 
   146 	val ranT = range_type fT
   147 
   148 	val h = Free (variant allused "h", domT --> ranT)
   149 	val y = Free (variant allused "y", ranT)
   150 	val x = Free (variant allused "x", domT)
   151 	val z = Free (variant allused "z", domT)
   152 	val a = Free (variant allused "a", domT)
   153 	val D = Free (variant allused "D", HOLogic.mk_setT domT)
   154 	val P = Free (variant allused "P", domT --> boolT)
   155 	val Pbool = Free (variant allused "P", boolT)
   156 	val fvarname = variant allused "f"
   157 	val fvar = Free (fvarname, domT --> ranT)
   158 
   159 	val GT = mk_relT (domT, ranT)
   160 	val RT = mk_relT (domT, domT)
   161 	val G_name = defname ^ "_graph"
   162 	val R_name = defname ^ "_rel"
   163 
   164 	val glrs' = mk_primed_vars thy glrs
   165 
   166 	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
   167 
   168 	val G = Const (Sign.full_name thy G_name, GT)
   169 	val R = Const (Sign.full_name thy R_name, RT)
   170 	val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
   171 
   172 	val f_eq = Logic.mk_equals (f $ x, 
   173 				    Const ("The", (ranT --> boolT) --> ranT) $
   174 					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
   175 
   176 	val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
   177     in
   178 	(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)
   179     end
   180 
   181 
   182 (* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
   183 fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
   184     (implies $ Trueprop (mk_eq (lhs, lhs'))
   185 	     $ Trueprop (mk_eq (rhs, rhs')))
   186 	|> fold_rev (curry Logic.mk_implies) (gs @ gs')
   187 
   188 
   189 (* all proof obligations *)
   190 fun mk_compat_proof_obligations glrs glrs' =
   191     map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (upairs (glrs ~~ glrs'))
   192 
   193 
   194 fun extract_Ris thy congs f R tree (qs, gs, lhs, rhs) =
   195     let
   196 	fun add_Ri2 (fixes,assumes) (_ $ arg) _ (_, x) = ([], (FundefCtxTree.export_term (fixes, map prop_of assumes) (mk_relmem (arg, lhs) R)) :: x)
   197 	  | add_Ri2 _ _ _ _ = raise Match
   198 
   199 	val preRis = rev (FundefCtxTree.traverse_tree add_Ri2 tree [])
   200 	val (vRis, preRis_unq) = split_list (map dest_all_all preRis)
   201 
   202 	val Ris = map (fold_rev (curry Logic.mk_implies) gs) preRis_unq
   203     in
   204 	(map (map dest_Free) vRis, preRis, Ris)
   205     end
   206 
   207 fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
   208     let
   209 	val Names { domT, R, G, f, fvar, h, y, Pbool, ... } = names
   210 
   211 	val z = Var (("z",0), domT)
   212 	val x = Var (("x",0), domT)
   213 
   214 	val rew1 = (mk_mem (mk_prod (z, x), R),
   215 		    mk_mem (mk_prod (z, fvar $ z), G))
   216 	val rew2 = (f, fvar)
   217 
   218 	val prems = map (Pattern.rewrite_term thy [rew1, rew2] []) Ris
   219 	val rhs' = Pattern.rewrite_term thy [rew2] [] rhs 
   220     in
   221 	mk_relmem (lhs, rhs') G
   222 		  |> fold_rev (curry Logic.mk_implies) prems
   223 		  |> fold_rev (curry Logic.mk_implies) gs
   224     end
   225 
   226 fun mk_completeness names glrs =
   227     let
   228 	val Names {domT, x, Pbool, ...} = names
   229 
   230 	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
   231 						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
   232 						|> fold_rev (curry Logic.mk_implies) gs
   233 						|> fold_rev mk_forall qs
   234     in
   235 	Trueprop Pbool
   236 		 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
   237     end
   238 
   239 
   240 fun extract_conditions thy names trees congs =
   241     let
   242 	val Names {f, R, glrs, glrs', ...} = names
   243 
   244 	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
   245 	val Gis = map2 (mk_GIntro thy names) glrs preRiss
   246 	val complete = mk_completeness names glrs
   247 	val compat = mk_compat_proof_obligations glrs glrs'
   248     in
   249 	{G_intros = Gis, vRiss = vRiss, R_intross = Riss, complete = complete, compat = compat}
   250     end
   251 
   252 
   253 fun inductive_def defs (thy, const) =
   254     let
   255  	val (thy, {intrs, elims = [elim], ...}) = 
   256 	    InductivePackage.add_inductive_i true (*verbose*)
   257 					     false (*add_consts*)
   258 					     "" (* no altname *)
   259 					     false (* no coind *)
   260 					     false (* elims, please *)
   261 					     false (* induction thm please *)
   262 					     [const] (* the constant *)
   263 					     (map (fn t=>(("", t),[])) defs) (* the intros *)
   264 					     [] (* no special monos *)
   265 					     thy
   266     in
   267 	(intrs, (thy, elim))
   268     end
   269 
   270 
   271 
   272 (*
   273  * This is the first step in a function definition.
   274  *
   275  * Defines the function, the graph and the termination relation, synthesizes completeness
   276  * and comatibility conditions and returns everything.
   277  *)
   278 fun prepare_fundef thy congs defname f glrs used =
   279     let
   280 	val (names, thy) = setup_context (f, glrs, used) defname congs thy
   281 	val Names {G, R, glrs, trees, ...} = names
   282 
   283 	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
   284 
   285 	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
   286 	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
   287 
   288 	val n = length glrs
   289 	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
   290     in
   291 	(Prep {names = names, complete=complete, compat=compat, clauses = clauses},
   292 	 thy) 
   293     end
   294 
   295 
   296 
   297 
   298 end