equal
deleted
inserted
replaced
506 (*instantiate the variable to a tuple, if it is non-trivial, in order to |
506 (*instantiate the variable to a tuple, if it is non-trivial, in order to |
507 allow the predicate to be "opened up". |
507 allow the predicate to be "opened up". |
508 The name "x.1" comes from the "RS spec" !*) |
508 The name "x.1" comes from the "RS spec" !*) |
509 val inst = |
509 val inst = |
510 case elem_frees of [_] => I |
510 case elem_frees of [_] => I |
511 | _ => Drule.instantiate_normalize (TVars.empty, Vars.make [(((("x",1), Ind_Syntax.iT)), |
511 | _ => Drule.instantiate_normalize (TVars.empty, |
512 Thm.global_cterm_of thy4 elem_tuple)]); |
512 Vars.make [(\<^var>\<open>?x1::i\<close>, Thm.global_cterm_of thy4 elem_tuple)]); |
513 |
513 |
514 (*strip quantifier and the implication*) |
514 (*strip quantifier and the implication*) |
515 val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp})); |
515 val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp})); |
516 |
516 |
517 val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (pred_var $ _) = Thm.concl_of induct0 |
517 val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (pred_var $ _) = Thm.concl_of induct0 |