# Theory Tests

```(*  Title:      HOL/Eisbach/Tests.thy
Author:     Daniel Matichuk, NICTA/UNSW
*)

section ‹Miscellaneous Eisbach tests›

theory Tests
imports Main Eisbach_Tools
begin

subsection ‹Named Theorems Tests›

named_theorems foo

method foo declares foo = (rule foo)

lemma
assumes A [foo]: A
shows A
apply foo
done

method abs_used for P = (match (P) in "λa. ?Q" ⇒ fail ¦ _ ⇒ -)

subsection ‹Match Tests›

begin
have dup: "⋀A. A ⟹ A ⟹ A" by simp

fix A y
have "(⋀x. A x) ⟹ A y"
apply (rule dup, match premises in Y: "⋀B. P B" for P ⇒ ‹match (P) in A ⇒ ‹print_fact Y, rule Y››)
apply (rule dup, match premises in Y: "⋀B :: 'a. P B" for P ⇒ ‹match (P) in A ⇒ ‹print_fact Y, rule Y››)
apply (rule dup, match premises in Y: "⋀B :: 'a. P B" for P ⇒ ‹match conclusion in "P y" for y ⇒ ‹print_fact Y, print_term y, rule Y[where B=y]››)
apply (rule dup, match premises in Y: "⋀B :: 'a. P B" for P ⇒ ‹match conclusion in "P z" for z ⇒ ‹print_fact Y, print_term y, rule Y[where B=z]››)
apply (rule dup, match conclusion in "P y" for P ⇒ ‹match premises in Y: "⋀z. P z" ⇒ ‹print_fact Y, rule Y[where z=y]››)
apply (match premises in Y: "⋀z :: 'a. P z" for P ⇒ ‹match conclusion in "P y" ⇒ ‹print_fact Y, rule Y[where z=y]››)
done

assume X: "⋀x. A x" "A y"
have "A y"
apply (match X in Y:"⋀B. A B" and Y':"B ?x" for B ⇒ ‹print_fact Y[where B=y], print_term B›)
apply (match X in Y:"B ?x" and Y':"B ?x" for B ⇒ ‹print_fact Y, print_term B›)
apply (match X in Y:"B x" and Y':"B x" for B x ⇒ ‹print_fact Y, print_term B, print_term x›)
apply (insert X)
apply (match premises in Y:"⋀B. A B" and Y':"B y" for B and y :: 'a ⇒ ‹print_fact Y[where B=y], print_term B›)
apply (match premises in Y:"B ?x" and Y':"B ?x" for B ⇒ ‹print_fact Y, print_term B›)
apply (match premises in Y:"B x" and Y':"B x" for B x ⇒ ‹print_fact Y, print_term B›)
apply (match conclusion in "P x" and "P y" for P x ⇒ ‹print_term P, print_term x›)
apply assumption
done

{
fix B x y
assume X: "⋀x y. B x x y"
have "B x x y"
by (match X in Y:"⋀y. B y y z" for z ⇒ ‹rule Y[where y=x]›)

fix A B
have "(⋀x y. A (B x) y) ⟹ A (B x) y"
by (match premises in Y: "⋀xx. ?H (B xx)" ⇒ ‹rule Y›)
}

(* match focusing retains prems *)
fix B x
have "(⋀x. A x) ⟹ (⋀z. B z) ⟹ A y ⟹ B x"
apply (match premises in Y: "⋀z :: 'a. A z"  ⇒ ‹match premises in Y': "⋀z :: 'b. B z" ⇒ ‹print_fact Y, print_fact Y', rule Y'[where z=x]››)
done

(*Attributes *)
fix C
have "(⋀x :: 'a. A x)  ⟹ (⋀z. B z) ⟹ A y ⟹ B x ∧ B x ∧ A y"
apply (intro conjI)
apply (match premises in Y: "⋀z :: 'a. A z" and Y'[intro]:"⋀z :: 'b. B z" ⇒ fastforce)
apply (match premises in Y: "⋀z :: 'a. A z"  ⇒ ‹match premises in Y'[intro]:"⋀z :: 'b. B z" ⇒ fastforce›)
apply (match premises in Y[thin]: "⋀z :: 'a. A z"  ⇒ ‹(match premises in Y':"⋀z :: 'a. A z" ⇒ ‹print_fact Y,fail› ¦ _ ⇒ ‹print_fact Y›)›)
(*apply (match premises in Y: "⋀z :: 'b. B z"  ⇒ ‹(match premises in Y'[thin]:"⋀z :: 'b. B z" ⇒ ‹(match premises in Y':"⋀z :: 'a. A z" ⇒ fail ¦ Y': _ ⇒ -)›)›)*)
apply assumption
done

fix A B C D
have "⋀uu'' uu''' uu uu'. (⋀x :: 'a. A uu' x)  ⟹ D uu y ⟹ (⋀z. B uu z) ⟹ C uu y ⟹ (⋀z y. C uu z)  ⟹ B uu x ∧ B uu x ∧ C uu y"
apply (match premises in Y[thin]: "⋀z :: 'a. A ?zz' z" and
Y'[thin]: "⋀rr :: 'b. B ?zz rr" ⇒
‹print_fact Y, print_fact Y', intro conjI, rule Y', insert Y', insert Y'[where rr=x]›)
apply (match premises in Y:"B ?u ?x" ⇒ ‹rule Y›)
apply (insert TrueI)
apply (match premises in Y'[thin]: "⋀ff. B uu ff" for uu ⇒ ‹insert Y', drule meta_spec[where x=x]›)
apply assumption
done

(* Multi-matches. As many facts as match are bound. *)
fix A B C x
have "(⋀x :: 'a. A x) ⟹ (⋀y :: 'a. B y) ⟹ C y ⟹ (A x ∧ B y ∧ C y)"
apply (match premises in Y[thin]: "⋀z :: 'a. ?A z" (multi) ⇒ ‹intro conjI, (rule Y)+›)
apply (match premises in Y[thin]: "⋀z :: 'a. ?A z" (multi) ⇒ fail ¦ "C y" ⇒ -) (* multi-match must bind something *)
apply (match premises in Y: "C y" ⇒ ‹rule Y›)
done

fix A B C x
have "(⋀x :: 'a. A x) ⟹ (⋀y :: 'a. B y) ⟹ C y ⟹ (A x ∧ B y ∧ C y)"
apply (match premises in Y[thin]: "⋀z. ?A z" (multi) ⇒ ‹intro conjI, (rule Y)+›)
apply (match premises in Y[thin]: "⋀z. ?A z" (multi) ⇒ fail ¦ "C y" ⇒ -) (* multi-match must bind something *)
apply (match premises in Y: "C y" ⇒ ‹rule Y›)
done

fix A B C P Q and x :: 'a and y :: 'a
have "(⋀x y :: 'a. A x y ∧ Q) ⟹ (⋀a b. B (a :: 'a) (b :: 'a) ∧ Q) ⟹ (⋀x y. C (x :: 'a) (y :: 'a) ∧ P) ⟹ A y x ∧ B y x"
by (match premises in Y: "⋀z a. ?A (z :: 'a) (a :: 'a) ∧ R" (multi) for R ⇒ ‹rule conjI, rule Y[where z=x,THEN conjunct1], rule Y[THEN conjunct1]›)

(*We may use for-fixes in multi-matches too. All bound facts must agree on the fixed term *)
fix A B C x
have "(⋀y :: 'a. B y ∧ C y) ⟹ (⋀x :: 'a. A x ∧ B x) ⟹ (⋀y :: 'a. A y ∧ C y) ⟹ C y ⟹ (A x ∧ B y ∧ C y)"
apply (match premises in Y: "⋀x :: 'a. P x ∧ ?U x" (multi) for P ⇒
‹match (P) in B ⇒ fail
¦ "λa. B" ⇒ fail
¦ _ ⇒ -,
intro conjI, (rule Y[THEN conjunct1])›)
apply (rule dup)
apply (match premises in Y':"⋀x :: 'a. ?U x ∧ Q x" and Y: "⋀x :: 'a. Q x ∧ ?U x" (multi)  for Q ⇒ ‹insert Y[THEN conjunct1]›)
apply assumption (* Previous match requires that Q is consistent *)
apply (match premises in Y: "⋀z :: 'a. ?A z ⟶ False" (multi) ⇒ ‹print_fact Y, fail› ¦ "C y" ⇒ ‹print_term C›) (* multi-match must bind something *)
apply (match premises in Y: "⋀x. B x ∧ C x" ⇒ ‹intro conjI Y[THEN conjunct1]›)
apply (match premises in Y: "C ?x" ⇒ ‹rule Y›)
done

(* All bindings must be tried for a particular theorem.
However all combinations are NOT explored. *)
fix B A C
assume asms:"⋀a b. B (a :: 'a) (b :: 'a) ∧ Q" "⋀x :: 'a. A x x ∧ Q" "⋀a b. C (a :: 'a) (b :: 'a) ∧ Q"
have "B y x ∧ C x y ∧ B x y ∧ C y x ∧ A x x"
apply (intro conjI)
apply (match asms in Y: "⋀z a. ?A (z :: 'a) (a :: 'a) ∧ R" (multi) for R ⇒ ‹rule Y[where z=x,THEN conjunct1]›)
apply (match asms in Y: "⋀z a. ?A (z :: 'a) (a :: 'a) ∧ R" (multi) for R ⇒ ‹rule Y[where a=x,THEN conjunct1]›)
apply (match asms in Y: "⋀z a. ?A (z :: 'a) (a :: 'a) ∧ R" (multi) for R ⇒ ‹rule Y[where a=x,THEN conjunct1]›)
apply (match asms in Y: "⋀z a. ?A (z :: 'a) (a :: 'a) ∧ R" (multi) for R ⇒ ‹rule Y[where z=x,THEN conjunct1]›)
apply (match asms in Y: "⋀z a. A (z :: 'a) (a :: 'a) ∧ R"  for R ⇒ fail ¦ _ ⇒ -)
apply (rule asms[THEN conjunct1])
done

(* Attributes *)
fix A B C x
have "(⋀x :: 'a. A x ∧ B x) ⟹ (⋀y :: 'a. A y ∧ C y) ⟹ (⋀y :: 'a. B y ∧ C y) ⟹ C y ⟹ (A x ∧ B y ∧ C y)"
apply (match premises in Y: "⋀x :: 'a. P x ∧ ?U x" (multi) for P ⇒ ‹match Y[THEN conjunct1]  in Y':"?H"  (multi) ⇒ ‹intro conjI,rule Y'››)
apply (match premises in Y: "⋀x :: 'a. P x ∧ ?U x" (multi) for P ⇒ ‹match Y[THEN conjunct2]  in Y':"?H"  (multi) ⇒ ‹rule Y'››)
apply assumption
done

(* Removed feature for now *)
(*
fix A B C x
have "(⋀x :: 'a. A x ∧ B x) ⟹ (⋀y :: 'a. A y ∧ C y) ⟹ (⋀y :: 'a. B y ∧ C y) ⟹ C y ⟹ (A x ∧ B y ∧ C y)"
apply (match prems in Y: "⋀x :: 'a. P x ∧ ?U x" (multi) for P ⇒ ‹match ‹K @{thms Y TrueI}› in Y':"?H"  (multi) ⇒ ‹rule conjI; (rule Y')?››)
apply (match prems in Y: "⋀x :: 'a. P x ∧ ?U x" (multi) for P ⇒ ‹match ‹K [@{thm Y}]› in Y':"?H"  (multi) ⇒ ‹rule Y'››)
done
*)
(* Testing THEN_ALL_NEW within match *)
fix A B C x
have "(⋀x :: 'a. A x ∧ B x) ⟹ (⋀y :: 'a. A y ∧ C y) ⟹ (⋀y :: 'a. B y ∧ C y) ⟹ C y ⟹ (A x ∧ B y ∧ C y)"
apply (match premises in Y: "⋀x :: 'a. P x ∧ ?U x" (multi) for P ⇒ ‹intro conjI ; ((rule Y[THEN conjunct1])?); rule Y[THEN conjunct2] ›)
done

(* Cut tests *)
fix A B C D

have "D ∧ C  ⟹ A ∧ B  ⟹ A ⟶ C ⟹ D ⟶ True ⟹ C"
by (((match premises in I: "P ∧ Q" (cut)
and I': "P ⟶ ?U" for P Q ⇒ ‹rule mp [OF I' I[THEN conjunct1]]›)?), simp)

have "D ∧ C  ⟹ A ∧ B  ⟹ A ⟶ C ⟹ D ⟶ True ⟹ C"
by (match premises in I: "P ∧ Q" (cut 2)
and I': "P ⟶ ?U" for P Q ⇒ ‹rule mp [OF I' I[THEN conjunct1]]›)

have "A ∧ B ⟹ A ⟶ C ⟹ C"
by (((match premises in I: "P ∧ Q" (cut)
and I': "P ⟶ ?U" for P Q ⇒ ‹rule mp [OF I' I[THEN conjunct1]]›)?, simp) | simp)

fix f x y
have "f x y ⟹ f x y"
by (match conclusion in "f x y" for f x y  ⇒ ‹print_term f›)

fix A B C
assume X: "A ∧ B" "A ∧ C" C
have "A ∧ B ∧ C"
by (match X in H: "A ∧ ?H" (multi, cut) ⇒
‹match H in "A ∧ C" and "A ∧ B" ⇒ fail›

(* Thinning an inner focus *)
(* Thinning should persist within a match, even when on an external premise *)

fix A
have "(⋀x. A x ∧ B) ⟹ B ∧ C ⟹ C"
apply (match premises in H:"⋀x. A x ∧ B" ⇒
‹match premises in H'[thin]: "⋀x. A x ∧ B" ⇒
‹match premises in H'':"⋀x. A x ∧ B" ⇒ fail
¦ _ ⇒ -›
,match premises in H'':"⋀x. A x ∧ B" ⇒ fail ¦ _ ⇒ -›)
apply (match premises in H:"⋀x. A x ∧ B" ⇒ fail
¦ H':_ ⇒ ‹rule H'[THEN conjunct2]›)
done

(* Local premises *)
(* Only match premises which actually existed in the goal we just focused.*)

fix A
assume asms: "C ∧ D"
have "B ∧ C ⟹ C"
by (match premises in _ ⇒ ‹insert asms,
match premises (local) in "B ∧ C" ⇒ fail
¦ H:"C ∧ D" ⇒ ‹rule H[THEN conjunct1]››)
end

(* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
by retrofitting. This needs to be done more carefully to avoid smashing
legitimate pairs.*)

schematic_goal "?A x ⟹ A x"
apply (match conclusion in "H" for H ⇒ ‹match conclusion in Y for Y ⇒ ‹print_term Y››)
apply assumption
done

(* Ensure short-circuit after first match failure *)
lemma
assumes A: "P ∧ Q"
shows "P"
by ((match A in "P ∧ Q" ⇒ fail ¦ "?H" ⇒ -) | simp add: A)

lemma
assumes A: "D ∧ C" "A ∧ B" "A ⟶ B"
shows "A"
apply ((match A in U: "P ∧ Q" (cut) and "P' ⟶ Q'" for P Q P' Q' ⇒
‹simp add: U› ¦ "?H" ⇒ -) | -)
done

subsection ‹Uses Tests›

ML ‹
fun test_internal_fact ctxt factnm =
(case \<^try>‹Proof_Context.get_thms ctxt factnm› of
NONE => ()
| SOME _ => error "Found internal fact");
›

method uses_test⇩1 uses uses_test⇩1_uses = (rule uses_test⇩1_uses)

lemma assumes A shows A by (uses_test⇩1 uses_test⇩1_uses: assms)

ML ‹test_internal_fact \<^context> "uses_test⇩1_uses"›

ML ‹test_internal_fact \<^context> "Tests.uses_test⇩1_uses"›
ML ‹test_internal_fact \<^context> "Tests.uses_test⇩1.uses_test⇩1_uses"›

subsection ‹Basic fact passing›

method find_fact for x y :: bool uses facts1 facts2 =
(match facts1 in U: "x" ⇒ ‹insert U,
match facts2 in U: "y" ⇒ ‹insert U››)

lemma assumes A: A and B: B shows "A ∧ B"
apply (find_fact "A" "B" facts1: A facts2: B)
apply (rule conjI; assumption)
done

subsection ‹Testing term and fact passing in recursion›

method recursion_example for x :: bool uses facts =
(match (x) in
"A ∧ B" for A B ⇒ ‹(recursion_example A facts: facts, recursion_example B facts: facts)›
¦ "?H" ⇒ ‹match facts in U: "x" ⇒ ‹insert U››)

lemma
assumes asms: "A" "B" "C" "D"
shows "(A ∧ B) ∧ (C ∧ D)"
apply (recursion_example "(A ∧ B) ∧ (C ∧ D)" facts: asms)
apply simp
done

(* uses facts are not accumulated *)

method recursion_example' for A :: bool and B :: bool uses facts =
(match facts in
H: "A" and H': "B" ⇒ ‹recursion_example' "A" "B" facts: H TrueI›
¦ "A" and "True" ⇒ ‹recursion_example' "A" "B" facts: TrueI›
¦ "True" ⇒ -
¦ "PROP ?P" ⇒ fail)

lemma
assumes asms: "A" "B"
shows "True"
apply (recursion_example' "A" "B" facts: asms)
apply simp
done

(*Method.sections in existing method*)
method my_simp⇩1 uses my_simp⇩1_facts = (simp add: my_simp⇩1_facts)
lemma assumes A shows A by (my_simp⇩1 my_simp⇩1_facts: assms)

(*Method.sections via Eisbach argument parser*)
method uses_test⇩2 uses uses_test⇩2_uses = (uses_test⇩1 uses_test⇩1_uses: uses_test⇩2_uses)
lemma assumes A shows A by (uses_test⇩2 uses_test⇩2_uses: assms)

subsection ‹Declaration Tests›

named_theorems declare_facts⇩1

method declares_test⇩1 declares declare_facts⇩1 = (rule declare_facts⇩1)

lemma assumes A shows A by (declares_test⇩1 declare_facts⇩1: assms)

lemma assumes A[declare_facts⇩1]: A shows A by declares_test⇩1

subsection ‹Rule Instantiation Tests›

method my_allE⇩1 for x :: 'a and P :: "'a ⇒ bool" =
(erule allE [where x = x and P = P])

lemma "∀x. Q x ⟹ Q x" by (my_allE⇩1 x Q)

method my_allE⇩2 for x :: 'a and P :: "'a ⇒ bool" =
(erule allE [of P x])

lemma "∀x. Q x ⟹ Q x" by (my_allE⇩2 x Q)

method my_allE⇩3 for x :: 'a and P :: "'a ⇒ bool" =
(match allE [where 'a = 'a] in X: "⋀(x :: 'a) P R. ∀x. P x ⟹ (P x ⟹ R) ⟹ R" ⇒
‹erule X [where x = x and P = P]›)

lemma "∀x. Q x ⟹ Q x" by (my_allE⇩3 x Q)

method my_allE⇩4 for x :: 'a and P :: "'a ⇒ bool" =
(match allE [where 'a = 'a] in X: "⋀(x :: 'a) P R. ∀x. P x ⟹ (P x ⟹ R) ⟹ R" ⇒
‹erule X [of x P]›)

lemma "∀x. Q x ⟹ Q x" by (my_allE⇩4 x Q)

subsection ‹Polymorphism test›

axiomatization foo' :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
axiomatization where foo'_ax1: "foo' x y z ⟹ z ∧ y"
axiomatization where foo'_ax2: "foo' x y y ⟹ x ∧ z"
axiomatization where foo'_ax3: "foo' (x :: int) y y ⟹ y ∧ y"

lemmas my_thms = foo'_ax1 foo'_ax2 foo'_ax3

definition first_id where "first_id x = x"

lemmas my_thms' = my_thms[of "first_id x" for x]

method print_conclusion = (match conclusion in concl for concl ⇒ ‹print_term concl›)

lemma
assumes foo: "⋀x (y :: bool). foo' (A x) B (A x)"
shows "⋀z. A z ∧ B"
apply
(match conclusion in "f x y" for f y and x :: "'d :: type" ⇒ ‹
match my_thms' in R:"⋀(x :: 'f :: type). ?P (first_id x) ⟹ ?R"
and R':"⋀(x :: 'f :: type). ?P' (first_id x) ⟹ ?R'" ⇒ ‹
match (x) in "q :: 'f" for q ⇒ ‹
rule R[of q,simplified first_id_def],
print_conclusion,
rule foo
›››)
done

subsection ‹Unchecked rule instantiation, with the possibility of runtime errors›

named_theorems my_thms_named

declare foo'_ax3[my_thms_named]

method foo_method3 declares my_thms_named =
(match my_thms_named[of (unchecked) z for z] in R:"PROP ?H" ⇒ ‹rule R›)

begin

(*FIXME: Shouldn't need unchecked keyword here. See Tests_Failing.thy *)
fix A B x
have "foo' x B A ⟹ A ∧ B"
by (match my_thms[of (unchecked) z for z] in R:"PROP ?H" ⇒ ‹rule R›)

fix A B x
note foo'_ax1[my_thms_named]
have "foo' x B A ⟹ A ∧ B"
by (match my_thms_named[where x=z for z] in R:"PROP ?H" ⇒ ‹rule R›)

fix A B x
note foo'_ax1[my_thms_named] foo'_ax2[my_thms_named] foo'_ax3[my_thms_named]
have "foo' x B A ⟹ A ∧ B"
by foo_method3

end

ML ‹
structure Data = Generic_Data
(
type T = thm list;
val empty: T = [];
fun merge data : T = Thm.merge_thms data;
);
›

setup ‹Context.theory_map (Data.put @{thms TrueI})›

method dynamic_thms_test = (rule test_dyn)

locale foo =
fixes A
assumes A : "A"
begin

declaration ‹fn phi => Data.put (Morphism.fact phi @{thms A})›

lemma A by dynamic_thms_test

end

begin
fix A x
assume X: "⋀x. A x"
have "A x"
by (match X in H[of x]:"⋀x. A x" ⇒ ‹print_fact H,match H in "A x" ⇒ ‹rule H››)

fix A x B
assume X: "⋀x :: bool. A x ⟹ B" "⋀x. A x"
assume Y: "A B"
have "B ∧ B ∧ B ∧ B ∧ B ∧ B"
apply (intro conjI)
apply (match X in H[OF X(2)]:"⋀x. A x ⟹ B" ⇒ ‹print_fact H,rule H›)
apply (match X in H':"⋀x. A x" and H[OF H']:"⋀x. A x ⟹ B" ⇒ ‹print_fact H',print_fact H,rule H›)
apply (match X in H[of Q]:"⋀x. A x ⟹ ?R" and "?P ⟹ Q" for Q ⇒ ‹print_fact H,rule H, rule Y›)
apply (match X in H[of Q,OF Y]:"⋀x. A x ⟹ ?R" and "?P ⟹ Q" for Q ⇒ ‹print_fact H,rule H›)
apply (match X in H[OF Y,intro]:"⋀x. A x ⟹ ?R" ⇒ ‹print_fact H,fastforce›)
apply (match X in H[intro]:"⋀x. A x ⟹ ?R" ⇒ ‹rule H[where x=B], rule Y›)
done

fix x :: "prop" and A
assume X: "TERM x"
assume Y: "⋀x :: prop. A x"
have "A TERM x"
apply (match X in "PROP y" for y ⇒ ‹rule Y[where x="PROP y"]›)
done
end

subsection ‹Proper context for method parameters›

method add_simp methods m uses f = (match f in H[simp]:_ ⇒ m)

method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ ⇒ m)

method rule_my_thms = (rule my_thms_named)
method rule_my_thms' declares my_thms_named = (rule my_thms_named)

lemma
assumes A: A and B: B
shows
"(A ∨ B) ∧ A ∧ A ∧ A"
apply (intro conjI)
done

subsection ‹Shallow parser tests›

method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = fail

lemma True
by (all_args True False - fail f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)

subsection ‹Method name internalization test›

method test2 = (simp)

method simp = fail

lemma "A ⟹ A" by test2

subsection ‹Dynamic facts›

named_theorems my_thms_named'

method foo_method1 for x =
(match my_thms_named' [of (unchecked) x] in R: "PROP ?H" ⇒ ‹rule R›)

lemma
assumes A [my_thms_named']: "⋀x. A x"
shows "A y"
by (foo_method1 y)

subsection ‹Eisbach method invocation from ML›

method test_method for x y uses r = (print_term x, print_term y, rule r)

method_setup test_method' = ‹
Args.term -- Args.term --
(Scan.lift (Args.\$\$\$ "rule" -- Args.colon) |-- Attrib.thms) >>
(fn ((x, y), r) => fn ctxt =>
Method_Closure.apply_method ctxt \<^method>‹test_method› [x, y] [r] [] ctxt)
›

lemma
fixes a b :: nat
assumes "a = b"
shows "b = a"
apply (test_method a b)?
apply (test_method' a b rule: refl)?
apply (test_method' a b rule: assms [symmetric])?
done

subsection ‹Eisbach methods in locales›

locale my_locale1 = fixes A assumes A: A begin

method apply_A =
(match conclusion in "A" ⇒
‹match A in U:"A" ⇒
‹print_term A, print_fact A, rule U››)

end

locale my_locale2 = fixes B assumes B: B begin

interpretation my_locale1 B by (unfold_locales; rule B)

lemma B by apply_A

end

context fixes C assumes C: C begin

interpretation my_locale1 C by (unfold_locales; rule C)

lemma C by apply_A

end

context begin

interpretation my_locale1 "True ⟶ True" by (unfold_locales; blast)

lemma "True ⟶ True" by apply_A

end

locale locale_poly = fixes P assumes P: "⋀x :: 'a. P x" begin

method solve_P for z :: 'a = (rule P[where x = z])

end

context begin

interpretation locale_poly "λx:: nat. 0 ≤ x" by (unfold_locales; blast)

lemma "0 ≤ (n :: nat)" by (solve_P n)

end

subsection ‹Mutual recursion via higher-order methods›

experiment begin

method inner_method methods passed_method = (rule conjI; passed_method)

method outer_method = (inner_method ‹outer_method› | assumption)

lemma "Q ⟹ R ⟹ P ⟹ (Q ∧ R) ∧ P"
by outer_method

end

end
```