71 end) |
71 end) |
72 else (t, T, vTs, env) |
72 else (t, T, vTs, env) |
73 | infer_type thy env Ts vTs (t as Free (s, T)) = |
73 | infer_type thy env Ts vTs (t as Free (s, T)) = |
74 if T = dummyT then (case Symtab.lookup vTs s of |
74 if T = dummyT then (case Symtab.lookup vTs s of |
75 NONE => |
75 NONE => |
76 let val (env', T) = mk_tvar (env, []) |
76 let val (T, env') = mk_tvar [] env |
77 in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end |
77 in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end |
78 | SOME T => (Free (s, T), T, vTs, env)) |
78 | SOME T => (Free (s, T), T, vTs, env)) |
79 else (t, T, vTs, env) |
79 else (t, T, vTs, env) |
80 | infer_type thy env Ts vTs (Var _) = error "reconstruct_proof: internal error" |
80 | infer_type thy env Ts vTs (Var _) = error "reconstruct_proof: internal error" |
81 | infer_type thy env Ts vTs (Abs (s, T, t)) = |
81 | infer_type thy env Ts vTs (Abs (s, T, t)) = |
82 let |
82 let |
83 val (env', T') = if T = dummyT then mk_tvar (env, []) else (env, T); |
83 val (T', env') = if T = dummyT then mk_tvar [] env else (T, env); |
84 val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t |
84 val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t |
85 in (Abs (s, T', t'), T' --> U, vTs', env'') end |
85 in (Abs (s, T', t'), T' --> U, vTs', env'') end |
86 | infer_type thy env Ts vTs (t $ u) = |
86 | infer_type thy env Ts vTs (t $ u) = |
87 let |
87 let |
88 val (t', T, vTs1, env1) = infer_type thy env Ts vTs t; |
88 val (t', T, vTs1, env1) = infer_type thy env Ts vTs t; |
89 val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u; |
89 val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u; |
90 in (case chaseT env2 T of |
90 in (case chaseT env2 T of |
91 Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') |
91 Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') |
92 | _ => |
92 | _ => |
93 let val (env3, V) = mk_tvar (env2, []) |
93 let val (V, env3) = mk_tvar [] env2 |
94 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) |
94 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) |
95 end |
95 end |
96 | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) |
96 | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) |
97 handle Subscript => error ("infer_type: bad variable index " ^ string_of_int i)); |
97 handle Subscript => error ("infer_type: bad variable index " ^ string_of_int i)); |
98 |
98 |
99 fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^ |
99 fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^ |
100 Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u); |
100 Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u); |
101 |
101 |
102 fun decompose thy Ts (env, p as (t, u)) = |
102 fun decompose thy Ts (p as (t, u)) env = |
103 let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p |
103 let |
104 else apsnd flat (Library.foldl_map (decompose thy Ts) (uT env T U, ts ~~ us)) |
104 fun rigrig (a, T) (b, U) uT ts us = |
105 in case pairself (strip_comb o Envir.head_norm env) p of |
105 if a <> b then cantunify thy p |
|
106 else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U)) |
|
107 in |
|
108 case pairself (strip_comb o Envir.head_norm env) p of |
106 ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us |
109 ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us |
107 | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us |
110 | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us |
108 | ((Bound i, ts), (Bound j, us)) => |
111 | ((Bound i, ts), (Bound j, us)) => |
109 rigrig (i, dummyT) (j, dummyT) (K o K) ts us |
112 rigrig (i, dummyT) (j, dummyT) (K o K) ts us |
110 | ((Abs (_, T, t), []), (Abs (_, U, u), [])) => |
113 | ((Abs (_, T, t), []), (Abs (_, U, u), [])) => |
111 decompose thy (T::Ts) (unifyT thy env T U, (t, u)) |
114 decompose thy (T::Ts) (t, u) (unifyT thy env T U) |
112 | ((Abs (_, T, t), []), _) => |
115 | ((Abs (_, T, t), []), _) => |
113 decompose thy (T::Ts) (env, (t, incr_boundvars 1 u $ Bound 0)) |
116 decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env |
114 | (_, (Abs (_, T, u), [])) => |
117 | (_, (Abs (_, T, u), [])) => |
115 decompose thy (T::Ts) (env, (incr_boundvars 1 t $ Bound 0, u)) |
118 decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env |
116 | _ => (env, [(mk_abs Ts t, mk_abs Ts u)]) |
119 | _ => ([(mk_abs Ts t, mk_abs Ts u)], env) |
117 end; |
120 end; |
118 |
121 |
119 fun make_constraints_cprf thy env cprf = |
122 fun make_constraints_cprf thy env cprf = |
120 let |
123 let |
121 fun add_cnstrt Ts prop prf cs env vTs (t, u) = |
124 fun add_cnstrt Ts prop prf cs env vTs (t, u) = |
123 val t' = mk_abs Ts t; |
126 val t' = mk_abs Ts t; |
124 val u' = mk_abs Ts u |
127 val u' = mk_abs Ts u |
125 in |
128 in |
126 (prop, prf, cs, Pattern.unify thy (t', u') env, vTs) |
129 (prop, prf, cs, Pattern.unify thy (t', u') env, vTs) |
127 handle Pattern.Pattern => |
130 handle Pattern.Pattern => |
128 let val (env', cs') = decompose thy [] (env, (t', u')) |
131 let val (cs', env') = decompose thy [] (t', u') env |
129 in (prop, prf, cs @ cs', env', vTs) end |
132 in (prop, prf, cs @ cs', env', vTs) end |
130 | Pattern.Unif => |
133 | Pattern.Unif => |
131 cantunify thy (Envir.norm_term env t', Envir.norm_term env u') |
134 cantunify thy (Envir.norm_term env t', Envir.norm_term env u') |
132 end; |
135 end; |
133 |
136 |
134 fun mk_cnstrts_atom env vTs prop opTs prf = |
137 fun mk_cnstrts_atom env vTs prop opTs prf = |
135 let |
138 let |
136 val tvars = OldTerm.term_tvars prop; |
139 val tvars = OldTerm.term_tvars prop; |
137 val tfrees = OldTerm.term_tfrees prop; |
140 val tfrees = OldTerm.term_tfrees prop; |
138 val (env', Ts) = |
141 val (Ts, env') = |
139 (case opTs of |
142 (case opTs of |
140 NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees) |
143 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env |
141 | SOME Ts => (env, Ts)); |
144 | SOME Ts => (Ts, env)); |
142 val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) |
145 val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) |
143 (forall_intr_vfs prop) handle Library.UnequalLengths => |
146 (forall_intr_vfs prop) handle Library.UnequalLengths => |
144 error ("Wrong number of type arguments for " ^ |
147 error ("Wrong number of type arguments for " ^ |
145 quote (get_name [] prop prf)) |
148 quote (get_name [] prop prf)) |
146 in (prop', change_type (SOME Ts) prf, [], env', vTs) end; |
149 in (prop', change_type (SOME Ts) prf, [], env', vTs) end; |
150 |
153 |
151 fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs) |
154 fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs) |
152 handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i)) |
155 handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i)) |
153 | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = |
156 | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = |
154 let |
157 let |
155 val (env', T) = (case opT of |
158 val (T, env') = |
156 NONE => mk_tvar (env, []) | SOME T => (env, T)); |
159 (case opT of |
|
160 NONE => mk_tvar [] env |
|
161 | SOME T => (T, env)); |
157 val (t, prf, cnstrts, env'', vTs') = |
162 val (t, prf, cnstrts, env'', vTs') = |
158 mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; |
163 mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; |
159 in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), |
164 in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), |
160 cnstrts, env'', vTs') |
165 cnstrts, env'', vTs') |
161 end |
166 end |
165 val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf; |
170 val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf; |
166 in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'') |
171 in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'') |
167 end |
172 end |
168 | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) = |
173 | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) = |
169 let |
174 let |
170 val (env', t) = mk_var env Ts propT; |
175 val (t, env') = mk_var env Ts propT; |
171 val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf; |
176 val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf; |
172 in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs') |
177 in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs') |
173 end |
178 end |
174 | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) = |
179 | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) = |
175 let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2 |
180 let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2 |
176 in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of |
181 in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of |
177 (Const ("==>", _) $ u' $ t', prf1, cnstrts', env'', vTs'') => |
182 (Const ("==>", _) $ u' $ t', prf1, cnstrts', env'', vTs'') => |
178 add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts) |
183 add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts) |
179 env'' vTs'' (u, u') |
184 env'' vTs'' (u, u') |
180 | (t, prf1, cnstrts', env'', vTs'') => |
185 | (t, prf1, cnstrts', env'', vTs'') => |
181 let val (env''', v) = mk_var env'' Ts propT |
186 let val (v, env''') = mk_var env'' Ts propT |
182 in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts) |
187 in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts) |
183 env''' vTs'' (t, Logic.mk_implies (u, v)) |
188 env''' vTs'' (t, Logic.mk_implies (u, v)) |
184 end) |
189 end) |
185 end |
190 end |
186 | mk_cnstrts env Ts Hs vTs (cprf % SOME t) = |
191 | mk_cnstrts env Ts Hs vTs (cprf % SOME t) = |
190 prf, cnstrts, env2, vTs2) => |
195 prf, cnstrts, env2, vTs2) => |
191 let val env3 = unifyT thy env2 T U |
196 let val env3 = unifyT thy env2 T U |
192 in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) |
197 in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) |
193 end |
198 end |
194 | (u, prf, cnstrts, env2, vTs2) => |
199 | (u, prf, cnstrts, env2, vTs2) => |
195 let val (env3, v) = mk_var env2 Ts (U --> propT); |
200 let val (v, env3) = mk_var env2 Ts (U --> propT); |
196 in |
201 in |
197 add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2 |
202 add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2 |
198 (u, Const ("all", (U --> propT) --> propT) $ v) |
203 (u, Const ("all", (U --> propT) --> propT) $ v) |
199 end) |
204 end) |
200 end |
205 end |
201 | mk_cnstrts env Ts Hs vTs (cprf % NONE) = |
206 | mk_cnstrts env Ts Hs vTs (cprf % NONE) = |
202 (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of |
207 (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of |
203 (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, |
208 (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, |
204 prf, cnstrts, env', vTs') => |
209 prf, cnstrts, env', vTs') => |
205 let val (env'', t) = mk_var env' Ts T |
210 let val (t, env'') = mk_var env' Ts T |
206 in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs') |
211 in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs') |
207 end |
212 end |
208 | (u, prf, cnstrts, env', vTs') => |
213 | (u, prf, cnstrts, env', vTs') => |
209 let |
214 let |
210 val (env1, T) = mk_tvar (env', []); |
215 val (T, env1) = mk_tvar [] env'; |
211 val (env2, v) = mk_var env1 Ts (T --> propT); |
216 val (v, env2) = mk_var env1 Ts (T --> propT); |
212 val (env3, t) = mk_var env2 Ts T |
217 val (t, env3) = mk_var env2 Ts T |
213 in |
218 in |
214 add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs' |
219 add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs' |
215 (u, Const ("all", (T --> propT) --> propT) $ v) |
220 (u, Const ("all", (T --> propT) --> propT) $ v) |
216 end) |
221 end) |
217 | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs), _))) = |
222 | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs), _))) = |