|
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; |