--- 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 \<longleftrightarrow> 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 \<le> of_int z \<longleftrightarrow> w \<le> 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 \<longleftrightarrow> w < z"
@@ -391,8 +383,7 @@
begin
lemma of_nat_nat: "0 \<le> z \<Longrightarrow> 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
--- 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 [])