4 *) |
4 *) |
5 |
5 |
6 structure Predicate_Compile_Aux = |
6 structure Predicate_Compile_Aux = |
7 struct |
7 struct |
8 |
8 |
|
9 (* general syntactic functions *) |
|
10 |
|
11 (*Like dest_conj, but flattens conjunctions however nested*) |
|
12 fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs) |
|
13 | conjuncts_aux t conjs = t::conjs; |
|
14 |
|
15 fun conjuncts t = conjuncts_aux t []; |
|
16 |
9 (* syntactic functions *) |
17 (* syntactic functions *) |
10 |
18 |
11 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true |
19 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true |
12 | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true |
20 | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true |
13 | is_equationlike_term _ = false |
21 | is_equationlike_term _ = false |
14 |
22 |
15 val is_equationlike = is_equationlike_term o prop_of |
23 val is_equationlike = is_equationlike_term o prop_of |
71 |
79 |
72 (* introduction rule combinators *) |
80 (* introduction rule combinators *) |
73 |
81 |
74 (* combinators to apply a function to all literals of an introduction rules *) |
82 (* combinators to apply a function to all literals of an introduction rules *) |
75 |
83 |
76 (* |
|
77 fun map_atoms f intro = |
84 fun map_atoms f intro = |
78 *) |
85 let |
|
86 val (literals, head) = Logic.strip_horn intro |
|
87 fun appl t = (case t of |
|
88 (@{term "Not"} $ t') => HOLogic.mk_not (f t') |
|
89 | _ => f t) |
|
90 in |
|
91 Logic.list_implies |
|
92 (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head) |
|
93 end |
79 |
94 |
80 fun fold_atoms f intro s = |
95 fun fold_atoms f intro s = |
81 let |
96 let |
82 val (literals, head) = Logic.strip_horn intro |
97 val (literals, head) = Logic.strip_horn intro |
83 fun appl t s = (case t of |
98 fun appl t s = (case t of |
87 |
102 |
88 fun fold_map_atoms f intro s = |
103 fun fold_map_atoms f intro s = |
89 let |
104 let |
90 val (literals, head) = Logic.strip_horn intro |
105 val (literals, head) = Logic.strip_horn intro |
91 fun appl t s = (case t of |
106 fun appl t s = (case t of |
92 (@{term "Not"} $ t') => |
107 (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s) |
93 let |
|
94 val (t'', s') = f t' s |
|
95 in (@{term "Not"} $ t'', s') end |
|
96 | _ => f t s) |
108 | _ => f t s) |
97 val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s |
109 val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s |
98 in |
110 in |
99 (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') |
111 (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') |
100 end; |
112 end; |
101 |
113 |
|
114 fun maps_premises f intro = |
|
115 let |
|
116 val (premises, head) = Logic.strip_horn intro |
|
117 in |
|
118 Logic.list_implies (maps f premises, head) |
|
119 end |
|
120 |
|
121 (* lifting term operations to theorems *) |
|
122 |
|
123 fun map_term thy f th = |
|
124 setmp quick_and_dirty true (SkipProof.make_thm thy) (f (prop_of th)) |
|
125 |
102 (* |
126 (* |
103 fun equals_conv lhs_cv rhs_cv ct = |
127 fun equals_conv lhs_cv rhs_cv ct = |
104 case Thm.term_of ct of |
128 case Thm.term_of ct of |
105 Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct |
129 Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct |
106 | _ => error "equals_conv" |
130 | _ => error "equals_conv" |
120 inductify : bool, |
144 inductify : bool, |
121 rpred : bool |
145 rpred : bool |
122 }; |
146 }; |
123 |
147 |
124 fun show_steps (Options opt) = #show_steps opt |
148 fun show_steps (Options opt) = #show_steps opt |
|
149 fun show_mode_inference (Options opt) = #show_mode_inference opt |
125 fun show_intermediate_results (Options opt) = #show_intermediate_results opt |
150 fun show_intermediate_results (Options opt) = #show_intermediate_results opt |
126 fun show_proof_trace (Options opt) = #show_proof_trace opt |
151 fun show_proof_trace (Options opt) = #show_proof_trace opt |
127 |
152 |
128 fun is_inductify (Options opt) = #inductify opt |
153 fun is_inductify (Options opt) = #inductify opt |
129 fun is_rpred (Options opt) = #rpred opt |
154 fun is_rpred (Options opt) = #rpred opt |
188 val intro'' = Thm.instantiate (T_insts, t_insts') intro |
213 val intro'' = Thm.instantiate (T_insts, t_insts') intro |
189 val [intro'''] = Variable.export ctxt3 ctxt [intro''] |
214 val [intro'''] = Variable.export ctxt3 ctxt [intro''] |
190 val intro'''' = Simplifier.full_simplify |
215 val intro'''' = Simplifier.full_simplify |
191 (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) |
216 (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) |
192 intro''' |
217 intro''' |
193 in |
218 (* splitting conjunctions introduced by Pair_eq*) |
194 intro'''' |
219 fun split_conj prem = |
|
220 map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem)) |
|
221 val intro''''' = map_term thy (maps_premises split_conj) intro'''' |
|
222 in |
|
223 intro''''' |
195 end |
224 end |
196 |
225 |
197 |
226 |
198 |
227 |
199 end; |
228 end; |