531 val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl |
531 val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl |
532 (fn {prems, ...} => EVERY |
532 (fn {prems, ...} => EVERY |
533 [rewrite_goals_tac [inductive_conj_def], |
533 [rewrite_goals_tac [inductive_conj_def], |
534 DETERM (rtac raw_fp_induct 1), |
534 DETERM (rtac raw_fp_induct 1), |
535 REPEAT (resolve_tac [le_funI, le_boolI] 1), |
535 REPEAT (resolve_tac [le_funI, le_boolI] 1), |
536 rewrite_goals_tac (map mk_meta_eq [inf_fun_eq, inf_bool_eq] @ simp_thms'), |
536 rewrite_goals_tac (inf_fun_eq :: inf_bool_eq :: simp_thms'), |
537 (*This disjE separates out the introduction rules*) |
537 (*This disjE separates out the introduction rules*) |
538 REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), |
538 REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), |
539 (*Now break down the individual cases. No disjE here in case |
539 (*Now break down the individual cases. No disjE here in case |
540 some premise involves disjunction.*) |
540 some premise involves disjunction.*) |
541 REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)), |
541 REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)), |