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