64431
|
1 |
(* Title: local_typedef.ML
|
|
2 |
Author: Ondřej Kunčar, TU München
|
|
3 |
|
|
4 |
Implements the Local Typedef Rule and extends the logic by the rule.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature LOCAL_TYPEDEF =
|
|
8 |
sig
|
|
9 |
val cancel_type_definition: thm -> thm
|
|
10 |
val cancel_type_definition_attr: attribute
|
|
11 |
end;
|
|
12 |
|
|
13 |
structure Local_Typedef : LOCAL_TYPEDEF =
|
|
14 |
struct
|
|
15 |
|
|
16 |
(*
|
|
17 |
Local Typedef Rule (LT)
|
|
18 |
|
|
19 |
\<Gamma> \<turnstile> (\<exists>(Rep::\<beta> \<Rightarrow> \<tau>) Abs. type_definition Rep Abs A) \<Longrightarrow> \<phi>
|
|
20 |
------------------------------------------------------------- [\<beta> not in \<phi>, \<Gamma>, A;
|
|
21 |
\<Gamma> \<turnstile> A \<noteq> \<emptyset> \<Longrightarrow> \<phi> sort(\<beta>)=HOL.type]
|
|
22 |
*)
|
|
23 |
|
|
24 |
(** BEGINNING OF THE CRITICAL CODE **)
|
|
25 |
|
|
26 |
fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _,
|
|
27 |
(Const (@{const_name Ex}, _) $ Abs (_, Abs_type,
|
|
28 |
(Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) =
|
|
29 |
(Abs_type, set)
|
|
30 |
| dest_typedef t = raise TERM ("dest_typedef", [t]);
|
|
31 |
|
|
32 |
fun cancel_type_definition_cterm thm =
|
|
33 |
let
|
|
34 |
fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]);
|
|
35 |
|
|
36 |
val thy = Thm.theory_of_thm thm;
|
|
37 |
val prop = Thm.prop_of thm;
|
|
38 |
val hyps = Thm.hyps_of thm;
|
|
39 |
|
|
40 |
val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs";
|
|
41 |
|
|
42 |
val (typedef_assm, phi) = Logic.dest_implies prop
|
|
43 |
handle TERM _ => err "the theorem is not an implication";
|
|
44 |
val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef
|
|
45 |
handle TERM _ => err ("the assumption is not of the form "
|
|
46 |
^ quote "\<exists>Rep Abs. type_definition Rep Abs A");
|
|
47 |
|
|
48 |
val (repT, absT) = Term.dest_funT abs_type;
|
|
49 |
val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable";
|
|
50 |
val (absT_name, sorts) = Term.dest_TVar absT;
|
|
51 |
|
|
52 |
val typeS = Sign.defaultS thy;
|
|
53 |
val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort "
|
|
54 |
^ quote (Syntax.string_of_sort_global thy typeS));
|
|
55 |
|
|
56 |
fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts);
|
|
57 |
fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type "
|
|
58 |
^ quote (fst absT_name));
|
|
59 |
val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion";
|
|
60 |
val _ = not (contains_absT set) orelse err_contains_absT_in "the set term";
|
|
61 |
(* the following test is superfluous; the meta hypotheses cannot currently contain TVars *)
|
|
62 |
val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses";
|
|
63 |
|
|
64 |
val not_empty_assm = HOLogic.mk_Trueprop
|
|
65 |
(HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT [])));
|
|
66 |
val prop = Logic.list_implies (hyps @ [not_empty_assm], phi);
|
|
67 |
in
|
|
68 |
Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm)
|
|
69 |
end;
|
|
70 |
|
|
71 |
(** END OF THE CRITICAL CODE **)
|
|
72 |
|
|
73 |
val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
|
|
74 |
(Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
|
|
75 |
|
|
76 |
fun cancel_type_definition thm =
|
|
77 |
Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
|
|
78 |
|
|
79 |
val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
|
|
80 |
|
|
81 |
val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition}
|
|
82 |
(Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
|
|
83 |
|
|
84 |
end; |