src/Provers/clasimp.ML
changeset 45375 7fe19930dfc9
parent 44890 22f665a2e91c
child 47967 c422128d3889
equal deleted inserted replaced
45374:e99fd663c4a3 45375:7fe19930dfc9
    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 *)