Quelle  Tests.thy

(*  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›

notepad
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› \<bar> _ ==> ‹print_fact Y›)›)
    (*apply (match premises in Y: "\<And>z :: 'b. B z"  \<Rightarrow> \<open>(match premises in Y'[thin]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> fail \<bar> Y': _ \<Rightarrow> -)\<close>)\<close>)*)
    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›
        | simp add: X)


  (* 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" ==> -) | -)
  apply (simp add: A)
  done


subsection ‹Uses Tests›

ML ‹
  fun test_internal_fact ctxt factnm =
  (case 🍋‹Proof_Context.get_thms ctxt factnm› o
      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 🍋 "uses_test🪙1_uses"›

ML ‹test_internal_fact 🍋 "Tests.uses_test🪙1_uses"›
ML ‹test_internal_fact 🍋 "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›)

notepad
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;
 );
 ›

local_setup ‹Local_Theory.add_thms_dynamic (🍋‹test_dyn›, Data.get)›

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


notepad
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)
  apply (add_simp ‹add_simp simp f: B› f: A)
  apply (add_my_thms rule_my_thms f:A)
  apply (add_my_thms rule_my_thms' f:A)
  apply (add_my_thms ‹rule my_thms_named› f:A)
  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 🍋‹test_method› [
›

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