--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/LocaleInst.thy Fri Apr 02 14:08:30 2004 +0200
@@ -0,0 +1,114 @@
+(* Title: FOL/ex/LocaleInst.thy
+ ID: $Id$
+ Author: Clemens Ballarin
+ Copyright (c) 2004 by Clemens Ballarin
+
+Test of locale instantiation mechanism, also provides a few examples.
+*)
+
+header {* Test of Locale instantiation *}
+
+theory LocaleInst = FOL:
+
+ML {* set show_hyps *}
+
+section {* Locale without assumptions *}
+
+locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
+
+lemma "[| A; B |] ==> A & B"
+proof -
+ instantiate my: L1 txt {* No chained fact required. *}
+ assume B and A txt {* order reversed *}
+ then show "A & B" ..
+ txt {* Applies @{thm my.rev_conjI}. *}
+qed
+
+section {* Simple locale with assumptions *}
+
+typedecl i
+arities i :: "term"
+
+consts bin :: "[i, i] => i" (infixl "#" 60)
+
+axioms i_assoc: "(x # y) # z = x # (y # z)"
+ i_comm: "x # y = y # x"
+
+locale L2 =
+ fixes OP (infixl "+" 60)
+ assumes assoc: "(x + y) + z = x + (y + z)"
+ and comm: "x + y = y + x"
+
+lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
+proof -
+ have "x + (y + z) = (x + y) + z" by (simp add: assoc)
+ also have "... = (y + x) + z" by (simp add: comm)
+ also have "... = y + (x + z)" by (simp add: assoc)
+ finally show ?thesis .
+qed
+
+lemmas (in L2) AC = comm assoc lcomm
+
+lemma "(x::i) # y # z # w = y # x # w # z"
+proof -
+ have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm])
+ then instantiate my: L2
+ txt {* Chained fact required to discharge assumptions of @{text L2}
+ and instantiate parameters. *}
+ show ?thesis by (simp only: my.OP.AC) (* or simply AC *)
+qed
+
+section {* Nested locale with assumptions *}
+
+locale L3 =
+ fixes OP (infixl "+" 60)
+ assumes assoc: "(x + y) + z = x + (y + z)"
+
+locale L4 = L3 +
+ assumes comm: "x + y = y + x"
+
+lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
+proof -
+ have "x + (y + z) = (x + y) + z" by (simp add: assoc)
+ also have "... = (y + x) + z" by (simp add: comm)
+ also have "... = y + (x + z)" by (simp add: assoc)
+ finally show ?thesis .
+qed
+
+lemmas (in L4) AC = comm assoc lcomm
+
+text {* Conceptually difficult locale:
+ 2nd context fragment contains facts with differing metahyps. *}
+
+lemma L4_intro:
+ fixes OP (infixl "+" 60)
+ assumes assoc: "!!x y z. (x + y) + z = x + (y + z)"
+ and comm: "!!x y. x + y = y + x"
+ shows "L4 (op+)"
+ by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm)
+
+lemma "(x::i) # y # z # w = y # x # w # z"
+proof -
+ have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm])
+ then instantiate my: L4
+ show ?thesis by (simp only: my.OP.AC) (* or simply AC *)
+qed
+
+section {* Locale with definition *}
+
+text {* This example is admittedly not very creative :-) *}
+
+locale L5 = L4 + var A +
+ defines A_def: "A == True"
+
+lemma (in L5) lem: A
+ by (unfold A_def) rule
+
+lemma "L5(op #) ==> True"
+proof -
+ assume "L5(op #)"
+ then instantiate my: L5
+ show ?thesis by (rule lem) (* lem instantiated to True *)
+qed
+
+end