1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Guess_ExI
8imports
9  Eisbach_Methods
10  Apply_Debug
11begin
12
13(*
14This file contains the experimental methods guess_exI and guess_spec. Each, as the name suggests,
15attempts to guess an instantiation for their respective rules. It does so by looking
16for a matching premise for the quantifying binder, checking that
17this could be the only match for safety.
18*)
19
20method abs_used for P = (match (P) in "\<lambda>s. ?P" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)
21
22method in_conj for P Q = (
23      match (Q) in "P" \<Rightarrow> \<open>-\<close>
24    | match (Q) in "\<lambda>y. A y \<and> B y"  for A B  \<Rightarrow>
25            \<open> match (A) in "(Q' :: 'b)" for Q' \<Rightarrow> \<open>match (B) in "(Q'' :: 'b)"  for Q'' \<Rightarrow>
26             \<open> in_conj P Q' | in_conj P Q''\<close>\<close>\<close>
27    )
28
29method guess_exI =
30    (require_determ \<open>(match conclusion in "\<exists>x. Q x" for Q \<Rightarrow>
31                            \<open>match premises in "P y" for P y \<Rightarrow>
32                             \<open>abs_used P, in_conj P Q, rule exI[where x=y]\<close>\<close>)\<close>)
33
34lemma fun_uncurry:
35  "(P \<longrightarrow> Q \<longrightarrow> R) \<longleftrightarrow> (P \<and> Q) \<longrightarrow> R"
36  by auto
37
38method guess_spec_inner for P uses I =
39    ((match I in "\<forall>x. C x \<longrightarrow> _ x" for C \<Rightarrow> \<open>in_conj P C\<close> ))
40
41method guess_spec =
42    (require_determ \<open>(match premises in I:"\<forall>x. _ x \<longrightarrow> _ x" \<Rightarrow>
43                            \<open>match premises in "P y" for P y \<Rightarrow>
44                            \<open>abs_used P, guess_spec_inner P I:I[simplified fun_uncurry],
45                                         insert I, drule spec[where x=y]\<close>\<close>)\<close>)
46
47text \<open>Tests and examples\<close>
48experiment begin
49
50 lemma
51    assumes Q: "Q x"
52    shows  "P x \<Longrightarrow> \<forall>x. Q x \<longrightarrow> P x \<longrightarrow> R  \<Longrightarrow> R"
53    by (guess_spec, blast intro: Q)
54
55  (* Conflicting premises are checked *)
56  lemma
57    assumes Q: "Q x"
58    shows "\<lbrakk> P x; P y \<rbrakk> \<Longrightarrow>  \<forall>x. Q x \<longrightarrow> P x \<longrightarrow> R \<Longrightarrow> R"
59    apply (fails \<open>guess_spec\<close>)
60    by (blast intro: Q)
61
62  (* Conflicts between different conjuncts are checked *)
63  lemma
64    assumes Q: "Q x"
65    shows "\<lbrakk> P x; Q y \<rbrakk> \<Longrightarrow> \<forall>x. Q x \<longrightarrow> P x \<longrightarrow> R \<Longrightarrow> R"
66    apply (fails \<open>guess_spec\<close>)
67    by (blast intro: Q)
68end
69
70text \<open>Tests and examples\<close>
71experiment begin
72  lemma "P x \<Longrightarrow> \<exists>x. P x"
73    by guess_exI
74
75  lemma
76    assumes Q: "Q x"
77    shows "P x \<Longrightarrow> \<exists>x. Q x \<and> P x"
78    apply guess_exI
79    by (blast intro: Q)
80
81  (* Conflicting premises are checked *)
82  lemma
83    assumes Q: "Q x"
84    shows "\<lbrakk> P x; P y \<rbrakk> \<Longrightarrow> \<exists>x. Q x \<and> P x"
85    apply (fails \<open>guess_exI\<close>)
86    by (blast intro: Q)
87
88  (* Conflicts between different conjuncts are checked *)
89  lemma
90    assumes Q: "Q x"
91    shows "\<lbrakk> P x; Q y \<rbrakk> \<Longrightarrow> \<exists>x. Q x \<and> P x"
92    apply (fails \<open>guess_exI\<close>)
93    by (blast intro: Q)
94end
95
96end