# HG changeset patch # User huffman # Date 1338618762 -7200 # Node ID 9f458b3efb5c2351d01f1a1d2ea2eed4f3339882 # Parent c6783c9b87bfdbe30f5205f2d0384479dbc130c3# Parent 9014e78ccde2fd0bf89281ac21145130dd168a5c merged diff -r 9014e78ccde2 -r 9f458b3efb5c src/HOL/Finite_Set.thy --- 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" diff -r 9014e78ccde2 -r 9f458b3efb5c src/HOL/Int.thy --- 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 \ 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 9014e78ccde2 -r 9f458b3efb5c src/HOL/Library/Cardinality.thy --- 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 \ 'b) = CARD('a) * CARD('b)" unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product) diff -r 9014e78ccde2 -r 9f458b3efb5c src/HOL/Library/Numeral_Type.thy --- 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] diff -r 9014e78ccde2 -r 9f458b3efb5c src/HOL/Tools/transfer.ML --- 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)