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 (Proof_Context.theory_of ctxt))); |
60 |> map (apply2 (Thm.cterm_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 = Proof_Context.theory_of ctxt; |
|
90 val cert = Thm.cterm_of thy; |
|
91 |
|
92 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; |
89 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_ctxt))) defs; |
90 val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs; |
94 |
91 |
95 val finish_rule = |
92 val finish_rule = |
96 split_all_tuples defs_ctxt |
93 split_all_tuples defs_ctxt |
97 #> rename_params_rule true |
94 #> rename_params_rule true |
98 (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); |
95 (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); |
99 |
96 |
100 fun rule_cases ctxt r = |
97 fun rule_cases ctxt r = |
101 let val r' = if simp then Induct.simplified_rule ctxt r else r |
98 let val r' = if simp then Induct.simplified_rule ctxt r else r |
102 in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end; |
99 in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end; |
103 in |
100 in |
104 (fn i => fn st => |
101 (fn i => fn st => |
105 rules |
102 rules |
106 |> inst_mutual_rule ctxt insts avoiding |
103 |> inst_mutual_rule ctxt insts avoiding |
107 |> Rule_Cases.consume ctxt (flat defs) facts |
104 |> Rule_Cases.consume ctxt (flat defs) facts |
108 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => |
105 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => |
109 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => |
106 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => |
110 (CONJUNCTS (ALLGOALS |
107 (CONJUNCTS (ALLGOALS |
111 let |
108 let |
112 val adefs = nth_list atomized_defs (j - 1); |
109 val adefs = nth_list atomized_defs (j - 1); |
113 val frees = fold (Term.add_frees o prop_of) adefs []; |
110 val frees = fold (Term.add_frees o Thm.prop_of) adefs []; |
114 val xs = nth_list fixings (j - 1); |
111 val xs = nth_list fixings (j - 1); |
115 val k = nth concls (j - 1) + more_consumes |
112 val k = nth concls (j - 1) + more_consumes |
116 in |
113 in |
117 Method.insert_tac (more_facts @ adefs) THEN' |
114 Method.insert_tac (more_facts @ adefs) THEN' |
118 (if simp then |
115 (if simp then |
129 |> Seq.maps (fn rule' => |
126 |> Seq.maps (fn rule' => |
130 CASES (rule_cases ctxt rule' cases) |
127 CASES (rule_cases ctxt rule' cases) |
131 (Tactic.rtac (rename_params_rule false [] rule') i THEN |
128 (Tactic.rtac (rename_params_rule false [] rule') i THEN |
132 PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) |
129 PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) |
133 THEN_ALL_NEW_CASES |
130 THEN_ALL_NEW_CASES |
134 ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac) |
131 ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt) |
135 else K all_tac) |
132 else K all_tac) |
136 THEN_ALL_NEW Induct.rulify_tac ctxt) |
133 THEN_ALL_NEW Induct.rulify_tac ctxt) |
137 end; |
134 end; |
138 |
135 |
139 |
136 |
174 |
171 |
175 val nominal_induct_method = |
172 val nominal_induct_method = |
176 Scan.lift (Args.mode Induct.no_simpN) -- |
173 Scan.lift (Args.mode Induct.no_simpN) -- |
177 (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- |
174 (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- |
178 avoiding -- fixing -- rule_spec) >> |
175 avoiding -- fixing -- rule_spec) >> |
179 (fn (no_simp, (((x, y), z), w)) => fn ctxt => |
176 (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts => |
180 RAW_METHOD_CASES (fn facts => |
177 HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)); |
181 HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts))); |
|
182 |
178 |
183 end |
179 end |
184 |
180 |
185 end; |
181 end; |