# HG changeset patch
# User kuncar
# Date 1444347867 -7200
# Node ID 33a62b54f381815e0f039d4e03e995515597d4e4
# Parent  46af4f577c7e20ba8b5a7edc4084b81b8e3e5526
add a file with examples of debugging transfer

diff -r 46af4f577c7e -r 33a62b54f381 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Oct 09 01:37:57 2015 +0200
+++ b/src/HOL/ROOT	Fri Oct 09 01:44:27 2015 +0200
@@ -583,6 +583,7 @@
     Reflection_Examples
     Sqrt
     Sqrt_Script
+    Transfer_Debug
     Transfer_Ex
     Transfer_Int_Nat
     Transitive_Closure_Table_Ex
diff -r 46af4f577c7e -r 33a62b54f381 src/HOL/ex/Transfer_Debug.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Transfer_Debug.thy	Fri Oct 09 01:44:27 2015 +0200
@@ -0,0 +1,108 @@
+(*  Title:      HOL/ex/Transfer_Debug.thy
+    Author:     Ondřej Kunčar, TU München
+*)
+theory Transfer_Debug 
+imports Main "~~/src/HOL/Library/FSet"
+begin                              
+
+(*
+  This file demonstrates some of the typical scenarios 
+  when transfer or transfer_prover does not produce expected results
+  and how the user might handle such cases.
+*)
+
+(* As an example, we use finite sets. The following command recreates the environment in which
+   the type of finite sets was created and allows us to do transferring on this type. *)
+context
+includes fset.lifting
+begin
+
+subsection \<open>1. A missing transfer rule\<close>
+
+(* We will simulate the situation in which there is not any transfer rules for fmember. *)
+declare fmember.transfer[transfer_rule del] fmember_transfer[transfer_rule del]
+
+(* We want to prove the following theorem about |\<subseteq>| by transfer *)
+lemma "(A |\<subseteq>| B) = fBall A (\<lambda>x. x |\<in>| B)"
+apply transfer
+(* 
+   Transfer complains that it could not find a transfer rule for |\<subseteq>| with a matching transfer
+   relation. An experienced user could notice that |\<in>| was transferred to |\<in>| by a 
+   a default reflexivity transfer rule (because there was not any genuine transfer rule for |\<in>|)
+   and fBall was transferred to Ball using the transfer relation pcr_fset. Therefore transfer
+   is looking for a transfer rule for |\<subseteq>| with a transfer relation that mixes op= and pcr_fset.
+   This situation might be confusing because the real problem (a missing transfer rule) propagates
+   during the transferring algorithm and manifests later in an obfuscated way. Fortunately,
+   we could inspect the behavior of transfer in a more interactive way to pin down the real problem.
+*)
+oops
+
+lemma "(A |\<subseteq>| B) = fBall A (\<lambda>x. x |\<in>| B)"
+apply transfer_start 
+(* Setups 6 goals for 6 transfer rules that have to be found and the result as the 7. goal, which
+   gets synthesized to the final result of transferring when we find the 6 transfer rules. *)
+apply transfer_step
+(* We can see that the default reflexivity transfer rule was applied and |\<in>| 
+  was transferred to |\<in>| \<Longrightarrow> there is no genuine transfer rule for |\<in>|. *)
+oops
+
+(* We provide a transfer rule for |\<in>|. *)
+lemma [transfer_rule]: "bi_unique A \<Longrightarrow> rel_fun A (rel_fun (pcr_fset A) op =) op \<in> op |\<in>|"
+by (rule fmember.transfer)
+
+lemma "(A |\<subseteq>| B) = fBall A (\<lambda>x. x |\<in>| B)"
+apply transfer_start
+apply transfer_step (* The new transfer rule was selected and |\<in>| was transferred to \<in>. *)
+apply transfer_step+
+apply transfer_end
+by blast
+
+(* Of course in the real life, we would use transfer instead of transfer_start, transfer_step+ and 
+   transfer_end. *) 
+lemma "(A |\<subseteq>| B) = fBall A (\<lambda>x. x |\<in>| B)"
+by transfer blast
+
+subsection \<open>2. Unwanted instantiation of a transfer relation variable\<close>
+
+(* We want to prove the following fact. *)
+lemma "finite (UNIV :: 'a::finite fset set)"
+apply transfer
+(* Transfer does not do anything here. *)
+oops
+
+(* Let us inspect interactively what happened. *)
+lemma "finite (UNIV :: 'a::finite fset set)"
+apply transfer_start
+apply transfer_step 
+(* 
+   Here we can realize that not an expected transfer rule was chosen. 
+   We stumbled upon a limitation of Transfer: the tool used the rule Lifting_Set.UNIV_transfer,
+   which transfers UNIV to UNIV and assumes that the transfer relation has to be bi-total.
+   The problem is that at this point the transfer relation is not known (it is represented by
+   a schematic variable ?R) and therefore in order to discharge the assumption "bi_total ?R", ?R is
+   instantiated to op=. If the relation had been known (we wish pcr_fset op=, which is not bi-total),
+   the assumption bi_total pcr_fset op= could not have been discharged and the tool would have 
+   backtracked and chosen Lifting.right_total_UNIV_transfer, which assumes only right-totalness 
+   (and pcr_fset is right-total).
+*)
+back back (* We can force the tool to backtrack and choose the desired transfer rule. *)
+apply transfer_step
+apply transfer_end
+by auto
+
+(* Of course, to use "back" in proofs is not a desired style. But we can prioritize
+   the rule Lifting.right_total_UNIV_transfer by redeclaring it LOCALLY as a transfer rule.
+ *)
+lemma "finite (UNIV :: 'a::finite fset set)"
+proof -
+  note right_total_UNIV_transfer[transfer_rule]
+  show ?thesis by transfer auto
+qed
+
+end
+
+(* Let us close the environment of fset transferring and add the rule that we deleted. *)
+lifting_forget fset.lifting (* deletes the extra added transfer rule for |\<in>| *)
+declare fmember_transfer[transfer_rule] (* we want to keep parametricity of |\<in>| *)
+
+end