src/HOL/ex/Transfer_Debug.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61368 33a62b54f381
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/ex/Transfer_Debug.thy
     2     Author:     Ondřej Kunčar, TU München
     3 *)
     4 theory Transfer_Debug 
     5 imports Main "~~/src/HOL/Library/FSet"
     6 begin                              
     7 
     8 (*
     9   This file demonstrates some of the typical scenarios 
    10   when transfer or transfer_prover does not produce expected results
    11   and how the user might handle such cases.
    12 *)
    13 
    14 (* As an example, we use finite sets. The following command recreates the environment in which
    15    the type of finite sets was created and allows us to do transferring on this type. *)
    16 context
    17 includes fset.lifting
    18 begin
    19 
    20 subsection \<open>1. A missing transfer rule\<close>
    21 
    22 (* We will simulate the situation in which there is not any transfer rules for fmember. *)
    23 declare fmember.transfer[transfer_rule del] fmember_transfer[transfer_rule del]
    24 
    25 (* We want to prove the following theorem about |\<subseteq>| by transfer *)
    26 lemma "(A |\<subseteq>| B) = fBall A (\<lambda>x. x |\<in>| B)"
    27 apply transfer
    28 (* 
    29    Transfer complains that it could not find a transfer rule for |\<subseteq>| with a matching transfer
    30    relation. An experienced user could notice that |\<in>| was transferred to |\<in>| by a 
    31    a default reflexivity transfer rule (because there was not any genuine transfer rule for |\<in>|)
    32    and fBall was transferred to Ball using the transfer relation pcr_fset. Therefore transfer
    33    is looking for a transfer rule for |\<subseteq>| with a transfer relation that mixes op= and pcr_fset.
    34    This situation might be confusing because the real problem (a missing transfer rule) propagates
    35    during the transferring algorithm and manifests later in an obfuscated way. Fortunately,
    36    we could inspect the behavior of transfer in a more interactive way to pin down the real problem.
    37 *)
    38 oops
    39 
    40 lemma "(A |\<subseteq>| B) = fBall A (\<lambda>x. x |\<in>| B)"
    41 apply transfer_start 
    42 (* Setups 6 goals for 6 transfer rules that have to be found and the result as the 7. goal, which
    43    gets synthesized to the final result of transferring when we find the 6 transfer rules. *)
    44 apply transfer_step
    45 (* We can see that the default reflexivity transfer rule was applied and |\<in>| 
    46   was transferred to |\<in>| \<Longrightarrow> there is no genuine transfer rule for |\<in>|. *)
    47 oops
    48 
    49 (* We provide a transfer rule for |\<in>|. *)
    50 lemma [transfer_rule]: "bi_unique A \<Longrightarrow> rel_fun A (rel_fun (pcr_fset A) op =) op \<in> op |\<in>|"
    51 by (rule fmember.transfer)
    52 
    53 lemma "(A |\<subseteq>| B) = fBall A (\<lambda>x. x |\<in>| B)"
    54 apply transfer_start
    55 apply transfer_step (* The new transfer rule was selected and |\<in>| was transferred to \<in>. *)
    56 apply transfer_step+
    57 apply transfer_end
    58 by blast
    59 
    60 (* Of course in the real life, we would use transfer instead of transfer_start, transfer_step+ and 
    61    transfer_end. *) 
    62 lemma "(A |\<subseteq>| B) = fBall A (\<lambda>x. x |\<in>| B)"
    63 by transfer blast
    64 
    65 subsection \<open>2. Unwanted instantiation of a transfer relation variable\<close>
    66 
    67 (* We want to prove the following fact. *)
    68 lemma "finite (UNIV :: 'a::finite fset set)"
    69 apply transfer
    70 (* Transfer does not do anything here. *)
    71 oops
    72 
    73 (* Let us inspect interactively what happened. *)
    74 lemma "finite (UNIV :: 'a::finite fset set)"
    75 apply transfer_start
    76 apply transfer_step 
    77 (* 
    78    Here we can realize that not an expected transfer rule was chosen. 
    79    We stumbled upon a limitation of Transfer: the tool used the rule Lifting_Set.UNIV_transfer,
    80    which transfers UNIV to UNIV and assumes that the transfer relation has to be bi-total.
    81    The problem is that at this point the transfer relation is not known (it is represented by
    82    a schematic variable ?R) and therefore in order to discharge the assumption "bi_total ?R", ?R is
    83    instantiated to op=. If the relation had been known (we wish pcr_fset op=, which is not bi-total),
    84    the assumption bi_total pcr_fset op= could not have been discharged and the tool would have 
    85    backtracked and chosen Lifting.right_total_UNIV_transfer, which assumes only right-totalness 
    86    (and pcr_fset is right-total).
    87 *)
    88 back back (* We can force the tool to backtrack and choose the desired transfer rule. *)
    89 apply transfer_step
    90 apply transfer_end
    91 by auto
    92 
    93 (* Of course, to use "back" in proofs is not a desired style. But we can prioritize
    94    the rule Lifting.right_total_UNIV_transfer by redeclaring it LOCALLY as a transfer rule.
    95  *)
    96 lemma "finite (UNIV :: 'a::finite fset set)"
    97 proof -
    98   note right_total_UNIV_transfer[transfer_rule]
    99   show ?thesis by transfer auto
   100 qed
   101 
   102 end
   103 
   104 (* Let us close the environment of fset transferring and add the rule that we deleted. *)
   105 lifting_forget fset.lifting (* deletes the extra added transfer rule for |\<in>| *)
   106 declare fmember_transfer[transfer_rule] (* we want to keep parametricity of |\<in>| *)
   107 
   108 end