author | wenzelm |
Wed, 16 Jun 2004 20:37:29 +0200 | |
changeset 14957 | 0e94a1ccc6ae |
parent 14551 | 2cb6ff394bfb |
permissions | -rw-r--r-- |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
1 |
(* Title: FOL/ex/LocaleInst.thy |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
2 |
ID: $Id$ |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
3 |
Author: Clemens Ballarin |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
4 |
Copyright (c) 2004 by Clemens Ballarin |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
5 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
6 |
Test of locale instantiation mechanism, also provides a few examples. |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
7 |
*) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
8 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
9 |
header {* Test of Locale instantiation *} |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
10 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
11 |
theory LocaleInst = FOL: |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
12 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
13 |
ML {* set show_hyps *} |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
14 |
|
14957 | 15 |
subsection {* Locale without assumptions *} |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
16 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
17 |
locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]] |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
18 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
19 |
lemma "[| A; B |] ==> A & B" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
20 |
proof - |
14551 | 21 |
instantiate my: L1 txt {* No chained fact required. *} |
22 |
assume B and A txt {* order reversed *} |
|
23 |
then show "A & B" .. txt {* Applies @{thm my.rev_conjI}. *} |
|
24 |
qed |
|
25 |
||
26 |
locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]] |
|
27 |
||
28 |
lemma "[| A; B |] ==> A & B" |
|
29 |
proof - |
|
30 |
instantiate [intro]: L11 txt {* Attribute supplied at instantiation. *} |
|
31 |
assume B and A |
|
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
32 |
then show "A & B" .. |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
33 |
qed |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
34 |
|
14957 | 35 |
subsection {* Simple locale with assumptions *} |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
36 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
37 |
typedecl i |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
38 |
arities i :: "term" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
39 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
40 |
consts bin :: "[i, i] => i" (infixl "#" 60) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
41 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
42 |
axioms i_assoc: "(x # y) # z = x # (y # z)" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
43 |
i_comm: "x # y = y # x" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
44 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
45 |
locale L2 = |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
46 |
fixes OP (infixl "+" 60) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
47 |
assumes assoc: "(x + y) + z = x + (y + z)" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
48 |
and comm: "x + y = y + x" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
49 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
50 |
lemma (in L2) lcomm: "x + (y + z) = y + (x + z)" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
51 |
proof - |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
52 |
have "x + (y + z) = (x + y) + z" by (simp add: assoc) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
53 |
also have "... = (y + x) + z" by (simp add: comm) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
54 |
also have "... = y + (x + z)" by (simp add: assoc) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
55 |
finally show ?thesis . |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
56 |
qed |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
57 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
58 |
lemmas (in L2) AC = comm assoc lcomm |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
59 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
60 |
lemma "(x::i) # y # z # w = y # x # w # z" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
61 |
proof - |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
62 |
have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm]) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
63 |
then instantiate my: L2 |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
64 |
txt {* Chained fact required to discharge assumptions of @{text L2} |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
65 |
and instantiate parameters. *} |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
66 |
show ?thesis by (simp only: my.OP.AC) (* or simply AC *) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
67 |
qed |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
68 |
|
14957 | 69 |
subsection {* Nested locale with assumptions *} |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
70 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
71 |
locale L3 = |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
72 |
fixes OP (infixl "+" 60) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
73 |
assumes assoc: "(x + y) + z = x + (y + z)" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
74 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
75 |
locale L4 = L3 + |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
76 |
assumes comm: "x + y = y + x" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
77 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
78 |
lemma (in L4) lcomm: "x + (y + z) = y + (x + z)" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
79 |
proof - |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
80 |
have "x + (y + z) = (x + y) + z" by (simp add: assoc) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
81 |
also have "... = (y + x) + z" by (simp add: comm) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
82 |
also have "... = y + (x + z)" by (simp add: assoc) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
83 |
finally show ?thesis . |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
84 |
qed |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
85 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
86 |
lemmas (in L4) AC = comm assoc lcomm |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
87 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
88 |
text {* Conceptually difficult locale: |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
89 |
2nd context fragment contains facts with differing metahyps. *} |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
90 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
91 |
lemma L4_intro: |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
92 |
fixes OP (infixl "+" 60) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
93 |
assumes assoc: "!!x y z. (x + y) + z = x + (y + z)" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
94 |
and comm: "!!x y. x + y = y + x" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
95 |
shows "L4 (op+)" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
96 |
by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
97 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
98 |
lemma "(x::i) # y # z # w = y # x # w # z" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
99 |
proof - |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
100 |
have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm]) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
101 |
then instantiate my: L4 |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
102 |
show ?thesis by (simp only: my.OP.AC) (* or simply AC *) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
103 |
qed |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
104 |
|
14957 | 105 |
subsection {* Locale with definition *} |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
106 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
107 |
text {* This example is admittedly not very creative :-) *} |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
108 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
109 |
locale L5 = L4 + var A + |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
110 |
defines A_def: "A == True" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
111 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
112 |
lemma (in L5) lem: A |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
113 |
by (unfold A_def) rule |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
114 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
115 |
lemma "L5(op #) ==> True" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
116 |
proof - |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
117 |
assume "L5(op #)" |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
118 |
then instantiate my: L5 |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
119 |
show ?thesis by (rule lem) (* lem instantiated to True *) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
120 |
qed |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
121 |
|
14957 | 122 |
subsection {* Instantiation in a context with target *} |
14551 | 123 |
|
124 |
lemma (in L4) (* Target might confuse instantiation command. *) |
|
125 |
fixes A (infixl "$" 60) |
|
126 |
assumes A: "L4(A)" |
|
127 |
shows "(x::i) $ y $ z $ w = y $ x $ w $ z" |
|
128 |
proof - |
|
129 |
from A instantiate A: L4 |
|
130 |
show ?thesis by (simp only: A.OP.AC) |
|
131 |
qed |
|
132 |
||
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
diff
changeset
|
133 |
end |