src/HOL/Library/Types_To_Sets/local_typedef.ML
changeset 64551 79e9587dbcca
parent 64550 3e20defb1e3c
child 64552 7aa3c52f27aa
     1.1 --- a/src/HOL/Library/Types_To_Sets/local_typedef.ML	Thu Dec 08 15:11:20 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,84 +0,0 @@
     1.4 -(*  Title:      local_typedef.ML
     1.5 -    Author:     Ondřej Kunčar, TU München
     1.6 -
     1.7 -    Implements the Local Typedef Rule and extends the logic by the rule.
     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;
    1.88 \ No newline at end of file