--- a/src/HOL/Finite_Set.thy Fri Jun 01 20:40:34 2012 +0200
+++ b/src/HOL/Finite_Set.thy Sat Jun 02 08:32:42 2012 +0200
@@ -2081,7 +2081,7 @@
ultimately show "finite (UNIV :: 'b set)" by simp
qed
-lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
+lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"
unfolding UNIV_unit by simp
lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
--- a/src/HOL/Int.thy Fri Jun 01 20:40:34 2012 +0200
+++ b/src/HOL/Int.thy Sat Jun 02 08:32:42 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/Library/Cardinality.thy Fri Jun 01 20:40:34 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy Sat Jun 02 08:32:42 2012 +0200
@@ -44,9 +44,6 @@
in [(@{const_syntax card}, card_univ_tr')] end
*}
-lemma card_unit [simp]: "CARD(unit) = 1"
- unfolding UNIV_unit by simp
-
lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a) * CARD('b)"
unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
--- a/src/HOL/Library/Numeral_Type.thy Fri Jun 01 20:40:34 2012 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Sat Jun 02 08:32:42 2012 +0200
@@ -31,7 +31,7 @@
lemma card_num1 [simp]: "CARD(num1) = 1"
unfolding type_definition.card [OF type_definition_num1]
- by (simp only: card_unit)
+ by (simp only: card_UNIV_unit)
lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
unfolding type_definition.card [OF type_definition_bit0]
--- a/src/HOL/Tools/transfer.ML Fri Jun 01 20:40:34 2012 +0200
+++ b/src/HOL/Tools/transfer.ML Sat Jun 02 08:32:42 2012 +0200
@@ -19,20 +19,80 @@
structure Transfer : TRANSFER =
struct
-structure Data = Named_Thms
+(** Theory Data **)
+
+structure Data = Generic_Data
(
- val name = @{binding transfer_raw}
- val description = "raw transfer rule for transfer method"
+ 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,
+ 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) }
)
-structure Relator_Eq = Named_Thms
-(
- val name = @{binding relator_eq}
- val description = "relator equality rule (used by transfer method)"
-)
+fun get_relator_eq ctxt = ctxt
+ |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
+ |> map (Thm.symmetric o mk_meta_eq)
+
+fun get_transfer_raw ctxt = ctxt
+ |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
+
+fun get_known_frees ctxt = ctxt
+ |> (#known_frees o Data.get o Context.Proof)
+
+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,
+ compound_rhs = f3 compound_rhs,
+ relator_eq = f4 relator_eq }
-fun get_relator_eq ctxt =
- map (Thm.symmetric o mk_meta_eq) (Relator_Eq.get ctxt)
+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))
+
+val relator_eq_setup =
+ let
+ val name = @{binding relator_eq}
+ fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
+ fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
+ val add = Thm.declaration_attribute add_thm
+ val del = Thm.declaration_attribute del_thm
+ val text = "declaration of relator equality rule (used by transfer method)"
+ val content = Item_Net.content o #relator_eq o Data.get
+ in
+ Attrib.setup name (Attrib.add_del add del) text
+ #> Global_Theory.add_thms_dynamic (name, content)
+ end
(** Conversions **)
@@ -83,34 +143,13 @@
fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
let
+ val keepers = keepers @ get_known_frees ctxt
val vs = rev (Term.add_frees t [])
val vs' = filter_out (member (op =) keepers) vs
in
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 =
@@ -177,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 [])
@@ -193,7 +257,7 @@
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 rules = get_transfer_raw ctxt
(* allow unsolved subgoals only for standard transfer method, not for transfer' *)
val end_tac = if equiv then K all_tac else K no_tac
in
@@ -214,7 +278,7 @@
let
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
+ val rules = get_transfer_raw ctxt
in
EVERY
[CONVERSION prep_conv i,
@@ -245,10 +309,10 @@
val prep_rule = Conv.fconv_rule prep_conv
val transfer_add =
- Thm.declaration_attribute (Data.add_thm o prep_rule)
+ Thm.declaration_attribute (add_transfer_thm o prep_rule)
val transfer_del =
- Thm.declaration_attribute (Data.del_thm o prep_rule)
+ Thm.declaration_attribute (del_transfer_thm o prep_rule)
val transfer_attribute =
Attrib.add_del transfer_add transfer_del
@@ -256,10 +320,11 @@
(* Theory setup *)
val setup =
- Data.setup
- #> Relator_Eq.setup
+ relator_eq_setup
#> Attrib.setup @{binding transfer_rule} transfer_attribute
"transfer rule for transfer method"
+ #> Global_Theory.add_thms_dynamic
+ (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
#> Method.setup @{binding transfer} (transfer_method true)
"generic theorem transfer method"
#> Method.setup @{binding transfer'} (transfer_method false)