src/HOL/Types_To_Sets/local_typedef.ML
author wenzelm
Sat Jan 05 17:24:33 2019 +0100 (8 months ago)
changeset 69597 ff784d5a5bfb
parent 64551 79e9587dbcca
permissions -rw-r--r--
isabelle update -u control_cartouches;
     1 (*  Title:      HOL/Types_To_Sets/local_typedef.ML
     2     Author:     Ondřej Kunčar, TU München
     3 
     4 The Local Typedef Rule (extension of the logic).
     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>\<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 
    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>\<open>cancel_type_definition\<close>, 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>\<open>cancel_type_definition\<close>
    82   (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
    83 
    84 end;