equal
deleted
inserted
replaced
26 (fn s => case Symtab.lookup (tab, s) of |
26 (fn s => case Symtab.lookup (tab, s) of |
27 None => error ("Unknown theorem " ^ quote s) |
27 None => error ("Unknown theorem " ^ quote s) |
28 | Some thm => thm) |
28 | Some thm => thm) |
29 end; |
29 end; |
30 |
30 |
31 fun beta_eta_convert thm = |
31 val beta_eta_convert = |
32 let |
32 MetaSimplifier.fconv_rule MetaSimplifier.beta_eta_conversion; |
33 val beta_thm = beta_conversion true (cprop_of thm); |
|
34 val (_, rhs) = Drule.dest_equals (cprop_of beta_thm); |
|
35 in Thm.equal_elim (Thm.transitive beta_thm (eta_conversion rhs)) thm end; |
|
36 |
33 |
37 fun thm_of_proof thy prf = |
34 fun thm_of_proof thy prf = |
38 let |
35 let |
39 val names = add_prf_names ([], prf); |
36 val names = add_prf_names ([], prf); |
40 val sg = sign_of thy; |
37 val sg = sign_of thy; |
51 |
48 |
52 fun thm_of _ _ (PThm ((name, _), _, prop', Some Ts)) = |
49 fun thm_of _ _ (PThm ((name, _), _, prop', Some Ts)) = |
53 let |
50 let |
54 val thm = Thm.implies_intr_hyps (lookup name); |
51 val thm = Thm.implies_intr_hyps (lookup name); |
55 val {prop, ...} = rep_thm thm; |
52 val {prop, ...} = rep_thm thm; |
56 val _ = if prop=prop' then () else |
53 val _ = if prop aconv prop' then () else |
57 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
54 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
58 Sign.string_of_term sg prop ^ "\n\n" ^ |
55 Sign.string_of_term sg prop ^ "\n\n" ^ |
59 Sign.string_of_term sg prop'); |
56 Sign.string_of_term sg prop'); |
60 in thm_of_atom thm Ts end |
57 in thm_of_atom thm Ts end |
61 |
58 |
96 |
93 |
97 | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of sg t) |
94 | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of sg t) |
98 |
95 |
99 | thm_of _ _ _ = error "thm_of_proof: partial proof term"; |
96 | thm_of _ _ _ = error "thm_of_proof: partial proof term"; |
100 |
97 |
101 in thm_of [] [] prf end; |
98 in beta_eta_convert (thm_of [] [] prf) end; |
102 |
99 |
103 end; |
100 end; |
104 |
|