84 Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make |
84 Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make |
85 |
85 |
86 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
86 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
87 fixes that seem to be missing over there; or maybe the two code portions are |
87 fixes that seem to be missing over there; or maybe the two code portions are |
88 not doing the same? *) |
88 not doing the same? *) |
89 fun fold_body_thms thm_name f = |
89 fun fold_body_thms thm_name name_map = |
90 let |
90 let |
|
91 val thm_name' = name_map thm_name |
91 fun app n (PBody {thms, ...}) = |
92 fun app n (PBody {thms, ...}) = |
92 thms |> fold (fn (_, (name, _, body)) => fn accum => |
93 thms |> fold (fn (_, (name, _, body)) => fn accum => |
93 let |
94 let |
94 (* The second disjunct caters for the uncommon case where the proved |
95 val name' = name_map name |
95 theorem occurs in its own proof (e.g., |
96 val collect = union (op =) o the_list |
96 "Transitive_Closure.trancl_into_trancl"). *) |
97 (* The "name = thm_name" case caters for the uncommon case where the |
97 val no_name = (name = "" orelse (n = 1 andalso name = thm_name)) |
98 proved theorem occurs in its own proof (e.g., |
|
99 "Transitive_Closure.trancl_into_trancl"). The "name' = thm_name'" |
|
100 case is to unfold low-level class facts ("Xxx.yyy.zzz") in the |
|
101 proof of high-level class facts ("XXX.yyy_class.zzz"). *) |
|
102 val no_name = |
|
103 (name = "" orelse |
|
104 (n = 1 andalso (name = thm_name orelse name' = thm_name'))) |
98 val accum = |
105 val accum = |
99 accum |> (if n = 1 andalso not no_name then f name else I) |
106 accum |> (if n = 1 andalso not no_name then collect name' else I) |
100 val n = n + (if no_name then 0 else 1) |
107 val n = n + (if no_name then 0 else 1) |
101 in accum |> (if n <= 1 then app n (Future.join body) else I) end) |
108 in accum |> (if n <= 1 then app n (Future.join body) else I) end) |
102 in fold (app 0) end |
109 in fold (app 0) end |
103 |
110 |
104 fun thms_in_proof all_names th = |
111 fun thms_in_proof all_names th = |
105 let |
112 let |
106 val collect = |
113 val name_map = |
107 case all_names of |
114 case all_names of |
108 SOME names => |
115 SOME names => Symtab.lookup names |
109 (fn s => case Symtab.lookup names s of |
116 | NONE => SOME |
110 SOME s' => insert (op =) s' |
|
111 | NONE => I) |
|
112 | NONE => insert (op =) |
|
113 val names = |
117 val names = |
114 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] |
118 [] |> fold_body_thms (Thm.get_name_hint th) name_map [Thm.proof_body_of th] |
115 in names end |
119 in names end |
116 |
120 |
117 fun thms_of_name ctxt name = |
121 fun thms_of_name ctxt name = |
118 let |
122 let |
119 val lex = Keyword.get_lexicons |
123 val lex = Keyword.get_lexicons |