64 the Safe Intr rule B==>A and |
64 the Safe Intr rule B==>A and |
65 the Safe Destruct rule A==>B. |
65 the Safe Destruct rule A==>B. |
66 Also ~A goes to the Safe Elim rule A ==> ?R |
66 Also ~A goes to the Safe Elim rule A ==> ?R |
67 Failing other cases, A is added as a Safe Intr rule*) |
67 Failing other cases, A is added as a Safe Intr rule*) |
68 |
68 |
69 fun app (att: attribute) th context = #1 (att (context, th)); |
|
70 |
|
71 fun add_iff safe unsafe = |
69 fun add_iff safe unsafe = |
72 Thm.declaration_attribute (fn th => |
70 Thm.declaration_attribute (fn th => |
73 let |
71 let |
74 val n = nprems_of th; |
72 val n = nprems_of th; |
75 val (elim, intro) = if n = 0 then safe else unsafe; |
73 val (elim, intro) = if n = 0 then safe else unsafe; |
76 val zero_rotate = zero_var_indexes o rotate_prems n; |
74 val zero_rotate = zero_var_indexes o rotate_prems n; |
77 in |
75 in |
78 app intro (zero_rotate (th RS Data.iffD2)) #> |
76 Thm.attribute_declaration intro (zero_rotate (th RS Data.iffD2)) #> |
79 app elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) |
77 Thm.attribute_declaration elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) |
80 handle THM _ => (app elim (zero_rotate (th RS Data.notE)) handle THM _ => app intro th) |
78 handle THM _ => |
|
79 (Thm.attribute_declaration elim (zero_rotate (th RS Data.notE)) |
|
80 handle THM _ => Thm.attribute_declaration intro th) |
81 end); |
81 end); |
82 |
82 |
83 fun del_iff del = Thm.declaration_attribute (fn th => |
83 fun del_iff del = Thm.declaration_attribute (fn th => |
84 let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in |
84 let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in |
85 app del (zero_rotate (th RS Data.iffD2)) #> |
85 Thm.attribute_declaration del (zero_rotate (th RS Data.iffD2)) #> |
86 app del (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) |
86 Thm.attribute_declaration del (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) |
87 handle THM _ => (app del (zero_rotate (th RS Data.notE)) handle THM _ => app del th) |
87 handle THM _ => |
|
88 (Thm.attribute_declaration del (zero_rotate (th RS Data.notE)) |
|
89 handle THM _ => Thm.attribute_declaration del th) |
88 end); |
90 end); |
89 |
91 |
90 in |
92 in |
91 |
93 |
92 val iff_add = |
94 val iff_add = |
93 add_iff |
95 Thm.declaration_attribute (fn th => |
94 (Classical.safe_elim NONE, Classical.safe_intro NONE) |
96 Thm.attribute_declaration (add_iff |
95 (Classical.haz_elim NONE, Classical.haz_intro NONE) |
97 (Classical.safe_elim NONE, Classical.safe_intro NONE) |
96 #> Simplifier.simp_add; |
98 (Classical.haz_elim NONE, Classical.haz_intro NONE)) th |
|
99 #> Thm.attribute_declaration Simplifier.simp_add th); |
97 |
100 |
98 val iff_add' = |
101 val iff_add' = |
99 add_iff |
102 add_iff |
100 (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE) |
103 (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE) |
101 (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE); |
104 (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE); |
102 |
105 |
103 val iff_del = |
106 val iff_del = |
104 del_iff Classical.rule_del #> |
107 Thm.declaration_attribute (fn th => |
105 del_iff Context_Rules.rule_del #> |
108 Thm.attribute_declaration (del_iff Classical.rule_del) th #> |
106 Simplifier.simp_del; |
109 Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #> |
|
110 Thm.attribute_declaration Simplifier.simp_del th); |
107 |
111 |
108 end; |
112 end; |
109 |
113 |
110 |
114 |
111 (* tactics *) |
115 (* tactics *) |