summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

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 *)

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

20 subsection \<open>1. A missing transfer rule\<close>

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]

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

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

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)

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

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

65 subsection \<open>2. Unwanted instantiation of a transfer relation variable\<close>

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

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

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

102 end

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>| *)

108 end