1(*  Title:      HOL/Types_To_Sets/local_typedef.ML
2    Author:     Ond��ej Kun��ar, TU M��nchen
3
4The Local Typedef Rule (extension of the logic).
5*)
6
7signature LOCAL_TYPEDEF =
8sig
9  val cancel_type_definition: thm -> thm
10  val cancel_type_definition_attr: attribute
11end;
12
13structure Local_Typedef : LOCAL_TYPEDEF =
14struct
15
16(*
17Local 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
26fun dest_typedef (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _,
27      (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, Abs_type,
28      (Const (\<^const_name>\<open>type_definition\<close>, _)) $ Bound 1 $ Bound 0 $ set)))) =
29    (Abs_type, set)
30   | dest_typedef t = raise TERM ("dest_typedef", [t]);
31
32fun 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
73val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
74  (Thm.add_oracle (\<^binding>\<open>cancel_type_definition\<close>, cancel_type_definition_cterm)));
75
76fun cancel_type_definition thm =
77  Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
78
79val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
80
81val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>cancel_type_definition\<close>
82  (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
83
84end;
85