104 val may_be_induction = |
104 val may_be_induction = |
105 exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => |
105 exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => |
106 body_type T = @{typ bool} |
106 body_type T = @{typ bool} |
107 | _ => false) |
107 | _ => false) |
108 |
108 |
|
109 fun normalize_vars t = |
|
110 let |
|
111 fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s |
|
112 | normT (TVar (z as (_, S))) = |
|
113 (fn ((knownT, nT), accum) => |
|
114 case find_index (equal z) knownT of |
|
115 ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum)) |
|
116 | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum))) |
|
117 | normT (T as TFree _) = pair T |
|
118 fun norm (t $ u) = norm t ##>> norm u #>> op $ |
|
119 | norm (Const (s, T)) = normT T #>> curry Const s |
|
120 | norm (Var (z as (_, T))) = |
|
121 normT T |
|
122 #> (fn (T, (accumT, (known, n))) => |
|
123 case find_index (equal z) known of |
|
124 ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1))) |
|
125 | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n)))) |
|
126 | norm (Abs (_, T, t)) = |
|
127 norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t)) |
|
128 | norm (Bound j) = pair (Bound j) |
|
129 | norm (Free (s, T)) = normT T #>> curry Free s |
|
130 in fst (norm t (([], 0), ([], 0))) end |
|
131 |
109 fun status_of_thm css name th = |
132 fun status_of_thm css name th = |
110 (* FIXME: use structured name *) |
133 let val t = normalize_vars (prop_of th) in |
111 if (String.isSubstring ".induct" name orelse |
134 (* FIXME: use structured name *) |
112 String.isSubstring ".inducts" name) andalso |
135 if String.isSubstring ".induct" name andalso may_be_induction t then |
113 may_be_induction (prop_of th) then |
136 Induction |
114 Induction |
137 else case Termtab.lookup css t of |
115 else case Termtab.lookup css (prop_of th) of |
138 SOME status => status |
116 SOME status => status |
139 | NONE => |
117 | NONE => General |
140 let val concl = Logic.strip_imp_concl t in |
|
141 case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of |
|
142 SOME lrhss => |
|
143 let |
|
144 val prems = Logic.strip_imp_prems t |
|
145 val t' = Logic.list_implies (prems, Logic.mk_equals lrhss) |
|
146 in |
|
147 Termtab.lookup css t' |> the_default General |
|
148 end |
|
149 | NONE => General |
|
150 end |
|
151 end |
118 |
152 |
119 fun stature_of_thm global assms chained css name th = |
153 fun stature_of_thm global assms chained css name th = |
120 (scope_of_thm global assms chained th, status_of_thm css name th) |
154 (scope_of_thm global assms chained th, status_of_thm css name th) |
121 |
155 |
122 fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) = |
156 fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) = |
272 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote |
306 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote |
273 fun backquote_thm ctxt = backquote_term ctxt o prop_of |
307 fun backquote_thm ctxt = backquote_term ctxt o prop_of |
274 |
308 |
275 fun clasimpset_rule_table_of ctxt = |
309 fun clasimpset_rule_table_of ctxt = |
276 let |
310 let |
277 val thy = Proof_Context.theory_of ctxt |
311 fun add stature th = |
278 val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy |
312 Termtab.update (normalize_vars (prop_of th), stature) |
279 fun add stature normalizers get_th = |
|
280 fold (fn rule => |
|
281 let |
|
282 val th = rule |> get_th |
|
283 val t = |
|
284 th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of |
|
285 in |
|
286 fold (fn normalize => Termtab.update (normalize t, stature)) |
|
287 (I :: normalizers) |
|
288 end) |
|
289 val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = |
313 val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = |
290 ctxt |> claset_of |> Classical.rep_cs |
314 ctxt |> claset_of |> Classical.rep_cs |
291 val intros = Item_Net.content safeIs @ Item_Net.content hazIs |
315 val intros = Item_Net.content safeIs @ Item_Net.content hazIs |
292 (* Add once it is used: |
316 (* Add once it is used: |
293 val elims = |
317 val elims = |
304 val spec_intros = |
328 val spec_intros = |
305 specs |> filter (member (op =) [Spec_Rules.Inductive, |
329 specs |> filter (member (op =) [Spec_Rules.Inductive, |
306 Spec_Rules.Co_Inductive] o fst) |
330 Spec_Rules.Co_Inductive] o fst) |
307 |> maps (snd o snd) |
331 |> maps (snd o snd) |
308 in |
332 in |
309 Termtab.empty |> add Simp [atomize] snd simps |
333 Termtab.empty |> fold (add Simp o snd) simps |
310 |> add Rec_Def [] I rec_defs |
334 |> fold (add Rec_Def) rec_defs |
311 |> add Non_Rec_Def [] I nonrec_defs |
335 |> fold (add Non_Rec_Def) nonrec_defs |
312 (* Add once it is used: |
336 (* Add once it is used: |
313 |> add Elim [] I elims |
337 |> fold (add Elim) elims |
314 *) |
338 *) |
315 |> add Intro [] I intros |
339 |> fold (add Intro) intros |
316 |> add Inductive [] I spec_intros |
340 |> fold (add Inductive) spec_intros |
317 end |
341 end |
318 |
342 |
319 fun normalize_eq (t as @{const Trueprop} |
343 fun normalize_eq (t as @{const Trueprop} |
320 $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) = |
344 $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) = |
321 if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t |
345 if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t |