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