author | wenzelm |
Tue, 01 Nov 2016 01:20:33 +0100 | |
changeset 64439 | 2bafda87b524 |
parent 63186 | dc221b8945f2 |
child 69216 | 1a52baa70aed |
permissions | -rw-r--r-- |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
1 |
(* Title: HOL/Eisbach/Tests.thy |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
2 |
Author: Daniel Matichuk, NICTA/UNSW |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
3 |
*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
4 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
5 |
section \<open>Miscellaneous Eisbach tests\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
6 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
7 |
theory Tests |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
8 |
imports Main Eisbach_Tools |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
9 |
begin |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
10 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
11 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
12 |
subsection \<open>Named Theorems Tests\<close> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
13 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
14 |
named_theorems foo |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
15 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
16 |
method foo declares foo = (rule foo) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
17 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
18 |
lemma |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
19 |
assumes A [foo]: A |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
20 |
shows A |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
21 |
apply foo |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
22 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
23 |
|
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
24 |
method abs_used for P = (match (P) in "\<lambda>a. ?Q" \<Rightarrow> fail \<bar> _ \<Rightarrow> -) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
25 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
26 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
27 |
subsection \<open>Match Tests\<close> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
28 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
29 |
notepad |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
30 |
begin |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
31 |
have dup: "\<And>A. A \<Longrightarrow> A \<Longrightarrow> A" by simp |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
32 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
33 |
fix A y |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
34 |
have "(\<And>x. A x) \<Longrightarrow> A y" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
35 |
apply (rule dup, match premises in Y: "\<And>B. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
36 |
apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
37 |
apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P y" for y \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=y]\<close>\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
38 |
apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P z" for z \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=z]\<close>\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
39 |
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>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
40 |
apply (match premises in Y: "\<And>z :: 'a. P z" for P \<Rightarrow> \<open>match conclusion in "P y" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
41 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
42 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
43 |
assume X: "\<And>x. A x" "A y" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
44 |
have "A y" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
45 |
apply (match X in Y:"\<And>B. A B" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
46 |
apply (match X in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
47 |
apply (match X in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B, print_term x\<close>) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
48 |
apply (insert X) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
49 |
apply (match premises in Y:"\<And>B. A B" and Y':"B y" for B and y :: 'a \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
50 |
apply (match premises in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
51 |
apply (match premises in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
52 |
apply (match conclusion in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
53 |
apply assumption |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
54 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
55 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
56 |
{ |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
57 |
fix B x y |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
58 |
assume X: "\<And>x y. B x x y" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
59 |
have "B x x y" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
60 |
by (match X in Y:"\<And>y. B y y z" for z \<Rightarrow> \<open>rule Y[where y=x]\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
61 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
62 |
fix A B |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
63 |
have "(\<And>x y. A (B x) y) \<Longrightarrow> A (B x) y" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
64 |
by (match premises in Y: "\<And>xx. ?H (B xx)" \<Rightarrow> \<open>rule Y\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
65 |
} |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
66 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
67 |
(* match focusing retains prems *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
68 |
fix B x |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
69 |
have "(\<And>x. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
70 |
apply (match premises in Y: "\<And>z :: 'a. A z" \<Rightarrow> \<open>match premises in Y': "\<And>z :: 'b. B z" \<Rightarrow> \<open>print_fact Y, print_fact Y', rule Y'[where z=x]\<close>\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
71 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
72 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
73 |
(*Attributes *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
74 |
fix C |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
75 |
have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x \<and> B x \<and> A y" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
76 |
apply (intro conjI) |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
77 |
apply (match premises in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce) |
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
78 |
apply (match premises in Y: "\<And>z :: 'a. A z" \<Rightarrow> \<open>match premises in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce\<close>) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
79 |
apply (match premises in Y[thin]: "\<And>z :: 'a. A z" \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>print_fact Y,fail\<close> \<bar> _ \<Rightarrow> \<open>print_fact Y\<close>)\<close>) |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
80 |
(*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>)*) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
81 |
apply assumption |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
82 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
83 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
84 |
fix A B C D |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
85 |
have "\<And>uu'' uu''' uu uu'. (\<And>x :: 'a. A uu' x) \<Longrightarrow> D uu y \<Longrightarrow> (\<And>z. B uu z) \<Longrightarrow> C uu y \<Longrightarrow> (\<And>z y. C uu z) \<Longrightarrow> B uu x \<and> B uu x \<and> C uu y" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
86 |
apply (match premises in Y[thin]: "\<And>z :: 'a. A ?zz' z" and |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
87 |
Y'[thin]: "\<And>rr :: 'b. B ?zz rr" \<Rightarrow> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
88 |
\<open>print_fact Y, print_fact Y', intro conjI, rule Y', insert Y', insert Y'[where rr=x]\<close>) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
89 |
apply (match premises in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
90 |
apply (insert TrueI) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
91 |
apply (match premises in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
92 |
apply assumption |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
93 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
94 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
95 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
96 |
(* Multi-matches. As many facts as match are bound. *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
97 |
fix A B C x |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
98 |
have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
99 |
apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>) |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
100 |
apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
101 |
apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
102 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
103 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
104 |
fix A B C x |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
105 |
have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
106 |
apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>) |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
107 |
apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
108 |
apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
109 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
110 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
111 |
fix A B C P Q and x :: 'a and y :: 'a |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
112 |
have "(\<And>x y :: 'a. A x y \<and> Q) \<Longrightarrow> (\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q) \<Longrightarrow> (\<And>x y. C (x :: 'a) (y :: 'a) \<and> P) \<Longrightarrow> A y x \<and> B y x" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
113 |
by (match premises in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule conjI, rule Y[where z=x,THEN conjunct1], rule Y[THEN conjunct1]\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
114 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
115 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
116 |
(*We may use for-fixes in multi-matches too. All bound facts must agree on the fixed term *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
117 |
fix A B C x |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
118 |
have "(\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> (\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)" |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
119 |
apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
120 |
\<open>match (P) in B \<Rightarrow> fail |
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
121 |
\<bar> "\<lambda>a. B" \<Rightarrow> fail |
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
122 |
\<bar> _ \<Rightarrow> -, |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
123 |
intro conjI, (rule Y[THEN conjunct1])\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
124 |
apply (rule dup) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
125 |
apply (match premises in Y':"\<And>x :: 'a. ?U x \<and> Q x" and Y: "\<And>x :: 'a. Q x \<and> ?U x" (multi) for Q \<Rightarrow> \<open>insert Y[THEN conjunct1]\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
126 |
apply assumption (* Previous match requires that Q is consistent *) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
127 |
apply (match premises in Y: "\<And>z :: 'a. ?A z \<longrightarrow> False" (multi) \<Rightarrow> \<open>print_fact Y, fail\<close> \<bar> "C y" \<Rightarrow> \<open>print_term C\<close>) (* multi-match must bind something *) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
128 |
apply (match premises in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
129 |
apply (match premises in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
130 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
131 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
132 |
(* All bindings must be tried for a particular theorem. |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
133 |
However all combinations are NOT explored. *) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
134 |
fix B A C |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
135 |
assume asms:"\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q" "\<And>x :: 'a. A x x \<and> Q" "\<And>a b. C (a :: 'a) (b :: 'a) \<and> Q" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
136 |
have "B y x \<and> C x y \<and> B x y \<and> C y x \<and> A x x" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
137 |
apply (intro conjI) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
138 |
apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
139 |
apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
140 |
apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
141 |
apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>) |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
142 |
apply (match asms in Y: "\<And>z a. A (z :: 'a) (a :: 'a) \<and> R" for R \<Rightarrow> fail \<bar> _ \<Rightarrow> -) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
143 |
apply (rule asms[THEN conjunct1]) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
144 |
done |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
145 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
146 |
(* Attributes *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
147 |
fix A B C x |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
148 |
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)" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
149 |
apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct1] in Y':"?H" (multi) \<Rightarrow> \<open>intro conjI,rule Y'\<close>\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
150 |
apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct2] in Y':"?H" (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
151 |
apply assumption |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
152 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
153 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
154 |
(* Removed feature for now *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
155 |
(* |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
156 |
fix A B C x |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
157 |
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)" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
158 |
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>) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
159 |
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>) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
160 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
161 |
*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
162 |
(* Testing THEN_ALL_NEW within match *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
163 |
fix A B C x |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
164 |
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)" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
165 |
apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI ; ((rule Y[THEN conjunct1])?); rule Y[THEN conjunct2] \<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
166 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
167 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
168 |
(* Cut tests *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
169 |
fix A B C |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
170 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
171 |
have "D \<and> C \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
172 |
by (((match premises in I: "P \<and> Q" (cut) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
173 |
and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?), simp) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
174 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
175 |
have "D \<and> C \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
176 |
by (match premises in I: "P \<and> Q" (cut 2) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
177 |
and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
178 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
179 |
have "A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
180 |
by (((match premises in I: "P \<and> Q" (cut) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
181 |
and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?, simp) | simp) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
182 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
183 |
fix f x y |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
184 |
have "f x y \<Longrightarrow> f x y" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
185 |
by (match conclusion in "f x y" for f x y \<Rightarrow> \<open>print_term f\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
186 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
187 |
fix A B C |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
188 |
assume X: "A \<and> B" "A \<and> C" C |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
189 |
have "A \<and> B \<and> C" |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
190 |
by (match X in H: "A \<and> ?H" (multi, cut) \<Rightarrow> |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
191 |
\<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> fail\<close> |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
192 |
| simp add: X) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
193 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
194 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
195 |
(* Thinning an inner focus *) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
196 |
(* Thinning should persist within a match, even when on an external premise *) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
197 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
198 |
fix A |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
199 |
have "(\<And>x. A x \<and> B) \<Longrightarrow> B \<and> C \<Longrightarrow> C" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
200 |
apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow> |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
201 |
\<open>match premises in H'[thin]: "\<And>x. A x \<and> B" \<Rightarrow> |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
202 |
\<open>match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail |
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
203 |
\<bar> _ \<Rightarrow> -\<close> |
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
204 |
,match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail \<bar> _ \<Rightarrow> -\<close>) |
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
205 |
apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow> fail |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
206 |
\<bar> H':_ \<Rightarrow> \<open>rule H'[THEN conjunct2]\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
207 |
done |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
208 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
209 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
210 |
(* Local premises *) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
211 |
(* Only match premises which actually existed in the goal we just focused.*) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
212 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
213 |
fix A |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
214 |
assume asms: "C \<and> D" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
215 |
have "B \<and> C \<Longrightarrow> C" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
216 |
by (match premises in _ \<Rightarrow> \<open>insert asms, |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
217 |
match premises (local) in "B \<and> C" \<Rightarrow> fail |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
218 |
\<bar> H:"C \<and> D" \<Rightarrow> \<open>rule H[THEN conjunct1]\<close>\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
219 |
end |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
220 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
221 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
222 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
223 |
(* Testing inner focusing. This fails if we don't smash flex-flex pairs produced |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
224 |
by retrofitting. This needs to be done more carefully to avoid smashing |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
225 |
legitimate pairs.*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
226 |
|
61337 | 227 |
schematic_goal "?A x \<Longrightarrow> A x" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
228 |
apply (match conclusion in "H" for H \<Rightarrow> \<open>match conclusion in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
229 |
apply assumption |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
230 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
231 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
232 |
(* Ensure short-circuit after first match failure *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
233 |
lemma |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
234 |
assumes A: "P \<and> Q" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
235 |
shows "P" |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
236 |
by ((match A in "P \<and> Q" \<Rightarrow> fail \<bar> "?H" \<Rightarrow> -) | simp add: A) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
237 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
238 |
lemma |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
239 |
assumes A: "D \<and> C" "A \<and> B" "A \<longrightarrow> B" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
240 |
shows "A" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
241 |
apply ((match A in U: "P \<and> Q" (cut) and "P' \<longrightarrow> Q'" for P Q P' Q' \<Rightarrow> |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
242 |
\<open>simp add: U\<close> \<bar> "?H" \<Rightarrow> -) | -) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
243 |
apply (simp add: A) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
244 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
245 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
246 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
247 |
subsection \<open>Uses Tests\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
248 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
249 |
ML \<open> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
250 |
fun test_internal_fact ctxt factnm = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
251 |
(case try (Proof_Context.get_thms ctxt) factnm of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
252 |
NONE => () |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
253 |
| SOME _ => error "Found internal fact"); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
254 |
\<close> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
255 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
256 |
method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = (rule uses_test\<^sub>1_uses) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
257 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
258 |
lemma assumes A shows A by (uses_test\<^sub>1 uses_test\<^sub>1_uses: assms) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
259 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
260 |
ML \<open>test_internal_fact @{context} "uses_test\<^sub>1_uses"\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
261 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
262 |
ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1_uses"\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
263 |
ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
264 |
|
63185
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
265 |
subsection \<open>Basic fact passing\<close> |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
266 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
267 |
method find_fact for x y :: bool uses facts1 facts2 = |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
268 |
(match facts1 in U: "x" \<Rightarrow> \<open>insert U, |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
269 |
match facts2 in U: "y" \<Rightarrow> \<open>insert U\<close>\<close>) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
270 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
271 |
lemma assumes A: A and B: B shows "A \<and> B" |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
272 |
apply (find_fact "A" "B" facts1: A facts2: B) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
273 |
apply (rule conjI; assumption) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
274 |
done |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
275 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
276 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
277 |
subsection \<open>Testing term and fact passing in recursion\<close> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
278 |
|
63185
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
279 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
280 |
method recursion_example for x :: bool uses facts = |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
281 |
(match (x) in |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
282 |
"A \<and> B" for A B \<Rightarrow> \<open>(recursion_example A facts: facts, recursion_example B facts: facts)\<close> |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
283 |
\<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
284 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
285 |
lemma |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
286 |
assumes asms: "A" "B" "C" "D" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
287 |
shows "(A \<and> B) \<and> (C \<and> D)" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
288 |
apply (recursion_example "(A \<and> B) \<and> (C \<and> D)" facts: asms) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
289 |
apply simp |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
290 |
done |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
291 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
292 |
(* uses facts are not accumulated *) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
293 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
294 |
method recursion_example' for A :: bool and B :: bool uses facts = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
295 |
(match facts in |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
296 |
H: "A" and H': "B" \<Rightarrow> \<open>recursion_example' "A" "B" facts: H TrueI\<close> |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
297 |
\<bar> "A" and "True" \<Rightarrow> \<open>recursion_example' "A" "B" facts: TrueI\<close> |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
298 |
\<bar> "True" \<Rightarrow> - |
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
299 |
\<bar> "PROP ?P" \<Rightarrow> fail) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
300 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
301 |
lemma |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
302 |
assumes asms: "A" "B" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
303 |
shows "True" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
304 |
apply (recursion_example' "A" "B" facts: asms) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
305 |
apply simp |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
306 |
done |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
307 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
308 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
309 |
(*Method.sections in existing method*) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
310 |
method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = (simp add: my_simp\<^sub>1_facts) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
311 |
lemma assumes A shows A by (my_simp\<^sub>1 my_simp\<^sub>1_facts: assms) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
312 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
313 |
(*Method.sections via Eisbach argument parser*) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
314 |
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) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
315 |
lemma assumes A shows A by (uses_test\<^sub>2 uses_test\<^sub>2_uses: assms) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
316 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
317 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
318 |
subsection \<open>Declaration Tests\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
319 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
320 |
named_theorems declare_facts\<^sub>1 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
321 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
322 |
method declares_test\<^sub>1 declares declare_facts\<^sub>1 = (rule declare_facts\<^sub>1) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
323 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
324 |
lemma assumes A shows A by (declares_test\<^sub>1 declare_facts\<^sub>1: assms) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
325 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
326 |
lemma assumes A[declare_facts\<^sub>1]: A shows A by declares_test\<^sub>1 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
327 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
328 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
329 |
subsection \<open>Rule Instantiation Tests\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
330 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
331 |
method my_allE\<^sub>1 for x :: 'a and P :: "'a \<Rightarrow> bool" = |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
332 |
(erule allE [where x = x and P = P]) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
333 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
334 |
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>1 x Q) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
335 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
336 |
method my_allE\<^sub>2 for x :: 'a and P :: "'a \<Rightarrow> bool" = |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
337 |
(erule allE [of P x]) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
338 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
339 |
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>2 x Q) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
340 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
341 |
method my_allE\<^sub>3 for x :: 'a and P :: "'a \<Rightarrow> bool" = |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
342 |
(match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow> |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
343 |
\<open>erule X [where x = x and P = P]\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
344 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
345 |
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>3 x Q) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
346 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
347 |
method my_allE\<^sub>4 for x :: 'a and P :: "'a \<Rightarrow> bool" = |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
348 |
(match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow> |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
349 |
\<open>erule X [of x P]\<close>) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
350 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
351 |
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>4 x Q) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
352 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
353 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
354 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
355 |
subsection \<open>Polymorphism test\<close> |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
356 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
357 |
axiomatization foo' :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
358 |
axiomatization where foo'_ax1: "foo' x y z \<Longrightarrow> z \<and> y" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
359 |
axiomatization where foo'_ax2: "foo' x y y \<Longrightarrow> x \<and> z" |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
360 |
axiomatization where foo'_ax3: "foo' (x :: int) y y \<Longrightarrow> y \<and> y" |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
361 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
362 |
lemmas my_thms = foo'_ax1 foo'_ax2 foo'_ax3 |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
363 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
364 |
definition first_id where "first_id x = x" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
365 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
366 |
lemmas my_thms' = my_thms[of "first_id x" for x] |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
367 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
368 |
method print_conclusion = (match conclusion in concl for concl \<Rightarrow> \<open>print_term concl\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
369 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
370 |
lemma |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
371 |
assumes foo: "\<And>x (y :: bool). foo' (A x) B (A x)" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
372 |
shows "\<And>z. A z \<and> B" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
373 |
apply |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
374 |
(match conclusion in "f x y" for f y and x :: "'d :: type" \<Rightarrow> \<open> |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
375 |
match my_thms' in R:"\<And>(x :: 'f :: type). ?P (first_id x) \<Longrightarrow> ?R" |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
376 |
and R':"\<And>(x :: 'f :: type). ?P' (first_id x) \<Longrightarrow> ?R'" \<Rightarrow> \<open> |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
377 |
match (x) in "q :: 'f" for q \<Rightarrow> \<open> |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
378 |
rule R[of q,simplified first_id_def], |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
379 |
print_conclusion, |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
380 |
rule foo |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
381 |
\<close>\<close>\<close>) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
382 |
done |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
383 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
384 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
385 |
subsection \<open>Unchecked rule instantiation, with the possibility of runtime errors\<close> |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
386 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
387 |
named_theorems my_thms_named |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
388 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
389 |
declare foo'_ax3[my_thms_named] |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
390 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
391 |
method foo_method3 declares my_thms_named = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
392 |
(match my_thms_named[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
393 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
394 |
notepad |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
395 |
begin |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
396 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
397 |
(*FIXME: Shouldn't need unchecked keyword here. See Tests_Failing.thy *) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
398 |
fix A B x |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
399 |
have "foo' x B A \<Longrightarrow> A \<and> B" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
400 |
by (match my_thms[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
401 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
402 |
fix A B x |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
403 |
note foo'_ax1[my_thms_named] |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
404 |
have "foo' x B A \<Longrightarrow> A \<and> B" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
405 |
by (match my_thms_named[where x=z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
406 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
407 |
fix A B x |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
408 |
note foo'_ax1[my_thms_named] foo'_ax2[my_thms_named] foo'_ax3[my_thms_named] |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
409 |
have "foo' x B A \<Longrightarrow> A \<and> B" |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
410 |
by foo_method3 |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
411 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
412 |
end |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
413 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
414 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
415 |
ML \<open> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
416 |
structure Data = Generic_Data |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
417 |
( |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
418 |
type T = thm list; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
419 |
val empty: T = []; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
420 |
val extend = I; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
421 |
fun merge data : T = Thm.merge_thms data; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
422 |
); |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
423 |
\<close> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
424 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
425 |
local_setup \<open>Local_Theory.add_thms_dynamic (@{binding test_dyn}, Data.get)\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
426 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
427 |
setup \<open>Context.theory_map (Data.put @{thms TrueI})\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
428 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
429 |
method dynamic_thms_test = (rule test_dyn) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
430 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
431 |
locale foo = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
432 |
fixes A |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
433 |
assumes A : "A" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
434 |
begin |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
435 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
436 |
local_setup |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
437 |
\<open>Local_Theory.declaration {pervasive = false, syntax = false} |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
438 |
(fn phi => Data.put (Morphism.fact phi @{thms A}))\<close> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
439 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
440 |
lemma A by dynamic_thms_test |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
441 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
442 |
end |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
443 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
444 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
445 |
notepad |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
446 |
begin |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
447 |
fix A x |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
448 |
assume X: "\<And>x. A x" |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
449 |
have "A x" |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
450 |
by (match X in H[of x]:"\<And>x. A x" \<Rightarrow> \<open>print_fact H,match H in "A x" \<Rightarrow> \<open>rule H\<close>\<close>) |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
451 |
|
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
452 |
fix A x B |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
453 |
assume X: "\<And>x :: bool. A x \<Longrightarrow> B" "\<And>x. A x" |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
454 |
assume Y: "A B" |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
455 |
have "B \<and> B \<and> B \<and> B \<and> B \<and> B" |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
456 |
apply (intro conjI) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
457 |
apply (match X in H[OF X(2)]:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H,rule H\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
458 |
apply (match X in H':"\<And>x. A x" and H[OF H']:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H',print_fact H,rule H\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
459 |
apply (match X in H[of Q]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H, rule Y\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
460 |
apply (match X in H[of Q,OF Y]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
461 |
apply (match X in H[OF Y,intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>print_fact H,fastforce\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
462 |
apply (match X in H[intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>rule H[where x=B], rule Y\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
463 |
done |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
464 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
465 |
fix x :: "prop" and A |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
466 |
assume X: "TERM x" |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
467 |
assume Y: "\<And>x :: prop. A x" |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
468 |
have "A TERM x" |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
469 |
apply (match X in "PROP y" for y \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
470 |
done |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
471 |
end |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
472 |
|
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
473 |
subsection \<open>Proper context for method parameters\<close> |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
474 |
|
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
475 |
method add_simp methods m uses f = (match f in H[simp]:_ \<Rightarrow> m) |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
476 |
|
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
477 |
method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ \<Rightarrow> m) |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
478 |
|
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
479 |
method rule_my_thms = (rule my_thms_named) |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
480 |
method rule_my_thms' declares my_thms_named = (rule my_thms_named) |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
481 |
|
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
482 |
lemma |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
483 |
assumes A: A and B: B |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
484 |
shows |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
485 |
"(A \<or> B) \<and> A \<and> A \<and> A" |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
486 |
apply (intro conjI) |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
487 |
apply (add_simp \<open>add_simp simp f: B\<close> f: A) |
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
488 |
apply (add_my_thms rule_my_thms f:A) |
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
489 |
apply (add_my_thms rule_my_thms' f:A) |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
490 |
apply (add_my_thms \<open>rule my_thms_named\<close> f:A) |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
491 |
done |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
492 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
493 |
|
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
494 |
subsection \<open>Shallow parser tests\<close> |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
495 |
|
61813 | 496 |
method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = fail |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
497 |
|
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
498 |
lemma True |
61912
ad710de5c576
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
wenzelm
parents:
61813
diff
changeset
|
499 |
by (all_args True False - fail f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
500 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
501 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
502 |
subsection \<open>Method name internalization test\<close> |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
503 |
|
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
504 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
505 |
method test2 = (simp) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
506 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
507 |
method simp = fail |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
508 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
509 |
lemma "A \<Longrightarrow> A" by test2 |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
510 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
511 |
|
62078
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
512 |
subsection \<open>Dynamic facts\<close> |
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
513 |
|
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
514 |
named_theorems my_thms_named' |
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
515 |
|
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
516 |
method foo_method1 for x = |
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
517 |
(match my_thms_named' [of (unchecked) x] in R: "PROP ?H" \<Rightarrow> \<open>rule R\<close>) |
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
518 |
|
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
519 |
lemma |
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
520 |
assumes A [my_thms_named']: "\<And>x. A x" |
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
521 |
shows "A y" |
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
522 |
by (foo_method1 y) |
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
523 |
|
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62075
diff
changeset
|
524 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
525 |
subsection \<open>Eisbach method invocation from ML\<close> |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
526 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
527 |
method test_method for x y uses r = (print_term x, print_term y, rule r) |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
528 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
529 |
method_setup test_method' = \<open> |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
530 |
Args.term -- Args.term -- |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
531 |
(Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >> |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
532 |
(fn ((x, y), r) => fn ctxt => |
62075 | 533 |
Method_Closure.apply_method ctxt @{method test_method} [x, y] [r] [] ctxt); |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
534 |
\<close> |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
535 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
536 |
lemma |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
537 |
fixes a b :: nat |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
538 |
assumes "a = b" |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
539 |
shows "b = a" |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
540 |
apply (test_method a b)? |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
541 |
apply (test_method' a b rule: refl)? |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
542 |
apply (test_method' a b rule: assms [symmetric])? |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
543 |
done |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
61912
diff
changeset
|
544 |
|
63185
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
545 |
subsection \<open>Eisbach methods in locales\<close> |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
546 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
547 |
locale my_locale1 = fixes A assumes A: A begin |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
548 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
549 |
method apply_A = |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
550 |
(match conclusion in "A" \<Rightarrow> |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
551 |
\<open>match A in U:"A" \<Rightarrow> |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
552 |
\<open>print_term A, print_fact A, rule U\<close>\<close>) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
553 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
554 |
end |
63185
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
555 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
556 |
locale my_locale2 = fixes B assumes B: B begin |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
557 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
558 |
interpretation my_locale1 B by (unfold_locales; rule B) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
559 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
560 |
lemma B by apply_A |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
561 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
562 |
end |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
563 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
564 |
context fixes C assumes C: C begin |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
565 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
566 |
interpretation my_locale1 C by (unfold_locales; rule C) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
567 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
568 |
lemma C by apply_A |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
569 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
570 |
end |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
571 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
572 |
context begin |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
573 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
574 |
interpretation my_locale1 "True \<longrightarrow> True" by (unfold_locales; blast) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
575 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
576 |
lemma "True \<longrightarrow> True" by apply_A |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
577 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
578 |
end |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
579 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
580 |
locale locale_poly = fixes P assumes P: "\<And>x :: 'a. P x" begin |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
581 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
582 |
method solve_P for z :: 'a = (rule P[where x = z]) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
583 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
584 |
end |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
585 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
586 |
context begin |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
587 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
588 |
interpretation locale_poly "\<lambda>x:: nat. 0 \<le> x" by (unfold_locales; blast) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
589 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
590 |
lemma "0 \<le> (n :: nat)" by (solve_P n) |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
591 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
592 |
end |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
593 |
|
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
594 |
subsection \<open>Mutual recursion via higher-order methods\<close> |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
595 |
|
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
596 |
experiment begin |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
597 |
|
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
598 |
method inner_method methods passed_method = (rule conjI; passed_method) |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
599 |
|
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
600 |
method outer_method = (inner_method \<open>outer_method\<close> | assumption) |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
601 |
|
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
602 |
lemma "Q \<Longrightarrow> R \<Longrightarrow> P \<Longrightarrow> (Q \<and> R) \<and> P" |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
603 |
by outer_method |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
604 |
|
63185
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62078
diff
changeset
|
605 |
end |
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
606 |
|
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
607 |
end |