13 end; |
13 end; |
14 |
14 |
15 structure InductiveRealizer : INDUCTIVE_REALIZER = |
15 structure InductiveRealizer : INDUCTIVE_REALIZER = |
16 struct |
16 struct |
17 |
17 |
18 (* FIXME: LocalTheory.note should return theorems with proper names! *) |
18 (* FIXME: LocalTheory.note should return theorems with proper names! *) (* FIXME ?? *) |
19 fun name_of_thm thm = |
19 fun name_of_thm thm = |
20 (case Symtab.dest (Proofterm.thms_of_proof' (Thm.proof_of thm) Symtab.empty) of |
20 (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I) |
21 [(name, _)] => name |
21 [Proofterm.proof_of (Thm.proof_of thm)] [] of |
22 | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm)); |
22 [name] => name |
|
23 | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm)); |
23 |
24 |
24 val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps"); |
25 val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps"); |
25 |
26 |
26 fun prf_of thm = |
27 fun prf_of thm = |
27 let |
28 let |
28 val thy = Thm.theory_of_thm thm; |
29 val thy = Thm.theory_of_thm thm; |
29 val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm); |
30 val thm' = |
|
31 Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Proofterm.proof_of (Thm.proof_of thm)); |
30 in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *) |
32 in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *) |
31 |
33 |
32 fun forall_intr_prf t prf = |
34 fun forall_intr_prf t prf = |
33 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
35 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
34 in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; |
36 in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; |