# HG changeset patch # User huffman # Date 1338618449 -7200 # Node ID c6783c9b87bfdbe30f5205f2d0384479dbc130c3 # Parent 8aa05d38299a4805c04c570cc9eb27e62325bc06 transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters diff -r 8aa05d38299a -r c6783c9b87bf src/HOL/Int.thy --- a/src/HOL/Int.thy Fri Jun 01 11:55:06 2012 +0200 +++ b/src/HOL/Int.thy Sat Jun 02 08:27:29 2012 +0200 @@ -212,25 +212,22 @@ of_nat_add [symmetric] simp del: of_nat_add) lemma of_int_0 [simp]: "of_int 0 = 0" -by (simp add: of_int.abs_eq zero_int.abs_eq) (* FIXME: transfer *) + by transfer simp lemma of_int_1 [simp]: "of_int 1 = 1" -by (simp add: of_int.abs_eq one_int.abs_eq) (* FIXME: transfer *) + by transfer simp lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" -(* FIXME: transfer *) -by (cases w, cases z) (simp add: algebra_simps of_int.abs_eq plus_int.abs_eq) + by transfer (clarsimp simp add: algebra_simps) lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" -(* FIXME: transfer *) -by (cases z) (simp add: algebra_simps of_int.abs_eq uminus_int.abs_eq) + by (transfer fixing: uminus) clarsimp lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z" by (simp add: diff_minus Groups.diff_minus) lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" -by (cases w, cases z, (* FIXME: transfer *) - simp add: algebra_simps of_int.abs_eq times_int.abs_eq of_nat_mult) + by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult) text{*Collapse nested embeddings*} lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n" @@ -254,12 +251,8 @@ lemma of_int_eq_iff [simp]: "of_int w = of_int z \ w = z" -(* FIXME: transfer *) -apply (cases w, cases z) -apply (simp add: of_int.abs_eq int.abs_eq_iff) -apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq) -apply (simp only: of_nat_add [symmetric] of_nat_eq_iff) -done + by transfer (clarsimp simp add: algebra_simps + of_nat_add [symmetric] simp del: of_nat_add) text{*Special cases where either operand is zero*} lemma of_int_eq_0_iff [simp]: @@ -280,9 +273,8 @@ lemma of_int_le_iff [simp]: "of_int w \ of_int z \ w \ z" - by (cases w, cases z) (* FIXME: transfer *) - (simp add: of_int.abs_eq less_eq_int.abs_eq - algebra_simps of_nat_add [symmetric] del: of_nat_add) + by (transfer fixing: less_eq) (clarsimp simp add: algebra_simps + of_nat_add [symmetric] simp del: of_nat_add) lemma of_int_less_iff [simp]: "of_int w < of_int z \ w < z" @@ -391,8 +383,7 @@ begin lemma of_nat_nat: "0 \ z \ of_nat (nat z) = of_int z" - by (cases z rule: eq_Abs_Integ) (* FIXME: transfer *) - (simp add: nat.abs_eq less_eq_int.abs_eq of_int.abs_eq zero_int.abs_eq of_nat_diff) + by transfer (clarsimp simp add: of_nat_diff) end diff -r 8aa05d38299a -r c6783c9b87bf src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Fri Jun 01 11:55:06 2012 +0200 +++ b/src/HOL/Tools/transfer.ML Sat Jun 02 08:27:29 2012 +0200 @@ -26,16 +26,22 @@ type T = { transfer_raw : thm Item_Net.T, known_frees : (string * typ) list, + compound_rhs : unit Net.net, relator_eq : thm Item_Net.T } val empty = { transfer_raw = Thm.full_rules, known_frees = [], + compound_rhs = Net.empty, relator_eq = Thm.full_rules } val extend = I - fun merge ({transfer_raw = t1, known_frees = k1, relator_eq = r1}, - {transfer_raw = t2, known_frees = k2, relator_eq = r2}) = + fun merge + ( { transfer_raw = t1, known_frees = k1, + compound_rhs = c1, relator_eq = r1}, + { transfer_raw = t2, known_frees = k2, + compound_rhs = c2, relator_eq = r2}) = { transfer_raw = Item_Net.merge (t1, t2), known_frees = Library.merge (op =) (k1, k2), + compound_rhs = Net.merge (K true) (c1, c2), relator_eq = Item_Net.merge (r1, r2) } ) @@ -49,17 +55,27 @@ fun get_known_frees ctxt = ctxt |> (#known_frees o Data.get o Context.Proof) -fun map_data f1 f2 f3 {transfer_raw, known_frees, relator_eq} = +fun get_compound_rhs ctxt = ctxt + |> (#compound_rhs o Data.get o Context.Proof) + +fun map_data f1 f2 f3 f4 + { transfer_raw, known_frees, compound_rhs, relator_eq } = { transfer_raw = f1 transfer_raw, known_frees = f2 known_frees, - relator_eq = f3 relator_eq } + compound_rhs = f3 compound_rhs, + relator_eq = f4 relator_eq } -fun map_transfer_raw f = map_data f I I -fun map_known_frees f = map_data I f I -fun map_relator_eq f = map_data I I f +fun map_transfer_raw f = map_data f I I I +fun map_known_frees f = map_data I f I I +fun map_compound_rhs f = map_data I I f I +fun map_relator_eq f = map_data I I I f fun add_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.update thm) o + map_compound_rhs + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of + _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ()) + | _ => I) o map_known_frees (Term.add_frees (Thm.concl_of thm))) fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm)) @@ -134,28 +150,6 @@ Induct.arbitrary_tac ctxt 0 vs' i end) -(* 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 = @@ -222,6 +216,31 @@ fun transfer_rule_of_term ctxt t = let + val compound_rhs = get_compound_rhs ctxt + val is_rhs = not o null o Net.unify_term compound_rhs + fun dummy ctxt = + let + val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt + in + (Free (c, dummyT), ctxt) + end + (* 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 (tu as (t $ u)) ctxt = + if is_rhs tu then dummy ctxt else + let + val (t', ctxt) = skeleton t ctxt + val (u', ctxt) = skeleton u ctxt + in + (t' $ u', ctxt) + end + | skeleton _ ctxt = dummy ctxt 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 [])