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