TFL/tfl.sml
changeset 6498 1ebbe18fe236
parent 6397 e70ae9b575cc
child 6566 7ed743d18af7
equal deleted inserted replaced
6497:120ca2bb27e1 6498:1ebbe18fe236
     7 *)
     7 *)
     8 
     8 
     9 structure Prim : TFL_sig =
     9 structure Prim : TFL_sig =
    10 struct
    10 struct
    11 
    11 
       
    12 val trace = ref false;
       
    13 
    12 (* Abbreviations *)
    14 (* Abbreviations *)
    13 structure R = Rules;
    15 structure R = Rules;
    14 structure S = USyntax;
    16 structure S = USyntax;
    15 structure U = S.Utils;
    17 structure U = S.Utils;
    16 
    18 
    26   | stringize [i] = Int.toString i
    28   | stringize [i] = Int.toString i
    27   | stringize (h::t) = (Int.toString h^", "^stringize t);
    29   | stringize (h::t) = (Int.toString h^", "^stringize t);
    28 
    30 
    29 
    31 
    30 fun TFL_ERR{func,mesg} = U.ERR{module = "Tfl", func = func, mesg = mesg};
    32 fun TFL_ERR{func,mesg} = U.ERR{module = "Tfl", func = func, mesg = mesg};
       
    33 
       
    34 
       
    35 (*---------------------------------------------------------------------------
       
    36           handling of user-supplied congruence rules: lcp*)
       
    37 
       
    38 (*Convert conclusion from = to ==*)
       
    39 val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
       
    40 
       
    41 (*default congruence rules include those for LET and IF*)
       
    42 val default_congs = eq_reflect_list [Thms.LET_CONG, if_cong];
       
    43 
       
    44 fun congs ths = default_congs @ eq_reflect_list ths;
       
    45 
       
    46 val default_simps = 
       
    47     [less_Suc_eq RS iffD2, lex_prod_def, measure_def, inv_image_def];
       
    48 
       
    49 
    31 
    50 
    32 
    51 
    33 (*---------------------------------------------------------------------------
    52 (*---------------------------------------------------------------------------
    34  * The next function is common to pattern-match translation and 
    53  * The next function is common to pattern-match translation and 
    35  * proof of completeness of cases for the induction theorem.
    54  * proof of completeness of cases for the induction theorem.
   312  *                    PRINCIPLES OF DEFINITION
   331  *                    PRINCIPLES OF DEFINITION
   313  *
   332  *
   314  *---------------------------------------------------------------------------*)
   333  *---------------------------------------------------------------------------*)
   315 
   334 
   316 
   335 
       
   336 (*For Isabelle, the lhs of a definition must be a constant.*)
       
   337 fun mk_const_def sign (Name, Ty, rhs) =
       
   338     Sign.infer_types sign (K None) (K None) [] false
       
   339 	       ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT)
       
   340     |> #1;
       
   341 
   317 (*Make all TVars available for instantiation by adding a ? to the front*)
   342 (*Make all TVars available for instantiation by adding a ? to the front*)
   318 fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
   343 fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
   319   | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
   344   | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
   320   | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
   345   | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
   321 
   346 
   333 				      quote Name}
   358 				      quote Name}
   334 		    else Name ^ "_def"
   359 		    else Name ^ "_def"
   335      val wfrec_R_M =  map_term_types poly_tvars 
   360      val wfrec_R_M =  map_term_types poly_tvars 
   336 	                  (wfrec $ map_term_types poly_tvars R) 
   361 	                  (wfrec $ map_term_types poly_tvars R) 
   337 	              $ functional
   362 	              $ functional
   338      val (def_term, _) = 
   363      val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
   339 	 Sign.infer_types (Theory.sign_of thy) (K None) (K None) [] false
       
   340 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
       
   341 		propT)
       
   342   in  PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy  end
   364   in  PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy  end
   343 end;
   365 end;
   344 
   366 
   345 
   367 
   346 
   368 
   377 
   399 
   378 fun givens [] = []
   400 fun givens [] = []
   379   | givens (GIVEN(tm,_)::pats) = tm :: givens pats
   401   | givens (GIVEN(tm,_)::pats) = tm :: givens pats
   380   | givens (OMITTED _::pats)   = givens pats;
   402   | givens (OMITTED _::pats)   = givens pats;
   381 
   403 
   382 fun post_definition (ss, tflCongs) (theory, (def, pats)) =
   404 (*called only by Tfl.simplify_defn*)
       
   405 fun post_definition meta_tflCongs (theory, (def, pats)) =
   383  let val tych = Thry.typecheck theory 
   406  let val tych = Thry.typecheck theory 
   384      val f = #lhs(S.dest_eq(concl def))
   407      val f = #lhs(S.dest_eq(concl def))
   385      val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
   408      val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
   386      val given_pats = givens pats
   409      val given_pats = givens pats
   387      val WFR = #ant(S.dest_imp(concl corollary))
   410      val WFR = #ant(S.dest_imp(concl corollary))
   390      val corollaries = map (fn pat => R.SPEC (tych pat) corollary') 
   413      val corollaries = map (fn pat => R.SPEC (tych pat) corollary') 
   391 	                   given_pats
   414 	                   given_pats
   392      val (case_rewrites,context_congs) = extraction_thms theory
   415      val (case_rewrites,context_congs) = extraction_thms theory
   393      val corollaries' = map(rewrite_rule case_rewrites) corollaries
   416      val corollaries' = map(rewrite_rule case_rewrites) corollaries
   394      val extract = R.CONTEXT_REWRITE_RULE 
   417      val extract = R.CONTEXT_REWRITE_RULE 
   395 	             (ss, f, R,
   418 	             (f, [R], cut_apply, meta_tflCongs@context_congs)
   396 		      R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
       
   397 		      tflCongs@context_congs)
       
   398      val (rules, TCs) = ListPair.unzip (map extract corollaries')
   419      val (rules, TCs) = ListPair.unzip (map extract corollaries')
   399      val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
   420      val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
   400      val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   421      val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   401      val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   422      val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   402  in
   423  in
   403  {theory = theory,   (* holds def, if it's needed *)
   424  {theory = theory,   (* holds def, if it's needed *)
   404   rules = rules1,
   425   rules = rules1,
   405   full_pats_TCs = merge (map pat_of pats) 
   426   full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)), 
   406                         (ListPair.zip (given_pats, TCs)), 
       
   407   TCs = TCs, 
   427   TCs = TCs, 
   408   patterns = pats}
   428   patterns = pats}
   409  end;
   429  end;
   410 
   430 
       
   431 
   411 (*---------------------------------------------------------------------------
   432 (*---------------------------------------------------------------------------
   412  * Perform the extraction without making the definition. Definition and
   433  * Perform the extraction without making the definition. Definition and
   413  * extraction commute for the non-nested case. For hol90 users, this 
   434  * extraction commute for the non-nested case.  (Deferred recdefs)
   414  * function can be invoked without being in draft mode.
   435  *---------------------------------------------------------------------------*)
   415  * CURRENTLY UNUSED
   436 fun wfrec_eqns thy fid tflCongs eqns =
   416 fun wfrec_eqns (ss, tflCongs) thy eqns =
   437  let val {functional as Abs(Name, Ty, _),  pats} = mk_functional thy eqns
   417  let val {functional,pats} = mk_functional thy eqns
       
   418      val given_pats = givens pats
   438      val given_pats = givens pats
   419      val {Bvar = f, Body} = S.dest_abs functional
   439      val f = #1 (S.strip_comb(#lhs(S.dest_eq (hd eqns))))
   420      val {Bvar = x, ...} = S.dest_abs Body
   440      (* val f = Free(Name,Ty) *)
   421      val (Name, Type("fun", [f_dty, f_rty])) = dest_Free f
   441      val Type("fun", [f_dty, f_rty]) = Ty
       
   442      val dummy = if Name<>fid then 
       
   443 			raise TFL_ERR{func = "lazyR_def",
       
   444 				      mesg = "Expected a definition of " ^ 
       
   445 				      quote fid ^ " but found one of " ^
       
   446 				      quote Name}
       
   447 		 else ()
       
   448      val SV = S.free_vars_lr functional  (* schema variables *)
   422      val (case_rewrites,context_congs) = extraction_thms thy
   449      val (case_rewrites,context_congs) = extraction_thms thy
   423      val tych = Thry.typecheck thy
   450      val tych = Thry.typecheck thy
   424      val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
   451      val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
   425      val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   452      val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   426      val R = Free (variant (foldr add_term_names (eqns,[])) Rname,
   453      val R = Free (variant (foldr add_term_names (eqns,[])) Rname,
   427 		   Rtype)
   454 		   Rtype)
   428      val WFREC_THM = R.ISPECL [tych R, tych f] WFREC_THM0
   455      val WFREC_THM = R.ISPECL [tych R, tych f] WFREC_THM0
   429      val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
   456      val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
       
   457      val dummy = 
       
   458 	   if !trace then
       
   459 	       writeln ("ORIGINAL PROTO_DEF: " ^ 
       
   460 			  Sign.string_of_term (Theory.sign_of thy) proto_def)
       
   461            else ()
   430      val R1 = S.rand WFR
   462      val R1 = S.rand WFR
   431      val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
   463      val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
   432      val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
   464      val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
   433      val corollaries' = map (rewrite_rule case_rewrites) corollaries
   465      val corollaries' = map (rewrite_rule case_rewrites) corollaries
   434      val extract = R.CONTEXT_REWRITE_RULE 
   466      fun extract X = R.CONTEXT_REWRITE_RULE 
   435 	               (ss, f, R1, 
   467 	               (f, R1::SV, cut_apply, tflCongs@context_congs) X
   436 		        R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA, 
   468  in {proto_def =   (*Use == rather than = for definitions*)
   437 			tflCongs@context_congs)
   469 	 mk_const_def (Theory.sign_of thy) 
   438  in {proto_def=proto_def, 
   470 	              (Name, Ty, S.rhs proto_def), 
       
   471      SV=SV,
   439      WFR=WFR, 
   472      WFR=WFR, 
   440      pats=pats,
   473      pats=pats,
   441      extracta = map extract corollaries'}
   474      extracta = map extract corollaries'}
   442  end;
   475  end;
   443  *---------------------------------------------------------------------------*)
       
   444 
   476 
   445 
   477 
   446 (*---------------------------------------------------------------------------
   478 (*---------------------------------------------------------------------------
   447  * Define the constant after extracting the termination conditions. The 
   479  * Define the constant after extracting the termination conditions. The 
   448  * wellfounded relation used in the definition is computed by using the
   480  * wellfounded relation used in the definition is computed by using the
   449  * choice operator on the extracted conditions (plus the condition that
   481  * choice operator on the extracted conditions (plus the condition that
   450  * such a relation must be wellfounded).
   482  * such a relation must be wellfounded).
   451  * CURRENTLY UNUSED
   483  *---------------------------------------------------------------------------*)
   452 fun lazyR_def ss thy eqns =
   484 fun lazyR_def thy fid tflCongs eqns =
   453  let val {proto_def,WFR,pats,extracta} = wfrec_eqns ss thy eqns
   485  let val {proto_def,WFR,pats,extracta,SV} = 
       
   486 	   wfrec_eqns thy fid (congs tflCongs) eqns
   454      val R1 = S.rand WFR
   487      val R1 = S.rand WFR
   455      val f = S.lhs proto_def
   488      val f = #1 (Logic.dest_equals proto_def)
   456      val (Name,_) = dest_Free f
       
   457      val (extractants,TCl) = ListPair.unzip extracta
   489      val (extractants,TCl) = ListPair.unzip extracta
       
   490      val dummy = if !trace 
       
   491 		 then (writeln "Extractants = ";
       
   492 		       prths extractants;
       
   493 		       ())
       
   494 		 else ()
   458      val TCs = foldr (gen_union (op aconv)) (TCl, [])
   495      val TCs = foldr (gen_union (op aconv)) (TCl, [])
   459      val full_rqt = WFR::TCs
   496      val full_rqt = WFR::TCs
   460      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   497      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   461      val R'abs = S.rand R'
   498      val R'abs = S.rand R'
       
   499      val proto_def' = subst_free[(R1,R')] proto_def
       
   500      val dummy = if !trace then writeln ("proto_def' = " ^
       
   501 					 Sign.string_of_term
       
   502 					 (Theory.sign_of thy) proto_def')
       
   503 	                   else ()
   462      val theory =
   504      val theory =
   463        thy
   505        thy
   464        |> PureThy.add_defs_i [Thm.no_attributes (Name ^ "_def", subst_free[(R1,R')] proto_def)];
   506        |> PureThy.add_defs_i 
   465      val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
   507             [Thm.no_attributes (fid ^ "_def", proto_def')];
       
   508      val def = get_axiom theory (fid ^ "_def") RS meta_eq_to_obj_eq
       
   509      val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
       
   510 	                   else ()
   466      val fconst = #lhs(S.dest_eq(concl def)) 
   511      val fconst = #lhs(S.dest_eq(concl def)) 
   467      val tych = Thry.typecheck theory
   512      val tych = Thry.typecheck theory
   468      val baz = R.DISCH (tych proto_def)
   513      val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
   469                  (U.itlist (R.DISCH o tych) full_rqt (R.LIST_CONJ extractants))
   514 	 (*lcp: a lot of object-logic inference to remove*)
       
   515      val baz = R.DISCH_ALL
       
   516                  (U.itlist R.DISCH full_rqt_prop 
       
   517 		  (R.LIST_CONJ extractants))
       
   518      val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
       
   519 	                   else ()
       
   520      val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
   470      val def' = R.MP (R.SPEC (tych fconst) 
   521      val def' = R.MP (R.SPEC (tych fconst) 
   471                              (R.SPEC (tych R') (R.GENL[tych R1, tych f] baz)))
   522                              (R.SPEC (tych R')
       
   523 			      (R.GENL[tych R1, tych f_free] baz)))
   472                      def
   524                      def
   473      val body_th = R.LIST_CONJ (map (R.ASSUME o tych) full_rqt)
   525      val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
   474      val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)
   526      val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)
   475                     body_th
   527                     body_th
   476  in {theory = theory, R=R1,
   528  in {theory = theory, R=R1, SV=SV,
   477      rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
   529      rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
   478      full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
   530      full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
   479      patterns = pats}
   531      patterns = pats}
   480  end;
   532  end;
   481  *---------------------------------------------------------------------------*)
       
   482 
   533 
   483 
   534 
   484 
   535 
   485 (*----------------------------------------------------------------------------
   536 (*----------------------------------------------------------------------------
   486  *
   537  *
   615  * to do so, it would have to be from a nested definition, and we don't
   666  * to do so, it would have to be from a nested definition, and we don't
   616  * allow nested defns to have R variable.
   667  * allow nested defns to have R variable.
   617  *
   668  *
   618  * Note. When the context is empty, there can be no local variables.
   669  * Note. When the context is empty, there can be no local variables.
   619  *---------------------------------------------------------------------------*)
   670  *---------------------------------------------------------------------------*)
   620 
   671 (*
   621 local infix 5 ==>
   672 local infix 5 ==>
   622       fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   673       fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   623 in
   674 in
   624 fun build_ih f P (pat,TCs) = 
   675 fun build_ih f P (pat,TCs) = 
   625  let val globals = S.free_vars_lr pat
   676  let val globals = S.free_vars_lr pat
   642                  val ind_clause = S.list_mk_conj ihs ==> P$pat
   693                  val ind_clause = S.list_mk_conj ihs ==> P$pat
   643              in (S.list_mk_forall(globals,ind_clause), TCs_locals)
   694              in (S.list_mk_forall(globals,ind_clause), TCs_locals)
   644              end
   695              end
   645  end
   696  end
   646 end;
   697 end;
   647 
   698 *)
   648 
   699 
   649 
   700 local infix 5 ==>
   650 (*---------------------------------------------------------------------------
   701       fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   651  * This function makes good on the promise made in "build_ih: we prove
   702 in
   652  * <something>.
   703 fun build_ih f (P,SV) (pat,TCs) = 
       
   704  let val pat_vars = S.free_vars_lr pat
       
   705      val globals = pat_vars@SV
       
   706      fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
       
   707      fun dest_TC tm = 
       
   708          let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
       
   709              val (R,y,_) = S.dest_relation R_y_pat
       
   710              val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
       
   711          in case cntxt 
       
   712               of [] => (P_y, (tm,[]))
       
   713                | _  => let 
       
   714                     val imp = S.list_mk_conj cntxt ==> P_y
       
   715                     val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
       
   716                     val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs
       
   717                     in (S.list_mk_forall(locals,imp), (tm,locals)) end
       
   718          end
       
   719  in case TCs
       
   720     of [] => (S.list_mk_forall(pat_vars, P$pat), [])
       
   721      |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
       
   722                  val ind_clause = S.list_mk_conj ihs ==> P$pat
       
   723              in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals)
       
   724              end
       
   725  end
       
   726 end;
       
   727 
       
   728 (*---------------------------------------------------------------------------
       
   729  * This function makes good on the promise made in "build_ih". 
   653  *
   730  *
   654  * Input  is tm = "(!y. R y pat ==> P y) ==> P pat",  
   731  * Input  is tm = "(!y. R y pat ==> P y) ==> P pat",  
   655  *           TCs = TC_1[pat] ... TC_n[pat]
   732  *           TCs = TC_1[pat] ... TC_n[pat]
   656  *           thm = ih1 /\ ... /\ ih_n |- ih[pat]
   733  *           thm = ih1 /\ ... /\ ih_n |- ih[pat]
   657  *---------------------------------------------------------------------------*)
   734  *---------------------------------------------------------------------------*)
   709  *
   786  *
   710  * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove
   787  * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove
   711  * recursion induction (Rinduct) by proving the antecedent of Sinduct from 
   788  * recursion induction (Rinduct) by proving the antecedent of Sinduct from 
   712  * the antecedent of Rinduct.
   789  * the antecedent of Rinduct.
   713  *---------------------------------------------------------------------------*)
   790  *---------------------------------------------------------------------------*)
   714 fun mk_induction thy f R pat_TCs_list =
   791 fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
   715 let val tych = Thry.typecheck thy
   792 let val tych = Thry.typecheck thy
   716     val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
   793     val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
   717     val (pats,TCsl) = ListPair.unzip pat_TCs_list
   794     val (pats,TCsl) = ListPair.unzip pat_TCs_list
   718     val case_thm = complete_cases thy pats
   795     val case_thm = complete_cases thy pats
   719     val domain = (type_of o hd) pats
   796     val domain = (type_of o hd) pats
   720     val Pname = Term.variant (foldr (foldr add_term_names) 
   797     val Pname = Term.variant (foldr (foldr add_term_names) 
   721 			      (pats::TCsl, [])) "P"
   798 			      (pats::TCsl, [])) "P"
   722     val P = Free(Pname, domain --> HOLogic.boolT)
   799     val P = Free(Pname, domain --> HOLogic.boolT)
   723     val Sinduct = R.SPEC (tych P) Sinduction
   800     val Sinduct = R.SPEC (tych P) Sinduction
   724     val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
   801     val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
   725     val Rassums_TCl' = map (build_ih f P) pat_TCs_list
   802     val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
   726     val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
   803     val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
   727     val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
   804     val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
   728     val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
   805     val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
   729     val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
   806     val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
   730     val proved_cases = map (prove_case f thy) tasks
   807     val proved_cases = map (prove_case fconst thy) tasks
   731     val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
   808     val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
   732 		    "v",
   809 		    "v",
   733 		  domain)
   810 		  domain)
   734     val vtyped = tych v
   811     val vtyped = tych v
   735     val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   812     val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   801     *
   878     *
   802     *   1. if |- tc = T, then eliminate it with eqT; otherwise,
   879     *   1. if |- tc = T, then eliminate it with eqT; otherwise,
   803     *   2. apply the terminator to tc'. If |- tc' = T then eliminate; else
   880     *   2. apply the terminator to tc'. If |- tc' = T then eliminate; else
   804     *   3. replace tc by tc' in both the rules and the induction theorem.
   881     *   3. replace tc by tc' in both the rules and the induction theorem.
   805     *---------------------------------------------------------------------*)
   882     *---------------------------------------------------------------------*)
       
   883 
       
   884 fun print_thms s L = 
       
   885   if !trace then writeln (cat_lines (s :: map string_of_thm L))
       
   886   else ();
       
   887 
       
   888 fun print_cterms s L = 
       
   889   if !trace then writeln (cat_lines (s :: map string_of_cterm L))
       
   890   else ();;
       
   891 
   806    fun simplify_tc tc (r,ind) =
   892    fun simplify_tc tc (r,ind) =
   807        let val tc_eq = simplifier (tych tc)
   893        let val tc1 = tych tc
       
   894            val _ = print_cterms "TC before simplification: " [tc1]
       
   895            val tc_eq = simplifier tc1
       
   896            val _ = print_thms "result: " [tc_eq]
   808        in 
   897        in 
   809        elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
   898        elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
   810        handle _ => 
   899        handle _ => 
   811         (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   900         (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   812 		  (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))), 
   901 		  (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),