src/HOL/Types_To_Sets/local_typedef.ML
changeset 64551 79e9587dbcca
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Types_To_Sets/local_typedef.ML	Mon Dec 12 11:33:14 2016 +0100
     1.3 @@ -0,0 +1,84 @@
     1.4 +(*  Title:      HOL/Types_To_Sets/local_typedef.ML
     1.5 +    Author:     Ondřej Kunčar, TU München
     1.6 +
     1.7 +The Local Typedef Rule (extension of the logic).
     1.8 +*)
     1.9 +
    1.10 +signature LOCAL_TYPEDEF =
    1.11 +sig
    1.12 +  val cancel_type_definition: thm -> thm
    1.13 +  val cancel_type_definition_attr: attribute
    1.14 +end;
    1.15 +
    1.16 +structure Local_Typedef : LOCAL_TYPEDEF =
    1.17 +struct
    1.18 +
    1.19 +(*
    1.20 +Local Typedef Rule (LT)
    1.21 +
    1.22 +  \<Gamma> \<turnstile> (\<exists>(Rep::\<beta> \<Rightarrow> \<tau>) Abs. type_definition Rep Abs A) \<Longrightarrow> \<phi>
    1.23 +------------------------------------------------------------- [\<beta> not in \<phi>, \<Gamma>, A;
    1.24 +                       \<Gamma> \<turnstile> A \<noteq> \<emptyset> \<Longrightarrow> \<phi>                        sort(\<beta>)=HOL.type]
    1.25 +*)
    1.26 +
    1.27 +(** BEGINNING OF THE CRITICAL CODE **)
    1.28 +
    1.29 +fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _,
    1.30 +      (Const (@{const_name Ex}, _) $ Abs (_, Abs_type,
    1.31 +      (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) =
    1.32 +    (Abs_type, set)
    1.33 +   | dest_typedef t = raise TERM ("dest_typedef", [t]);
    1.34 +
    1.35 +fun cancel_type_definition_cterm thm =
    1.36 +  let
    1.37 +    fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]);
    1.38 +
    1.39 +    val thy = Thm.theory_of_thm thm;
    1.40 +    val prop = Thm.prop_of thm;
    1.41 +    val hyps = Thm.hyps_of thm;
    1.42 +
    1.43 +    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs";
    1.44 +
    1.45 +    val (typedef_assm, phi) = Logic.dest_implies prop
    1.46 +      handle TERM _ => err "the theorem is not an implication";
    1.47 +    val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef
    1.48 +      handle TERM _ => err ("the assumption is not of the form "
    1.49 +        ^ quote "\<exists>Rep Abs. type_definition Rep Abs A");
    1.50 +
    1.51 +    val (repT, absT) = Term.dest_funT abs_type;
    1.52 +    val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable";
    1.53 +    val (absT_name, sorts) = Term.dest_TVar absT;
    1.54 +
    1.55 +    val typeS = Sign.defaultS thy;
    1.56 +    val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort "
    1.57 +      ^ quote (Syntax.string_of_sort_global thy typeS));
    1.58 +
    1.59 +    fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts);
    1.60 +    fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type "
    1.61 +      ^ quote (fst absT_name));
    1.62 +    val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion";
    1.63 +    val _ = not (contains_absT set) orelse err_contains_absT_in "the set term";
    1.64 +    (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *)
    1.65 +    val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses";
    1.66 +
    1.67 +    val not_empty_assm = HOLogic.mk_Trueprop
    1.68 +      (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT [])));
    1.69 +    val prop = Logic.list_implies (hyps @ [not_empty_assm], phi);
    1.70 +  in
    1.71 +    Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm)
    1.72 +  end;
    1.73 +
    1.74 +(** END OF THE CRITICAL CODE **)
    1.75 +
    1.76 +val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
    1.77 +  (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
    1.78 +
    1.79 +fun cancel_type_definition thm =
    1.80 +  Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
    1.81 +
    1.82 +val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
    1.83 +
    1.84 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition}
    1.85 +  (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
    1.86 +
    1.87 +end;