88 let |
88 let |
89 val thy = Proof_Context.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_ctxt))) defs; |
94 |
94 |
95 val finish_rule = |
95 val finish_rule = |
96 split_all_tuples defs_ctxt |
96 split_all_tuples defs_ctxt |
97 #> rename_params_rule true |
97 #> rename_params_rule true |
98 (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); |
98 (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); |
102 in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end; |
102 in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end; |
103 in |
103 in |
104 (fn i => fn st => |
104 (fn i => fn st => |
105 rules |
105 rules |
106 |> inst_mutual_rule ctxt insts avoiding |
106 |> inst_mutual_rule ctxt insts avoiding |
107 |> Rule_Cases.consume (flat defs) facts |
107 |> Rule_Cases.consume ctxt (flat defs) facts |
108 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => |
108 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => |
109 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => |
109 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => |
110 (CONJUNCTS (ALLGOALS |
110 (CONJUNCTS (ALLGOALS |
111 let |
111 let |
112 val adefs = nth_list atomized_defs (j - 1); |
112 val adefs = nth_list atomized_defs (j - 1); |
120 Induct.arbitrary_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.arbitrary_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 ctxt) j)) |
126 THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' => |
126 THEN' Induct.atomize_tac ctxt) 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 ctxt 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 (Proof_Context.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 ctxt) |
137 end; |
137 end; |
138 |
138 |
139 |
139 |
140 (* concrete syntax *) |
140 (* concrete syntax *) |
141 |
141 |