make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
authorhuffman
Fri Apr 20 10:18:08 2012 +0200 (2012-04-20)
changeset 476181568dadd598a
parent 47617 f5eaa7fa8d72
child 47620 148d0b3db78d
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Tools/transfer.ML	Thu Apr 19 23:18:47 2012 +0200
     1.2 +++ b/src/HOL/Tools/transfer.ML	Fri Apr 20 10:18:08 2012 +0200
     1.3 @@ -86,8 +86,7 @@
     1.4        Conv.implies_conv Conv.all_conv (correspond_conv ctxt)
     1.5        else_conv
     1.6        Trueprop_conv
     1.7 -      (Conv.combination_conv
     1.8 -         (Conv.combination_conv Rel_conv (fo_conv ctxt)) (fo_conv ctxt))
     1.9 +      (Conv.combination_conv (Conv.fun_conv Rel_conv) (fo_conv ctxt))
    1.10        else_conv
    1.11        Conv.all_conv) ct
    1.12  
    1.13 @@ -156,8 +155,11 @@
    1.14    in
    1.15      EVERY
    1.16        [CONVERSION (correspond_conv ctxt) i,
    1.17 +       rtac @{thm correspondence_start} i,
    1.18         REPEAT_ALL_NEW
    1.19 -         (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) i]
    1.20 +         (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i+1),
    1.21 +       rewrite_goal_tac @{thms App_def Abs_def} i,
    1.22 +       rtac @{thm refl} i]
    1.23    end
    1.24  
    1.25  val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
     2.1 --- a/src/HOL/Transfer.thy	Thu Apr 19 23:18:47 2012 +0200
     2.2 +++ b/src/HOL/Transfer.thy	Fri Apr 20 10:18:08 2012 +0200
     2.3 @@ -81,6 +81,9 @@
     2.4  lemma transfer_start': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q"
     2.5    unfolding Rel_def by simp
     2.6  
     2.7 +lemma correspondence_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
     2.8 +  by simp
     2.9 +
    2.10  lemma Rel_eq_refl: "Rel (op =) x x"
    2.11    unfolding Rel_def ..
    2.12