# HG changeset patch # User huffman # Date 1335528451 -7200 # Node ID 71a526ee569ab61ccdba985c02de921018350964 # Parent 44b33c1e702e0cd93849a3a632a61301fa20e7af implement transfer tactic with more scalable forward proof methods diff -r 44b33c1e702e -r 71a526ee569a src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Fri Apr 27 13:19:21 2012 +0200 +++ b/src/HOL/Tools/transfer.ML Fri Apr 27 14:07:31 2012 +0200 @@ -6,7 +6,6 @@ signature TRANSFER = sig - val fo_conv: Proof.context -> conv val prep_conv: conv val get_relator_eq: Proof.context -> thm list val transfer_add: attribute @@ -14,7 +13,6 @@ val transfer_tac: bool -> Proof.context -> int -> tactic val transfer_prover_tac: Proof.context -> int -> tactic val setup: theory -> theory - val abs_tac: int -> tactic end structure Transfer : TRANSFER = @@ -37,22 +35,12 @@ (** Conversions **) -val App_rule = Thm.symmetric @{thm App_def} -val Abs_rule = Thm.symmetric @{thm Abs_def} val Rel_rule = Thm.symmetric @{thm Rel_def} fun dest_funcT cT = (case Thm.dest_ctyp cT of [T, U] => (T, U) | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], [])) -fun App_conv ct = - let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct) - in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] App_rule end - -fun Abs_conv ct = - let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct) - in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Abs_rule end - fun Rel_conv ct = let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct) val (cU, _) = dest_funcT cT' @@ -63,14 +51,6 @@ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct | _ => raise CTERM ("Trueprop_conv", [ct])) -(* Conversion to insert tags on every application and abstraction. *) -fun fo_conv ctxt ct = ( - Conv.combination_conv (fo_conv ctxt then_conv App_conv) (fo_conv ctxt) - else_conv - Conv.abs_conv (fo_conv o snd) ctxt then_conv Abs_conv - else_conv - Conv.all_conv) ct - (* Conversion to preprocess a transfer rule *) fun prep_conv ct = ( Conv.implies_conv Conv.all_conv prep_conv @@ -79,24 +59,10 @@ else_conv Conv.all_conv) ct -(* Conversion to prep a proof goal containing a transfer rule *) -fun transfer_goal_conv ctxt ct = ( - Conv.forall_conv (transfer_goal_conv o snd) ctxt - else_conv - Conv.implies_conv Conv.all_conv (transfer_goal_conv ctxt) - else_conv - Trueprop_conv - (Conv.combination_conv (Conv.fun_conv Rel_conv) (fo_conv ctxt)) - else_conv - Conv.all_conv) ct - - (** Transfer proof method **) -fun dest_Rel (Const (@{const_name Rel}, _) $ r $ x $ y) = (r, x, y) - | dest_Rel t = raise TERM ("dest_Rel", [t]) - fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y + | RelT t = raise TERM ("RelT", [t]) (* Tactic to correspond a value to itself *) fun eq_tac ctxt = SUBGOAL (fn (t, i) => @@ -111,7 +77,7 @@ end handle Match => no_tac | TERM _ => no_tac) val post_simps = - @{thms App_def Abs_def transfer_forall_eq [symmetric] + @{thms transfer_forall_eq [symmetric] transfer_implies_eq [symmetric] transfer_bforall_unfold} fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) => @@ -122,47 +88,141 @@ Induct.arbitrary_tac ctxt 0 vs' i end) -(* Apply rule Rel_Abs with appropriate bound variable name *) -val abs_tac = SUBGOAL (fn (t, i) => +(* create a lambda term of the same shape as the given term *) +fun skeleton (Bound i) ctxt = (Bound i, ctxt) + | skeleton (Abs (x, _, t)) ctxt = + let + val (t', ctxt) = skeleton t ctxt + in + (Abs (x, dummyT, t'), ctxt) + end + | skeleton (t $ u) ctxt = + let + val (t', ctxt) = skeleton t ctxt + val (u', ctxt) = skeleton u ctxt + in + (t' $ u', ctxt) + end + | skeleton _ ctxt = + let + val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt + in + (Free (c, dummyT), ctxt) + end + +fun mk_relT (T, U) = T --> U --> HOLogic.boolT + +fun mk_Rel t = + let val T = fastype_of t + in Const (@{const_name Transfer.Rel}, T --> T) $ t end + +fun transfer_rule_of_terms ctxt tab t u = let - val pat = (#2 o dest_Rel o HOLogic.dest_Trueprop o Thm.concl_of) @{thm Rel_Abs} - val obj = (#3 o dest_Rel o HOLogic.dest_Trueprop o Logic.strip_assums_concl) t - val rule = Thm.rename_boundvars pat obj @{thm Rel_Abs} + val thy = Proof_Context.theory_of ctxt + (* precondition: T must consist of only TFrees and function space *) + fun rel (T as TFree (a, _)) U = + Free (the (AList.lookup (op =) tab a), mk_relT (T, U)) + | rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) = + let + val r1 = rel T1 U1 + val r2 = rel T2 U2 + val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U) + in + Const (@{const_name fun_rel}, rT) $ r1 $ r2 + end + | rel T U = raise TYPE ("rel", [T, U], []) + fun zip _ thms (Bound i) (Bound _) = (nth thms i, []) + | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) = + let + val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt + val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U) + val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop) + val thm0 = Thm.assume cprop + val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u + val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop)) + val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1)) + val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1)) + val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2)) + val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2] + val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)] + val rule = Drule.instantiate' tinsts insts @{thm Rel_abs} + val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1)) + in + (thm2 COMP rule, hyps) + end + | zip ctxt thms (f $ t) (g $ u) = + let + val (thm1, hyps1) = zip ctxt thms f g + val (thm2, hyps2) = zip ctxt thms t u + in + (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2) + end + | zip _ _ (t as Free (_, T)) u = + let + val U = fastype_of u + val prop = mk_Rel (rel T U) $ t $ u + val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop) + in + (Thm.assume cprop, [cprop]) + end + | zip _ _ t u = raise TERM ("zip_relterm", [t, u]) + val r = mk_Rel (rel (fastype_of t) (fastype_of u)) + val goal = HOLogic.mk_Trueprop (r $ t $ u) + val rename = Thm.trivial (cterm_of thy goal) + val (thm, hyps) = zip ctxt [] t u in - rtac rule i - end handle TERM _ => no_tac) + Drule.implies_intr_list hyps (thm RS rename) + end -fun transfer_tac equiv ctxt = SUBGOAL (fn (t, i) => +fun transfer_rule_of_term ctxt t = let + val s = skeleton t ctxt |> fst |> Syntax.check_term ctxt |> + map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS))) + val frees = map fst (Term.add_frees s []) + val tfrees = map fst (Term.add_tfrees s []) + fun prep a = "R" ^ Library.unprefix "'" a + val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt + val thm = transfer_rule_of_terms ctxt' (tfrees ~~ rnames) s t + in + Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm + end + +fun transfer_tac equiv ctxt i = + let + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} + val start_rule = + if equiv then @{thm transfer_start} else @{thm transfer_start'} val rules = Data.get ctxt - val app_tac = rtac @{thm Rel_App} - val start_rule = - if equiv then @{thm transfer_start} else @{thm transfer_start'} in EVERY - [rewrite_goal_tac @{thms transfer_forall_eq transfer_implies_eq} i, - CONVERSION (Trueprop_conv (fo_conv ctxt)) i, - rtac start_rule i, - SOLVED' (REPEAT_ALL_NEW (app_tac ORELSE' abs_tac ORELSE' atac - ORELSE' SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)) - ORELSE' eq_tac ctxt)) (i + 1), + [rewrite_goal_tac pre_simps i THEN + SUBGOAL (fn (t, i) => + rtac start_rule i THEN + (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t)) + THEN_ALL_NEW + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)) + ORELSE' eq_tac ctxt)) (i + 1)) i, (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) rewrite_goal_tac post_simps i, rtac @{thm _} i] - end) + end -fun transfer_prover_tac ctxt i = +fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) => let - val rules = @{thms Rel_App Rel_Abs} @ Data.get ctxt + val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t + val rule1 = transfer_rule_of_term ctxt rhs + val rules = Data.get ctxt in EVERY - [CONVERSION (transfer_goal_conv ctxt) i, + [CONVERSION prep_conv i, rtac @{thm transfer_prover_start} i, - REPEAT_ALL_NEW - (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i+1), - rewrite_goal_tac @{thms App_def Abs_def} i, + (rtac rule1 THEN_ALL_NEW + REPEAT_ALL_NEW + (resolve_tac rules ORELSE' eq_tac ctxt)) (i+1), rtac @{thm refl} i] - end + end) + +(** Methods and attributes **) val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)) diff -r 44b33c1e702e -r 71a526ee569a src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Fri Apr 27 13:19:21 2012 +0200 +++ b/src/HOL/Transfer.thy Fri Apr 27 14:07:31 2012 +0200 @@ -42,14 +42,8 @@ subsection {* Transfer method *} -text {* Explicit tags for application, abstraction, and relation -membership allow for backward proof methods. *} - -definition App :: "('a \ 'b) \ 'a \ 'b" - where "App f \ f" - -definition Abs :: "('a \ 'b) \ 'a \ 'b" - where "Abs f \ f" +text {* Explicit tag for relation membership allows for + backward proof methods. *} definition Rel :: "('a \ 'b \ bool) \ 'a \ 'b \ bool" where "Rel r \ r" @@ -87,15 +81,15 @@ lemma Rel_eq_refl: "Rel (op =) x x" unfolding Rel_def .. -lemma Rel_App: +lemma Rel_app: assumes "Rel (A ===> B) f g" and "Rel A x y" - shows "Rel B (App f x) (App g y)" - using assms unfolding Rel_def App_def fun_rel_def by fast + shows "Rel B (f x) (g y)" + using assms unfolding Rel_def fun_rel_def by fast -lemma Rel_Abs: +lemma Rel_abs: assumes "\x y. Rel A x y \ Rel B (f x) (g y)" - shows "Rel (A ===> B) (Abs (\x. f x)) (Abs (\y. g y))" - using assms unfolding Rel_def Abs_def fun_rel_def by fast + shows "Rel (A ===> B) (\x. f x) (\y. g y)" + using assms unfolding Rel_def fun_rel_def by fast use "Tools/transfer.ML" @@ -103,7 +97,7 @@ declare fun_rel_eq [relator_eq] -hide_const (open) App Abs Rel +hide_const (open) Rel subsection {* Predicates on relations, i.e. ``class constraints'' *}