56 lemma cr_S_rep[intro, simp]: "cr_S (rep a) a" by (simp add: cr_S_def) |
57 lemma cr_S_rep[intro, simp]: "cr_S (rep a) a" by (simp add: cr_S_def) |
57 lemma cr_S_Abs[intro, simp]: "a\<in>S \<Longrightarrow> cr_S a (Abs a)" by (simp add: cr_S_def) |
58 lemma cr_S_Abs[intro, simp]: "a\<in>S \<Longrightarrow> cr_S a (Abs a)" by (simp add: cr_S_def) |
58 |
59 |
59 end |
60 end |
60 |
61 |
|
62 subsection \<open>some \<close> |
|
63 |
|
64 subsection \<open>Tool support\<close> |
|
65 |
|
66 lemmas subset_iff' = subset_iff[folded Ball_def] |
|
67 |
|
68 ML \<open> |
|
69 structure More_Simplifier = |
|
70 struct |
|
71 |
|
72 fun 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 |
|
81 fun var_simplify_only ctxt ths thm = |
|
82 asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm |
|
83 |
|
84 val var_simplified = Attrib.thms >> |
|
85 (fn ths => Thm.rule_attribute ths |
|
86 (fn context => var_simplify_only (Context.proof_of context) ths)) |
|
87 |
|
88 val _ = Theory.setup (Attrib.setup \<^binding>\<open>var_simplified\<close> var_simplified "simplified rule (with vars)") |
|
89 |
61 end |
90 end |
|
91 \<close> |
|
92 |
|
93 ML \<open> |
|
94 val _ = Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas_with\<close> "note theorems with (the same) attributes" |
|
95 (Parse.attribs --| @{keyword :} -- 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 |
|
101 end |