4 Turn elimination rules into atomic expressions in the object logic. |
4 Turn elimination rules into atomic expressions in the object logic. |
5 *) |
5 *) |
6 |
6 |
7 signature ATOMIZE_ELIM = |
7 signature ATOMIZE_ELIM = |
8 sig |
8 sig |
9 val declare_atomize_elim : attribute |
9 val declare_atomize_elim : attribute |
10 |
|
11 val atomize_elim_conv : Proof.context -> conv |
10 val atomize_elim_conv : Proof.context -> conv |
12 val full_atomize_elim_conv : Proof.context -> conv |
11 val full_atomize_elim_conv : Proof.context -> conv |
13 |
|
14 val atomize_elim_tac : Proof.context -> int -> tactic |
12 val atomize_elim_tac : Proof.context -> int -> tactic |
15 |
|
16 val setup : theory -> theory |
|
17 end |
13 end |
18 |
14 |
19 structure AtomizeElim : ATOMIZE_ELIM = |
15 structure Atomize_Elim : ATOMIZE_ELIM = |
20 struct |
16 struct |
21 |
17 |
22 (* theory data *) |
18 (* theory data *) |
23 |
19 |
24 structure AtomizeElimData = Named_Thms |
20 structure AtomizeElimData = Named_Thms |
25 ( |
21 ( |
26 val name = @{binding atomize_elim}; |
22 val name = @{binding atomize_elim}; |
27 val description = "atomize_elim rewrite rule"; |
23 val description = "atomize_elim rewrite rule"; |
28 ); |
24 ); |
|
25 |
|
26 val _ = Theory.setup AtomizeElimData.setup; |
29 |
27 |
30 val declare_atomize_elim = AtomizeElimData.add |
28 val declare_atomize_elim = AtomizeElimData.add |
31 |
29 |
32 (* More conversions: *) |
30 (* More conversions: *) |
33 local open Conv in |
31 local open Conv in |
48 val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd))) |
46 val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd))) |
49 |> Drule.rearrange_prems (invert_perm pi') |
47 |> Drule.rearrange_prems (invert_perm pi') |
50 in Thm.equal_intr fwd back end |
48 in Thm.equal_intr fwd back end |
51 |
49 |
52 |
50 |
53 (* convert !!thesis. (!!x y z. ... => thesis) ==> ... |
51 (* convert !!thesis. (!!x y z. ... => thesis) ==> ... |
54 ==> (!!a b c. ... => thesis) |
52 ==> (!!a b c. ... => thesis) |
55 ==> thesis |
53 ==> thesis |
56 |
54 |
57 to |
55 to |
58 |
56 |
69 |
67 |
70 (* Move the thesis-quantifier inside over other quantifiers and unrelated prems *) |
68 (* Move the thesis-quantifier inside over other quantifiers and unrelated prems *) |
71 fun thesis_miniscope_conv inner_cv ctxt = |
69 fun thesis_miniscope_conv inner_cv ctxt = |
72 let |
70 let |
73 (* check if the outermost quantifier binds the conclusion *) |
71 (* check if the outermost quantifier binds the conclusion *) |
74 fun is_forall_thesis t = |
72 fun is_forall_thesis t = |
75 case Logic.strip_assums_concl t of |
73 case Logic.strip_assums_concl t of |
76 (_ $ Bound i) => i = length (Logic.strip_params t) - 1 |
74 (_ $ Bound i) => i = length (Logic.strip_params t) - 1 |
77 | _ => false |
75 | _ => false |
78 |
76 |
79 (* move unrelated assumptions out of the quantification *) |
77 (* move unrelated assumptions out of the quantification *) |
91 then_conv (funpow (length idxs) skip_over_assm (inner_cv ctxt))) |
89 then_conv (funpow (length idxs) skip_over_assm (inner_cv ctxt))) |
92 ct |
90 ct |
93 end |
91 end |
94 |
92 |
95 (* move current quantifier to the right *) |
93 (* move current quantifier to the right *) |
96 fun moveq_conv ctxt = |
94 fun moveq_conv ctxt = |
97 (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt)) |
95 (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt)) |
98 else_conv (movea_conv ctxt) |
96 else_conv (movea_conv ctxt) |
99 |
97 |
100 fun ms_conv ctxt ct = |
98 fun ms_conv ctxt ct = |
101 if is_forall_thesis (term_of ct) |
99 if is_forall_thesis (term_of ct) |
102 then moveq_conv ctxt ct |
100 then moveq_conv ctxt ct |
103 else (implies_concl_conv (ms_conv ctxt) |
101 else (implies_concl_conv (ms_conv ctxt) |
104 else_conv |
102 else_conv |
105 (forall_conv (ms_conv o snd) ctxt)) |
103 (forall_conv (ms_conv o snd) ctxt)) |
106 ct |
104 ct |
107 in |
105 in |
108 ms_conv ctxt |
106 ms_conv ctxt |
109 end |
107 end |
110 |
108 |
111 val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv |
109 val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv |
112 |
110 |
113 end |
111 end |
115 |
113 |
116 fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) => |
114 fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) => |
117 let |
115 let |
118 val thy = Proof_Context.theory_of ctxt |
116 val thy = Proof_Context.theory_of ctxt |
119 val _ $ thesis = Logic.strip_assums_concl subg |
117 val _ $ thesis = Logic.strip_assums_concl subg |
120 |
118 |
121 (* Introduce a quantifier first if the thesis is not bound *) |
119 (* Introduce a quantifier first if the thesis is not bound *) |
122 val quantify_thesis = |
120 val quantify_thesis = |
123 if is_Bound thesis then all_tac |
121 if is_Bound thesis then all_tac |
124 else let |
122 else let |
125 val cthesis = cterm_of thy thesis |
123 val cthesis = cterm_of thy thesis |
126 val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] |
124 val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] |
127 @{thm meta_spec} |
125 @{thm meta_spec} |
128 in |
126 in |
129 compose_tac (false, rule, 1) i |
127 compose_tac (false, rule, 1) i |
130 end |
128 end |
131 in |
129 in |
132 quantify_thesis |
130 quantify_thesis |
133 THEN (CONVERSION (full_atomize_elim_conv ctxt) i) |
131 THEN (CONVERSION (full_atomize_elim_conv ctxt) i) |
134 end) |
132 end) |
135 |
133 |
136 val setup = |
134 val _ = |
137 Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac)) |
135 Theory.setup |
138 "convert obtains statement to atomic object logic goal" |
136 (Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac)) |
139 #> AtomizeElimData.setup |
137 "convert obtains statement to atomic object logic goal") |
140 |
138 |
141 end |
139 end |