src/HOL/Tools/function_package/fundef_proof.ML
author haftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 19818 5c5c1208a3fa
parent 19782 48c4632e2c28
child 19876 11d447d5d68c
permissions -rw-r--r--
adding case theorems for code generator
     1 (*  Title:      HOL/Tools/function_package/fundef_proof.ML
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 
     5 A package for general recursive function definitions. 
     6 Internal proofs.
     7 *)
     8 
     9 
    10 signature FUNDEF_PROOF =
    11 sig
    12 
    13     val mk_partial_rules : theory -> thm list -> FundefCommon.prep_result 
    14 			   -> thm -> thm list -> FundefCommon.fundef_result
    15 end
    16 
    17 
    18 structure FundefProof : FUNDEF_PROOF = 
    19 struct
    20 
    21 open FundefCommon
    22 open FundefAbbrev
    23 
    24 (* Theory dependencies *)
    25 val subsetD = thm "subsetD"
    26 val subset_refl = thm "subset_refl"
    27 val split_apply = thm "Product_Type.split"
    28 val wf_induct_rule = thm "wf_induct_rule";
    29 val Pair_inject = thm "Product_Type.Pair_inject";
    30 
    31 val acc_induct_rule = thm "acc_induct_rule" (* from: Accessible_Part *)
    32 val acc_downward = thm "acc_downward"
    33 val accI = thm "accI"
    34 
    35 val ex1_implies_ex = thm "fundef_ex1_existence"   (* from: Fundef.thy *) 
    36 val ex1_implies_un = thm "fundef_ex1_uniqueness"
    37 val ex1_implies_iff = thm "fundef_ex1_iff"
    38 val acc_subset_induct = thm "acc_subset_induct"
    39 
    40 
    41 
    42 
    43 
    44     
    45 fun mk_psimp thy names f_iff graph_is_function clause valthm =
    46     let
    47 	val Names {R, acc_R, domT, z, ...} = names
    48 	val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause
    49 	val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *)
    50 	val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
    51     in
    52 	((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
    53 	    |> (fn it => it COMP graph_is_function)
    54 	    |> implies_intr z_smaller
    55 	    |> forall_intr (cterm_of thy z)
    56 	    |> (fn it => it COMP valthm)
    57 	    |> implies_intr lhs_acc 
    58 	    |> asm_simplify (HOL_basic_ss addsimps [f_iff])
    59 (*	    |> fold forall_intr cqs
    60 	    |> forall_elim_vars 0
    61 	    |> varifyT
    62 	    |> Drule.close_derivation*)
    63     end
    64 
    65 
    66 
    67 
    68 fun mk_partial_induct_rule thy names complete_thm clauses =
    69     let
    70 	val Names {domT, R, acc_R, x, z, a, P, D, ...} = names
    71 
    72 	val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
    73 	val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))
    74 
    75 	val D_subset = cterm_of thy (Trueprop (mk_subset domT D acc_R))
    76 
    77 	val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
    78 	    mk_forall x
    79 		      (mk_forall z (Logic.mk_implies (Trueprop (mk_mem (x, D)),
    80 						      Logic.mk_implies (mk_relmem (z, x) R,
    81 									Trueprop (mk_mem (z, D))))))
    82 		      |> cterm_of thy
    83 
    84 
    85 	(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
    86 	val ihyp = all domT $ Abs ("z", domT, 
    87 				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
    88 					   $ Trueprop (P $ Bound 0))
    89 		       |> cterm_of thy
    90 
    91 	val aihyp = assume ihyp |> forall_elim_vars 0
    92 
    93 	fun prove_case clause =
    94 	    let
    95 		val ClauseInfo {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
    96 								       
    97 		val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
    98 		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
    99 		val sih = full_simplify replace_x_ss aihyp
   100 					
   101 					(* FIXME: Variable order destroyed by forall_intr_vars *)
   102 		val P_recs = map (fn RCInfo {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs   (*  [P rec1, P rec2, ... ]  *)
   103 			     
   104 		val step = Trueprop (P $ lhs)
   105 				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   106 				    |> fold_rev (curry Logic.mk_implies) gs
   107 				    |> curry Logic.mk_implies (Trueprop (mk_mem (lhs, D)))
   108 				    |> fold_rev mk_forall qs
   109 				    |> cterm_of thy
   110 			   
   111 		val P_lhs = assume step
   112 				   |> fold forall_elim cqs
   113 				   |> implies_elim_swp lhs_D 
   114 				   |> fold_rev implies_elim_swp ags
   115 				   |> fold implies_elim_swp P_recs
   116 			    
   117 		val res = cterm_of thy (Trueprop (P $ x))
   118 				   |> Simplifier.rewrite replace_x_ss
   119 				   |> symmetric (* P lhs == P x *)
   120 				   |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
   121 				   |> implies_intr (cprop_of case_hyp)
   122 				   |> fold_rev (implies_intr o cprop_of) ags
   123 				   |> fold_rev forall_intr cqs
   124 	    in
   125 		(res, step)
   126 	    end
   127 
   128 	val (cases, steps) = split_list (map prove_case clauses)
   129 
   130 	val istep =  complete_thm
   131 			 |> fold (curry op COMP) cases (*  P x  *)
   132 			 |> implies_intr ihyp
   133 			 |> implies_intr (cprop_of x_D)
   134 			 |> forall_intr (cterm_of thy x)
   135 			   
   136 	val subset_induct_rule = 
   137 	    acc_subset_induct
   138 		|> (curry op COMP) (assume D_subset)
   139 		|> (curry op COMP) (assume D_dcl)
   140 		|> (curry op COMP) (assume a_D)
   141 		|> (curry op COMP) istep
   142 		|> fold_rev implies_intr steps
   143 		|> implies_intr a_D
   144 		|> implies_intr D_dcl
   145 		|> implies_intr D_subset
   146 
   147 	val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
   148 
   149 	val simple_induct_rule =
   150 	    subset_induct_rule
   151 		|> forall_intr (cterm_of thy D)
   152 		|> forall_elim (cterm_of thy acc_R)
   153 		|> (curry op COMP) subset_refl
   154 		|> (curry op COMP) (acc_downward
   155 					|> (instantiate' [SOME (ctyp_of thy domT)]
   156 							 (map (SOME o cterm_of thy) [x, R, z]))
   157 					|> forall_intr (cterm_of thy z)
   158 					|> forall_intr (cterm_of thy x))
   159 		|> forall_intr (cterm_of thy a)
   160 		|> forall_intr (cterm_of thy P)
   161     in
   162 	(subset_induct_all, simple_induct_rule)
   163     end
   164 
   165 
   166 
   167 
   168 
   169 (***********************************************)
   170 (* Compat thms are stored in normal form (with vars) *)
   171 
   172 (* replace this by a table later*)
   173 fun store_compat_thms 0 cts = []
   174   | store_compat_thms n cts =
   175     let
   176 	val (cts1, cts2) = chop n cts
   177     in
   178 	(cts1 :: store_compat_thms (n - 1) cts2)
   179     end
   180 
   181 
   182 (* needs i <= j *)
   183 fun lookup_compat_thm i j cts =
   184     nth (nth cts (i - 1)) (j - i)
   185 (***********************************************)
   186 
   187 
   188 (* recover the order of Vars *)
   189 fun get_var_order thy clauses =
   190     map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
   191 
   192 
   193 (* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
   194 (* if j < i, then turn around *)
   195 fun get_compat_thm thy cts clausei clausej =
   196     let 
   197 	val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
   198 	val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
   199 
   200 	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
   201     in if j < i then
   202 	   let 
   203 	       val (var_ord, compat) = lookup_compat_thm j i cts
   204 	   in
   205 	       compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
   206 		|> instantiate ([],(var_ord ~~ (qsj' @ qsi))) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
   207 		|> fold implies_elim_swp gsj'
   208 		|> fold implies_elim_swp gsi
   209 		|> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
   210 	   end
   211        else
   212 	   let
   213 	       val (var_ord, compat) = lookup_compat_thm i j cts
   214 	   in
   215 	       compat        (* "?Gsi => ?Gsj' => ?lhsi = ?lhsj' ==> ?rhsi = ?rhsj'" *)
   216 	         |> instantiate ([], (var_ord ~~ (qsi @ qsj'))) (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
   217 		 |> fold implies_elim_swp gsi
   218 		 |> fold implies_elim_swp gsj'
   219 		 |> implies_elim_swp (assume lhsi_eq_lhsj')
   220 		 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
   221 	   end
   222     end
   223 
   224 
   225 
   226 
   227 
   228 (* Generates the replacement lemma with primed variables. A problem here is that one should not do
   229 the complete requantification at the end to replace the variables. One should find a way to be more efficient
   230 here. *)
   231 fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
   232     let 
   233 	val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
   234 	val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
   235 
   236 	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
   237 
   238 	val Ris = map (fn RCInfo {lRIq, ...} => lRIq) RCs
   239 	val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
   240 	val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
   241 
   242 	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
   243 
   244 	val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
   245 
   246 	val replace_lemma = (eql RS meta_eq_to_obj_eq)
   247 				|> implies_intr (cprop_of case_hyp)
   248 				|> fold_rev (implies_intr o cprop_of) h_assums
   249 				|> fold_rev (implies_intr o cprop_of) ags
   250 				|> fold_rev forall_intr cqs
   251 				|> fold forall_elim cqs'
   252 				|> fold implies_elim_swp ags'
   253 				|> fold implies_elim_swp h_assums'
   254     in
   255 	replace_lemma
   256     end
   257 
   258 
   259 
   260 
   261 fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
   262     let
   263 	val Names {f, h, y, ...} = names
   264 	val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
   265 	val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
   266 
   267 	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
   268 	val compat = get_compat_thm thy compat_store clausei clausej
   269 	val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
   270 
   271 	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
   272 	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)
   273 
   274 	val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
   275     in
   276 	(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   277         |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   278 	|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
   279 	|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
   280 	|> implies_intr (cprop_of y_eq_rhsj'h)
   281 	|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
   282 	|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
   283 	|> implies_elim_swp eq_pairs
   284 	|> fold_rev (implies_intr o cprop_of) Ghsj' 
   285 	|> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
   286 	|> implies_intr (cprop_of eq_pairs)
   287 	|> fold_rev forall_intr ordcqs'j
   288     end
   289 
   290 
   291 
   292 fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
   293     let
   294 	val Names {x, y, G, fvar, f, ranT, ...} = names
   295 	val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
   296 
   297 	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
   298 
   299 	fun prep_RC (RCInfo {lRIq,RIvs, ...}) = lRIq
   300 						    |> fold (forall_elim o cterm_of thy o Free) RIvs
   301 						    |> (fn it => it RS ih_intro_case)
   302 						    |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   303 
   304 	val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])
   305 			    |> fold (curry op COMP o prep_RC) RCs 
   306 
   307 
   308 	val a = cterm_of thy (mk_prod (lhs, y))
   309 	val P = cterm_of thy (mk_eq (y, rhs))
   310 	val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
   311 
   312 	val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
   313 
   314 	val uniqueness = G_cases 
   315 			     |> instantiate' [] [SOME a, SOME P]
   316 			     |> implies_elim_swp a_in_G
   317 			     |> fold implies_elim_swp unique_clauses
   318 			     |> implies_intr (cprop_of a_in_G)
   319 			     |> forall_intr (cterm_of thy y) 
   320 
   321 	val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
   322 
   323 	val exactly_one =
   324 	    ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
   325 		 |> curry (op COMP) existence
   326 		 |> curry (op COMP) uniqueness
   327 		 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
   328 		 |> implies_intr (cprop_of case_hyp) 
   329 		 |> fold_rev (implies_intr o cprop_of) ags
   330 		 |> fold_rev forall_intr cqs
   331 	val function_value =
   332 	    existence 
   333 		|> fold_rev (implies_intr o cprop_of) ags
   334 		|> implies_intr ihyp
   335 		|> implies_intr (cprop_of case_hyp)
   336 		|> forall_intr (cterm_of thy x)
   337 		|> forall_elim (cterm_of thy lhs)
   338 		|> curry (op RS) refl
   339     in
   340 	(exactly_one, function_value)
   341     end
   342 
   343 
   344 
   345 (* Does this work with Guards??? *)
   346 fun mk_domain_intro thy names R_cases clause =
   347     let
   348 	val Names {z, R, acc_R, ...} = names
   349 	val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
   350 	val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
   351                      |> fold_rev (curry Logic.mk_implies) gs
   352                      |> cterm_of thy
   353     in
   354 	Goal.init goal 
   355 		  |> (SINGLE (resolve_tac [accI] 1)) |> the
   356 		  |> (SINGLE (eresolve_tac [R_cases] 1))  |> the
   357 		  |> (SINGLE (CLASIMPSET auto_tac)) |> the
   358 		  |> Goal.conclude
   359     end
   360 
   361 
   362 
   363 
   364 fun mk_nest_term_case thy names R' ihyp clause =
   365     let
   366 	val Names {x, z, ...} = names
   367 	val ClauseInfo {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
   368 
   369 	val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
   370 
   371 	fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
   372 	    let
   373 		val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
   374 
   375 		val hyp = mk_relmem (arg, lhs) R'
   376 				    |> fold_rev (curry Logic.mk_implies o prop_of) used
   377 				    |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
   378 				    |> fold_rev (curry Logic.mk_implies o prop_of) ags
   379 				    |> fold_rev mk_forall qs
   380 				    |> cterm_of thy
   381 
   382 		val thm = assume hyp
   383 				 |> fold forall_elim cqs
   384 				 |> fold implies_elim_swp ags
   385 				 |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
   386 				 |> fold implies_elim_swp used
   387 
   388 		val acc = thm COMP ih_case
   389 
   390 		val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
   391 
   392 		val arg_eq_z = (assume z_eq_arg) RS sym
   393 
   394 		val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
   395 				     |> implies_intr (cprop_of case_hyp)
   396 				     |> implies_intr z_eq_arg
   397 
   398 		val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs))))
   399 
   400 		val z_acc' = z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject)
   401 
   402 		val ethm = z_acc'
   403 			       |> FundefCtxTree.export_thm thy (fixes, (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))
   404 			       |> fold_rev forall_intr cqs
   405 
   406 
   407 		val sub' = sub @ [(([],[]), acc)]
   408 	    in
   409 		(sub', (hyp :: hyps, ethm :: thms))
   410 	    end
   411 	  | step _ _ _ _ = raise Match
   412     in
   413 	FundefCtxTree.traverse_tree step tree
   414     end
   415 
   416 
   417 fun mk_nest_term_rule thy names clauses =
   418     let
   419 	val Names { R, acc_R, domT, x, z, ... } = names
   420 
   421 	val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R))))))
   422 
   423 	val R' = Free ("R", fastype_of R)
   424 
   425 	val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wf", mk_relT (domT, domT) --> boolT) $ R')) (* "wf R'" *)
   426 
   427 	(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   428 	val ihyp = all domT $ Abs ("z", domT, 
   429 				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R')
   430 					   $ Trueprop ((Const ("op :", [domT, HOLogic.mk_setT domT] ---> boolT))
   431 							   $ Bound 0 $ acc_R))
   432 		       |> cterm_of thy
   433 
   434 	val ihyp_a = assume ihyp |> forall_elim_vars 0
   435 
   436 	val z_ltR_x = cterm_of thy (mk_relmem (z, x) R) (* "(z, x) : R" *)
   437 	val z_acc = cterm_of thy (mk_mem (z, acc_R))
   438 
   439 	val (hyps,cases) = fold (mk_nest_term_case thy names R' ihyp_a) clauses ([],[])
   440     in
   441 	R_elim
   442 	    |> freezeT
   443 	    |> instantiate' [] [SOME (cterm_of thy (mk_prod (z,x))), SOME z_acc]
   444 	    |> curry op COMP (assume z_ltR_x)
   445 	    |> fold_rev (curry op COMP) cases
   446 	    |> implies_intr z_ltR_x
   447 	    |> forall_intr (cterm_of thy z)
   448 	    |> (fn it => it COMP accI)
   449 	    |> implies_intr ihyp
   450 	    |> forall_intr (cterm_of thy x)
   451 	    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
   452 	    |> implies_elim_swp (assume wfR')
   453 	    |> fold implies_intr hyps
   454 	    |> implies_intr wfR'
   455 	    |> forall_intr (cterm_of thy R')
   456 	    |> forall_elim_vars 0
   457 	    |> varifyT
   458     end
   459 
   460 
   461 
   462 
   463 fun mk_partial_rules thy congs data complete_thm compat_thms =
   464     let
   465 	val Prep {names, clauses, complete, compat, ...} = data
   466 	val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
   467 
   468 (*	val _ = Output.debug "closing derivation: completeness"
   469 	val _ = Output.debug (Proofterm.size_of_proof (proof_of complete_thm))
   470 	val _ = Output.debug (map (Proofterm.size_of_proof o proof_of) compat_thms)*)
   471 	val complete_thm = Drule.close_derivation complete_thm
   472 (*	val _ = Output.debug "closing derivation: compatibility"*)
   473 	val compat_thms = map Drule.close_derivation compat_thms
   474 (*	val _ = Output.debug "  done"*)
   475 
   476 	val complete_thm_fr = freezeT complete_thm
   477 	val compat_thms_fr = map freezeT compat_thms
   478 	val f_def_fr = freezeT f_def
   479 
   480 	val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] 
   481 						[SOME (cterm_of thy f), SOME (cterm_of thy G)])
   482 				      #> curry op COMP (forall_intr_vars f_def_fr)
   483 			  
   484 	val inst_ex1_ex = instantiate_and_def ex1_implies_ex
   485 	val inst_ex1_un = instantiate_and_def ex1_implies_un
   486 	val inst_ex1_iff = instantiate_and_def ex1_implies_iff
   487 
   488 	(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   489 	val ihyp = all domT $ Abs ("z", domT, 
   490 				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
   491 					   $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   492 							     Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
   493 		       |> cterm_of thy
   494 		   
   495 	val ihyp_thm = assume ihyp
   496 			      |> forall_elim_vars 0
   497 		       
   498 	val ih_intro = ihyp_thm RS inst_ex1_ex
   499 	val ih_elim = ihyp_thm RS inst_ex1_un
   500 
   501 	val _ = Output.debug "Proving Replacement lemmas..."
   502 	val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
   503 
   504 	val n = length clauses
   505 	val var_order = get_var_order thy clauses
   506 	val compat_store = store_compat_thms n (var_order ~~ compat_thms_fr)
   507 
   508 	val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> freezeT
   509 	val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> freezeT
   510 
   511 	val _ = Output.debug "Proving cases for unique existence..."
   512 	val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses repLemmas) clauses)
   513 
   514 	val _ = Output.debug "Proving: Graph is a function"
   515 	val graph_is_function = complete_thm_fr
   516 				    |> fold (curry op COMP) ex1s
   517 				    |> implies_intr (ihyp)
   518 				    |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
   519 				    |> forall_intr (cterm_of thy x)
   520 				    |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   521 				    |> Drule.close_derivation
   522 
   523 	val f_iff = (graph_is_function RS inst_ex1_iff)
   524 
   525 	val _ = Output.debug "Proving simplification rules"
   526 	val psimps  = map2 (mk_psimp thy names f_iff graph_is_function) clauses values
   527 
   528 	val _ = Output.debug "Proving partial induction rule"
   529 	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses
   530 
   531 	val _ = Output.debug "Proving nested termination rule"
   532 	val total_intro = mk_nest_term_rule thy names clauses
   533 
   534 	val _ = Output.debug "Proving domain introduction rules"
   535 	val dom_intros = map (mk_domain_intro thy names R_cases) clauses
   536     in 
   537 	FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
   538 	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
   539 	 dom_intros=dom_intros}
   540     end
   541 
   542 
   543 end
   544 
   545