100 is_before_skolemize_rule () then |
100 is_before_skolemize_rule () then |
101 add_lines_pass2 ((name, role, t, rule, deps) :: res) lines |
101 add_lines_pass2 ((name, role, t, rule, deps) :: res) lines |
102 else |
102 else |
103 add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines) |
103 add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines) |
104 end |
104 end |
105 |
|
106 val add_labels_of_proof = |
|
107 steps_of_proof |
|
108 #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I)) |
|
109 |
|
110 fun kill_useless_labels_in_proof proof = |
|
111 let |
|
112 val used_ls = add_labels_of_proof proof [] |
|
113 |
|
114 fun kill_label l = if member (op =) used_ls l then l else no_label |
|
115 fun kill_assms assms = map (apfst kill_label) assms |
|
116 |
|
117 fun kill_step (Prove (qs, xs, l, t, subproofs, by)) = |
|
118 Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by) |
|
119 | kill_step step = step |
|
120 and kill_proof (Proof (fix, assms, steps)) = |
|
121 Proof (fix, kill_assms assms, map kill_step steps) |
|
122 in |
|
123 kill_proof proof |
|
124 end |
|
125 |
|
126 val assume_prefix = "a" |
|
127 val have_prefix = "f" |
|
128 |
|
129 val relabel_proof = |
|
130 let |
|
131 fun fresh_label depth prefix (accum as (l, subst, next)) = |
|
132 if l = no_label then |
|
133 accum |
|
134 else |
|
135 let val l' = (replicate_string (depth + 1) prefix, next) in |
|
136 (l', (l, l') :: subst, next + 1) |
|
137 end |
|
138 |
|
139 fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst)) |
|
140 |
|
141 fun relabel_assm depth (l, t) (subst, next) = |
|
142 let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in |
|
143 ((l, t), (subst, next)) |
|
144 end |
|
145 |
|
146 fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst |
|
147 |
|
148 fun relabel_steps _ _ _ [] = [] |
|
149 | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) = |
|
150 let |
|
151 val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix |
|
152 val sub = relabel_proofs subst depth sub |
|
153 val by = apfst (relabel_facts subst) by |
|
154 in |
|
155 Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps |
|
156 end |
|
157 | relabel_steps subst depth next (step :: steps) = |
|
158 step :: relabel_steps subst depth next steps |
|
159 and relabel_proof subst depth (Proof (fix, assms, steps)) = |
|
160 let val (assms, subst) = relabel_assms subst depth assms in |
|
161 Proof (fix, assms, relabel_steps subst depth 1 steps) |
|
162 end |
|
163 and relabel_proofs subst depth = map (relabel_proof subst (depth + 1)) |
|
164 in |
|
165 relabel_proof [] 0 |
|
166 end |
|
167 |
|
168 val chain_direct_proof = |
|
169 let |
|
170 fun chain_qs_lfs NONE lfs = ([], lfs) |
|
171 | chain_qs_lfs (SOME l0) lfs = |
|
172 if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs) |
|
173 fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) = |
|
174 let val (qs', lfs) = chain_qs_lfs lbl lfs in |
|
175 Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss)) |
|
176 end |
|
177 | chain_step _ step = step |
|
178 and chain_steps _ [] = [] |
|
179 | chain_steps (prev as SOME _) (i :: is) = |
|
180 chain_step prev i :: chain_steps (label_of_step i) is |
|
181 | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is |
|
182 and chain_proof (Proof (fix, assms, steps)) = |
|
183 Proof (fix, assms, chain_steps (try (List.last #> fst) assms) steps) |
|
184 and chain_proofs proofs = map (chain_proof) proofs |
|
185 in |
|
186 chain_proof |
|
187 end |
|
188 |
105 |
189 type isar_params = |
106 type isar_params = |
190 bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm |
107 bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm |
191 |
108 |
192 val arith_methodss = |
109 val arith_methodss = |