29 val beta_eta_convert = |
29 val beta_eta_convert = |
30 Drule.fconv_rule Drule.beta_eta_conversion; |
30 Drule.fconv_rule Drule.beta_eta_conversion; |
31 |
31 |
32 fun thm_of_proof thy prf = |
32 fun thm_of_proof thy prf = |
33 let |
33 let |
34 val names = add_prf_names ([], prf); |
34 val names = Proofterm.fold_proof_terms Term.declare_term_names (K I) prf Name.context; |
35 val sg = sign_of thy; |
|
36 val lookup = lookup_thm thy; |
35 val lookup = lookup_thm thy; |
37 |
36 |
38 fun thm_of_atom thm Ts = |
37 fun thm_of_atom thm Ts = |
39 let |
38 let |
40 val tvars = term_tvars (Thm.full_prop_of thm); |
39 val tvars = term_tvars (Thm.full_prop_of thm); |
41 val (fmap, thm') = Thm.varifyT' [] thm; |
40 val (fmap, thm') = Thm.varifyT' [] thm; |
42 val ctye = map (pairself (Thm.ctyp_of sg)) |
41 val ctye = map (pairself (Thm.ctyp_of thy)) |
43 (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) |
42 (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) |
44 in |
43 in |
45 Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
44 Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
46 end; |
45 end; |
47 |
46 |
49 let |
48 let |
50 val thm = Drule.implies_intr_hyps (lookup name); |
49 val thm = Drule.implies_intr_hyps (lookup name); |
51 val {prop, ...} = rep_thm thm; |
50 val {prop, ...} = rep_thm thm; |
52 val _ = if prop aconv prop' then () else |
51 val _ = if prop aconv prop' then () else |
53 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
52 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
54 Sign.string_of_term sg prop ^ "\n\n" ^ |
53 Sign.string_of_term thy prop ^ "\n\n" ^ |
55 Sign.string_of_term sg prop'); |
54 Sign.string_of_term thy prop'); |
56 in thm_of_atom thm Ts end |
55 in thm_of_atom thm Ts end |
57 |
56 |
58 | thm_of _ _ (PAxm (name, _, SOME Ts)) = |
57 | thm_of _ _ (PAxm (name, _, SOME Ts)) = |
59 thm_of_atom (get_axiom thy name) Ts |
58 thm_of_atom (get_axiom thy name) Ts |
60 |
59 |
61 | thm_of _ Hs (PBound i) = List.nth (Hs, i) |
60 | thm_of _ Hs (PBound i) = List.nth (Hs, i) |
62 |
61 |
63 | thm_of vs Hs (Abst (s, SOME T, prf)) = |
62 | thm_of vs Hs (Abst (s, SOME T, prf)) = |
64 let |
63 let |
65 val x = Name.variant (names @ map fst vs) s; |
64 val ([x], _) = Name.variants [s] (fold (Name.declare o fst) vs names); |
66 val thm = thm_of ((x, T) :: vs) Hs prf |
65 val thm = thm_of ((x, T) :: vs) Hs prf |
67 in |
66 in |
68 Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm |
67 Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm |
69 end |
68 end |
70 |
69 |
71 | thm_of vs Hs (prf % SOME t) = |
70 | thm_of vs Hs (prf % SOME t) = |
72 let |
71 let |
73 val thm = thm_of vs Hs prf |
72 val thm = thm_of vs Hs prf |
74 val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t)) |
73 val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t)) |
75 in Thm.forall_elim ct thm end |
74 in Thm.forall_elim ct thm end |
76 |
75 |
77 | thm_of vs Hs (AbsP (s, SOME t, prf)) = |
76 | thm_of vs Hs (AbsP (s, SOME t, prf)) = |
78 let |
77 let |
79 val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t)); |
78 val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t)); |
80 val thm = thm_of vs (Thm.assume ct :: Hs) prf |
79 val thm = thm_of vs (Thm.assume ct :: Hs) prf |
81 in |
80 in |
82 Thm.implies_intr ct thm |
81 Thm.implies_intr ct thm |
83 end |
82 end |
84 |
83 |
85 | thm_of vs Hs (prf %% prf') = |
84 | thm_of vs Hs (prf %% prf') = |
86 let |
85 let |
87 val thm = beta_eta_convert (thm_of vs Hs prf); |
86 val thm = beta_eta_convert (thm_of vs Hs prf); |
88 val thm' = beta_eta_convert (thm_of vs Hs prf') |
87 val thm' = beta_eta_convert (thm_of vs Hs prf') |
89 in |
88 in |
90 Thm.implies_elim thm thm' |
89 Thm.implies_elim thm thm' |
91 end |
90 end |
92 |
91 |
93 | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of sg t) |
92 | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t) |
94 |
93 |
95 | thm_of _ _ _ = error "thm_of_proof: partial proof term"; |
94 | thm_of _ _ _ = error "thm_of_proof: partial proof term"; |
96 |
95 |
97 in beta_eta_convert (thm_of [] [] prf) end; |
96 in beta_eta_convert (thm_of [] [] prf) end; |
98 |
97 |