1.1 --- a/src/HOL/Library/FSet.thy Thu Apr 10 17:48:17 2014 +0200
1.2 +++ b/src/HOL/Library/FSet.thy Thu Apr 10 17:48:18 2014 +0200
1.3 @@ -846,10 +846,10 @@
1.4 thm right_unique_rel_fset left_unique_rel_fset
1.5
1.6 lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)"
1.7 -by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_iff)
1.8 +by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_alt_def)
1.9
1.10 lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
1.11 -by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff)
1.12 +by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_alt_def)
1.13
1.14 lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
1.15
2.1 --- a/src/HOL/Lifting.thy Thu Apr 10 17:48:17 2014 +0200
2.2 +++ b/src/HOL/Lifting.thy Thu Apr 10 17:48:18 2014 +0200
2.3 @@ -161,6 +161,11 @@
2.4 (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
2.5 unfolding Quotient_alt_def3 fun_eq_iff by auto
2.6
2.7 +lemma Quotient_alt_def5:
2.8 + "Quotient R Abs Rep T \<longleftrightarrow>
2.9 + T \<le> BNF_Util.Grp UNIV Abs \<and> BNF_Util.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
2.10 + unfolding Quotient_alt_def4 Grp_def by blast
2.11 +
2.12 lemma fun_quotient:
2.13 assumes 1: "Quotient R1 abs1 rep1 T1"
2.14 assumes 2: "Quotient R2 abs2 rep2 T2"
2.15 @@ -210,32 +215,6 @@
2.16 lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x"
2.17 unfolding Respects_def by simp
2.18
2.19 -subsection {* Invariant *}
2.20 -
2.21 -definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
2.22 - where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
2.23 -
2.24 -lemma eq_onp_to_eq:
2.25 - assumes "eq_onp P x y"
2.26 - shows "x = y"
2.27 -using assms by (simp add: eq_onp_def)
2.28 -
2.29 -lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
2.30 -unfolding eq_onp_def rel_fun_def by auto
2.31 -
2.32 -lemma rel_fun_eq_onp_rel:
2.33 - shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
2.34 -by (auto simp add: eq_onp_def rel_fun_def)
2.35 -
2.36 -lemma eq_onp_same_args:
2.37 - shows "eq_onp P x x \<equiv> P x"
2.38 -using assms by (auto simp add: eq_onp_def)
2.39 -
2.40 -lemma eq_onp_transfer [transfer_rule]:
2.41 - assumes [transfer_rule]: "bi_unique A"
2.42 - shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
2.43 -unfolding eq_onp_def[abs_def] by transfer_prover
2.44 -
2.45 lemma UNIV_typedef_to_Quotient:
2.46 assumes "type_definition Rep Abs UNIV"
2.47 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
2.48 @@ -574,6 +553,8 @@
2.49 declare fun_mono[relator_mono]
2.50 lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
2.51
2.52 +ML_file "Tools/Lifting/lifting_bnf.ML"
2.53 +
2.54 ML_file "Tools/Lifting/lifting_term.ML"
2.55
2.56 ML_file "Tools/Lifting/lifting_def.ML"
3.1 --- a/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:17 2014 +0200
3.2 +++ b/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:18 2014 +0200
3.3 @@ -75,7 +75,7 @@
3.4
3.5 lemma bi_total_rel_set [transfer_rule]:
3.6 "bi_total A \<Longrightarrow> bi_total (rel_set A)"
3.7 -by(simp add: bi_total_conv_left_right left_total_rel_set right_total_rel_set)
3.8 +by(simp add: bi_total_alt_def left_total_rel_set right_total_rel_set)
3.9
3.10 lemma bi_unique_rel_set [transfer_rule]:
3.11 "bi_unique A \<Longrightarrow> bi_unique (rel_set A)"
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Thu Apr 10 17:48:18 2014 +0200
4.3 @@ -0,0 +1,118 @@
4.4 +(* Title: HOL/Tools/Transfer/transfer_bnf.ML
4.5 + Author: Ondrej Kuncar, TU Muenchen
4.6 +
4.7 +Setup for Lifting for types that are BNF.
4.8 +*)
4.9 +
4.10 +signature LIFTING_BNF =
4.11 +sig
4.12 +end
4.13 +
4.14 +structure Lifting_BNF : LIFTING_BNF =
4.15 +struct
4.16 +
4.17 +open BNF_Util
4.18 +open BNF_Def
4.19 +open Transfer_BNF
4.20 +
4.21 +(* Quotient map theorem *)
4.22 +
4.23 +fun Quotient_tac bnf ctxt i =
4.24 + let
4.25 + val rel_Grp = rel_Grp_of_bnf bnf
4.26 + fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
4.27 + val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
4.28 + val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
4.29 + val inst = map2 (curry(pairself (certify ctxt))) vars UNIVs
4.30 + val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst)
4.31 + |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
4.32 + |> (fn thm => thm RS sym)
4.33 + val rel_mono = rel_mono_of_bnf bnf
4.34 + val rel_conversep_sym = rel_conversep_of_bnf bnf RS sym
4.35 + in
4.36 + EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]),
4.37 + REPEAT_DETERM o (etac conjE), rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]),
4.38 + rtac rel_mono THEN_ALL_NEW atac, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt
4.39 + [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW atac,
4.40 + SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]),
4.41 + hyp_subst_tac ctxt, rtac refl] i
4.42 + end
4.43 +
4.44 +fun mk_Quotient args =
4.45 + let
4.46 + val argTs = map fastype_of args
4.47 + in
4.48 + list_comb (Const (@{const_name Quotient}, argTs ---> HOLogic.boolT), args)
4.49 + end
4.50 +
4.51 +fun prove_Quotient_map bnf ctxt =
4.52 + let
4.53 + val live = live_of_bnf bnf
4.54 + val old_ctxt = ctxt
4.55 + val (((As, Bs), Ds), ctxt) = ctxt
4.56 + |> mk_TFrees live
4.57 + ||>> mk_TFrees live
4.58 + ||>> mk_TFrees (dead_of_bnf bnf)
4.59 + val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs
4.60 + val ((argss, argss'), ctxt) = fold_map2 mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt
4.61 + |>> `transpose
4.62 +
4.63 + val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss
4.64 + val R_rel = list_comb (mk_rel_of_bnf Ds As As bnf, nth argss' 0)
4.65 + val Abs_map = list_comb (mk_map_of_bnf Ds As Bs bnf, nth argss' 1)
4.66 + val Rep_map = list_comb (mk_map_of_bnf Ds Bs As bnf, nth argss' 2)
4.67 + val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3)
4.68 + val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop
4.69 + val goal = Logic.list_implies (assms, concl)
4.70 + val thm = Goal.prove ctxt [] [] goal
4.71 + (fn {context = ctxt, prems = _} => Quotient_tac bnf ctxt 1)
4.72 + in
4.73 + Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
4.74 + end
4.75 +
4.76 +
4.77 +fun Quotient_map bnf ctxt =
4.78 + let
4.79 + val Quotient = prove_Quotient_map bnf ctxt
4.80 + fun qualify defname suffix = Binding.qualified true suffix defname
4.81 + val Quotient_thm_name = qualify (base_name_of_bnf bnf) "Quotient"
4.82 + val notes = [((Quotient_thm_name, []), [([Quotient], @{attributes [quot_map]})])]
4.83 + in
4.84 + notes
4.85 + end
4.86 +
4.87 +(* relator_eq_onp *)
4.88 +
4.89 +fun relator_eq_onp bnf ctxt =
4.90 + let
4.91 + val pred_data = lookup_defined_pred_data ctxt (type_name_of_bnf bnf)
4.92 + in
4.93 + [((Binding.empty, []), [([Transfer.rel_eq_onp pred_data], @{attributes [relator_eq_onp]})])]
4.94 + end
4.95 +
4.96 +(* relator_mono *)
4.97 +
4.98 +fun relator_mono bnf =
4.99 + [((Binding.empty, []), [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])]
4.100 +
4.101 +(* relator_distr *)
4.102 +
4.103 +fun relator_distr bnf =
4.104 + [((Binding.empty, []), [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])]
4.105 +
4.106 +(* interpretation *)
4.107 +
4.108 +fun lifting_bnf_interpretation bnf lthy =
4.109 + if dead_of_bnf bnf > 0 then lthy
4.110 + else
4.111 + let
4.112 + val notes = relator_eq_onp bnf lthy @ Quotient_map bnf lthy @ relator_mono bnf
4.113 + @ relator_distr bnf
4.114 + in
4.115 + snd (Local_Theory.notes notes lthy)
4.116 + end
4.117 +
4.118 +val _ = Context.>> (Context.map_theory (bnf_interpretation
4.119 + (bnf_only_type_ctr (fn bnf => map_local_theory (lifting_bnf_interpretation bnf)))))
4.120 +
4.121 +end
5.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 10 17:48:17 2014 +0200
5.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 10 17:48:18 2014 +0200
5.3 @@ -534,7 +534,7 @@
5.4 end
5.5
5.6 val unfold_ret_val_invs = Conv.bottom_conv
5.7 - (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy
5.8 + (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
5.9 val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
5.10 val unfold_inv_conv =
5.11 Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy
6.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Apr 10 17:48:17 2014 +0200
6.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Apr 10 17:48:18 2014 +0200
6.3 @@ -121,7 +121,7 @@
6.4 end
6.5
6.6 val unfold_ret_val_invs = Conv.bottom_conv
6.7 - (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy
6.8 + (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
6.9 val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
6.10 val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
6.11 val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Tools/Transfer/transfer.ML Thu Apr 10 17:48:18 2014 +0200
7.3 @@ -0,0 +1,868 @@
7.4 +(* Title: HOL/Tools/Transfer/transfer.ML
7.5 + Author: Brian Huffman, TU Muenchen
7.6 + Author: Ondrej Kuncar, TU Muenchen
7.7 +
7.8 +Generic theorem transfer method.
7.9 +*)
7.10 +
7.11 +signature TRANSFER =
7.12 +sig
7.13 + type pred_data
7.14 + val rel_eq_onp: pred_data -> thm
7.15 +
7.16 + val bottom_rewr_conv: thm list -> conv
7.17 + val top_rewr_conv: thm list -> conv
7.18 +
7.19 + val prep_conv: conv
7.20 + val get_transfer_raw: Proof.context -> thm list
7.21 + val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
7.22 + val get_relator_eq: Proof.context -> thm list
7.23 + val get_sym_relator_eq: Proof.context -> thm list
7.24 + val get_relator_eq_raw: Proof.context -> thm list
7.25 + val get_relator_domain: Proof.context -> thm list
7.26 + val morph_pred_data: morphism -> pred_data -> pred_data
7.27 + val lookup_pred_data: Proof.context -> string -> pred_data option
7.28 + val update_pred_data: string -> pred_data -> Context.generic -> Context.generic
7.29 + val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T
7.30 + val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
7.31 + val transfer_add: attribute
7.32 + val transfer_del: attribute
7.33 + val transfer_raw_add: thm -> Context.generic -> Context.generic
7.34 + val transfer_raw_del: thm -> Context.generic -> Context.generic
7.35 + val transferred_attribute: thm list -> attribute
7.36 + val untransferred_attribute: thm list -> attribute
7.37 + val prep_transfer_domain_thm: Proof.context -> thm -> thm
7.38 + val transfer_domain_add: attribute
7.39 + val transfer_domain_del: attribute
7.40 + val transfer_rule_of_term: Proof.context -> bool -> term -> thm
7.41 + val transfer_rule_of_lhs: Proof.context -> term -> thm
7.42 + val eq_tac: Proof.context -> int -> tactic
7.43 + val transfer_step_tac: Proof.context -> int -> tactic
7.44 + val transfer_tac: bool -> Proof.context -> int -> tactic
7.45 + val transfer_prover_tac: Proof.context -> int -> tactic
7.46 + val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
7.47 + val setup: theory -> theory
7.48 +end
7.49 +
7.50 +structure Transfer : TRANSFER =
7.51 +struct
7.52 +
7.53 +(** Theory Data **)
7.54 +
7.55 +val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
7.56 +val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
7.57 + o HOLogic.dest_Trueprop o Thm.concl_of);
7.58 +
7.59 +type pred_data = {rel_eq_onp: thm}
7.60 +
7.61 +val rel_eq_onp = #rel_eq_onp
7.62 +
7.63 +structure Data = Generic_Data
7.64 +(
7.65 + type T =
7.66 + { transfer_raw : thm Item_Net.T,
7.67 + known_frees : (string * typ) list,
7.68 + compound_lhs : (term * thm) Item_Net.T,
7.69 + compound_rhs : (term * thm) Item_Net.T,
7.70 + relator_eq : thm Item_Net.T,
7.71 + relator_eq_raw : thm Item_Net.T,
7.72 + relator_domain : thm Item_Net.T,
7.73 + pred_data : pred_data Symtab.table }
7.74 + val empty =
7.75 + { transfer_raw = Thm.intro_rules,
7.76 + known_frees = [],
7.77 + compound_lhs = compound_xhs_empty_net,
7.78 + compound_rhs = compound_xhs_empty_net,
7.79 + relator_eq = rewr_rules,
7.80 + relator_eq_raw = Thm.full_rules,
7.81 + relator_domain = Thm.full_rules,
7.82 + pred_data = Symtab.empty }
7.83 + val extend = I
7.84 + fun merge
7.85 + ( { transfer_raw = t1, known_frees = k1,
7.86 + compound_lhs = l1,
7.87 + compound_rhs = c1, relator_eq = r1,
7.88 + relator_eq_raw = rw1, relator_domain = rd1,
7.89 + pred_data = pd1 },
7.90 + { transfer_raw = t2, known_frees = k2,
7.91 + compound_lhs = l2,
7.92 + compound_rhs = c2, relator_eq = r2,
7.93 + relator_eq_raw = rw2, relator_domain = rd2,
7.94 + pred_data = pd2 } ) =
7.95 + { transfer_raw = Item_Net.merge (t1, t2),
7.96 + known_frees = Library.merge (op =) (k1, k2),
7.97 + compound_lhs = Item_Net.merge (l1, l2),
7.98 + compound_rhs = Item_Net.merge (c1, c2),
7.99 + relator_eq = Item_Net.merge (r1, r2),
7.100 + relator_eq_raw = Item_Net.merge (rw1, rw2),
7.101 + relator_domain = Item_Net.merge (rd1, rd2),
7.102 + pred_data = Symtab.merge (K true) (pd1, pd2) }
7.103 +)
7.104 +
7.105 +fun get_transfer_raw ctxt = ctxt
7.106 + |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
7.107 +
7.108 +fun get_known_frees ctxt = ctxt
7.109 + |> (#known_frees o Data.get o Context.Proof)
7.110 +
7.111 +fun get_compound_lhs ctxt = ctxt
7.112 + |> (#compound_lhs o Data.get o Context.Proof)
7.113 +
7.114 +fun get_compound_rhs ctxt = ctxt
7.115 + |> (#compound_rhs o Data.get o Context.Proof)
7.116 +
7.117 +fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
7.118 +
7.119 +fun get_relator_eq ctxt = ctxt
7.120 + |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
7.121 + |> map safe_mk_meta_eq
7.122 +
7.123 +fun get_sym_relator_eq ctxt = ctxt
7.124 + |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
7.125 + |> map (Thm.symmetric o safe_mk_meta_eq)
7.126 +
7.127 +fun get_relator_eq_raw ctxt = ctxt
7.128 + |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
7.129 +
7.130 +fun get_relator_domain ctxt = ctxt
7.131 + |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
7.132 +
7.133 +fun get_pred_data ctxt = ctxt
7.134 + |> (#pred_data o Data.get o Context.Proof)
7.135 +
7.136 +fun map_data f1 f2 f3 f4 f5 f6 f7 f8
7.137 + { transfer_raw, known_frees, compound_lhs, compound_rhs,
7.138 + relator_eq, relator_eq_raw, relator_domain, pred_data } =
7.139 + { transfer_raw = f1 transfer_raw,
7.140 + known_frees = f2 known_frees,
7.141 + compound_lhs = f3 compound_lhs,
7.142 + compound_rhs = f4 compound_rhs,
7.143 + relator_eq = f5 relator_eq,
7.144 + relator_eq_raw = f6 relator_eq_raw,
7.145 + relator_domain = f7 relator_domain,
7.146 + pred_data = f8 pred_data }
7.147 +
7.148 +fun map_transfer_raw f = map_data f I I I I I I I
7.149 +fun map_known_frees f = map_data I f I I I I I I
7.150 +fun map_compound_lhs f = map_data I I f I I I I I
7.151 +fun map_compound_rhs f = map_data I I I f I I I I
7.152 +fun map_relator_eq f = map_data I I I I f I I I
7.153 +fun map_relator_eq_raw f = map_data I I I I I f I I
7.154 +fun map_relator_domain f = map_data I I I I I I f I
7.155 +fun map_pred_data f = map_data I I I I I I I f
7.156 +
7.157 +fun add_transfer_thm thm = Data.map
7.158 + (map_transfer_raw (Item_Net.update thm) o
7.159 + map_compound_lhs
7.160 + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
7.161 + Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
7.162 + Item_Net.update (lhs, thm)
7.163 + | _ => I) o
7.164 + map_compound_rhs
7.165 + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
7.166 + Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
7.167 + Item_Net.update (rhs, thm)
7.168 + | _ => I) o
7.169 + map_known_frees (Term.add_frees (Thm.concl_of thm)))
7.170 +
7.171 +fun del_transfer_thm thm = Data.map
7.172 + (map_transfer_raw (Item_Net.remove thm) o
7.173 + map_compound_lhs
7.174 + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
7.175 + Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
7.176 + Item_Net.remove (lhs, thm)
7.177 + | _ => I) o
7.178 + map_compound_rhs
7.179 + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
7.180 + Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
7.181 + Item_Net.remove (rhs, thm)
7.182 + | _ => I))
7.183 +
7.184 +fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt
7.185 +fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt
7.186 +
7.187 +(** Conversions **)
7.188 +
7.189 +fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
7.190 +fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
7.191 +
7.192 +fun transfer_rel_conv conv =
7.193 + Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))
7.194 +
7.195 +val Rel_rule = Thm.symmetric @{thm Rel_def}
7.196 +
7.197 +fun dest_funcT cT =
7.198 + (case Thm.dest_ctyp cT of [T, U] => (T, U)
7.199 + | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
7.200 +
7.201 +fun Rel_conv ct =
7.202 + let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
7.203 + val (cU, _) = dest_funcT cT'
7.204 + in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
7.205 +
7.206 +(* Conversion to preprocess a transfer rule *)
7.207 +fun safe_Rel_conv ct =
7.208 + Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
7.209 +
7.210 +fun prep_conv ct = (
7.211 + Conv.implies_conv safe_Rel_conv prep_conv
7.212 + else_conv
7.213 + safe_Rel_conv
7.214 + else_conv
7.215 + Conv.all_conv) ct
7.216 +
7.217 +(** Replacing explicit equalities with is_equality premises **)
7.218 +
7.219 +fun mk_is_equality t =
7.220 + Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
7.221 +
7.222 +val is_equality_lemma =
7.223 + @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
7.224 + by (unfold is_equality_def, rule, drule meta_spec,
7.225 + erule meta_mp, rule refl, simp)}
7.226 +
7.227 +fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
7.228 + let
7.229 + val thy = Thm.theory_of_thm thm
7.230 + val prop = Thm.prop_of thm
7.231 + val (t, mk_prop') = dest prop
7.232 + (* Only consider "op =" at non-base types *)
7.233 + fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
7.234 + (case T of Type (_, []) => false | _ => true)
7.235 + | is_eq _ = false
7.236 + val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
7.237 + val eq_consts = rev (add_eqs t [])
7.238 + val eqTs = map (snd o dest_Const) eq_consts
7.239 + val used = Term.add_free_names prop []
7.240 + val names = map (K "") eqTs |> Name.variant_list used
7.241 + val frees = map Free (names ~~ eqTs)
7.242 + val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
7.243 + val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
7.244 + val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
7.245 + val cprop = Thm.cterm_of thy prop2
7.246 + val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
7.247 + fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
7.248 + in
7.249 + forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
7.250 + end
7.251 + handle TERM _ => thm
7.252 +
7.253 +fun abstract_equalities_transfer ctxt thm =
7.254 + let
7.255 + fun dest prop =
7.256 + let
7.257 + val prems = Logic.strip_imp_prems prop
7.258 + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
7.259 + val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
7.260 + in
7.261 + (rel, fn rel' =>
7.262 + Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
7.263 + end
7.264 + val contracted_eq_thm =
7.265 + Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
7.266 + handle CTERM _ => thm
7.267 + in
7.268 + gen_abstract_equalities ctxt dest contracted_eq_thm
7.269 + end
7.270 +
7.271 +fun abstract_equalities_relator_eq ctxt rel_eq_thm =
7.272 + gen_abstract_equalities ctxt (fn x => (x, I))
7.273 + (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
7.274 +
7.275 +fun abstract_equalities_domain ctxt thm =
7.276 + let
7.277 + fun dest prop =
7.278 + let
7.279 + val prems = Logic.strip_imp_prems prop
7.280 + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
7.281 + val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl)
7.282 + in
7.283 + (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y)))
7.284 + end
7.285 + fun transfer_rel_conv conv =
7.286 + Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))
7.287 + val contracted_eq_thm =
7.288 + Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
7.289 + in
7.290 + gen_abstract_equalities ctxt dest contracted_eq_thm
7.291 + end
7.292 +
7.293 +
7.294 +(** Replacing explicit Domainp predicates with Domainp assumptions **)
7.295 +
7.296 +fun mk_Domainp_assm (T, R) =
7.297 + HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
7.298 +
7.299 +val Domainp_lemma =
7.300 + @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
7.301 + by (rule, drule meta_spec,
7.302 + erule meta_mp, rule refl, simp)}
7.303 +
7.304 +fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
7.305 + | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
7.306 + | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
7.307 + | fold_Domainp _ _ = I
7.308 +
7.309 +fun subst_terms tab t =
7.310 + let
7.311 + val t' = Termtab.lookup tab t
7.312 + in
7.313 + case t' of
7.314 + SOME t' => t'
7.315 + | NONE =>
7.316 + (case t of
7.317 + u $ v => (subst_terms tab u) $ (subst_terms tab v)
7.318 + | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
7.319 + | t => t)
7.320 + end
7.321 +
7.322 +fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
7.323 + let
7.324 + val thy = Thm.theory_of_thm thm
7.325 + val prop = Thm.prop_of thm
7.326 + val (t, mk_prop') = dest prop
7.327 + val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
7.328 + val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
7.329 + val used = Term.add_free_names t []
7.330 + val rels = map (snd o dest_comb) Domainp_tms
7.331 + val rel_names = map (fst o fst o dest_Var) rels
7.332 + val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
7.333 + val frees = map Free (names ~~ Domainp_Ts)
7.334 + val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
7.335 + val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
7.336 + val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
7.337 + val prop2 = Logic.list_rename_params (rev names) prop1
7.338 + val cprop = Thm.cterm_of thy prop2
7.339 + val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
7.340 + fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
7.341 + in
7.342 + forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
7.343 + end
7.344 + handle TERM _ => thm
7.345 +
7.346 +fun abstract_domains_transfer ctxt thm =
7.347 + let
7.348 + fun dest prop =
7.349 + let
7.350 + val prems = Logic.strip_imp_prems prop
7.351 + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
7.352 + val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
7.353 + in
7.354 + (x, fn x' =>
7.355 + Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
7.356 + end
7.357 + in
7.358 + gen_abstract_domains ctxt dest thm
7.359 + end
7.360 +
7.361 +fun abstract_domains_relator_domain ctxt thm =
7.362 + let
7.363 + fun dest prop =
7.364 + let
7.365 + val prems = Logic.strip_imp_prems prop
7.366 + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
7.367 + val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
7.368 + in
7.369 + (y, fn y' =>
7.370 + Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x $ y')))
7.371 + end
7.372 + in
7.373 + gen_abstract_domains ctxt dest thm
7.374 + end
7.375 +
7.376 +fun detect_transfer_rules thm =
7.377 + let
7.378 + fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
7.379 + (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
7.380 + | _ $ _ $ _ => true
7.381 + | _ => false
7.382 + fun safe_transfer_rule_conv ctm =
7.383 + if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
7.384 + in
7.385 + Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
7.386 + end
7.387 +
7.388 +(** Adding transfer domain rules **)
7.389 +
7.390 +fun prep_transfer_domain_thm ctxt thm =
7.391 + (abstract_equalities_domain ctxt o detect_transfer_rules) thm
7.392 +
7.393 +fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o
7.394 + prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
7.395 +
7.396 +fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o
7.397 + prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
7.398 +
7.399 +(** Transfer proof method **)
7.400 +
7.401 +val post_simps =
7.402 + @{thms transfer_forall_eq [symmetric]
7.403 + transfer_implies_eq [symmetric] transfer_bforall_unfold}
7.404 +
7.405 +fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
7.406 + let
7.407 + val keepers = keepers @ get_known_frees ctxt
7.408 + val vs = rev (Term.add_frees t [])
7.409 + val vs' = filter_out (member (op =) keepers) vs
7.410 + in
7.411 + Induct.arbitrary_tac ctxt 0 vs' i
7.412 + end)
7.413 +
7.414 +fun mk_relT (T, U) = T --> U --> HOLogic.boolT
7.415 +
7.416 +fun mk_Rel t =
7.417 + let val T = fastype_of t
7.418 + in Const (@{const_name Transfer.Rel}, T --> T) $ t end
7.419 +
7.420 +fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
7.421 + let
7.422 + val thy = Proof_Context.theory_of ctxt
7.423 + (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
7.424 + fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
7.425 + let
7.426 + val r1 = rel T1 U1
7.427 + val r2 = rel T2 U2
7.428 + val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
7.429 + in
7.430 + Const (@{const_name rel_fun}, rT) $ r1 $ r2
7.431 + end
7.432 + | rel T U =
7.433 + let
7.434 + val (a, _) = dest_TFree (prj (T, U))
7.435 + in
7.436 + Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
7.437 + end
7.438 + fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
7.439 + | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
7.440 + let
7.441 + val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
7.442 + val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
7.443 + val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
7.444 + val thm0 = Thm.assume cprop
7.445 + val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
7.446 + val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
7.447 + val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
7.448 + val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
7.449 + val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
7.450 + val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
7.451 + val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
7.452 + val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
7.453 + val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
7.454 + in
7.455 + (thm2 COMP rule, hyps)
7.456 + end
7.457 + | zip ctxt thms (f $ t) (g $ u) =
7.458 + let
7.459 + val (thm1, hyps1) = zip ctxt thms f g
7.460 + val (thm2, hyps2) = zip ctxt thms t u
7.461 + in
7.462 + (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
7.463 + end
7.464 + | zip _ _ t u =
7.465 + let
7.466 + val T = fastype_of t
7.467 + val U = fastype_of u
7.468 + val prop = mk_Rel (rel T U) $ t $ u
7.469 + val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
7.470 + in
7.471 + (Thm.assume cprop, [cprop])
7.472 + end
7.473 + val r = mk_Rel (rel (fastype_of t) (fastype_of u))
7.474 + val goal = HOLogic.mk_Trueprop (r $ t $ u)
7.475 + val rename = Thm.trivial (cterm_of thy goal)
7.476 + val (thm, hyps) = zip ctxt [] t u
7.477 + in
7.478 + Drule.implies_intr_list hyps (thm RS rename)
7.479 + end
7.480 +
7.481 +(* create a lambda term of the same shape as the given term *)
7.482 +fun skeleton (is_atom : term -> bool) ctxt t =
7.483 + let
7.484 + fun dummy ctxt =
7.485 + let
7.486 + val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
7.487 + in
7.488 + (Free (c, dummyT), ctxt)
7.489 + end
7.490 + fun go (Bound i) ctxt = (Bound i, ctxt)
7.491 + | go (Abs (x, _, t)) ctxt =
7.492 + let
7.493 + val (t', ctxt) = go t ctxt
7.494 + in
7.495 + (Abs (x, dummyT, t'), ctxt)
7.496 + end
7.497 + | go (tu as (t $ u)) ctxt =
7.498 + if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else
7.499 + let
7.500 + val (t', ctxt) = go t ctxt
7.501 + val (u', ctxt) = go u ctxt
7.502 + in
7.503 + (t' $ u', ctxt)
7.504 + end
7.505 + | go _ ctxt = dummy ctxt
7.506 + in
7.507 + go t ctxt |> fst |> Syntax.check_term ctxt |>
7.508 + map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
7.509 + end
7.510 +
7.511 +(** Monotonicity analysis **)
7.512 +
7.513 +(* TODO: Put extensible table in theory data *)
7.514 +val monotab =
7.515 + Symtab.make
7.516 + [(@{const_name transfer_implies}, [~1, 1]),
7.517 + (@{const_name transfer_forall}, [1])(*,
7.518 + (@{const_name implies}, [~1, 1]),
7.519 + (@{const_name All}, [1])*)]
7.520 +
7.521 +(*
7.522 +Function bool_insts determines the set of boolean-relation variables
7.523 +that can be instantiated to implies, rev_implies, or iff.
7.524 +
7.525 +Invariants: bool_insts p (t, u) requires that
7.526 + u :: _ => _ => ... => bool, and
7.527 + t is a skeleton of u
7.528 +*)
7.529 +fun bool_insts p (t, u) =
7.530 + let
7.531 + fun strip2 (t1 $ t2, u1 $ u2, tus) =
7.532 + strip2 (t1, u1, (t2, u2) :: tus)
7.533 + | strip2 x = x
7.534 + fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)
7.535 + fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab
7.536 + | go Ts p (t, u) tab =
7.537 + let
7.538 + val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))
7.539 + val (_, tf, tus) = strip2 (t, u, [])
7.540 + val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE
7.541 + val tab1 =
7.542 + case ps_opt of
7.543 + SOME ps =>
7.544 + let
7.545 + val ps' = map (fn x => p * x) (take (length tus) ps)
7.546 + in
7.547 + fold I (map2 (go Ts) ps' tus) tab
7.548 + end
7.549 + | NONE => tab
7.550 + val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]
7.551 + in
7.552 + Symtab.join (K or3) (tab1, tab2)
7.553 + end
7.554 + val tab = go [] p (t, u) Symtab.empty
7.555 + fun f (a, (true, false, false)) = SOME (a, @{const implies})
7.556 + | f (a, (false, true, false)) = SOME (a, @{const rev_implies})
7.557 + | f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT)
7.558 + | f _ = NONE
7.559 + in
7.560 + map_filter f (Symtab.dest tab)
7.561 + end
7.562 +
7.563 +fun retrieve_terms t net = map fst (Item_Net.retrieve net t)
7.564 +
7.565 +fun matches_list ctxt term =
7.566 + is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
7.567 +
7.568 +fun transfer_rule_of_term ctxt equiv t : thm =
7.569 + let
7.570 + val compound_rhs = get_compound_rhs ctxt
7.571 + fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t
7.572 + val s = skeleton is_rhs ctxt t
7.573 + val frees = map fst (Term.add_frees s [])
7.574 + val tfrees = map fst (Term.add_tfrees s [])
7.575 + fun prep a = "R" ^ Library.unprefix "'" a
7.576 + val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
7.577 + val tab = tfrees ~~ rnames
7.578 + fun prep a = the (AList.lookup (op =) tab a)
7.579 + val thm = transfer_rule_of_terms fst ctxt' tab s t
7.580 + val binsts = bool_insts (if equiv then 0 else 1) (s, t)
7.581 + val cbool = @{ctyp bool}
7.582 + val relT = @{typ "bool => bool => bool"}
7.583 + val idx = Thm.maxidx_of thm + 1
7.584 + val thy = Proof_Context.theory_of ctxt
7.585 + fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
7.586 + fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
7.587 + in
7.588 + thm
7.589 + |> Thm.generalize (tfrees, rnames @ frees) idx
7.590 + |> Thm.instantiate (map tinst binsts, map inst binsts)
7.591 + end
7.592 +
7.593 +fun transfer_rule_of_lhs ctxt t : thm =
7.594 + let
7.595 + val compound_lhs = get_compound_lhs ctxt
7.596 + fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t
7.597 + val s = skeleton is_lhs ctxt t
7.598 + val frees = map fst (Term.add_frees s [])
7.599 + val tfrees = map fst (Term.add_tfrees s [])
7.600 + fun prep a = "R" ^ Library.unprefix "'" a
7.601 + val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
7.602 + val tab = tfrees ~~ rnames
7.603 + fun prep a = the (AList.lookup (op =) tab a)
7.604 + val thm = transfer_rule_of_terms snd ctxt' tab t s
7.605 + val binsts = bool_insts 1 (s, t)
7.606 + val cbool = @{ctyp bool}
7.607 + val relT = @{typ "bool => bool => bool"}
7.608 + val idx = Thm.maxidx_of thm + 1
7.609 + val thy = Proof_Context.theory_of ctxt
7.610 + fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
7.611 + fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
7.612 + in
7.613 + thm
7.614 + |> Thm.generalize (tfrees, rnames @ frees) idx
7.615 + |> Thm.instantiate (map tinst binsts, map inst binsts)
7.616 + end
7.617 +
7.618 +fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules)
7.619 + THEN_ALL_NEW rtac @{thm is_equality_eq}
7.620 +
7.621 +fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
7.622 +
7.623 +fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt))
7.624 + THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
7.625 +
7.626 +fun transfer_tac equiv ctxt i =
7.627 + let
7.628 + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
7.629 + val start_rule =
7.630 + if equiv then @{thm transfer_start} else @{thm transfer_start'}
7.631 + val rules = get_transfer_raw ctxt
7.632 + val eq_rules = get_relator_eq_raw ctxt
7.633 + (* allow unsolved subgoals only for standard transfer method, not for transfer' *)
7.634 + val end_tac = if equiv then K all_tac else K no_tac
7.635 + val err_msg = "Transfer failed to convert goal to an object-logic formula"
7.636 + fun main_tac (t, i) =
7.637 + rtac start_rule i THEN
7.638 + (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
7.639 + THEN_ALL_NEW
7.640 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
7.641 + ORELSE' end_tac)) (i + 1)
7.642 + handle TERM (_, ts) => raise TERM (err_msg, ts)
7.643 + in
7.644 + EVERY
7.645 + [rewrite_goal_tac ctxt pre_simps i THEN
7.646 + SUBGOAL main_tac i,
7.647 + (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
7.648 + rewrite_goal_tac ctxt post_simps i,
7.649 + Goal.norm_hhf_tac ctxt i]
7.650 + end
7.651 +
7.652 +fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
7.653 + let
7.654 + val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
7.655 + val rule1 = transfer_rule_of_term ctxt false rhs
7.656 + val rules = get_transfer_raw ctxt
7.657 + val eq_rules = get_relator_eq_raw ctxt
7.658 + val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
7.659 + in
7.660 + EVERY
7.661 + [CONVERSION prep_conv i,
7.662 + rtac @{thm transfer_prover_start} i,
7.663 + ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
7.664 + THEN_ALL_NEW
7.665 + (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
7.666 + rtac @{thm refl} i]
7.667 + end)
7.668 +
7.669 +(** Transfer attribute **)
7.670 +
7.671 +fun transferred ctxt extra_rules thm =
7.672 + let
7.673 + val start_rule = @{thm transfer_start}
7.674 + val start_rule' = @{thm transfer_start'}
7.675 + val rules = extra_rules @ get_transfer_raw ctxt
7.676 + val eq_rules = get_relator_eq_raw ctxt
7.677 + val err_msg = "Transfer failed to convert goal to an object-logic formula"
7.678 + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
7.679 + val thm1 = Drule.forall_intr_vars thm
7.680 + val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
7.681 + |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
7.682 + val thm2 = thm1
7.683 + |> Thm.certify_instantiate (instT, [])
7.684 + |> Raw_Simplifier.rewrite_rule ctxt pre_simps
7.685 + val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
7.686 + val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
7.687 + val rule = transfer_rule_of_lhs ctxt' t
7.688 + val tac =
7.689 + resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
7.690 + (rtac rule
7.691 + THEN_ALL_NEW
7.692 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
7.693 + THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
7.694 + handle TERM (_, ts) => raise TERM (err_msg, ts)
7.695 + val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
7.696 + val tnames = map (fst o dest_TFree o snd) instT
7.697 + in
7.698 + thm3
7.699 + |> Raw_Simplifier.rewrite_rule ctxt' post_simps
7.700 + |> Simplifier.norm_hhf ctxt'
7.701 + |> Drule.generalize (tnames, [])
7.702 + |> Drule.zero_var_indexes
7.703 + end
7.704 +(*
7.705 + handle THM _ => thm
7.706 +*)
7.707 +
7.708 +fun untransferred ctxt extra_rules thm =
7.709 + let
7.710 + val start_rule = @{thm untransfer_start}
7.711 + val rules = extra_rules @ get_transfer_raw ctxt
7.712 + val eq_rules = get_relator_eq_raw ctxt
7.713 + val err_msg = "Transfer failed to convert goal to an object-logic formula"
7.714 + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
7.715 + val thm1 = Drule.forall_intr_vars thm
7.716 + val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
7.717 + |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
7.718 + val thm2 = thm1
7.719 + |> Thm.certify_instantiate (instT, [])
7.720 + |> Raw_Simplifier.rewrite_rule ctxt pre_simps
7.721 + val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
7.722 + val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
7.723 + val rule = transfer_rule_of_term ctxt' true t
7.724 + val tac =
7.725 + rtac (thm2 RS start_rule) 1 THEN
7.726 + (rtac rule
7.727 + THEN_ALL_NEW
7.728 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
7.729 + THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
7.730 + handle TERM (_, ts) => raise TERM (err_msg, ts)
7.731 + val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
7.732 + val tnames = map (fst o dest_TFree o snd) instT
7.733 + in
7.734 + thm3
7.735 + |> Raw_Simplifier.rewrite_rule ctxt' post_simps
7.736 + |> Simplifier.norm_hhf ctxt'
7.737 + |> Drule.generalize (tnames, [])
7.738 + |> Drule.zero_var_indexes
7.739 + end
7.740 +
7.741 +(** Methods and attributes **)
7.742 +
7.743 +val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
7.744 + error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))
7.745 +
7.746 +val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
7.747 + |-- Scan.repeat free) []
7.748 +
7.749 +fun transfer_method equiv : (Proof.context -> Proof.method) context_parser =
7.750 + fixing >> (fn vs => fn ctxt =>
7.751 + SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
7.752 +
7.753 +val transfer_prover_method : (Proof.context -> Proof.method) context_parser =
7.754 + Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
7.755 +
7.756 +(* Attribute for transfer rules *)
7.757 +
7.758 +fun prep_rule ctxt =
7.759 + abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
7.760 +
7.761 +val transfer_add =
7.762 + Thm.declaration_attribute (fn thm => fn ctxt =>
7.763 + (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
7.764 +
7.765 +val transfer_del =
7.766 + Thm.declaration_attribute (fn thm => fn ctxt =>
7.767 + (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
7.768 +
7.769 +val transfer_attribute =
7.770 + Attrib.add_del transfer_add transfer_del
7.771 +
7.772 +(* Attributes for transfer domain rules *)
7.773 +
7.774 +val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
7.775 +
7.776 +val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
7.777 +
7.778 +val transfer_domain_attribute =
7.779 + Attrib.add_del transfer_domain_add transfer_domain_del
7.780 +
7.781 +(* Attributes for transferred rules *)
7.782 +
7.783 +fun transferred_attribute thms = Thm.rule_attribute
7.784 + (fn context => transferred (Context.proof_of context) thms)
7.785 +
7.786 +fun untransferred_attribute thms = Thm.rule_attribute
7.787 + (fn context => untransferred (Context.proof_of context) thms)
7.788 +
7.789 +val transferred_attribute_parser =
7.790 + Attrib.thms >> transferred_attribute
7.791 +
7.792 +val untransferred_attribute_parser =
7.793 + Attrib.thms >> untransferred_attribute
7.794 +
7.795 +fun morph_pred_data phi {rel_eq_onp} = {rel_eq_onp = Morphism.thm phi rel_eq_onp}
7.796 +
7.797 +fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
7.798 + |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
7.799 +
7.800 +fun update_pred_data type_name qinfo ctxt =
7.801 + Data.map (map_pred_data (Symtab.update (type_name, qinfo))) ctxt
7.802 +
7.803 +(* Theory setup *)
7.804 +
7.805 +val relator_eq_setup =
7.806 + let
7.807 + val name = @{binding relator_eq}
7.808 + fun add_thm thm context = context
7.809 + |> Data.map (map_relator_eq (Item_Net.update thm))
7.810 + |> Data.map (map_relator_eq_raw
7.811 + (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
7.812 + fun del_thm thm context = context
7.813 + |> Data.map (map_relator_eq (Item_Net.remove thm))
7.814 + |> Data.map (map_relator_eq_raw
7.815 + (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
7.816 + val add = Thm.declaration_attribute add_thm
7.817 + val del = Thm.declaration_attribute del_thm
7.818 + val text = "declaration of relator equality rule (used by transfer method)"
7.819 + val content = Item_Net.content o #relator_eq o Data.get
7.820 + in
7.821 + Attrib.setup name (Attrib.add_del add del) text
7.822 + #> Global_Theory.add_thms_dynamic (name, content)
7.823 + end
7.824 +
7.825 +val relator_domain_setup =
7.826 + let
7.827 + val name = @{binding relator_domain}
7.828 + fun add_thm thm context =
7.829 + let
7.830 + val thm = abstract_domains_relator_domain (Context.proof_of context) thm
7.831 + in
7.832 + context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm
7.833 + end
7.834 + fun del_thm thm context =
7.835 + let
7.836 + val thm = abstract_domains_relator_domain (Context.proof_of context) thm
7.837 + in
7.838 + context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm
7.839 + end
7.840 + val add = Thm.declaration_attribute add_thm
7.841 + val del = Thm.declaration_attribute del_thm
7.842 + val text = "declaration of relator domain rule (used by transfer method)"
7.843 + val content = Item_Net.content o #relator_domain o Data.get
7.844 + in
7.845 + Attrib.setup name (Attrib.add_del add del) text
7.846 + #> Global_Theory.add_thms_dynamic (name, content)
7.847 + end
7.848 +
7.849 +val setup =
7.850 + relator_eq_setup
7.851 + #> relator_domain_setup
7.852 + #> Attrib.setup @{binding transfer_rule} transfer_attribute
7.853 + "transfer rule for transfer method"
7.854 + #> Global_Theory.add_thms_dynamic
7.855 + (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
7.856 + #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
7.857 + "transfer domain rule for transfer method"
7.858 + #> Attrib.setup @{binding transferred} transferred_attribute_parser
7.859 + "raw theorem transferred to abstract theorem using transfer rules"
7.860 + #> Attrib.setup @{binding untransferred} untransferred_attribute_parser
7.861 + "abstract theorem transferred to raw theorem using transfer rules"
7.862 + #> Global_Theory.add_thms_dynamic
7.863 + (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
7.864 + #> Method.setup @{binding transfer} (transfer_method true)
7.865 + "generic theorem transfer method"
7.866 + #> Method.setup @{binding transfer'} (transfer_method false)
7.867 + "generic theorem transfer method"
7.868 + #> Method.setup @{binding transfer_prover} transfer_prover_method
7.869 + "for proving transfer rules"
7.870 +
7.871 +end
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Thu Apr 10 17:48:18 2014 +0200
8.3 @@ -0,0 +1,353 @@
8.4 +(* Title: HOL/Tools/Transfer/transfer_bnf.ML
8.5 + Author: Ondrej Kuncar, TU Muenchen
8.6 +
8.7 +Setup for Transfer for types that are BNF.
8.8 +*)
8.9 +
8.10 +signature TRANSFER_BNF =
8.11 +sig
8.12 + val base_name_of_bnf: BNF_Def.bnf -> binding
8.13 + val type_name_of_bnf: BNF_Def.bnf -> string
8.14 + val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
8.15 + val map_local_theory: (local_theory -> local_theory) -> theory -> theory
8.16 + val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a
8.17 +end
8.18 +
8.19 +structure Transfer_BNF : TRANSFER_BNF =
8.20 +struct
8.21 +
8.22 +open BNF_Util
8.23 +open BNF_Def
8.24 +open BNF_FP_Def_Sugar
8.25 +
8.26 +(* util functions *)
8.27 +
8.28 +fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
8.29 +fun mk_Frees_free x Ts ctxt = Variable.variant_frees ctxt [] (mk_names (length Ts) x ~~ Ts) |> map Free
8.30 +
8.31 +fun mk_Domainp P =
8.32 + let
8.33 + val PT = fastype_of P
8.34 + val argT = hd (binder_types PT)
8.35 + in
8.36 + Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P
8.37 + end
8.38 +
8.39 +fun mk_pred pred_def args T =
8.40 + let
8.41 + val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
8.42 + |> head_of |> fst o dest_Const
8.43 + val argsT = map fastype_of args
8.44 + in
8.45 + list_comb (Const (pred_name, argsT ---> (T --> HOLogic.boolT)), args)
8.46 + end
8.47 +
8.48 +fun mk_eq_onp arg =
8.49 + let
8.50 + val argT = domain_type (fastype_of arg)
8.51 + in
8.52 + Const (@{const_name eq_onp}, (argT --> HOLogic.boolT) --> argT --> argT --> HOLogic.boolT)
8.53 + $ arg
8.54 + end
8.55 +
8.56 +fun subst_conv thm =
8.57 + Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) @{context}
8.58 +
8.59 +fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
8.60 +
8.61 +fun is_Type (Type _) = true
8.62 + | is_Type _ = false
8.63 +
8.64 +fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global
8.65 +
8.66 +fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
8.67 +
8.68 +fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
8.69 +
8.70 +fun fp_sugar_only_type_ctr f fp_sugar =
8.71 + if is_Type (T_of_bnf (bnf_of_fp_sugar fp_sugar)) then f fp_sugar else I
8.72 +
8.73 +(* relation constraints - bi_total & co. *)
8.74 +
8.75 +fun mk_relation_constraint name arg =
8.76 + (Const (name, fastype_of arg --> HOLogic.boolT)) $ arg
8.77 +
8.78 +fun side_constraint_tac bnf constr_defs ctxt i =
8.79 + let
8.80 + val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf,
8.81 + rel_OO_of_bnf bnf]
8.82 + in
8.83 + (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf)
8.84 + THEN_ALL_NEW atac) i
8.85 + end
8.86 +
8.87 +fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
8.88 + (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
8.89 + CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i
8.90 +
8.91 +fun generate_relation_constraint_goal ctxt bnf constraint_def =
8.92 + let
8.93 + val constr_name = constraint_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
8.94 + |> head_of |> fst o dest_Const
8.95 + val live = live_of_bnf bnf
8.96 + val (((As, Bs), Ds), ctxt) = ctxt
8.97 + |> mk_TFrees live
8.98 + ||>> mk_TFrees live
8.99 + ||>> mk_TFrees (dead_of_bnf bnf)
8.100 +
8.101 + val relator = mk_rel_of_bnf Ds As Bs bnf
8.102 + val relsT = map2 mk_pred2T As Bs
8.103 + val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
8.104 + val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args)))
8.105 + val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args
8.106 + val goal = Logic.list_implies (assms, concl)
8.107 + in
8.108 + (goal, ctxt)
8.109 + end
8.110 +
8.111 +fun prove_relation_side_constraint ctxt bnf constraint_def =
8.112 + let
8.113 + val old_ctxt = ctxt
8.114 + val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
8.115 + val thm = Goal.prove ctxt [] [] goal
8.116 + (fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1)
8.117 + in
8.118 + Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
8.119 + end
8.120 +
8.121 +fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints =
8.122 + let
8.123 + val old_ctxt = ctxt
8.124 + val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
8.125 + val thm = Goal.prove ctxt [] [] goal
8.126 + (fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1)
8.127 + in
8.128 + Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
8.129 + end
8.130 +
8.131 +val defs = [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}),
8.132 + ("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})]
8.133 +
8.134 +fun prove_relation_constraints bnf lthy =
8.135 + let
8.136 + val transfer_attr = @{attributes [transfer_rule]}
8.137 + val Tname = base_name_of_bnf bnf
8.138 + fun qualify suffix = Binding.qualified true suffix Tname
8.139 +
8.140 + val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs
8.141 + val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
8.142 + [snd (nth defs 0), snd (nth defs 1)]
8.143 + val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
8.144 + [snd (nth defs 2), snd (nth defs 3)]
8.145 + val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs
8.146 + val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs
8.147 + in
8.148 + notes
8.149 + end
8.150 +
8.151 +(* relator_eq *)
8.152 +
8.153 +fun relator_eq bnf =
8.154 + [((Binding.empty, []), [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
8.155 +
8.156 +(* predicator definition and Domainp and eq_onp theorem *)
8.157 +
8.158 +fun define_pred bnf lthy =
8.159 + let
8.160 + fun mk_pred_name c = Binding.prefix_name "pred_" c
8.161 + val live = live_of_bnf bnf
8.162 + val Tname = base_name_of_bnf bnf
8.163 + val ((As, Ds), lthy) = lthy
8.164 + |> mk_TFrees live
8.165 + ||>> mk_TFrees (dead_of_bnf bnf)
8.166 + val T = mk_T_of_bnf Ds As bnf
8.167 + val sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf
8.168 + val argTs = map mk_pred1T As
8.169 + val args = mk_Frees_free "P" argTs lthy
8.170 + val conjs = map (fn (set, arg) => mk_Ball (set $ Bound 0) arg) (sets ~~ args)
8.171 + val rhs = Abs ("x", T, foldr1 HOLogic.mk_conj conjs)
8.172 + val pred_name = mk_pred_name Tname
8.173 + val headT = argTs ---> (T --> HOLogic.boolT)
8.174 + val head = Free (Binding.name_of pred_name, headT)
8.175 + val lhs = list_comb (head, args)
8.176 + val def = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
8.177 + val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)),
8.178 + ((Binding.empty, []), def)) lthy
8.179 + in
8.180 + (pred_def, lthy)
8.181 + end
8.182 +
8.183 +fun Domainp_tac bnf pred_def ctxt i =
8.184 + let
8.185 + val n = live_of_bnf bnf
8.186 + val set_map's = set_map_of_bnf bnf
8.187 + in
8.188 + EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
8.189 + in_rel_of_bnf bnf, pred_def]), rtac iffI,
8.190 + REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
8.191 + CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
8.192 + etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
8.193 + hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
8.194 + etac @{thm DomainPI}]) set_map's,
8.195 + REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
8.196 + rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
8.197 + map_id_of_bnf bnf]),
8.198 + REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
8.199 + rtac @{thm fst_conv}]), rtac CollectI,
8.200 + CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
8.201 + REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
8.202 + dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's
8.203 + ] i
8.204 + end
8.205 +
8.206 +fun prove_Domainp_rel ctxt bnf pred_def =
8.207 + let
8.208 + val live = live_of_bnf bnf
8.209 + val old_ctxt = ctxt
8.210 + val (((As, Bs), Ds), ctxt) = ctxt
8.211 + |> mk_TFrees live
8.212 + ||>> mk_TFrees live
8.213 + ||>> mk_TFrees (dead_of_bnf bnf)
8.214 +
8.215 + val relator = mk_rel_of_bnf Ds As Bs bnf
8.216 + val relsT = map2 mk_pred2T As Bs
8.217 + val T = mk_T_of_bnf Ds As bnf
8.218 + val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
8.219 + val lhs = mk_Domainp (list_comb (relator, args))
8.220 + val rhs = mk_pred pred_def (map mk_Domainp args) T
8.221 + val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
8.222 + val thm = Goal.prove ctxt [] [] goal
8.223 + (fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
8.224 + in
8.225 + Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
8.226 + end
8.227 +
8.228 +fun pred_eq_onp_tac bnf pred_def ctxt i =
8.229 + (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp},
8.230 + @{thm Ball_Collect}, pred_def]) THEN' CONVERSION (subst_conv (map_id0_of_bnf bnf RS sym))
8.231 + THEN' rtac (rel_Grp_of_bnf bnf)) i
8.232 +
8.233 +fun prove_rel_eq_onp ctxt bnf pred_def =
8.234 + let
8.235 + val live = live_of_bnf bnf
8.236 + val old_ctxt = ctxt
8.237 + val ((As, Ds), ctxt) = ctxt
8.238 + |> mk_TFrees live
8.239 + ||>> mk_TFrees (dead_of_bnf bnf)
8.240 + val T = mk_T_of_bnf Ds As bnf
8.241 + val argTs = map mk_pred1T As
8.242 + val (args, ctxt) = mk_Frees "P" argTs ctxt
8.243 + val relator = mk_rel_of_bnf Ds As As bnf
8.244 + val lhs = list_comb (relator, map mk_eq_onp args)
8.245 + val rhs = mk_eq_onp (mk_pred pred_def args T)
8.246 + val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
8.247 + val thm = Goal.prove ctxt [] [] goal
8.248 + (fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1)
8.249 + in
8.250 + Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
8.251 + end
8.252 +
8.253 +fun predicator bnf lthy =
8.254 + let
8.255 + val (pred_def, lthy) = define_pred bnf lthy
8.256 + val pred_def = Morphism.thm (Local_Theory.target_morphism lthy) pred_def
8.257 + val Domainp_rel = prove_Domainp_rel lthy bnf pred_def
8.258 + val rel_eq_onp = prove_rel_eq_onp lthy bnf pred_def
8.259 + fun qualify defname suffix = Binding.qualified true suffix defname
8.260 + val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
8.261 + val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
8.262 + val pred_data = {rel_eq_onp = rel_eq_onp}
8.263 + val type_name = type_name_of_bnf bnf
8.264 + val relator_domain_attr = @{attributes [relator_domain]}
8.265 + val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
8.266 + ((rel_eq_onp_thm_name, []), [([rel_eq_onp], [])])]
8.267 + val lthy = Local_Theory.declaration {syntax = false, pervasive = true}
8.268 + (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) lthy
8.269 + in
8.270 + (notes, lthy)
8.271 + end
8.272 +
8.273 +(* BNF interpretation *)
8.274 +
8.275 +fun transfer_bnf_interpretation bnf lthy =
8.276 + let
8.277 + val constr_notes = if dead_of_bnf bnf > 0 then []
8.278 + else prove_relation_constraints bnf lthy
8.279 + val relator_eq_notes = if dead_of_bnf bnf > 0 then []
8.280 + else relator_eq bnf
8.281 + val (pred_notes, lthy) = predicator bnf lthy
8.282 + in
8.283 + snd (Local_Theory.notes (constr_notes @ relator_eq_notes @ pred_notes) lthy)
8.284 + end
8.285 +
8.286 +val _ = Context.>> (Context.map_theory (bnf_interpretation
8.287 + (bnf_only_type_ctr (fn bnf => map_local_theory (transfer_bnf_interpretation bnf)))))
8.288 +
8.289 +(* simplification rules for the predicator *)
8.290 +
8.291 +fun lookup_defined_pred_data lthy name =
8.292 + case (Transfer.lookup_pred_data lthy name) of
8.293 + SOME data => data
8.294 + | NONE => (error "lookup_pred_data: something went utterly wrong")
8.295 +
8.296 +fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
8.297 + let
8.298 + val involved_types = distinct op= (
8.299 + map type_name_of_bnf (#nested_bnfs fp_sugar)
8.300 + @ map type_name_of_bnf (#nesting_bnfs fp_sugar)
8.301 + @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
8.302 + val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
8.303 + val live = live_of_bnf (bnf_of_fp_sugar fp_sugar)
8.304 + val old_lthy = lthy
8.305 + val (As, lthy) = mk_TFrees live lthy
8.306 + val predTs = map mk_pred1T As
8.307 + val (preds, lthy) = mk_Frees "P" predTs lthy
8.308 + val args = map mk_eq_onp preds
8.309 + val cTs = map (SOME o certifyT lthy) (maps (replicate 2) As)
8.310 + val cts = map (SOME o certify lthy) args
8.311 + fun get_rhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
8.312 + fun is_eqn thm = can get_rhs thm
8.313 + fun rel2pred_massage thm =
8.314 + let
8.315 + fun pred_eq_onp_conj 0 = error "not defined"
8.316 + | pred_eq_onp_conj 1 = @{thm eq_onp_same_args}
8.317 + | pred_eq_onp_conj n =
8.318 + let
8.319 + val conj_cong = @{thm arg_cong2[of _ _ _ _ "op \<and>"]}
8.320 + val start = @{thm eq_onp_same_args} RS conj_cong
8.321 + in
8.322 + @{thm eq_onp_same_args} RS (funpow (n - 2) (fn thm => start RS thm) start)
8.323 + end
8.324 + val n = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj |> length else 0
8.325 + in
8.326 + thm
8.327 + |> Drule.instantiate' cTs cts
8.328 + |> Local_Defs.unfold lthy eq_onps
8.329 + |> (fn thm => if n > 0 then @{thm box_equals}
8.330 + OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj n]
8.331 + else thm RS (@{thm eq_onp_same_args} RS iffD1))
8.332 + end
8.333 + val rel_injects = #rel_injects fp_sugar
8.334 + in
8.335 + rel_injects
8.336 + |> map rel2pred_massage
8.337 + |> Variable.export lthy old_lthy
8.338 + |> map Drule.zero_var_indexes
8.339 + end
8.340 +
8.341 +(* fp_sugar interpretation *)
8.342 +
8.343 +fun transfer_fp_sugar_interpretation fp_sugar lthy =
8.344 + let
8.345 + val pred_injects = prove_pred_inject lthy fp_sugar
8.346 + fun qualify defname suffix = Binding.qualified true suffix defname
8.347 + val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject"
8.348 + val simp_attrs = @{attributes [simp]}
8.349 + in
8.350 + snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
8.351 + end
8.352 +
8.353 +val _ = Context.>> (Context.map_theory (fp_sugar_interpretation
8.354 + (fp_sugar_only_type_ctr (fn fp_sugar => map_local_theory (transfer_fp_sugar_interpretation fp_sugar)))))
8.355 +
8.356 +end
9.1 --- a/src/HOL/Tools/transfer.ML Thu Apr 10 17:48:17 2014 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,840 +0,0 @@
9.4 -(* Title: HOL/Tools/transfer.ML
9.5 - Author: Brian Huffman, TU Muenchen
9.6 - Author: Ondrej Kuncar, TU Muenchen
9.7 -
9.8 -Generic theorem transfer method.
9.9 -*)
9.10 -
9.11 -signature TRANSFER =
9.12 -sig
9.13 - val bottom_rewr_conv: thm list -> conv
9.14 - val top_rewr_conv: thm list -> conv
9.15 -
9.16 - val prep_conv: conv
9.17 - val get_transfer_raw: Proof.context -> thm list
9.18 - val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
9.19 - val get_relator_eq: Proof.context -> thm list
9.20 - val get_sym_relator_eq: Proof.context -> thm list
9.21 - val get_relator_eq_raw: Proof.context -> thm list
9.22 - val get_relator_domain: Proof.context -> thm list
9.23 - val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T
9.24 - val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
9.25 - val transfer_add: attribute
9.26 - val transfer_del: attribute
9.27 - val transfer_raw_add: thm -> Context.generic -> Context.generic
9.28 - val transfer_raw_del: thm -> Context.generic -> Context.generic
9.29 - val transferred_attribute: thm list -> attribute
9.30 - val untransferred_attribute: thm list -> attribute
9.31 - val prep_transfer_domain_thm: Proof.context -> thm -> thm
9.32 - val transfer_domain_add: attribute
9.33 - val transfer_domain_del: attribute
9.34 - val transfer_rule_of_term: Proof.context -> bool -> term -> thm
9.35 - val transfer_rule_of_lhs: Proof.context -> term -> thm
9.36 - val eq_tac: Proof.context -> int -> tactic
9.37 - val transfer_step_tac: Proof.context -> int -> tactic
9.38 - val transfer_tac: bool -> Proof.context -> int -> tactic
9.39 - val transfer_prover_tac: Proof.context -> int -> tactic
9.40 - val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
9.41 - val setup: theory -> theory
9.42 -end
9.43 -
9.44 -structure Transfer : TRANSFER =
9.45 -struct
9.46 -
9.47 -(** Theory Data **)
9.48 -
9.49 -val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
9.50 -val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
9.51 - o HOLogic.dest_Trueprop o Thm.concl_of);
9.52 -
9.53 -structure Data = Generic_Data
9.54 -(
9.55 - type T =
9.56 - { transfer_raw : thm Item_Net.T,
9.57 - known_frees : (string * typ) list,
9.58 - compound_lhs : (term * thm) Item_Net.T,
9.59 - compound_rhs : (term * thm) Item_Net.T,
9.60 - relator_eq : thm Item_Net.T,
9.61 - relator_eq_raw : thm Item_Net.T,
9.62 - relator_domain : thm Item_Net.T }
9.63 - val empty =
9.64 - { transfer_raw = Thm.intro_rules,
9.65 - known_frees = [],
9.66 - compound_lhs = compound_xhs_empty_net,
9.67 - compound_rhs = compound_xhs_empty_net,
9.68 - relator_eq = rewr_rules,
9.69 - relator_eq_raw = Thm.full_rules,
9.70 - relator_domain = Thm.full_rules }
9.71 - val extend = I
9.72 - fun merge
9.73 - ( { transfer_raw = t1, known_frees = k1,
9.74 - compound_lhs = l1,
9.75 - compound_rhs = c1, relator_eq = r1,
9.76 - relator_eq_raw = rw1, relator_domain = rd1 },
9.77 - { transfer_raw = t2, known_frees = k2,
9.78 - compound_lhs = l2,
9.79 - compound_rhs = c2, relator_eq = r2,
9.80 - relator_eq_raw = rw2, relator_domain = rd2 } ) =
9.81 - { transfer_raw = Item_Net.merge (t1, t2),
9.82 - known_frees = Library.merge (op =) (k1, k2),
9.83 - compound_lhs = Item_Net.merge (l1, l2),
9.84 - compound_rhs = Item_Net.merge (c1, c2),
9.85 - relator_eq = Item_Net.merge (r1, r2),
9.86 - relator_eq_raw = Item_Net.merge (rw1, rw2),
9.87 - relator_domain = Item_Net.merge (rd1, rd2) }
9.88 -)
9.89 -
9.90 -fun get_transfer_raw ctxt = ctxt
9.91 - |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
9.92 -
9.93 -fun get_known_frees ctxt = ctxt
9.94 - |> (#known_frees o Data.get o Context.Proof)
9.95 -
9.96 -fun get_compound_lhs ctxt = ctxt
9.97 - |> (#compound_lhs o Data.get o Context.Proof)
9.98 -
9.99 -fun get_compound_rhs ctxt = ctxt
9.100 - |> (#compound_rhs o Data.get o Context.Proof)
9.101 -
9.102 -fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
9.103 -
9.104 -fun get_relator_eq ctxt = ctxt
9.105 - |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
9.106 - |> map safe_mk_meta_eq
9.107 -
9.108 -fun get_sym_relator_eq ctxt = ctxt
9.109 - |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
9.110 - |> map (Thm.symmetric o safe_mk_meta_eq)
9.111 -
9.112 -fun get_relator_eq_raw ctxt = ctxt
9.113 - |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
9.114 -
9.115 -fun get_relator_domain ctxt = ctxt
9.116 - |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
9.117 -
9.118 -fun map_data f1 f2 f3 f4 f5 f6 f7
9.119 - { transfer_raw, known_frees, compound_lhs, compound_rhs,
9.120 - relator_eq, relator_eq_raw, relator_domain } =
9.121 - { transfer_raw = f1 transfer_raw,
9.122 - known_frees = f2 known_frees,
9.123 - compound_lhs = f3 compound_lhs,
9.124 - compound_rhs = f4 compound_rhs,
9.125 - relator_eq = f5 relator_eq,
9.126 - relator_eq_raw = f6 relator_eq_raw,
9.127 - relator_domain = f7 relator_domain }
9.128 -
9.129 -fun map_transfer_raw f = map_data f I I I I I I
9.130 -fun map_known_frees f = map_data I f I I I I I
9.131 -fun map_compound_lhs f = map_data I I f I I I I
9.132 -fun map_compound_rhs f = map_data I I I f I I I
9.133 -fun map_relator_eq f = map_data I I I I f I I
9.134 -fun map_relator_eq_raw f = map_data I I I I I f I
9.135 -fun map_relator_domain f = map_data I I I I I I f
9.136 -
9.137 -fun add_transfer_thm thm = Data.map
9.138 - (map_transfer_raw (Item_Net.update thm) o
9.139 - map_compound_lhs
9.140 - (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
9.141 - Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
9.142 - Item_Net.update (lhs, thm)
9.143 - | _ => I) o
9.144 - map_compound_rhs
9.145 - (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
9.146 - Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
9.147 - Item_Net.update (rhs, thm)
9.148 - | _ => I) o
9.149 - map_known_frees (Term.add_frees (Thm.concl_of thm)))
9.150 -
9.151 -fun del_transfer_thm thm = Data.map
9.152 - (map_transfer_raw (Item_Net.remove thm) o
9.153 - map_compound_lhs
9.154 - (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
9.155 - Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
9.156 - Item_Net.remove (lhs, thm)
9.157 - | _ => I) o
9.158 - map_compound_rhs
9.159 - (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
9.160 - Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
9.161 - Item_Net.remove (rhs, thm)
9.162 - | _ => I))
9.163 -
9.164 -fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt
9.165 -fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt
9.166 -
9.167 -(** Conversions **)
9.168 -
9.169 -fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
9.170 -fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
9.171 -
9.172 -fun transfer_rel_conv conv =
9.173 - Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))
9.174 -
9.175 -val Rel_rule = Thm.symmetric @{thm Rel_def}
9.176 -
9.177 -fun dest_funcT cT =
9.178 - (case Thm.dest_ctyp cT of [T, U] => (T, U)
9.179 - | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
9.180 -
9.181 -fun Rel_conv ct =
9.182 - let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
9.183 - val (cU, _) = dest_funcT cT'
9.184 - in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
9.185 -
9.186 -(* Conversion to preprocess a transfer rule *)
9.187 -fun safe_Rel_conv ct =
9.188 - Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
9.189 -
9.190 -fun prep_conv ct = (
9.191 - Conv.implies_conv safe_Rel_conv prep_conv
9.192 - else_conv
9.193 - safe_Rel_conv
9.194 - else_conv
9.195 - Conv.all_conv) ct
9.196 -
9.197 -(** Replacing explicit equalities with is_equality premises **)
9.198 -
9.199 -fun mk_is_equality t =
9.200 - Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
9.201 -
9.202 -val is_equality_lemma =
9.203 - @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
9.204 - by (unfold is_equality_def, rule, drule meta_spec,
9.205 - erule meta_mp, rule refl, simp)}
9.206 -
9.207 -fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
9.208 - let
9.209 - val thy = Thm.theory_of_thm thm
9.210 - val prop = Thm.prop_of thm
9.211 - val (t, mk_prop') = dest prop
9.212 - (* Only consider "op =" at non-base types *)
9.213 - fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
9.214 - (case T of Type (_, []) => false | _ => true)
9.215 - | is_eq _ = false
9.216 - val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
9.217 - val eq_consts = rev (add_eqs t [])
9.218 - val eqTs = map (snd o dest_Const) eq_consts
9.219 - val used = Term.add_free_names prop []
9.220 - val names = map (K "") eqTs |> Name.variant_list used
9.221 - val frees = map Free (names ~~ eqTs)
9.222 - val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
9.223 - val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
9.224 - val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
9.225 - val cprop = Thm.cterm_of thy prop2
9.226 - val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
9.227 - fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
9.228 - in
9.229 - forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
9.230 - end
9.231 - handle TERM _ => thm
9.232 -
9.233 -fun abstract_equalities_transfer ctxt thm =
9.234 - let
9.235 - fun dest prop =
9.236 - let
9.237 - val prems = Logic.strip_imp_prems prop
9.238 - val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
9.239 - val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
9.240 - in
9.241 - (rel, fn rel' =>
9.242 - Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
9.243 - end
9.244 - val contracted_eq_thm =
9.245 - Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
9.246 - handle CTERM _ => thm
9.247 - in
9.248 - gen_abstract_equalities ctxt dest contracted_eq_thm
9.249 - end
9.250 -
9.251 -fun abstract_equalities_relator_eq ctxt rel_eq_thm =
9.252 - gen_abstract_equalities ctxt (fn x => (x, I))
9.253 - (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
9.254 -
9.255 -fun abstract_equalities_domain ctxt thm =
9.256 - let
9.257 - fun dest prop =
9.258 - let
9.259 - val prems = Logic.strip_imp_prems prop
9.260 - val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
9.261 - val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl)
9.262 - in
9.263 - (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y)))
9.264 - end
9.265 - fun transfer_rel_conv conv =
9.266 - Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))
9.267 - val contracted_eq_thm =
9.268 - Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
9.269 - in
9.270 - gen_abstract_equalities ctxt dest contracted_eq_thm
9.271 - end
9.272 -
9.273 -
9.274 -(** Replacing explicit Domainp predicates with Domainp assumptions **)
9.275 -
9.276 -fun mk_Domainp_assm (T, R) =
9.277 - HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
9.278 -
9.279 -val Domainp_lemma =
9.280 - @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
9.281 - by (rule, drule meta_spec,
9.282 - erule meta_mp, rule refl, simp)}
9.283 -
9.284 -fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
9.285 - | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
9.286 - | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
9.287 - | fold_Domainp _ _ = I
9.288 -
9.289 -fun subst_terms tab t =
9.290 - let
9.291 - val t' = Termtab.lookup tab t
9.292 - in
9.293 - case t' of
9.294 - SOME t' => t'
9.295 - | NONE =>
9.296 - (case t of
9.297 - u $ v => (subst_terms tab u) $ (subst_terms tab v)
9.298 - | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
9.299 - | t => t)
9.300 - end
9.301 -
9.302 -fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
9.303 - let
9.304 - val thy = Thm.theory_of_thm thm
9.305 - val prop = Thm.prop_of thm
9.306 - val (t, mk_prop') = dest prop
9.307 - val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
9.308 - val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
9.309 - val used = Term.add_free_names t []
9.310 - val rels = map (snd o dest_comb) Domainp_tms
9.311 - val rel_names = map (fst o fst o dest_Var) rels
9.312 - val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
9.313 - val frees = map Free (names ~~ Domainp_Ts)
9.314 - val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
9.315 - val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
9.316 - val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
9.317 - val prop2 = Logic.list_rename_params (rev names) prop1
9.318 - val cprop = Thm.cterm_of thy prop2
9.319 - val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
9.320 - fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
9.321 - in
9.322 - forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
9.323 - end
9.324 - handle TERM _ => thm
9.325 -
9.326 -fun abstract_domains_transfer ctxt thm =
9.327 - let
9.328 - fun dest prop =
9.329 - let
9.330 - val prems = Logic.strip_imp_prems prop
9.331 - val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
9.332 - val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
9.333 - in
9.334 - (x, fn x' =>
9.335 - Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
9.336 - end
9.337 - in
9.338 - gen_abstract_domains ctxt dest thm
9.339 - end
9.340 -
9.341 -fun abstract_domains_relator_domain ctxt thm =
9.342 - let
9.343 - fun dest prop =
9.344 - let
9.345 - val prems = Logic.strip_imp_prems prop
9.346 - val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
9.347 - val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
9.348 - in
9.349 - (y, fn y' =>
9.350 - Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x $ y')))
9.351 - end
9.352 - in
9.353 - gen_abstract_domains ctxt dest thm
9.354 - end
9.355 -
9.356 -fun detect_transfer_rules thm =
9.357 - let
9.358 - fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
9.359 - (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
9.360 - | _ $ _ $ _ => true
9.361 - | _ => false
9.362 - fun safe_transfer_rule_conv ctm =
9.363 - if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
9.364 - in
9.365 - Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
9.366 - end
9.367 -
9.368 -(** Adding transfer domain rules **)
9.369 -
9.370 -fun prep_transfer_domain_thm ctxt thm =
9.371 - (abstract_equalities_domain ctxt o detect_transfer_rules) thm
9.372 -
9.373 -fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o
9.374 - prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
9.375 -
9.376 -fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o
9.377 - prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
9.378 -
9.379 -(** Transfer proof method **)
9.380 -
9.381 -val post_simps =
9.382 - @{thms transfer_forall_eq [symmetric]
9.383 - transfer_implies_eq [symmetric] transfer_bforall_unfold}
9.384 -
9.385 -fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
9.386 - let
9.387 - val keepers = keepers @ get_known_frees ctxt
9.388 - val vs = rev (Term.add_frees t [])
9.389 - val vs' = filter_out (member (op =) keepers) vs
9.390 - in
9.391 - Induct.arbitrary_tac ctxt 0 vs' i
9.392 - end)
9.393 -
9.394 -fun mk_relT (T, U) = T --> U --> HOLogic.boolT
9.395 -
9.396 -fun mk_Rel t =
9.397 - let val T = fastype_of t
9.398 - in Const (@{const_name Transfer.Rel}, T --> T) $ t end
9.399 -
9.400 -fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
9.401 - let
9.402 - val thy = Proof_Context.theory_of ctxt
9.403 - (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
9.404 - fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
9.405 - let
9.406 - val r1 = rel T1 U1
9.407 - val r2 = rel T2 U2
9.408 - val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
9.409 - in
9.410 - Const (@{const_name rel_fun}, rT) $ r1 $ r2
9.411 - end
9.412 - | rel T U =
9.413 - let
9.414 - val (a, _) = dest_TFree (prj (T, U))
9.415 - in
9.416 - Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
9.417 - end
9.418 - fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
9.419 - | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
9.420 - let
9.421 - val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
9.422 - val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
9.423 - val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
9.424 - val thm0 = Thm.assume cprop
9.425 - val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
9.426 - val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
9.427 - val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
9.428 - val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
9.429 - val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
9.430 - val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
9.431 - val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
9.432 - val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
9.433 - val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
9.434 - in
9.435 - (thm2 COMP rule, hyps)
9.436 - end
9.437 - | zip ctxt thms (f $ t) (g $ u) =
9.438 - let
9.439 - val (thm1, hyps1) = zip ctxt thms f g
9.440 - val (thm2, hyps2) = zip ctxt thms t u
9.441 - in
9.442 - (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
9.443 - end
9.444 - | zip _ _ t u =
9.445 - let
9.446 - val T = fastype_of t
9.447 - val U = fastype_of u
9.448 - val prop = mk_Rel (rel T U) $ t $ u
9.449 - val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
9.450 - in
9.451 - (Thm.assume cprop, [cprop])
9.452 - end
9.453 - val r = mk_Rel (rel (fastype_of t) (fastype_of u))
9.454 - val goal = HOLogic.mk_Trueprop (r $ t $ u)
9.455 - val rename = Thm.trivial (cterm_of thy goal)
9.456 - val (thm, hyps) = zip ctxt [] t u
9.457 - in
9.458 - Drule.implies_intr_list hyps (thm RS rename)
9.459 - end
9.460 -
9.461 -(* create a lambda term of the same shape as the given term *)
9.462 -fun skeleton (is_atom : term -> bool) ctxt t =
9.463 - let
9.464 - fun dummy ctxt =
9.465 - let
9.466 - val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
9.467 - in
9.468 - (Free (c, dummyT), ctxt)
9.469 - end
9.470 - fun go (Bound i) ctxt = (Bound i, ctxt)
9.471 - | go (Abs (x, _, t)) ctxt =
9.472 - let
9.473 - val (t', ctxt) = go t ctxt
9.474 - in
9.475 - (Abs (x, dummyT, t'), ctxt)
9.476 - end
9.477 - | go (tu as (t $ u)) ctxt =
9.478 - if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else
9.479 - let
9.480 - val (t', ctxt) = go t ctxt
9.481 - val (u', ctxt) = go u ctxt
9.482 - in
9.483 - (t' $ u', ctxt)
9.484 - end
9.485 - | go _ ctxt = dummy ctxt
9.486 - in
9.487 - go t ctxt |> fst |> Syntax.check_term ctxt |>
9.488 - map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
9.489 - end
9.490 -
9.491 -(** Monotonicity analysis **)
9.492 -
9.493 -(* TODO: Put extensible table in theory data *)
9.494 -val monotab =
9.495 - Symtab.make
9.496 - [(@{const_name transfer_implies}, [~1, 1]),
9.497 - (@{const_name transfer_forall}, [1])(*,
9.498 - (@{const_name implies}, [~1, 1]),
9.499 - (@{const_name All}, [1])*)]
9.500 -
9.501 -(*
9.502 -Function bool_insts determines the set of boolean-relation variables
9.503 -that can be instantiated to implies, rev_implies, or iff.
9.504 -
9.505 -Invariants: bool_insts p (t, u) requires that
9.506 - u :: _ => _ => ... => bool, and
9.507 - t is a skeleton of u
9.508 -*)
9.509 -fun bool_insts p (t, u) =
9.510 - let
9.511 - fun strip2 (t1 $ t2, u1 $ u2, tus) =
9.512 - strip2 (t1, u1, (t2, u2) :: tus)
9.513 - | strip2 x = x
9.514 - fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)
9.515 - fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab
9.516 - | go Ts p (t, u) tab =
9.517 - let
9.518 - val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))
9.519 - val (_, tf, tus) = strip2 (t, u, [])
9.520 - val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE
9.521 - val tab1 =
9.522 - case ps_opt of
9.523 - SOME ps =>
9.524 - let
9.525 - val ps' = map (fn x => p * x) (take (length tus) ps)
9.526 - in
9.527 - fold I (map2 (go Ts) ps' tus) tab
9.528 - end
9.529 - | NONE => tab
9.530 - val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]
9.531 - in
9.532 - Symtab.join (K or3) (tab1, tab2)
9.533 - end
9.534 - val tab = go [] p (t, u) Symtab.empty
9.535 - fun f (a, (true, false, false)) = SOME (a, @{const implies})
9.536 - | f (a, (false, true, false)) = SOME (a, @{const rev_implies})
9.537 - | f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT)
9.538 - | f _ = NONE
9.539 - in
9.540 - map_filter f (Symtab.dest tab)
9.541 - end
9.542 -
9.543 -fun retrieve_terms t net = map fst (Item_Net.retrieve net t)
9.544 -
9.545 -fun matches_list ctxt term =
9.546 - is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
9.547 -
9.548 -fun transfer_rule_of_term ctxt equiv t : thm =
9.549 - let
9.550 - val compound_rhs = get_compound_rhs ctxt
9.551 - fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t
9.552 - val s = skeleton is_rhs ctxt t
9.553 - val frees = map fst (Term.add_frees s [])
9.554 - val tfrees = map fst (Term.add_tfrees s [])
9.555 - fun prep a = "R" ^ Library.unprefix "'" a
9.556 - val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
9.557 - val tab = tfrees ~~ rnames
9.558 - fun prep a = the (AList.lookup (op =) tab a)
9.559 - val thm = transfer_rule_of_terms fst ctxt' tab s t
9.560 - val binsts = bool_insts (if equiv then 0 else 1) (s, t)
9.561 - val cbool = @{ctyp bool}
9.562 - val relT = @{typ "bool => bool => bool"}
9.563 - val idx = Thm.maxidx_of thm + 1
9.564 - val thy = Proof_Context.theory_of ctxt
9.565 - fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
9.566 - fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
9.567 - in
9.568 - thm
9.569 - |> Thm.generalize (tfrees, rnames @ frees) idx
9.570 - |> Thm.instantiate (map tinst binsts, map inst binsts)
9.571 - end
9.572 -
9.573 -fun transfer_rule_of_lhs ctxt t : thm =
9.574 - let
9.575 - val compound_lhs = get_compound_lhs ctxt
9.576 - fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t
9.577 - val s = skeleton is_lhs ctxt t
9.578 - val frees = map fst (Term.add_frees s [])
9.579 - val tfrees = map fst (Term.add_tfrees s [])
9.580 - fun prep a = "R" ^ Library.unprefix "'" a
9.581 - val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
9.582 - val tab = tfrees ~~ rnames
9.583 - fun prep a = the (AList.lookup (op =) tab a)
9.584 - val thm = transfer_rule_of_terms snd ctxt' tab t s
9.585 - val binsts = bool_insts 1 (s, t)
9.586 - val cbool = @{ctyp bool}
9.587 - val relT = @{typ "bool => bool => bool"}
9.588 - val idx = Thm.maxidx_of thm + 1
9.589 - val thy = Proof_Context.theory_of ctxt
9.590 - fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
9.591 - fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
9.592 - in
9.593 - thm
9.594 - |> Thm.generalize (tfrees, rnames @ frees) idx
9.595 - |> Thm.instantiate (map tinst binsts, map inst binsts)
9.596 - end
9.597 -
9.598 -fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules)
9.599 - THEN_ALL_NEW rtac @{thm is_equality_eq}
9.600 -
9.601 -fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
9.602 -
9.603 -fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt))
9.604 - THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
9.605 -
9.606 -fun transfer_tac equiv ctxt i =
9.607 - let
9.608 - val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
9.609 - val start_rule =
9.610 - if equiv then @{thm transfer_start} else @{thm transfer_start'}
9.611 - val rules = get_transfer_raw ctxt
9.612 - val eq_rules = get_relator_eq_raw ctxt
9.613 - (* allow unsolved subgoals only for standard transfer method, not for transfer' *)
9.614 - val end_tac = if equiv then K all_tac else K no_tac
9.615 - val err_msg = "Transfer failed to convert goal to an object-logic formula"
9.616 - fun main_tac (t, i) =
9.617 - rtac start_rule i THEN
9.618 - (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
9.619 - THEN_ALL_NEW
9.620 - (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
9.621 - ORELSE' end_tac)) (i + 1)
9.622 - handle TERM (_, ts) => raise TERM (err_msg, ts)
9.623 - in
9.624 - EVERY
9.625 - [rewrite_goal_tac ctxt pre_simps i THEN
9.626 - SUBGOAL main_tac i,
9.627 - (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
9.628 - rewrite_goal_tac ctxt post_simps i,
9.629 - Goal.norm_hhf_tac ctxt i]
9.630 - end
9.631 -
9.632 -fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
9.633 - let
9.634 - val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
9.635 - val rule1 = transfer_rule_of_term ctxt false rhs
9.636 - val rules = get_transfer_raw ctxt
9.637 - val eq_rules = get_relator_eq_raw ctxt
9.638 - val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
9.639 - in
9.640 - EVERY
9.641 - [CONVERSION prep_conv i,
9.642 - rtac @{thm transfer_prover_start} i,
9.643 - ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
9.644 - THEN_ALL_NEW
9.645 - (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
9.646 - rtac @{thm refl} i]
9.647 - end)
9.648 -
9.649 -(** Transfer attribute **)
9.650 -
9.651 -fun transferred ctxt extra_rules thm =
9.652 - let
9.653 - val start_rule = @{thm transfer_start}
9.654 - val start_rule' = @{thm transfer_start'}
9.655 - val rules = extra_rules @ get_transfer_raw ctxt
9.656 - val eq_rules = get_relator_eq_raw ctxt
9.657 - val err_msg = "Transfer failed to convert goal to an object-logic formula"
9.658 - val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
9.659 - val thm1 = Drule.forall_intr_vars thm
9.660 - val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
9.661 - |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
9.662 - val thm2 = thm1
9.663 - |> Thm.certify_instantiate (instT, [])
9.664 - |> Raw_Simplifier.rewrite_rule ctxt pre_simps
9.665 - val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
9.666 - val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
9.667 - val rule = transfer_rule_of_lhs ctxt' t
9.668 - val tac =
9.669 - resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
9.670 - (rtac rule
9.671 - THEN_ALL_NEW
9.672 - (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
9.673 - THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
9.674 - handle TERM (_, ts) => raise TERM (err_msg, ts)
9.675 - val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
9.676 - val tnames = map (fst o dest_TFree o snd) instT
9.677 - in
9.678 - thm3
9.679 - |> Raw_Simplifier.rewrite_rule ctxt' post_simps
9.680 - |> Simplifier.norm_hhf ctxt'
9.681 - |> Drule.generalize (tnames, [])
9.682 - |> Drule.zero_var_indexes
9.683 - end
9.684 -(*
9.685 - handle THM _ => thm
9.686 -*)
9.687 -
9.688 -fun untransferred ctxt extra_rules thm =
9.689 - let
9.690 - val start_rule = @{thm untransfer_start}
9.691 - val rules = extra_rules @ get_transfer_raw ctxt
9.692 - val eq_rules = get_relator_eq_raw ctxt
9.693 - val err_msg = "Transfer failed to convert goal to an object-logic formula"
9.694 - val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
9.695 - val thm1 = Drule.forall_intr_vars thm
9.696 - val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
9.697 - |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
9.698 - val thm2 = thm1
9.699 - |> Thm.certify_instantiate (instT, [])
9.700 - |> Raw_Simplifier.rewrite_rule ctxt pre_simps
9.701 - val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
9.702 - val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
9.703 - val rule = transfer_rule_of_term ctxt' true t
9.704 - val tac =
9.705 - rtac (thm2 RS start_rule) 1 THEN
9.706 - (rtac rule
9.707 - THEN_ALL_NEW
9.708 - (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
9.709 - THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
9.710 - handle TERM (_, ts) => raise TERM (err_msg, ts)
9.711 - val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
9.712 - val tnames = map (fst o dest_TFree o snd) instT
9.713 - in
9.714 - thm3
9.715 - |> Raw_Simplifier.rewrite_rule ctxt' post_simps
9.716 - |> Simplifier.norm_hhf ctxt'
9.717 - |> Drule.generalize (tnames, [])
9.718 - |> Drule.zero_var_indexes
9.719 - end
9.720 -
9.721 -(** Methods and attributes **)
9.722 -
9.723 -val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
9.724 - error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))
9.725 -
9.726 -val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
9.727 - |-- Scan.repeat free) []
9.728 -
9.729 -fun transfer_method equiv : (Proof.context -> Proof.method) context_parser =
9.730 - fixing >> (fn vs => fn ctxt =>
9.731 - SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
9.732 -
9.733 -val transfer_prover_method : (Proof.context -> Proof.method) context_parser =
9.734 - Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
9.735 -
9.736 -(* Attribute for transfer rules *)
9.737 -
9.738 -fun prep_rule ctxt =
9.739 - abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
9.740 -
9.741 -val transfer_add =
9.742 - Thm.declaration_attribute (fn thm => fn ctxt =>
9.743 - (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
9.744 -
9.745 -val transfer_del =
9.746 - Thm.declaration_attribute (fn thm => fn ctxt =>
9.747 - (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
9.748 -
9.749 -val transfer_attribute =
9.750 - Attrib.add_del transfer_add transfer_del
9.751 -
9.752 -(* Attributes for transfer domain rules *)
9.753 -
9.754 -val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
9.755 -
9.756 -val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
9.757 -
9.758 -val transfer_domain_attribute =
9.759 - Attrib.add_del transfer_domain_add transfer_domain_del
9.760 -
9.761 -(* Attributes for transferred rules *)
9.762 -
9.763 -fun transferred_attribute thms = Thm.rule_attribute
9.764 - (fn context => transferred (Context.proof_of context) thms)
9.765 -
9.766 -fun untransferred_attribute thms = Thm.rule_attribute
9.767 - (fn context => untransferred (Context.proof_of context) thms)
9.768 -
9.769 -val transferred_attribute_parser =
9.770 - Attrib.thms >> transferred_attribute
9.771 -
9.772 -val untransferred_attribute_parser =
9.773 - Attrib.thms >> untransferred_attribute
9.774 -
9.775 -(* Theory setup *)
9.776 -
9.777 -val relator_eq_setup =
9.778 - let
9.779 - val name = @{binding relator_eq}
9.780 - fun add_thm thm context = context
9.781 - |> Data.map (map_relator_eq (Item_Net.update thm))
9.782 - |> Data.map (map_relator_eq_raw
9.783 - (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
9.784 - fun del_thm thm context = context
9.785 - |> Data.map (map_relator_eq (Item_Net.remove thm))
9.786 - |> Data.map (map_relator_eq_raw
9.787 - (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
9.788 - val add = Thm.declaration_attribute add_thm
9.789 - val del = Thm.declaration_attribute del_thm
9.790 - val text = "declaration of relator equality rule (used by transfer method)"
9.791 - val content = Item_Net.content o #relator_eq o Data.get
9.792 - in
9.793 - Attrib.setup name (Attrib.add_del add del) text
9.794 - #> Global_Theory.add_thms_dynamic (name, content)
9.795 - end
9.796 -
9.797 -val relator_domain_setup =
9.798 - let
9.799 - val name = @{binding relator_domain}
9.800 - fun add_thm thm context =
9.801 - let
9.802 - val thm = abstract_domains_relator_domain (Context.proof_of context) thm
9.803 - in
9.804 - context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm
9.805 - end
9.806 - fun del_thm thm context =
9.807 - let
9.808 - val thm = abstract_domains_relator_domain (Context.proof_of context) thm
9.809 - in
9.810 - context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm
9.811 - end
9.812 - val add = Thm.declaration_attribute add_thm
9.813 - val del = Thm.declaration_attribute del_thm
9.814 - val text = "declaration of relator domain rule (used by transfer method)"
9.815 - val content = Item_Net.content o #relator_domain o Data.get
9.816 - in
9.817 - Attrib.setup name (Attrib.add_del add del) text
9.818 - #> Global_Theory.add_thms_dynamic (name, content)
9.819 - end
9.820 -
9.821 -val setup =
9.822 - relator_eq_setup
9.823 - #> relator_domain_setup
9.824 - #> Attrib.setup @{binding transfer_rule} transfer_attribute
9.825 - "transfer rule for transfer method"
9.826 - #> Global_Theory.add_thms_dynamic
9.827 - (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
9.828 - #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
9.829 - "transfer domain rule for transfer method"
9.830 - #> Attrib.setup @{binding transferred} transferred_attribute_parser
9.831 - "raw theorem transferred to abstract theorem using transfer rules"
9.832 - #> Attrib.setup @{binding untransferred} untransferred_attribute_parser
9.833 - "abstract theorem transferred to raw theorem using transfer rules"
9.834 - #> Global_Theory.add_thms_dynamic
9.835 - (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
9.836 - #> Method.setup @{binding transfer} (transfer_method true)
9.837 - "generic theorem transfer method"
9.838 - #> Method.setup @{binding transfer'} (transfer_method false)
9.839 - "generic theorem transfer method"
9.840 - #> Method.setup @{binding transfer_prover} transfer_prover_method
9.841 - "for proving transfer rules"
9.842 -
9.843 -end
10.1 --- a/src/HOL/Topological_Spaces.thy Thu Apr 10 17:48:17 2014 +0200
10.2 +++ b/src/HOL/Topological_Spaces.thy Thu Apr 10 17:48:18 2014 +0200
10.3 @@ -2508,7 +2508,7 @@
10.4 lemma bi_total_rel_filter [transfer_rule]:
10.5 assumes "bi_total A" "bi_unique A"
10.6 shows "bi_total (rel_filter A)"
10.7 -unfolding bi_total_conv_left_right using assms
10.8 +unfolding bi_total_alt_def using assms
10.9 by(simp add: left_total_rel_filter right_total_rel_filter)
10.10
10.11 lemma left_unique_rel_filter [transfer_rule]:
10.12 @@ -2535,7 +2535,7 @@
10.13
10.14 lemma bi_unique_rel_filter [transfer_rule]:
10.15 "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
10.16 -by(simp add: bi_unique_conv_left_right left_unique_rel_filter right_unique_rel_filter)
10.17 +by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
10.18
10.19 lemma top_filter_parametric [transfer_rule]:
10.20 "bi_total A \<Longrightarrow> (rel_filter A) top top"
11.1 --- a/src/HOL/Transfer.thy Thu Apr 10 17:48:17 2014 +0200
11.2 +++ b/src/HOL/Transfer.thy Thu Apr 10 17:48:18 2014 +0200
11.3 @@ -6,9 +6,13 @@
11.4 header {* Generic theorem transfer using relations *}
11.5
11.6 theory Transfer
11.7 -imports Hilbert_Choice Basic_BNFs Metis
11.8 +imports Hilbert_Choice Basic_BNFs BNF_FP_Base Metis Option
11.9 begin
11.10
11.11 +(* We include Option here altough it's not needed here.
11.12 + By doing this, we avoid a diamond problem for BNF and
11.13 + FP sugar interpretation defined in this file. *)
11.14 +
11.15 subsection {* Relator for function space *}
11.16
11.17 locale lifting_syntax
11.18 @@ -105,33 +109,6 @@
11.19 shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
11.20 using assms unfolding Rel_def rel_fun_def by fast
11.21
11.22 -end
11.23 -
11.24 -ML_file "Tools/transfer.ML"
11.25 -setup Transfer.setup
11.26 -
11.27 -declare refl [transfer_rule]
11.28 -
11.29 -declare rel_fun_eq [relator_eq]
11.30 -
11.31 -hide_const (open) Rel
11.32 -
11.33 -context
11.34 -begin
11.35 -interpretation lifting_syntax .
11.36 -
11.37 -text {* Handling of domains *}
11.38 -
11.39 -lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
11.40 - by auto
11.41 -
11.42 -lemma Domaimp_refl[transfer_domain_rule]:
11.43 - "Domainp T = Domainp T" ..
11.44 -
11.45 -lemma Domainp_prod_fun_eq[relator_domain]:
11.46 - "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
11.47 -by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
11.48 -
11.49 subsection {* Predicates on relations, i.e. ``class constraints'' *}
11.50
11.51 definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
11.52 @@ -181,7 +158,7 @@
11.53 lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
11.54 unfolding right_unique_def by fast
11.55
11.56 -lemma right_total_alt_def:
11.57 +lemma right_total_alt_def2:
11.58 "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
11.59 unfolding right_total_def rel_fun_def
11.60 apply (rule iffI, fast)
11.61 @@ -191,11 +168,11 @@
11.62 apply fast
11.63 done
11.64
11.65 -lemma right_unique_alt_def:
11.66 +lemma right_unique_alt_def2:
11.67 "right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
11.68 unfolding right_unique_def rel_fun_def by auto
11.69
11.70 -lemma bi_total_alt_def:
11.71 +lemma bi_total_alt_def2:
11.72 "bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
11.73 unfolding bi_total_def rel_fun_def
11.74 apply (rule iffI, fast)
11.75 @@ -208,7 +185,7 @@
11.76 apply fast
11.77 done
11.78
11.79 -lemma bi_unique_alt_def:
11.80 +lemma bi_unique_alt_def2:
11.81 "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
11.82 unfolding bi_unique_def rel_fun_def by auto
11.83
11.84 @@ -228,24 +205,72 @@
11.85 lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
11.86 by(auto simp add: bi_total_def)
11.87
11.88 -lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)"
11.89 +lemma right_unique_alt_def: "right_unique R = (conversep R OO R \<le> op=)" unfolding right_unique_def by blast
11.90 +lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \<le> op=)" unfolding left_unique_def by blast
11.91 +
11.92 +lemma right_total_alt_def: "right_total R = (conversep R OO R \<ge> op=)" unfolding right_total_def by blast
11.93 +lemma left_total_alt_def: "left_total R = (R OO conversep R \<ge> op=)" unfolding left_total_def by blast
11.94 +
11.95 +lemma bi_total_alt_def: "bi_total A = (left_total A \<and> right_total A)"
11.96 unfolding left_total_def right_total_def bi_total_def by blast
11.97
11.98 -lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
11.99 -by(simp add: left_total_def right_total_def bi_total_def)
11.100 -
11.101 -lemma bi_unique_iff: "bi_unique A \<longleftrightarrow> right_unique A \<and> left_unique A"
11.102 +lemma bi_unique_alt_def: "bi_unique A = (left_unique A \<and> right_unique A)"
11.103 unfolding left_unique_def right_unique_def bi_unique_def by blast
11.104
11.105 -lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
11.106 -by(auto simp add: left_unique_def right_unique_def bi_unique_def)
11.107 -
11.108 lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R"
11.109 -unfolding bi_total_iff ..
11.110 +unfolding bi_total_alt_def ..
11.111
11.112 lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R"
11.113 -unfolding bi_unique_iff ..
11.114 +unfolding bi_unique_alt_def ..
11.115
11.116 +end
11.117 +
11.118 +subsection {* Equality restricted by a predicate *}
11.119 +
11.120 +definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
11.121 + where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
11.122 +
11.123 +lemma eq_onp_Grp: "eq_onp P = BNF_Util.Grp (Collect P) id"
11.124 +unfolding eq_onp_def Grp_def by auto
11.125 +
11.126 +lemma eq_onp_to_eq:
11.127 + assumes "eq_onp P x y"
11.128 + shows "x = y"
11.129 +using assms by (simp add: eq_onp_def)
11.130 +
11.131 +lemma eq_onp_same_args:
11.132 + shows "eq_onp P x x = P x"
11.133 +using assms by (auto simp add: eq_onp_def)
11.134 +
11.135 +lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
11.136 +by (metis mem_Collect_eq subset_eq)
11.137 +
11.138 +ML_file "Tools/Transfer/transfer.ML"
11.139 +setup Transfer.setup
11.140 +declare refl [transfer_rule]
11.141 +
11.142 +ML_file "Tools/Transfer/transfer_bnf.ML"
11.143 +
11.144 +declare pred_fun_def [simp]
11.145 +declare rel_fun_eq [relator_eq]
11.146 +
11.147 +hide_const (open) Rel
11.148 +
11.149 +context
11.150 +begin
11.151 +interpretation lifting_syntax .
11.152 +
11.153 +text {* Handling of domains *}
11.154 +
11.155 +lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
11.156 + by auto
11.157 +
11.158 +lemma Domaimp_refl[transfer_domain_rule]:
11.159 + "Domainp T = Domainp T" ..
11.160 +
11.161 +lemma Domainp_prod_fun_eq[relator_domain]:
11.162 + "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
11.163 +by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
11.164
11.165 text {* Properties are preserved by relation composition. *}
11.166
11.167 @@ -333,12 +358,12 @@
11.168
11.169 lemma bi_total_fun[transfer_rule]:
11.170 "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
11.171 - unfolding bi_unique_iff bi_total_iff
11.172 + unfolding bi_unique_alt_def bi_total_alt_def
11.173 by (blast intro: right_total_fun left_total_fun)
11.174
11.175 lemma bi_unique_fun[transfer_rule]:
11.176 "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
11.177 - unfolding bi_unique_iff bi_total_iff
11.178 + unfolding bi_unique_alt_def bi_total_alt_def
11.179 by (blast intro: right_unique_fun left_unique_fun)
11.180
11.181 subsection {* Transfer rules *}
11.182 @@ -376,7 +401,7 @@
11.183
11.184 lemma eq_imp_transfer [transfer_rule]:
11.185 "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
11.186 - unfolding right_unique_alt_def .
11.187 + unfolding right_unique_alt_def2 .
11.188
11.189 text {* Transfer rules using equality. *}
11.190
11.191 @@ -490,6 +515,18 @@
11.192 using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
11.193 by metis
11.194
11.195 +lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
11.196 +unfolding eq_onp_def rel_fun_def by auto
11.197 +
11.198 +lemma rel_fun_eq_onp_rel:
11.199 + shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
11.200 +by (auto simp add: eq_onp_def rel_fun_def)
11.201 +
11.202 +lemma eq_onp_transfer [transfer_rule]:
11.203 + assumes [transfer_rule]: "bi_unique A"
11.204 + shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
11.205 +unfolding eq_onp_def[abs_def] by transfer_prover
11.206 +
11.207 end
11.208
11.209 end