203 in |
203 in |
204 if null tinst' then thm |
204 if null tinst' then thm |
205 else thm |> Drule.implies_intr_list (map cert hyps) |
205 else thm |> Drule.implies_intr_list (map cert hyps) |
206 |> Drule.tvars_intr_list (map #1 tinst') |
206 |> Drule.tvars_intr_list (map #1 tinst') |
207 |> (fn (th, al) => th |> Thm.instantiate |
207 |> (fn (th, al) => th |> Thm.instantiate |
208 ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), |
208 ((map (fn (a, T) => (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) tinst'), |
209 [])) |
209 [])) |
210 |> (fn th => Drule.implies_elim_list th |
210 |> (fn th => Drule.implies_elim_list th |
211 (map (Thm.assume o cert o tinst_tab_term tinst) hyps)) |
211 (map (Thm.assume o cert o tinst_tab_term tinst) hyps)) |
212 end; |
212 end; |
213 |
213 |
249 in |
249 in |
250 if null tinst' andalso null inst' then tinst_tab_thm thy tinst thm |
250 if null tinst' andalso null inst' then tinst_tab_thm thy tinst thm |
251 else thm |> Drule.implies_intr_list (map cert hyps) |
251 else thm |> Drule.implies_intr_list (map cert hyps) |
252 |> Drule.tvars_intr_list (map #1 tinst') |
252 |> Drule.tvars_intr_list (map #1 tinst') |
253 |> (fn (th, al) => th |> Thm.instantiate |
253 |> (fn (th, al) => th |> Thm.instantiate |
254 ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), |
254 ((map (fn (a, T) => (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) tinst'), |
255 [])) |
255 [])) |
256 |> Drule.forall_intr_list (map (cert o #1) inst') |
256 |> Drule.forall_intr_list (map (cert o #1) inst') |
257 |> Drule.forall_elim_list (map (cert o #2) inst') |
257 |> Drule.forall_elim_list (map (cert o #2) inst') |
258 |> Drule.fconv_rule (Thm.beta_conversion true) |
258 |> Drule.fconv_rule (Thm.beta_conversion true) |
259 |> (fn th => Drule.implies_elim_list th |
259 |> (fn th => Drule.implies_elim_list th |
689 |
689 |
690 |
690 |
691 (* type instantiation *) |
691 (* type instantiation *) |
692 |
692 |
693 fun inst_type [] T = T |
693 fun inst_type [] T = T |
694 | inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T; |
694 | inst_type env T = Term.map_type_tfree (fn v => AList.lookup (op =) env v |> the_default (TFree v)) T; |
695 |
695 |
696 fun inst_term [] t = t |
696 fun inst_term [] t = t |
697 | inst_term env t = Term.map_term_types (inst_type env) t; |
697 | inst_term env t = Term.map_term_types (inst_type env) t; |
698 |
698 |
699 fun inst_thm _ [] th = th |
699 fun inst_thm _ [] th = th |
711 th |
711 th |
712 |> Drule.implies_intr_list (map cert hyps) |
712 |> Drule.implies_intr_list (map cert hyps) |
713 |> Drule.tvars_intr_list (map (#1 o #1) env') |
713 |> Drule.tvars_intr_list (map (#1 o #1) env') |
714 |> (fn (th', al) => th' |> |
714 |> (fn (th', al) => th' |> |
715 Thm.instantiate ((map (fn ((a, _), T) => |
715 Thm.instantiate ((map (fn ((a, _), T) => |
716 (certT (TVar (valOf (assoc (al, a)))), certT T)) env'), [])) |
716 (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) env'), [])) |
717 |> (fn th'' => Drule.implies_elim_list th'' |
717 |> (fn th'' => Drule.implies_elim_list th'' |
718 (map (Thm.assume o cert o inst_term env') hyps)) |
718 (map (Thm.assume o cert o inst_term env') hyps)) |
719 end; |
719 end; |
720 |
720 |
721 fun inst_elem ctxt env = |
721 fun inst_elem ctxt env = |
939 (* propagate parameter types, to keep them consistent *) |
939 (* propagate parameter types, to keep them consistent *) |
940 val regs' = map (fn ((name, ps), ths) => |
940 val regs' = map (fn ((name, ps), ths) => |
941 ((name, map (rename ren) ps), ths)) regs; |
941 ((name, map (rename ren) ps), ths)) regs; |
942 val new_regs = gen_rems eq_fst (regs', ids); |
942 val new_regs = gen_rems eq_fst (regs', ids); |
943 val new_ids = map fst new_regs; |
943 val new_ids = map fst new_regs; |
944 val new_idTs = map (apsnd (map (fn p => (p, valOf (assoc (ps, p)))))) new_ids; |
944 val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids; |
945 |
945 |
946 val new_ths = map (fn (_, ths') => |
946 val new_ths = map (fn (_, ths') => |
947 map (Drule.satisfy_hyps ths o rename_thm ren o inst_thm ctxt env) ths') new_regs; |
947 map (Drule.satisfy_hyps ths o rename_thm ren o inst_thm ctxt env) ths') new_regs; |
948 val new_ids' = map (fn (id, ths) => |
948 val new_ids' = map (fn (id, ths) => |
949 (id, ([], Derived ths))) (new_ids ~~ new_ths); |
949 (id, ([], Derived ths))) (new_ids ~~ new_ths); |
1046 (* replace params in ids by params from axioms, |
1046 (* replace params in ids by params from axioms, |
1047 adjust types in mode *) |
1047 adjust types in mode *) |
1048 val all_params' = params_of' elemss; |
1048 val all_params' = params_of' elemss; |
1049 val all_params = param_types all_params'; |
1049 val all_params = param_types all_params'; |
1050 val elemss' = map (fn (((name, _), (ps, mode)), elems) => |
1050 val elemss' = map (fn (((name, _), (ps, mode)), elems) => |
1051 (((name, map (fn p => (p, assoc (all_params, p))) ps), mode), elems)) |
1051 (((name, map (fn p => (p, AList.lookup (op =) all_params p)) ps), mode), elems)) |
1052 elemss; |
1052 elemss; |
1053 fun inst_th th = let |
1053 fun inst_th th = let |
1054 val {hyps, prop, ...} = Thm.rep_thm th; |
1054 val {hyps, prop, ...} = Thm.rep_thm th; |
1055 val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []); |
1055 val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []); |
1056 val [env] = unify_parms ctxt all_params [ps]; |
1056 val [env] = unify_parms ctxt all_params [ps]; |
1421 (* CB: finish_parms introduces type info from parms to identifiers *) |
1421 (* CB: finish_parms introduces type info from parms to identifiers *) |
1422 (* CB: only needed for types that have been NONE so far??? |
1422 (* CB: only needed for types that have been NONE so far??? |
1423 If so, which are these??? *) |
1423 If so, which are these??? *) |
1424 |
1424 |
1425 fun finish_parms parms (((name, ps), mode), elems) = |
1425 fun finish_parms parms (((name, ps), mode), elems) = |
1426 (((name, map (fn (x, _) => (x, assoc (parms, x))) ps), mode), elems); |
1426 (((name, map (fn (x, _) => (x, AList.lookup (op =) parms x)) ps), mode), elems); |
1427 |
1427 |
1428 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) = |
1428 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) = |
1429 let |
1429 let |
1430 val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)]; |
1430 val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)]; |
1431 val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths; |
1431 val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths; |
1580 context elements obtained from import and elements. *) |
1580 context elements obtained from import and elements. *) |
1581 val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close |
1581 val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close |
1582 context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; |
1582 context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; |
1583 (* replace extended ids (for axioms) by ids *) |
1583 (* replace extended ids (for axioms) by ids *) |
1584 val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) => |
1584 val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) => |
1585 (((n, map (fn p => (p, assoc (ps', p) |> valOf)) ps), mode), elems)) |
1585 (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems)) |
1586 (ids ~~ all_elemss); |
1586 (ids ~~ all_elemss); |
1587 |
1587 |
1588 (* CB: all_elemss and parms contain the correct parameter types *) |
1588 (* CB: all_elemss and parms contain the correct parameter types *) |
1589 val (ps,qs) = splitAt(length raw_import_elemss, all_elemss') |
1589 val (ps,qs) = splitAt(length raw_import_elemss, all_elemss') |
1590 val (import_ctxt, (import_elemss, _)) = |
1590 val (import_ctxt, (import_elemss, _)) = |
2227 val given = List.mapPartial (fn (_, (NONE, _)) => NONE |
2227 val given = List.mapPartial (fn (_, (NONE, _)) => NONE |
2228 | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs)); |
2228 | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs)); |
2229 val (given_ps, given_insts) = split_list given; |
2229 val (given_ps, given_insts) = split_list given; |
2230 val tvars = foldr Term.add_typ_tvars [] pvTs; |
2230 val tvars = foldr Term.add_typ_tvars [] pvTs; |
2231 val used = foldr Term.add_typ_varnames [] pvTs; |
2231 val used = foldr Term.add_typ_varnames [] pvTs; |
2232 fun sorts (a, i) = assoc (tvars, (a, i)); |
2232 fun sorts (a, i) = AList.lookup (op =) tvars (a, i); |
2233 val (vs, vinst) = read_terms thy_ctxt sorts used given_insts; |
2233 val (vs, vinst) = read_terms thy_ctxt sorts used given_insts; |
2234 val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars; |
2234 val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars; |
2235 val vars' = fold Term.add_term_varnames vs vars; |
2235 val vars' = fold Term.add_term_varnames vs vars; |
2236 val _ = if null vars' then () |
2236 val _ = if null vars' then () |
2237 else error ("Illegal schematic variable(s) in instantiation: " ^ |
2237 else error ("Illegal schematic variable(s) in instantiation: " ^ |
2240 val new_Tnames = foldr Term.add_term_tfree_names [] vs; |
2240 val new_Tnames = foldr Term.add_term_tfree_names [] vs; |
2241 val new_Tnames' = Term.invent_names used "'a" (length new_Tnames); |
2241 val new_Tnames' = Term.invent_names used "'a" (length new_Tnames); |
2242 val renameT = |
2242 val renameT = |
2243 if is_local then I |
2243 if is_local then I |
2244 else Type.unvarifyT o Term.map_type_tfree (fn (a, s) => |
2244 else Type.unvarifyT o Term.map_type_tfree (fn (a, s) => |
2245 TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s)); |
2245 TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s)); |
2246 val rename = |
2246 val rename = |
2247 if is_local then I |
2247 if is_local then I |
2248 else Term.map_term_types renameT; |
2248 else Term.map_term_types renameT; |
2249 |
2249 |
2250 val tinst = Symtab.make (map |
2250 val tinst = Symtab.make (map |
2267 |
2267 |
2268 (** compute proof obligations **) |
2268 (** compute proof obligations **) |
2269 |
2269 |
2270 (* restore "small" ids *) |
2270 (* restore "small" ids *) |
2271 val ids' = map (fn ((n, ps), (_, mode)) => |
2271 val ids' = map (fn ((n, ps), (_, mode)) => |
2272 ((n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps), mode)) ids; |
2272 ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) ids; |
2273 (* instantiate ids and elements *) |
2273 (* instantiate ids and elements *) |
2274 val inst_elemss = map |
2274 val inst_elemss = map |
2275 (fn ((id, _), ((_, mode), elems)) => |
2275 (fn ((id, _), ((_, mode), elems)) => |
2276 inst_tab_elems thy (inst, tinst) (id, map (fn Int e => e) elems) |
2276 inst_tab_elems thy (inst, tinst) (id, map (fn Int e => e) elems) |
2277 |> apfst (fn id => (id, map_mode (map (inst_tab_thm thy (inst, tinst))) mode))) |
2277 |> apfst (fn id => (id, map_mode (map (inst_tab_thm thy (inst, tinst))) mode))) |
2346 | activate_id _ thy = thy; |
2346 | activate_id _ thy = thy; |
2347 |
2347 |
2348 fun activate_reg (vts, ((prfx, atts2), _)) thy = let |
2348 fun activate_reg (vts, ((prfx, atts2), _)) thy = let |
2349 val ((inst, tinst), wits) = |
2349 val ((inst, tinst), wits) = |
2350 collect_global_witnesses thy fixed t_ids vts; |
2350 collect_global_witnesses thy fixed t_ids vts; |
2351 fun inst_parms ps = map (fn p => |
2351 fun inst_parms ps = map |
2352 valOf (assoc (map #1 fixed ~~ vts, p))) ps; |
2352 (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps; |
2353 val disch = Drule.fconv_rule (Thm.beta_conversion true) o |
2353 val disch = Drule.fconv_rule (Thm.beta_conversion true) o |
2354 Drule.satisfy_hyps wits; |
2354 Drule.satisfy_hyps wits; |
2355 val new_elemss = List.filter (fn (((name, ps), _), _) => |
2355 val new_elemss = List.filter (fn (((name, ps), _), _) => |
2356 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss); |
2356 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss); |
2357 fun activate_assumed_id (((_, Derived _), _), _) thy = thy |
2357 fun activate_assumed_id (((_, Derived _), _), _) thy = thy |