182 thy (rhs_P, t) |
182 thy (rhs_P, t) |
183 (Envir.type_env (Envir.empty 0),Term.Vartab.empty) |
183 (Envir.type_env (Envir.empty 0),Term.Vartab.empty) |
184 val tml = Vartab.dest tmenv |
184 val tml = Vartab.dest tmenv |
185 val SOME (_,t') = AList.lookup (op =) tml (xn,0) |
185 val SOME (_,t') = AList.lookup (op =) tml (xn,0) |
186 val cvs = |
186 val cvs = |
187 cert (foldr (fn (x,xs) => Const("List.list.Cons", ntT --> ntlT --> ntlT)$x$xs) |
187 cert (fold_rev (fn x => fn xs => Const("List.list.Cons", ntT --> ntlT --> ntlT)$x$xs) |
188 (Free(vsn,ntlT)) bsT) |
188 bsT (Free (vsn, ntlT))) |
189 val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) |
189 val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) |
190 (AList.delete (op =) (xn,0) tml) |
190 (AList.delete (op =) (xn,0) tml) |
191 val th = (instantiate |
191 val th = (instantiate |
192 ([], |
192 ([], |
193 [(cert vs, cvs),(cert n, t' |> index_of |> HOLogic.mk_nat |> cert)] |
193 [(cert vs, cvs),(cert n, t' |> index_of |> HOLogic.mk_nat |> cert)] |
230 (* Generic reification procedure: *) |
230 (* Generic reification procedure: *) |
231 (* creates all needed cong rules and then just uses the theorem synthesis *) |
231 (* creates all needed cong rules and then just uses the theorem synthesis *) |
232 |
232 |
233 fun mk_congs ctxt raw_eqs = |
233 fun mk_congs ctxt raw_eqs = |
234 let |
234 let |
235 val fs = foldr (fn (eq,fns) => |
235 val fs = fold_rev (fn eq => |
236 insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop |
236 insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop |
237 |> HOLogic.dest_eq |> fst |> strip_comb |
237 |> HOLogic.dest_eq |> fst |> strip_comb |
238 |> fst) fns) [] raw_eqs |
238 |> fst)) raw_eqs [] |
239 val tys = foldr (fn (f,ts) => (f |> fastype_of |> binder_types |> split_last |> fst) |
239 val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> split_last |> fst) |
240 union ts) [] fs |
240 union ts) fs [] |
241 val _ = bds := AList.make (fn _ => ([],[])) tys |
241 val _ = bds := AList.make (fn _ => ([],[])) tys |
242 val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt |
242 val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt |
243 val thy = ProofContext.theory_of ctxt' |
243 val thy = ProofContext.theory_of ctxt' |
244 val cert = cterm_of thy |
244 val cert = cterm_of thy |
245 val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t))))) |
245 val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t))))) |