21 fun lookup_thm thy = |
21 fun lookup_thm thy = |
22 let val tab = foldr Symtab.update |
22 let val tab = foldr Symtab.update |
23 (flat (map thms_of (thy :: Theory.ancestors_of thy)), Symtab.empty) |
23 (flat (map thms_of (thy :: Theory.ancestors_of thy)), Symtab.empty) |
24 in |
24 in |
25 (fn s => case Symtab.lookup (tab, s) of |
25 (fn s => case Symtab.lookup (tab, s) of |
26 None => error ("Unknown theorem " ^ quote s) |
26 NONE => error ("Unknown theorem " ^ quote s) |
27 | Some thm => thm) |
27 | SOME thm => thm) |
28 end; |
28 end; |
29 |
29 |
30 val beta_eta_convert = |
30 val beta_eta_convert = |
31 Drule.fconv_rule Drule.beta_eta_conversion; |
31 Drule.fconv_rule Drule.beta_eta_conversion; |
32 |
32 |
43 val ctye = map fst tvars @ map snd fmap ~~ map (Thm.ctyp_of sg) Ts |
43 val ctye = map fst tvars @ map snd fmap ~~ map (Thm.ctyp_of sg) Ts |
44 in |
44 in |
45 Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
45 Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
46 end; |
46 end; |
47 |
47 |
48 fun thm_of _ _ (PThm ((name, _), _, prop', Some Ts)) = |
48 fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) = |
49 let |
49 let |
50 val thm = Thm.implies_intr_hyps (lookup name); |
50 val thm = Thm.implies_intr_hyps (lookup name); |
51 val {prop, ...} = rep_thm thm; |
51 val {prop, ...} = rep_thm thm; |
52 val _ = if prop aconv prop' then () else |
52 val _ = if prop aconv prop' then () else |
53 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
53 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
54 Sign.string_of_term sg prop ^ "\n\n" ^ |
54 Sign.string_of_term sg prop ^ "\n\n" ^ |
55 Sign.string_of_term sg prop'); |
55 Sign.string_of_term sg prop'); |
56 in thm_of_atom thm Ts end |
56 in thm_of_atom thm Ts end |
57 |
57 |
58 | thm_of _ _ (PAxm (name, _, Some Ts)) = |
58 | thm_of _ _ (PAxm (name, _, SOME Ts)) = |
59 thm_of_atom (get_axiom thy name) Ts |
59 thm_of_atom (get_axiom thy name) Ts |
60 |
60 |
61 | thm_of _ Hs (PBound i) = nth_elem (i, Hs) |
61 | thm_of _ Hs (PBound i) = nth_elem (i, Hs) |
62 |
62 |
63 | thm_of vs Hs (Abst (s, Some T, prf)) = |
63 | thm_of vs Hs (Abst (s, SOME T, prf)) = |
64 let |
64 let |
65 val x = variant (names @ map fst vs) s; |
65 val x = variant (names @ map fst vs) s; |
66 val thm = thm_of ((x, T) :: vs) Hs prf |
66 val thm = thm_of ((x, T) :: vs) Hs prf |
67 in |
67 in |
68 Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm |
68 Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm |
69 end |
69 end |
70 |
70 |
71 | thm_of vs Hs (prf % Some t) = |
71 | thm_of vs Hs (prf % SOME t) = |
72 let |
72 let |
73 val thm = thm_of vs Hs prf |
73 val thm = thm_of vs Hs prf |
74 val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t)) |
74 val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t)) |
75 in Thm.forall_elim ct thm end |
75 in Thm.forall_elim ct thm end |
76 |
76 |
77 | thm_of vs Hs (AbsP (s, Some t, prf)) = |
77 | thm_of vs Hs (AbsP (s, SOME t, prf)) = |
78 let |
78 let |
79 val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t)); |
79 val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t)); |
80 val thm = thm_of vs (Thm.assume ct :: Hs) prf |
80 val thm = thm_of vs (Thm.assume ct :: Hs) prf |
81 in |
81 in |
82 Thm.implies_intr ct thm |
82 Thm.implies_intr ct thm |