equal
deleted
inserted
replaced
3 The nominal induct proof method. |
3 The nominal induct proof method. |
4 *) |
4 *) |
5 |
5 |
6 structure NominalInduct: |
6 structure NominalInduct: |
7 sig |
7 sig |
8 val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> |
8 val nominal_induct_tac: bool -> (binding option * (term * bool)) option list list -> |
9 (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> Rule_Cases.cases_tactic |
9 (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> context_tactic |
10 |
|
11 val nominal_induct_method: (Proof.context -> Proof.method) context_parser |
10 val nominal_induct_method: (Proof.context -> Proof.method) context_parser |
12 end = |
11 end = |
13 |
12 |
14 struct |
13 struct |
15 |
14 |
17 |
16 |
18 fun tupleT Ts = HOLogic.unitT |> fold (fn T => fn U => HOLogic.mk_prodT (U, T)) Ts; |
17 fun tupleT Ts = HOLogic.unitT |> fold (fn T => fn U => HOLogic.mk_prodT (U, T)) Ts; |
19 fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts; |
18 fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts; |
20 |
19 |
21 fun tuple_fun Ts (xi, T) = |
20 fun tuple_fun Ts (xi, T) = |
22 Library.funpow (length Ts) HOLogic.mk_split |
21 Library.funpow (length Ts) HOLogic.mk_case_prod |
23 (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
22 (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
24 |
23 |
25 fun split_all_tuples ctxt = |
24 fun split_all_tuples ctxt = |
26 Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps |
25 Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps |
27 @{thms split_conv split_paired_all unit_all_eq1} @ |
26 @{thms split_conv split_paired_all unit_all_eq1} @ |
55 (x, tuple (map Free avoiding)) :: |
54 (x, tuple (map Free avoiding)) :: |
56 map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst) |
55 map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst) |
57 end; |
56 end; |
58 val substs = |
57 val substs = |
59 map2 subst insts concls |> flat |> distinct (op =) |
58 map2 subst insts concls |> flat |> distinct (op =) |
60 |> map (apply2 (Thm.cterm_of ctxt)); |
59 |> map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of ctxt u)); |
61 in |
60 in |
62 (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) |
61 (((cases, nconcls), consumes), infer_instantiate ctxt substs joined_rule) |
63 end; |
62 end; |
64 |
63 |
65 fun rename_params_rule internal xs rule = |
64 fun rename_params_rule internal xs rule = |
66 let |
65 let |
67 val tune = |
66 val tune = |
77 else map (tune o #1) (take (p - n) ps) @ xs; |
76 else map (tune o #1) (take (p - n) ps) @ xs; |
78 in Logic.list_rename_params ys prem end; |
77 in Logic.list_rename_params ys prem end; |
79 fun rename_prems prop = |
78 fun rename_prems prop = |
80 let val (As, C) = Logic.strip_horn prop |
79 let val (As, C) = Logic.strip_horn prop |
81 in Logic.list_implies (map rename As, C) end; |
80 in Logic.list_implies (map rename As, C) end; |
82 in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; |
81 in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end; |
83 |
82 |
84 |
83 |
85 (* nominal_induct_tac *) |
84 (* nominal_induct_tac *) |
86 |
85 |
87 fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts = |
86 fun nominal_induct_tac simp def_insts avoiding fixings rules facts i (ctxt, st) = |
88 let |
87 let |
89 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; |
88 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; |
90 val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs; |
89 val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs; |
91 |
90 |
92 val finish_rule = |
91 val finish_rule = |
95 (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); |
94 (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); |
96 |
95 |
97 fun rule_cases ctxt r = |
96 fun rule_cases ctxt r = |
98 let val r' = if simp then Induct.simplified_rule ctxt r else r |
97 let val r' = if simp then Induct.simplified_rule ctxt r else r |
99 in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end; |
98 in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end; |
100 in |
99 |
101 (fn i => fn st => |
100 fun context_tac _ _ = |
102 rules |
101 rules |
103 |> inst_mutual_rule ctxt insts avoiding |
102 |> inst_mutual_rule ctxt insts avoiding |
104 |> Rule_Cases.consume ctxt (flat defs) facts |
103 |> Rule_Cases.consume ctxt (flat defs) facts |
105 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => |
104 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => |
106 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => |
105 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => |
109 val adefs = nth_list atomized_defs (j - 1); |
108 val adefs = nth_list atomized_defs (j - 1); |
110 val frees = fold (Term.add_frees o Thm.prop_of) adefs []; |
109 val frees = fold (Term.add_frees o Thm.prop_of) adefs []; |
111 val xs = nth_list fixings (j - 1); |
110 val xs = nth_list fixings (j - 1); |
112 val k = nth concls (j - 1) + more_consumes |
111 val k = nth concls (j - 1) + more_consumes |
113 in |
112 in |
114 Method.insert_tac (more_facts @ adefs) THEN' |
113 Method.insert_tac ctxt (more_facts @ adefs) THEN' |
115 (if simp then |
114 (if simp then |
116 Induct.rotate_tac k (length adefs) THEN' |
115 Induct.rotate_tac k (length adefs) THEN' |
117 Induct.arbitrary_tac defs_ctxt k |
116 Induct.arbitrary_tac defs_ctxt k |
118 (List.partition (member op = frees) xs |> op @) |
117 (List.partition (member op = frees) xs |> op @) |
119 else |
118 else |
122 THEN' Induct.inner_atomize_tac ctxt) j)) |
121 THEN' Induct.inner_atomize_tac ctxt) j)) |
123 THEN' Induct.atomize_tac ctxt) i st |> Seq.maps (fn st' => |
122 THEN' Induct.atomize_tac ctxt) i st |> Seq.maps (fn st' => |
124 Induct.guess_instance ctxt |
123 Induct.guess_instance ctxt |
125 (finish_rule (Induct.internalize ctxt more_consumes rule)) i st' |
124 (finish_rule (Induct.internalize ctxt more_consumes rule)) i st' |
126 |> Seq.maps (fn rule' => |
125 |> Seq.maps (fn rule' => |
127 CASES (rule_cases ctxt rule' cases) |
126 CONTEXT_CASES (rule_cases ctxt rule' cases) |
128 (Tactic.rtac (rename_params_rule false [] rule') i THEN |
127 (resolve_tac ctxt [rename_params_rule false [] rule'] i THEN |
129 PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) |
128 PRIMITIVE |
130 THEN_ALL_NEW_CASES |
129 (singleton (Proof_Context.export defs_ctxt |
|
130 (Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) ctxt)))) (ctxt, st')))); |
|
131 in |
|
132 (context_tac CONTEXT_THEN_ALL_NEW |
131 ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt) |
133 ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt) |
132 else K all_tac) |
134 else K all_tac) THEN_ALL_NEW Induct.rulify_tac ctxt)) i (ctxt, st) |
133 THEN_ALL_NEW Induct.rulify_tac ctxt) |
|
134 end; |
135 end; |
135 |
136 |
136 |
137 |
137 (* concrete syntax *) |
138 (* concrete syntax *) |
138 |
139 |
171 |
172 |
172 val nominal_induct_method = |
173 val nominal_induct_method = |
173 Scan.lift (Args.mode Induct.no_simpN) -- |
174 Scan.lift (Args.mode Induct.no_simpN) -- |
174 (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- |
175 (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- |
175 avoiding -- fixing -- rule_spec) >> |
176 avoiding -- fixing -- rule_spec) >> |
176 (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts => |
177 (fn (no_simp, (((x, y), z), w)) => fn _ => fn facts => |
177 HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)); |
178 nominal_induct_tac (not no_simp) x y z w facts 1); |
178 |
179 |
179 end |
180 end |
180 |
181 |
181 end; |
182 end; |