1(* Title: HOL/Types_To_Sets/Examples/Prerequisites.thy 2 Author: Ond��ej Kun��ar, TU M��nchen 3*) 4 5theory Prerequisites 6 imports Main 7 keywords "lemmas_with" :: thy_decl 8begin 9 10context 11 fixes Rep Abs A T 12 assumes type: "type_definition Rep Abs A" 13 assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)" 14begin 15 16lemma type_definition_Domainp: "Domainp T = (\<lambda>x. x \<in> A)" 17proof - 18 interpret type_definition Rep Abs A by(rule type) 19 show ?thesis 20 unfolding Domainp_iff[abs_def] T_def fun_eq_iff 21 by (metis Abs_inverse Rep) 22qed 23 24end 25 26subsection \<open>setting up transfer for local typedef\<close> 27 28lemmas [transfer_rule] = \<comment> \<open>prefer right-total rules\<close> 29 right_total_All_transfer 30 right_total_UNIV_transfer 31 right_total_Ex_transfer 32 33locale local_typedef = fixes S ::"'b set" and s::"'s itself" 34 assumes Ex_type_definition_S: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" 35begin 36 37definition "rep = fst (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)" 38definition "Abs = snd (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)" 39 40lemma type_definition_S: "type_definition rep Abs S" 41 unfolding Abs_def rep_def split_beta' 42 by (rule someI_ex) (use Ex_type_definition_S in auto) 43 44lemma rep_in_S[simp]: "rep x \<in> S" 45 and rep_inverse[simp]: "Abs (rep x) = x" 46 and Abs_inverse[simp]: "y \<in> S \<Longrightarrow> rep (Abs y) = y" 47 using type_definition_S 48 unfolding type_definition_def by auto 49 50definition cr_S where "cr_S \<equiv> \<lambda>s b. s = rep b" 51lemmas Domainp_cr_S = type_definition_Domainp[OF type_definition_S cr_S_def, transfer_domain_rule] 52lemmas right_total_cr_S = typedef_right_total[OF type_definition_S cr_S_def, transfer_rule] 53 and bi_unique_cr_S = typedef_bi_unique[OF type_definition_S cr_S_def, transfer_rule] 54 and left_unique_cr_S = typedef_left_unique[OF type_definition_S cr_S_def, transfer_rule] 55 and right_unique_cr_S = typedef_right_unique[OF type_definition_S cr_S_def, transfer_rule] 56 57lemma cr_S_rep[intro, simp]: "cr_S (rep a) a" by (simp add: cr_S_def) 58lemma cr_S_Abs[intro, simp]: "a\<in>S \<Longrightarrow> cr_S a (Abs a)" by (simp add: cr_S_def) 59 60end 61 62subsection \<open>some \<close> 63 64subsection \<open>Tool support\<close> 65 66lemmas subset_iff' = subset_iff[folded Ball_def] 67 68ML \<open> 69structure More_Simplifier = 70struct 71 72fun asm_full_var_simplify ctxt thm = 73 let 74 val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt 75 in 76 Simplifier.asm_full_simplify ctxt' thm' 77 |> singleton (Variable.export ctxt' ctxt) 78 |> Drule.zero_var_indexes 79 end 80 81fun var_simplify_only ctxt ths thm = 82 asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm 83 84val var_simplified = Attrib.thms >> 85 (fn ths => Thm.rule_attribute ths 86 (fn context => var_simplify_only (Context.proof_of context) ths)) 87 88val _ = Theory.setup (Attrib.setup \<^binding>\<open>var_simplified\<close> var_simplified "simplified rule (with vars)") 89 90end 91\<close> 92 93ML \<open> 94val _ = Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas_with\<close> "note theorems with (the same) attributes" 95 (Parse.attribs --| \<^keyword>\<open>:\<close> -- Parse_Spec.name_facts -- Parse.for_fixes 96 >> (fn (((attrs),facts), fixes) => 97 #2 oo Specification.theorems_cmd Thm.theoremK 98 (map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes)) 99\<close> 100 101end 102