# HG changeset patch # User huffman # Date 1370745619 25200 # Node ID acb4f932dd24f75b07bd1f771ecf64d02b5f42bb # Parent dba3d398c3226462037c8ea9c9529598b54385f8 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==> diff -r dba3d398c322 -r acb4f932dd24 src/HOL/Quotient_Examples/Lift_FSet.thy --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Fri Jun 07 22:17:22 2013 -0400 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Sat Jun 08 19:40:19 2013 -0700 @@ -136,34 +136,22 @@ but sometimes more convenient. *} lemma "fmap f (fmap g xs) = fmap (f \ g) xs" - apply transfer' - apply (rule map_map) - done + using map_map [Transfer.transferred] . lemma "ffilter p (fmap f xs) = fmap f (ffilter (p \ f) xs)" - apply transfer' - apply (rule filter_map) - done + using filter_map [Transfer.transferred] . lemma "ffilter p (ffilter q xs) = ffilter (\x. q x \ p x) xs" - apply transfer' - apply (rule filter_filter) - done + using filter_filter [Transfer.transferred] . lemma "fset (fcons x xs) = insert x (fset xs)" - apply transfer - apply (rule set.simps) - done + using set.simps(2) [Transfer.transferred] . lemma "fset (fappend xs ys) = fset xs \ fset ys" - apply transfer - apply (rule set_append) - done + using set_append [Transfer.transferred] . lemma "fset (fconcat xss) = (\xs\fset xss. fset xs)" - apply transfer - apply (rule set_concat) - done + using set_concat [Transfer.transferred] . lemma "\x\fset xs. f x = g x \ fmap f xs = fmap g xs" apply transfer @@ -176,7 +164,7 @@ done lemma "fconcat (fmap (\x. fcons x fnil) xs) = xs" - apply transfer' + apply transfer apply simp done @@ -184,8 +172,6 @@ by (induct xsss, simp_all) lemma "fconcat (fmap fconcat xss) = fconcat (fconcat xss)" - apply transfer' - apply (rule concat_map_concat) - done + using concat_map_concat [Transfer.transferred] . end diff -r dba3d398c322 -r acb4f932dd24 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Fri Jun 07 22:17:22 2013 -0400 +++ b/src/HOL/Tools/transfer.ML Sat Jun 08 19:40:19 2013 -0700 @@ -15,11 +15,14 @@ val get_relator_domain: Proof.context -> thm list val transfer_add: attribute val transfer_del: attribute + val transferred_attribute: thm list -> attribute val transfer_domain_add: attribute val transfer_domain_del: attribute - val transfer_rule_of_term: Proof.context -> term -> thm + val transfer_rule_of_term: Proof.context -> bool -> term -> thm + val transfer_rule_of_lhs: Proof.context -> term -> thm val transfer_tac: bool -> Proof.context -> int -> tactic val transfer_prover_tac: Proof.context -> int -> tactic + val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic val setup: theory -> theory end @@ -33,13 +36,15 @@ type T = { transfer_raw : thm Item_Net.T, known_frees : (string * typ) list, + compound_lhs : unit Net.net, compound_rhs : unit Net.net, relator_eq : thm Item_Net.T, relator_eq_raw : thm Item_Net.T, relator_domain : thm Item_Net.T } val empty = - { transfer_raw = Thm.full_rules, + { transfer_raw = Thm.intro_rules, known_frees = [], + compound_lhs = Net.empty, compound_rhs = Net.empty, relator_eq = Thm.full_rules, relator_eq_raw = Thm.full_rules, @@ -47,13 +52,16 @@ val extend = I fun merge ( { transfer_raw = t1, known_frees = k1, + compound_lhs = l1, compound_rhs = c1, relator_eq = r1, relator_eq_raw = rw1, relator_domain = rd1 }, { transfer_raw = t2, known_frees = k2, + compound_lhs = l2, compound_rhs = c2, relator_eq = r2, relator_eq_raw = rw2, relator_domain = rd2 } ) = { transfer_raw = Item_Net.merge (t1, t2), known_frees = Library.merge (op =) (k1, k2), + compound_lhs = Net.merge (K true) (l1, l2), compound_rhs = Net.merge (K true) (c1, c2), relator_eq = Item_Net.merge (r1, r2), relator_eq_raw = Item_Net.merge (rw1, rw2), @@ -66,6 +74,9 @@ fun get_known_frees ctxt = ctxt |> (#known_frees o Data.get o Context.Proof) +fun get_compound_lhs ctxt = ctxt + |> (#compound_lhs o Data.get o Context.Proof) + fun get_compound_rhs ctxt = ctxt |> (#compound_rhs o Data.get o Context.Proof) @@ -83,27 +94,36 @@ fun get_relator_domain ctxt = ctxt |> (Item_Net.content o #relator_domain o Data.get o Context.Proof) -fun map_data f1 f2 f3 f4 f5 f6 - { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw, relator_domain } = +fun map_data f1 f2 f3 f4 f5 f6 f7 + { transfer_raw, known_frees, compound_lhs, compound_rhs, + relator_eq, relator_eq_raw, relator_domain } = { transfer_raw = f1 transfer_raw, known_frees = f2 known_frees, - compound_rhs = f3 compound_rhs, - relator_eq = f4 relator_eq, - relator_eq_raw = f5 relator_eq_raw, - relator_domain = f6 relator_domain } + compound_lhs = f3 compound_lhs, + compound_rhs = f4 compound_rhs, + relator_eq = f5 relator_eq, + relator_eq_raw = f6 relator_eq_raw, + relator_domain = f7 relator_domain } -fun map_transfer_raw f = map_data f I I I I I -fun map_known_frees f = map_data I f I I I I -fun map_compound_rhs f = map_data I I f I I I -fun map_relator_eq f = map_data I I I f I I -fun map_relator_eq_raw f = map_data I I I I f I -fun map_relator_domain f = map_data I I I I I f +fun map_transfer_raw f = map_data f I I I I I I +fun map_known_frees f = map_data I f I I I I I +fun map_compound_lhs f = map_data I I f I I I I +fun map_compound_rhs f = map_data I I I f I I I +fun map_relator_eq f = map_data I I I I f I I +fun map_relator_eq_raw f = map_data I I I I I f I +fun map_relator_domain f = map_data I I I I I I f fun add_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.update thm) o + map_compound_lhs + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of + Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ => + Net.insert_term_safe (K true) (lhs, ()) + | _ => I) o map_compound_rhs (case HOLogic.dest_Trueprop (Thm.concl_of thm) of - (Const (@{const_name Rel}, _)) $ _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ()) + Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) => + Net.insert_term_safe (K true) (rhs, ()) | _ => I) o map_known_frees (Term.add_frees (Thm.concl_of thm))) @@ -148,8 +168,11 @@ val thy = Thm.theory_of_thm thm val prop = Thm.prop_of thm val (t, mk_prop') = dest prop - val add_eqs = Term.fold_aterms - (fn t as Const (@{const_name HOL.eq}, _) => insert (op =) t | _ => I) + (* Only consider "op =" at non-base types *) + fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) = + (case T of Type (_, []) => false | _ => true) + | is_eq _ = false + val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I) val eq_consts = rev (add_eqs t []) val eqTs = map (snd o dest_Const) eq_consts val used = Term.add_free_names prop [] @@ -308,13 +331,11 @@ 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 = +fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u = let 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])) = + (* precondition: prj(T,U) must consist of only TFrees and type "fun" *) + fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) = let val r1 = rel T1 U1 val r2 = rel T2 U2 @@ -322,7 +343,12 @@ in Const (@{const_name fun_rel}, rT) $ r1 $ r2 end - | rel T U = raise TYPE ("rel", [T, U], []) + | rel T U = + let + val (a, _) = dest_TFree (prj (T, U)) + in + Free (the (AList.lookup (op =) tab a), mk_relT (T, U)) + end fun zip _ thms (Bound i) (Bound _) = (nth thms i, []) | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) = let @@ -349,15 +375,15 @@ in (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2) end - | zip _ _ (t as Free (_, T)) u = + | zip _ _ t u = let + val T = fastype_of t 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) @@ -366,42 +392,136 @@ Drule.implies_intr_list hyps (thm RS rename) end -fun transfer_rule_of_term ctxt t = +(* create a lambda term of the same shape as the given term *) +fun skeleton (is_atom : term -> bool) 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 = + fun go (Bound i) ctxt = (Bound i, ctxt) + | go (Abs (x, _, t)) ctxt = let - val (t', ctxt) = skeleton t ctxt + val (t', ctxt) = go t ctxt in (Abs (x, dummyT, t'), ctxt) end - | skeleton (tu as (t $ u)) ctxt = - if is_rhs tu andalso not (Term.is_open tu) then dummy ctxt else + | go (tu as (t $ u)) ctxt = + if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else let - val (t', ctxt) = skeleton t ctxt - val (u', ctxt) = skeleton u ctxt + val (t', ctxt) = go t ctxt + val (u', ctxt) = go u ctxt in (t' $ u', ctxt) end - | skeleton _ ctxt = dummy ctxt - val s = skeleton t ctxt |> fst |> Syntax.check_term ctxt |> + | go _ ctxt = dummy ctxt + in + go t ctxt |> fst |> Syntax.check_term ctxt |> map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS))) + end + +(** Monotonicity analysis **) + +(* TODO: Put extensible table in theory data *) +val monotab = + Symtab.make + [(@{const_name transfer_implies}, [~1, 1]), + (@{const_name transfer_forall}, [1])(*, + (@{const_name implies}, [~1, 1]), + (@{const_name All}, [1])*)] + +(* +Function bool_insts determines the set of boolean-relation variables +that can be instantiated to implies, rev_implies, or iff. + +Invariants: bool_insts p (t, u) requires that + u :: _ => _ => ... => bool, and + t is a skeleton of u +*) +fun bool_insts p (t, u) = + let + fun strip2 (t1 $ t2, u1 $ u2, tus) = + strip2 (t1, u1, (t2, u2) :: tus) + | strip2 x = x + fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z) + fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab + | go Ts p (t, u) tab = + let + val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t))) + val (_, tf, tus) = strip2 (t, u, []) + val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE + val tab1 = + case ps_opt of + SOME ps => + let + val ps' = map (fn x => p * x) (take (length tus) ps) + in + fold I (map2 (go Ts) ps' tus) tab + end + | NONE => tab + val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))] + in + Symtab.join (K or3) (tab1, tab2) + end + val tab = go [] p (t, u) Symtab.empty + fun f (a, (true, false, false)) = SOME (a, @{const implies}) + | f (a, (false, true, false)) = SOME (a, @{const rev_implies}) + | f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT) + | f _ = NONE + in + map_filter f (Symtab.dest tab) + end + +fun transfer_rule_of_term ctxt equiv t : thm = + let + val compound_rhs = get_compound_rhs ctxt + val is_rhs = not o null o Net.unify_term compound_rhs + val s = skeleton is_rhs ctxt t 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 + val tab = tfrees ~~ rnames + fun prep a = the (AList.lookup (op =) tab a) + val thm = transfer_rule_of_terms fst ctxt' tab s t + val binsts = bool_insts (if equiv then 0 else 1) (s, t) + val cbool = @{ctyp bool} + val relT = @{typ "bool => bool => bool"} + val idx = Thm.maxidx_of thm + 1 + val thy = Proof_Context.theory_of ctxt + fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool) + fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t) in - Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm + thm + |> Thm.generalize (tfrees, rnames @ frees) idx + |> Thm.instantiate (map tinst binsts, map inst binsts) + end + +fun transfer_rule_of_lhs ctxt t : thm = + let + val compound_lhs = get_compound_lhs ctxt + val is_lhs = not o null o Net.unify_term compound_lhs + val s = skeleton is_lhs ctxt t + 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 tab = tfrees ~~ rnames + fun prep a = the (AList.lookup (op =) tab a) + val thm = transfer_rule_of_terms snd ctxt' tab t s + val binsts = bool_insts 1 (s, t) + val cbool = @{ctyp bool} + val relT = @{typ "bool => bool => bool"} + val idx = Thm.maxidx_of thm + 1 + val thy = Proof_Context.theory_of ctxt + fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool) + fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t) + in + thm + |> Thm.generalize (tfrees, rnames @ frees) idx + |> Thm.instantiate (map tinst binsts, map inst binsts) end fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq} @@ -409,7 +529,7 @@ fun transfer_tac equiv ctxt i = let val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} - val start_rule = + val start_rule = if equiv then @{thm transfer_start} else @{thm transfer_start'} val rules = get_transfer_raw ctxt val eq_rules = get_relator_eq_raw ctxt @@ -418,7 +538,7 @@ val err_msg = "Transfer failed to convert goal to an object-logic formula" fun main_tac (t, i) = rtac start_rule i THEN - (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t)) + (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t)) THEN_ALL_NEW (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules)) ORELSE' end_tac)) (i + 1) @@ -429,13 +549,13 @@ SUBGOAL main_tac i, (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) rewrite_goal_tac post_simps i, - rtac @{thm _} i] + Goal.norm_hhf_tac i] end fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) => let val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t - val rule1 = transfer_rule_of_term ctxt rhs + val rule1 = transfer_rule_of_term ctxt false rhs val rules = get_transfer_raw ctxt val eq_rules = get_relator_eq_raw ctxt in @@ -447,6 +567,45 @@ rtac @{thm refl} i] end) +(** Transfer attribute **) + +fun transferred ctxt extra_rules thm = + let + val start_rule = @{thm transfer_start} + val start_rule' = @{thm transfer_start'} + val rules = extra_rules @ get_transfer_raw ctxt + val eq_rules = get_relator_eq_raw ctxt + val err_msg = "Transfer failed to convert goal to an object-logic formula" + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} + val thm1 = Drule.forall_intr_vars thm + val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) []) + |> map (fn v as ((a, _), S) => (v, TFree (a, S))) + val thm2 = thm1 + |> Thm.certify_instantiate (instT, []) + |> Raw_Simplifier.rewrite_rule pre_simps + val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt + val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) + val rule = transfer_rule_of_lhs ctxt' t + val tac = + resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN + (rtac rule + THEN_ALL_NEW + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) + THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1 + handle TERM (_, ts) => raise TERM (err_msg, ts) + val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac) + val tnames = map (fst o dest_TFree o snd) instT + in + thm3 + |> Raw_Simplifier.rewrite_rule post_simps + |> Raw_Simplifier.norm_hhf + |> Drule.generalize (tnames, []) + |> Drule.zero_var_indexes + end +(* + handle THM _ => thm +*) + (** Methods and attributes **) val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => @@ -484,6 +643,14 @@ val transfer_domain_attribute = Attrib.add_del transfer_domain_add transfer_domain_del +(* Attributes for transferred rules *) + +fun transferred_attribute thms = Thm.rule_attribute + (fn context => transferred (Context.proof_of context) thms) + +val transferred_attribute_parser = + Attrib.thms >> transferred_attribute + (* Theory setup *) val relator_eq_setup = @@ -528,6 +695,8 @@ (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get) #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute "transfer domain rule for transfer method" + #> Attrib.setup @{binding transferred} transferred_attribute_parser + "raw theorem transferred to abstract theorem using transfer rules" #> Global_Theory.add_thms_dynamic (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get) #> Method.setup @{binding transfer} (transfer_method true) diff -r dba3d398c322 -r acb4f932dd24 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Fri Jun 07 22:17:22 2013 -0400 +++ b/src/HOL/Transfer.thy Sat Jun 08 19:40:19 2013 -0700 @@ -61,6 +61,11 @@ lemma is_equality_eq: "is_equality (op =)" unfolding is_equality_def by simp +text {* Reverse implication for monotonicity rules *} + +definition rev_implies where + "rev_implies x y \ (y \ x)" + text {* Handling of meta-logic connectives *} definition transfer_forall where @@ -252,14 +257,31 @@ text {* Transfer rules using implication instead of equality on booleans. *} +lemma transfer_forall_transfer [transfer_rule]: + "bi_total A \ ((A ===> op =) ===> op =) transfer_forall transfer_forall" + "right_total A \ ((A ===> op =) ===> implies) transfer_forall transfer_forall" + "right_total A \ ((A ===> implies) ===> implies) transfer_forall transfer_forall" + "bi_total A \ ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall" + "bi_total A \ ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall" + unfolding transfer_forall_def rev_implies_def fun_rel_def right_total_def bi_total_def + by metis+ + +lemma transfer_implies_transfer [transfer_rule]: + "(op = ===> op = ===> op = ) transfer_implies transfer_implies" + "(rev_implies ===> implies ===> implies ) transfer_implies transfer_implies" + "(rev_implies ===> op = ===> implies ) transfer_implies transfer_implies" + "(op = ===> implies ===> implies ) transfer_implies transfer_implies" + "(op = ===> op = ===> implies ) transfer_implies transfer_implies" + "(implies ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" + "(implies ===> op = ===> rev_implies) transfer_implies transfer_implies" + "(op = ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" + "(op = ===> op = ===> rev_implies) transfer_implies transfer_implies" + unfolding transfer_implies_def rev_implies_def fun_rel_def by auto + lemma eq_imp_transfer [transfer_rule]: "right_unique A \ (A ===> A ===> op \) (op =) (op =)" unfolding right_unique_alt_def . -lemma forall_imp_transfer [transfer_rule]: - "right_total A \ ((A ===> op \) ===> op \) transfer_forall transfer_forall" - unfolding right_total_alt_def transfer_forall_def . - lemma eq_transfer [transfer_rule]: assumes "bi_unique A" shows "(A ===> A ===> op =) (op =) (op =)"