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