46 val fterms = add_fterms rhs [] |
46 val fterms = add_fterms rhs [] |
47 val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt' |
47 val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt' |
48 val tys = map fastype_of fterms |
48 val tys = map fastype_of fterms |
49 val vs = map Free (xs ~~ tys) |
49 val vs = map Free (xs ~~ tys) |
50 val env = fterms ~~ vs |
50 val env = fterms ~~ vs |
51 (* FIXME!!!!*) |
51 (* FIXME!!!!*) |
52 fun replace_fterms (t as t1 $ t2) = |
52 fun replace_fterms (t as t1 $ t2) = |
53 (case AList.lookup (op aconv) env t of |
53 (case AList.lookup (op aconv) env t of |
54 SOME v => v |
54 SOME v => v |
55 | NONE => replace_fterms t1 $ replace_fterms t2) |
55 | NONE => replace_fterms t1 $ replace_fterms t2) |
56 | replace_fterms t = (case AList.lookup (op aconv) env t of |
56 | replace_fterms t = (case AList.lookup (op aconv) env t of |
57 SOME v => v |
57 SOME v => v |
58 | NONE => t) |
58 | NONE => t) |
59 |
59 |
60 fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t))) |
60 fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t))) |
61 | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)) |
61 | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)) |
62 fun tryext x = (x RS ext2 handle THM _ => x) |
62 fun tryext x = (x RS ext2 handle THM _ => x) |
63 val cong = (Goal.prove ctxt'' [] (map mk_def env) |
63 val cong = (Goal.prove ctxt'' [] (map mk_def env) |
64 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs))) |
64 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs))) |
65 (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x)) |
65 (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x)) |
66 THEN rtac th' 1)) RS sym |
66 THEN rtac th' 1)) RS sym |
67 |
67 |
68 val (cong' :: vars') = |
68 val (cong' :: vars') = |
69 Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs) |
69 Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs) |
70 val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars' |
70 val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars' |
71 |
71 |
132 let |
132 let |
133 val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt |
133 val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt |
134 val (xn,ta) = variant_abs (xn,xT,ta) |
134 val (xn,ta) = variant_abs (xn,xT,ta) |
135 val x = Free(xn,xT) |
135 val x = Free(xn,xT) |
136 val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) |
136 val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) |
137 of NONE => error "tryabsdecomp: Type not found in the Environement" |
137 of NONE => error "tryabsdecomp: Type not found in the Environement" |
138 | SOME (bsT,atsT) => |
138 | SOME (bsT,atsT) => |
139 (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds)) |
139 (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds)) |
140 in (([(ta, ctxt')], |
140 in (([(ta, ctxt')], |
141 fn ([th], bds) => |
141 fn ([th], bds) => |
142 (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]), |
142 (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]), |
143 let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT)) |
143 let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT)) |
144 in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds |
144 in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds |
145 end)), |
145 end)), |
146 bds) |
146 bds) |
147 end) |
147 end) |
148 | _ => da (s,ctxt) bds) |
148 | _ => da (s,ctxt) bds) |
149 in (case cgns of |
149 in (case cgns of |
150 [] => tryabsdecomp (t,ctxt) bds |
150 [] => tryabsdecomp (t,ctxt) bds |
155 Pattern.match thy |
155 Pattern.match thy |
156 ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) |
156 ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) |
157 (Vartab.empty, Vartab.empty) |
157 (Vartab.empty, Vartab.empty) |
158 val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) |
158 val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) |
159 val (fts,its) = |
159 val (fts,its) = |
160 (map (snd o snd) fnvs, |
160 (map (snd o snd) fnvs, |
161 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) |
161 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) |
162 val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv) |
162 val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv) |
163 in ((fts ~~ (replicate (length fts) ctxt), |
163 in ((fts ~~ (replicate (length fts) ctxt), |
164 Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds) |
164 Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds) |
165 end) |
165 end) |
166 handle MATCH => decomp_genreif da congs (t,ctxt) bds)) |
166 handle MATCH => decomp_genreif da congs (t,ctxt) bds)) |
167 end; |
167 end; |
172 val tT = fastype_of t |
172 val tT = fastype_of t |
173 fun isat eq = |
173 fun isat eq = |
174 let |
174 let |
175 val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd |
175 val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd |
176 in exists_Const |
176 in exists_Const |
177 (fn (n,ty) => n = @{const_name "List.nth"} |
177 (fn (n,ty) => n = @{const_name "List.nth"} |
178 andalso |
178 andalso |
179 AList.defined Type.could_unify bds (domain_type ty)) rhs |
179 AList.defined Type.could_unify bds (domain_type ty)) rhs |
180 andalso Type.could_unify (fastype_of rhs, tT) |
180 andalso Type.could_unify (fastype_of rhs, tT) |
181 end |
181 end |
182 |
182 |
183 fun get_nths t acc = |
183 fun get_nths t acc = |
184 case t of |
184 case t of |
264 in Thm.instantiate ([],subst) eq |
264 in Thm.instantiate ([],subst) eq |
265 end |
265 end |
266 |
266 |
267 val bds = AList.make (fn _ => ([],[])) tys |
267 val bds = AList.make (fn _ => ([],[])) tys |
268 val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop |
268 val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop |
269 |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl |
269 |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl |
270 |> (insteq eq)) raw_eqs |
270 |> (insteq eq)) raw_eqs |
271 val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs) |
271 val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs) |
272 in (ps ~~ (Variable.export ctxt' ctxt congs), bds) |
272 in (ps ~~ (Variable.export ctxt' ctxt congs), bds) |
273 end |
273 end |
274 |
274 |
276 val congs = rearrange congs |
276 val congs = rearrange congs |
277 val (th, bds) = divide_and_conquer' (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt) bds |
277 val (th, bds) = divide_and_conquer' (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt) bds |
278 fun is_listVar (Var (_,t)) = can dest_listT t |
278 fun is_listVar (Var (_,t)) = can dest_listT t |
279 | is_listVar _ = false |
279 | is_listVar _ = false |
280 val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd |
280 val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd |
281 |> strip_comb |> snd |> filter is_listVar |
281 |> strip_comb |> snd |> filter is_listVar |
282 val cert = cterm_of (ProofContext.theory_of ctxt) |
282 val cert = cterm_of (ProofContext.theory_of ctxt) |
283 val cvs = map (fn (v as Var(n,t)) => (cert v, |
283 val cvs = map (fn (v as Var(n,t)) => (cert v, |
284 the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars |
284 the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars |
285 val th' = instantiate ([], cvs) th |
285 val th' = instantiate ([], cvs) th |
286 val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th' |
286 val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th' |
287 val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) |
287 val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) |
288 (fn _ => simp_tac (simpset_of ctxt) 1) |
288 (fn _ => simp_tac (simpset_of ctxt) 1) |
289 in FWD trans [th'',th'] |
289 in FWD trans [th'',th'] |
290 end |
290 end |
291 |
291 |
292 |
292 |
293 fun genreflect ctxt conv corr_thms raw_eqs t = |
293 fun genreflect ctxt conv corr_thms raw_eqs t = |