55 (x, tuple (map Free avoiding)) :: |
55 (x, tuple (map Free avoiding)) :: |
56 map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst) |
56 map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst) |
57 end; |
57 end; |
58 val substs = |
58 val substs = |
59 map2 subst insts concls |> flat |> distinct (op =) |
59 map2 subst insts concls |> flat |> distinct (op =) |
60 |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt))); |
60 |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt))); |
61 in |
61 in |
62 (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) |
62 (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) |
63 end; |
63 end; |
64 |
64 |
65 fun rename_params_rule internal xs rule = |
65 fun rename_params_rule internal xs rule = |
84 |
84 |
85 (* nominal_induct_tac *) |
85 (* nominal_induct_tac *) |
86 |
86 |
87 fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts = |
87 fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts = |
88 let |
88 let |
89 val thy = ProofContext.theory_of ctxt; |
89 val thy = Proof_Context.theory_of ctxt; |
90 val cert = Thm.cterm_of thy; |
90 val cert = Thm.cterm_of thy; |
91 |
91 |
92 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; |
92 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; |
93 val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; |
93 val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; |
94 |
94 |
115 val k = nth concls (j - 1) + more_consumes |
115 val k = nth concls (j - 1) + more_consumes |
116 in |
116 in |
117 Method.insert_tac (more_facts @ adefs) THEN' |
117 Method.insert_tac (more_facts @ adefs) THEN' |
118 (if simp then |
118 (if simp then |
119 Induct.rotate_tac k (length adefs) THEN' |
119 Induct.rotate_tac k (length adefs) THEN' |
120 Induct.fix_tac defs_ctxt k |
120 Induct.arbitrary_tac defs_ctxt k |
121 (List.partition (member op = frees) xs |> op @) |
121 (List.partition (member op = frees) xs |> op @) |
122 else |
122 else |
123 Induct.fix_tac defs_ctxt k xs) |
123 Induct.arbitrary_tac defs_ctxt k xs) |
124 end) |
124 end) |
125 THEN' Induct.inner_atomize_tac) j)) |
125 THEN' Induct.inner_atomize_tac) j)) |
126 THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' => |
126 THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' => |
127 Induct.guess_instance ctxt |
127 Induct.guess_instance ctxt |
128 (finish_rule (Induct.internalize more_consumes rule)) i st' |
128 (finish_rule (Induct.internalize more_consumes rule)) i st' |
129 |> Seq.maps (fn rule' => |
129 |> Seq.maps (fn rule' => |
130 CASES (rule_cases ctxt rule' cases) |
130 CASES (rule_cases ctxt rule' cases) |
131 (Tactic.rtac (rename_params_rule false [] rule') i THEN |
131 (Tactic.rtac (rename_params_rule false [] rule') i THEN |
132 PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) |
132 PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) |
133 THEN_ALL_NEW_CASES |
133 THEN_ALL_NEW_CASES |
134 ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac) |
134 ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac) |
135 else K all_tac) |
135 else K all_tac) |
136 THEN_ALL_NEW Induct.rulify_tac) |
136 THEN_ALL_NEW Induct.rulify_tac) |
137 end; |
137 end; |