Quelle Tests.thy Sprache: Isabelle

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

section \<open>Miscellaneous Eisbach tests\<close>

theory Tests
imports Main Eisbach_Tools
begin

subsection \<open>Named Theorems Tests\<close>

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 \<open>Match Tests\<close>

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 \<Rightarrow> \<open>match premises in Y: "\<And>z. P z" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
    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 \<Rightarrow> \<open>print_term P, print_term x\<close>)
    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: "\<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" \
          \<open>print_fact Y, print_fact Y', intro conjI, rule Y', insert Y', insert Y'[where rr=x]\<close>)
    apply (match premises in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
    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" \<Rightarrow> \<open>rule Y\<close>)
    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" \<Rightarrow> \<open>rule Y\<close>)
    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 \
                                  \<open>match (P) in B \<Rightarrow> fail
                                        \<bar> "\<lambda>a. B" \<Rightarrow> fail
                                        \<bar> _ \<Rightarrow> -,
                                  intro conjI, (rule Y[THEN conjunct1])\<close>)
    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" \<Rightarrow> \<open>rule Y\<close>)
    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 "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
  apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match \<open>K @{thms Y TrueI}\<close> in Y':"?H"  (multi) \<Rightarrow> \<open>rule conjI; (rule Y')?\<close>\<close>)
  apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match \<open>K [@{thm Y}]\<close> in Y':"?H"  (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>)
  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  \<Rightarrow> \<open>print_term f\<close>)

  fix A B C
  assume X: "A \ B" "A \ C" C
  have "A \ B \ C"
    by (match X in H: "A \ ?H" (multi, cut) \
          \<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> fail\<close>
        | 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" \
                     \<open>match premises in H'[thin]: "\<And>x. A x \<and> B" \<Rightarrow>
                      \<open>match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail
                                         \<bar> _ \<Rightarrow> -\<close>
                      ,match premises in H'':"\x. A x \ B" \ fail \ _ \ -\)
    apply (match premises in H:"\x. A x \ B" \ fail
                              \<bar> H':_ \<Rightarrow> \<open>rule H'[THEN conjunct2]\<close>)
    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 _ \<Rightarrow> \<open>insert asms,
            match premises (local) in "B \ C" \ fail
                                  \<bar> H:"C \<and> D" \<Rightarrow> \<open>rule H[THEN conjunct1]\<close>\<close>)
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 \<Rightarrow> \<open>match conclusion in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
  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' \
      \<open>simp add: U\<close> \<bar> "?H" \<Rightarrow> -) | -)
  apply (simp add: A)
  done

subsection \<open>Uses Tests\<close>

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

method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = (rule uses_test\<^sub>1_uses)

lemma assumes A shows A by (uses_test\<^sub>1 uses_test\<^sub>1_uses: assms)

ML \<open>test_internal_fact \<^context> "uses_test\<^sub>1_uses"\<close>

ML \<open>test_internal_fact \<^context> "Tests.uses_test\<^sub>1_uses"\<close>
ML \<open>test_internal_fact \<^context> "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\<close>

subsection \<open>Basic fact passing\<close>

method find_fact for x y :: bool uses facts1 facts2 =
  (match facts1 in U: "x" \<Rightarrow> \<open>insert U,
      match facts2 in U: "y" \<Rightarrow> \<open>insert U\<close>\<close>)

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 \<open>Testing term and fact passing in recursion\<close>

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)\
  \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>)

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\
  \<bar> "A" and "True" \<Rightarrow> \<open>recursion_example' "A" "B" facts: TrueI\<close>
  \<bar> "True" \<Rightarrow> -
  \<bar> "PROP ?P" \<Rightarrow> 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\<^sub>1 uses my_simp\<^sub>1_facts = (simp add: my_simp\<^sub>1_facts)
lemma assumes A shows A by (my_simp\<^sub>1 my_simp\<^sub>1_facts: assms)

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

subsection \<open>Declaration Tests\<close>

named_theorems declare_facts\<^sub>1

method declares_test\<^sub>1 declares declare_facts\<^sub>1 = (rule declare_facts\<^sub>1)

lemma assumes A shows A by (declares_test\<^sub>1 declare_facts\<^sub>1: assms)

lemma assumes A[declare_facts\<^sub>1]: A shows A by declares_test\<^sub>1

subsection \<open>Rule Instantiation Tests\<close>

method my_allE\<^sub>1 for x :: 'a and P :: "'a \<Rightarrow> bool" =
  (erule allE [where x = x and P = P])

lemma "\x. Q x \ Q x" by (my_allE\<^sub>1 x Q)

method my_allE\<^sub>2 for x :: 'a and P :: "'a \<Rightarrow> bool" =
  (erule allE [of P x])

lemma "\x. Q x \ Q x" by (my_allE\<^sub>2 x Q)

method my_allE\<^sub>3 for x :: 'a and P :: "'a \<Rightarrow> bool" =
  (match allE [where 'a = 'a] in X: "\(x :: 'a) P R. \x. P x \ (P x \ R) \ R" \
    \<open>erule X [where x = x and P = P]\<close>)

lemma "\x. Q x \ Q x" by (my_allE\<^sub>3 x Q)

method my_allE\<^sub>4 for x :: 'a and P :: "'a \<Rightarrow> bool" =
  (match allE [where 'a = 'a] in X: "\(x :: 'a) P R. \x. P x \ (P x \ R) \ R" \
    \<open>erule X [of x P]\<close>)

lemma "\x. Q x \ Q x" by (my_allE\<^sub>4 x Q)

subsection \<open>Polymorphism test\<close>

axiomatization foo' :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool"
axiomatization where foo'_ax1: "foo' x y z \<Longrightarrow> z \<and> y"
axiomatization where foo'_ax2: "foo' x y y \<Longrightarrow> x \<and> z"
axiomatization where foo'_ax3: "foo' (x :: int) y y \<Longrightarrow> y \<and> 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 \<Rightarrow> \<open>print_term concl\<close>)

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" \<Rightarrow> \<open>
      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 \<Rightarrow> \<open>
          rule R[of q,simplified first_id_def],
          print_conclusion,
          rule foo
      \<close>\<close>\<close>)
  done

subsection \<open>Unchecked rule instantiation, with the possibility of runtime errors\<close>

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" \<Rightarrow> \<open>rule R\<close>)

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" \<Rightarrow> \<open>rule R\<close>)

  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" \<Rightarrow> \<open>rule R\<close>)

  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 \<open>
structure Data = Generic_Data
(
  type T = thm list;
  val empty: T = [];
  fun merge data : T = Thm.merge_thms data;
);
\<close>

local_setup \<open>Local_Theory.add_thms_dynamic (\<^binding>\<open>test_dyn\<close>, Data.get)\<close>

setup \<open>Context.theory_map (Data.put @{thms TrueI})\<close>

method dynamic_thms_test = (rule test_dyn)

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

declaration \<open>fn phi => Data.put (Morphism.fact phi @{thms A})\<close>

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 \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>)
    done
end

subsection \<open>Proper context for method parameters\<close>

method add_simp methods m uses f = (match f in H[simp]:_ \<Rightarrow> m)

method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ \<Rightarrow> 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 \<open>add_simp simp f: B\<close> f: A)
  apply (add_my_thms rule_my_thms f:A)
  apply (add_my_thms rule_my_thms' f:A)
  apply (add_my_thms \<open>rule my_thms_named\<close> f:A)
  done

subsection \<open>Shallow parser tests\<close>

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 \<open>Method name internalization test\<close>

method test2 = (simp)

method simp = fail

lemma "A \ A" by test2

subsection \<open>Dynamic facts\<close>

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 \<open>Eisbach method invocation from ML\<close>

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>\<open>test_method\<close> [x, y] [r] [] ctxt)
\<close>

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 \<open>Eisbach methods in locales\<close>

locale my_locale1 = fixes A assumes A: A begin

method apply_A =
  (match conclusion in "A" \<Rightarrow>
    \<open>match A in U:"A" \<Rightarrow>
      \<open>print_term A, print_fact A, rule U\<close>\<close>)

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 \<open>Mutual recursion via higher-order methods\<close>

experiment begin

method inner_method methods passed_method = (rule conjI; passed_method)

method outer_method = (inner_method \<open>outer_method\<close> | assumption)

lemma "Q \ R \ P \ (Q \ R) \ P"
  by outer_method

end

end

quality98%

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.