setup for Transfer and Lifting from BNF; tuned thm names
authorkuncar
Thu Apr 10 17:48:18 2014 +0200 (2014-04-10)
changeset 56524f4ba736040fa
parent 56523 2ae16e3d8b6d
child 56525 b5b6ad5dc2ae
setup for Transfer and Lifting from BNF; tuned thm names
src/HOL/Library/FSet.thy
src/HOL/Lifting.thy
src/HOL/Lifting_Set.thy
src/HOL/Tools/Lifting/lifting_bnf.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
src/HOL/Tools/transfer.ML
src/HOL/Topological_Spaces.thy
src/HOL/Transfer.thy
     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