implement transfer tactic with more scalable forward proof methods
authorhuffman
Fri Apr 27 14:07:31 2012 +0200 (2012-04-27)
changeset 4778971a526ee569a
parent 47788 44b33c1e702e
child 47790 2e1636e45770
implement transfer tactic with more scalable forward proof methods
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Tools/transfer.ML	Fri Apr 27 13:19:21 2012 +0200
     1.2 +++ b/src/HOL/Tools/transfer.ML	Fri Apr 27 14:07:31 2012 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  signature TRANSFER =
     1.6  sig
     1.7 -  val fo_conv: Proof.context -> conv
     1.8    val prep_conv: conv
     1.9    val get_relator_eq: Proof.context -> thm list
    1.10    val transfer_add: attribute
    1.11 @@ -14,7 +13,6 @@
    1.12    val transfer_tac: bool -> Proof.context -> int -> tactic
    1.13    val transfer_prover_tac: Proof.context -> int -> tactic
    1.14    val setup: theory -> theory
    1.15 -  val abs_tac: int -> tactic
    1.16  end
    1.17  
    1.18  structure Transfer : TRANSFER =
    1.19 @@ -37,22 +35,12 @@
    1.20  
    1.21  (** Conversions **)
    1.22  
    1.23 -val App_rule = Thm.symmetric @{thm App_def}
    1.24 -val Abs_rule = Thm.symmetric @{thm Abs_def}
    1.25  val Rel_rule = Thm.symmetric @{thm Rel_def}
    1.26  
    1.27  fun dest_funcT cT =
    1.28    (case Thm.dest_ctyp cT of [T, U] => (T, U)
    1.29      | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
    1.30  
    1.31 -fun App_conv ct =
    1.32 -  let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct)
    1.33 -  in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] App_rule end
    1.34 -
    1.35 -fun Abs_conv ct =
    1.36 -  let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct)
    1.37 -  in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Abs_rule end
    1.38 -
    1.39  fun Rel_conv ct =
    1.40    let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
    1.41        val (cU, _) = dest_funcT cT'
    1.42 @@ -63,14 +51,6 @@
    1.43      Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    1.44    | _ => raise CTERM ("Trueprop_conv", [ct]))
    1.45  
    1.46 -(* Conversion to insert tags on every application and abstraction. *)
    1.47 -fun fo_conv ctxt ct = (
    1.48 -      Conv.combination_conv (fo_conv ctxt then_conv App_conv) (fo_conv ctxt)
    1.49 -      else_conv
    1.50 -      Conv.abs_conv (fo_conv o snd) ctxt then_conv Abs_conv
    1.51 -      else_conv
    1.52 -      Conv.all_conv) ct
    1.53 -
    1.54  (* Conversion to preprocess a transfer rule *)
    1.55  fun prep_conv ct = (
    1.56        Conv.implies_conv Conv.all_conv prep_conv
    1.57 @@ -79,24 +59,10 @@
    1.58        else_conv
    1.59        Conv.all_conv) ct
    1.60  
    1.61 -(* Conversion to prep a proof goal containing a transfer rule *)
    1.62 -fun transfer_goal_conv ctxt ct = (
    1.63 -      Conv.forall_conv (transfer_goal_conv o snd) ctxt
    1.64 -      else_conv
    1.65 -      Conv.implies_conv Conv.all_conv (transfer_goal_conv ctxt)
    1.66 -      else_conv
    1.67 -      Trueprop_conv
    1.68 -      (Conv.combination_conv (Conv.fun_conv Rel_conv) (fo_conv ctxt))
    1.69 -      else_conv
    1.70 -      Conv.all_conv) ct
    1.71 -
    1.72 -
    1.73  (** Transfer proof method **)
    1.74  
    1.75 -fun dest_Rel (Const (@{const_name Rel}, _) $ r $ x $ y) = (r, x, y)
    1.76 -  | dest_Rel t = raise TERM ("dest_Rel", [t])
    1.77 -
    1.78  fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
    1.79 +  | RelT t = raise TERM ("RelT", [t])
    1.80  
    1.81  (* Tactic to correspond a value to itself *)
    1.82  fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
    1.83 @@ -111,7 +77,7 @@
    1.84    end handle Match => no_tac | TERM _ => no_tac)
    1.85  
    1.86  val post_simps =
    1.87 -  @{thms App_def Abs_def transfer_forall_eq [symmetric]
    1.88 +  @{thms transfer_forall_eq [symmetric]
    1.89      transfer_implies_eq [symmetric] transfer_bforall_unfold}
    1.90  
    1.91  fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
    1.92 @@ -122,47 +88,141 @@
    1.93      Induct.arbitrary_tac ctxt 0 vs' i
    1.94    end)
    1.95  
    1.96 -(* Apply rule Rel_Abs with appropriate bound variable name *)
    1.97 -val abs_tac = SUBGOAL (fn (t, i) =>
    1.98 +(* create a lambda term of the same shape as the given term *)
    1.99 +fun skeleton (Bound i) ctxt = (Bound i, ctxt)
   1.100 +  | skeleton (Abs (x, _, t)) ctxt =
   1.101 +      let
   1.102 +        val (t', ctxt) = skeleton t ctxt
   1.103 +      in
   1.104 +        (Abs (x, dummyT, t'), ctxt)
   1.105 +      end
   1.106 +  | skeleton (t $ u) ctxt =
   1.107 +      let
   1.108 +        val (t', ctxt) = skeleton t ctxt
   1.109 +        val (u', ctxt) = skeleton u ctxt
   1.110 +      in
   1.111 +        (t' $ u', ctxt)
   1.112 +      end
   1.113 +  | skeleton _ ctxt =
   1.114 +      let
   1.115 +        val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
   1.116 +      in
   1.117 +        (Free (c, dummyT), ctxt)
   1.118 +      end
   1.119 +
   1.120 +fun mk_relT (T, U) = T --> U --> HOLogic.boolT
   1.121 +
   1.122 +fun mk_Rel t =
   1.123 +  let val T = fastype_of t
   1.124 +  in Const (@{const_name Transfer.Rel}, T --> T) $ t end
   1.125 +
   1.126 +fun transfer_rule_of_terms ctxt tab t u =
   1.127    let
   1.128 -    val pat = (#2 o dest_Rel o HOLogic.dest_Trueprop o Thm.concl_of) @{thm Rel_Abs}
   1.129 -    val obj = (#3 o dest_Rel o HOLogic.dest_Trueprop o Logic.strip_assums_concl) t
   1.130 -    val rule = Thm.rename_boundvars pat obj @{thm Rel_Abs}
   1.131 +    val thy = Proof_Context.theory_of ctxt
   1.132 +    (* precondition: T must consist of only TFrees and function space *)
   1.133 +    fun rel (T as TFree (a, _)) U =
   1.134 +          Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
   1.135 +      | rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
   1.136 +        let
   1.137 +          val r1 = rel T1 U1
   1.138 +          val r2 = rel T2 U2
   1.139 +          val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
   1.140 +        in
   1.141 +          Const (@{const_name fun_rel}, rT) $ r1 $ r2
   1.142 +        end
   1.143 +      | rel T U = raise TYPE ("rel", [T, U], [])
   1.144 +    fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
   1.145 +      | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
   1.146 +        let
   1.147 +          val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
   1.148 +          val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
   1.149 +          val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
   1.150 +          val thm0 = Thm.assume cprop
   1.151 +          val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
   1.152 +          val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
   1.153 +          val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
   1.154 +          val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
   1.155 +          val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
   1.156 +          val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
   1.157 +          val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
   1.158 +          val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
   1.159 +          val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
   1.160 +        in
   1.161 +          (thm2 COMP rule, hyps)
   1.162 +        end
   1.163 +      | zip ctxt thms (f $ t) (g $ u) =
   1.164 +        let
   1.165 +          val (thm1, hyps1) = zip ctxt thms f g
   1.166 +          val (thm2, hyps2) = zip ctxt thms t u
   1.167 +        in
   1.168 +          (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
   1.169 +        end
   1.170 +      | zip _ _ (t as Free (_, T)) u =
   1.171 +        let
   1.172 +          val U = fastype_of u
   1.173 +          val prop = mk_Rel (rel T U) $ t $ u
   1.174 +          val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
   1.175 +        in
   1.176 +          (Thm.assume cprop, [cprop])
   1.177 +        end
   1.178 +      | zip _ _ t u = raise TERM ("zip_relterm", [t, u])
   1.179 +    val r = mk_Rel (rel (fastype_of t) (fastype_of u))
   1.180 +    val goal = HOLogic.mk_Trueprop (r $ t $ u)
   1.181 +    val rename = Thm.trivial (cterm_of thy goal)
   1.182 +    val (thm, hyps) = zip ctxt [] t u
   1.183    in
   1.184 -    rtac rule i
   1.185 -  end handle TERM _ => no_tac)
   1.186 +    Drule.implies_intr_list hyps (thm RS rename)
   1.187 +  end
   1.188  
   1.189 -fun transfer_tac equiv ctxt = SUBGOAL (fn (t, i) =>
   1.190 +fun transfer_rule_of_term ctxt t =
   1.191    let
   1.192 +    val s = skeleton t ctxt |> fst |> Syntax.check_term ctxt |>
   1.193 +      map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
   1.194 +    val frees = map fst (Term.add_frees s [])
   1.195 +    val tfrees = map fst (Term.add_tfrees s [])
   1.196 +    fun prep a = "R" ^ Library.unprefix "'" a
   1.197 +    val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
   1.198 +    val thm = transfer_rule_of_terms ctxt' (tfrees ~~ rnames) s t
   1.199 +  in
   1.200 +    Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm
   1.201 +  end
   1.202 +
   1.203 +fun transfer_tac equiv ctxt i =
   1.204 +  let
   1.205 +    val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
   1.206 +    val start_rule = 
   1.207 +      if equiv then @{thm transfer_start} else @{thm transfer_start'}
   1.208      val rules = Data.get ctxt
   1.209 -    val app_tac = rtac @{thm Rel_App}
   1.210 -    val start_rule =
   1.211 -      if equiv then @{thm transfer_start} else @{thm transfer_start'}
   1.212    in
   1.213      EVERY
   1.214 -      [rewrite_goal_tac @{thms transfer_forall_eq transfer_implies_eq} i,
   1.215 -       CONVERSION (Trueprop_conv (fo_conv ctxt)) i,
   1.216 -       rtac start_rule i,
   1.217 -       SOLVED' (REPEAT_ALL_NEW (app_tac ORELSE' abs_tac ORELSE' atac
   1.218 -         ORELSE' SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
   1.219 -         ORELSE' eq_tac ctxt)) (i + 1),
   1.220 +      [rewrite_goal_tac pre_simps i THEN
   1.221 +       SUBGOAL (fn (t, i) =>
   1.222 +         rtac start_rule i THEN
   1.223 +         (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
   1.224 +           THEN_ALL_NEW
   1.225 +             (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
   1.226 +               ORELSE' eq_tac ctxt)) (i + 1)) i,
   1.227         (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
   1.228         rewrite_goal_tac post_simps i,
   1.229         rtac @{thm _} i]
   1.230 -  end)
   1.231 +  end
   1.232  
   1.233 -fun transfer_prover_tac ctxt i =
   1.234 +fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
   1.235    let
   1.236 -    val rules = @{thms Rel_App Rel_Abs} @ Data.get ctxt
   1.237 +    val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
   1.238 +    val rule1 = transfer_rule_of_term ctxt rhs
   1.239 +    val rules = Data.get ctxt
   1.240    in
   1.241      EVERY
   1.242 -      [CONVERSION (transfer_goal_conv ctxt) i,
   1.243 +      [CONVERSION prep_conv i,
   1.244         rtac @{thm transfer_prover_start} i,
   1.245 -       REPEAT_ALL_NEW
   1.246 -         (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i+1),
   1.247 -       rewrite_goal_tac @{thms App_def Abs_def} i,
   1.248 +       (rtac rule1 THEN_ALL_NEW
   1.249 +         REPEAT_ALL_NEW
   1.250 +           (resolve_tac rules ORELSE' eq_tac ctxt)) (i+1),
   1.251         rtac @{thm refl} i]
   1.252 -  end
   1.253 +  end)
   1.254 +
   1.255 +(** Methods and attributes **)
   1.256  
   1.257  val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
   1.258    error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))
     2.1 --- a/src/HOL/Transfer.thy	Fri Apr 27 13:19:21 2012 +0200
     2.2 +++ b/src/HOL/Transfer.thy	Fri Apr 27 14:07:31 2012 +0200
     2.3 @@ -42,14 +42,8 @@
     2.4  
     2.5  subsection {* Transfer method *}
     2.6  
     2.7 -text {* Explicit tags for application, abstraction, and relation
     2.8 -membership allow for backward proof methods. *}
     2.9 -
    2.10 -definition App :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    2.11 -  where "App f \<equiv> f"
    2.12 -
    2.13 -definition Abs :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    2.14 -  where "Abs f \<equiv> f"
    2.15 +text {* Explicit tag for relation membership allows for
    2.16 +  backward proof methods. *}
    2.17  
    2.18  definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    2.19    where "Rel r \<equiv> r"
    2.20 @@ -87,15 +81,15 @@
    2.21  lemma Rel_eq_refl: "Rel (op =) x x"
    2.22    unfolding Rel_def ..
    2.23  
    2.24 -lemma Rel_App:
    2.25 +lemma Rel_app:
    2.26    assumes "Rel (A ===> B) f g" and "Rel A x y"
    2.27 -  shows "Rel B (App f x) (App g y)"
    2.28 -  using assms unfolding Rel_def App_def fun_rel_def by fast
    2.29 +  shows "Rel B (f x) (g y)"
    2.30 +  using assms unfolding Rel_def fun_rel_def by fast
    2.31  
    2.32 -lemma Rel_Abs:
    2.33 +lemma Rel_abs:
    2.34    assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
    2.35 -  shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))"
    2.36 -  using assms unfolding Rel_def Abs_def fun_rel_def by fast
    2.37 +  shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
    2.38 +  using assms unfolding Rel_def fun_rel_def by fast
    2.39  
    2.40  use "Tools/transfer.ML"
    2.41  
    2.42 @@ -103,7 +97,7 @@
    2.43  
    2.44  declare fun_rel_eq [relator_eq]
    2.45  
    2.46 -hide_const (open) App Abs Rel
    2.47 +hide_const (open) Rel
    2.48  
    2.49  
    2.50  subsection {* Predicates on relations, i.e. ``class constraints'' *}