--- a/CookBook/Package/Ind_Code.thy Fri Mar 13 12:21:44 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy Fri Mar 13 16:57:16 2009 +0100
@@ -1,5 +1,5 @@
theory Ind_Code
-imports "../Base" Simple_Inductive_Package Ind_Prelims
+imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims
begin
section {* Code *}
@@ -14,24 +14,31 @@
ML{*fun make_defs ((binding, syn), trm) lthy =
let
val arg = ((binding, syn), (Attrib.empty_binding, trm))
- val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy
+ val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
in
- (thm, lthy)
+ (thm, lthy')
end*}
text {*
Returns the definition and the local theory in which this definition has
- been made. What is @{ML Thm.internalK}?
+ been made. The @{ML internalK in Thm} is just a flag attached to the
+ theorem (others flags are @{ML definitionK in Thm} or @{ML axiomK in Thm}).
+ These flags just classify theorems and have no significant meaning, except
+ for tools such as finding theorems in the theorem database.
*}
-ML{*let
- val lthy = TheoryTarget.init NONE @{theory}
-in
- make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy
-end*}
+local_setup {*
+ fn lthy =>
+ let
+ val (def, lthy') = make_defs ((Binding.name "MyTrue", NoSyn), @{term True}) lthy
+ val _ = warning (str_of_thm lthy' def)
+ in
+ lthy'
+ end
+*}
text {*
- Why is the output of MyTrue blue?
+ Prints out the theorem @{prop "MyTrue \<equiv> True"}.
*}
text {*
@@ -41,12 +48,12 @@
term.
*}
-ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_types) =
+ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
let
fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
val fresh_args =
- arg_types
+ arg_tys
|> map (pair "z")
|> Variable.variant_frees lthy orules
|> map Free
@@ -70,18 +77,22 @@
the (fresh) arguments of the predicate.
*}
-ML{*let
- val orules = [@{term "even 0"},
- @{term "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
- @{term "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}]
+
+local_setup {*
+fn lthy =>
+let
+ val orules = [@{prop "even 0"},
+ @{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
+ @{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}]
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+ val pred = @{term "even::nat\<Rightarrow>bool"}
+ val arg_tys = [@{typ "nat"}]
+ val def = defs_aux lthy orules preds (pred, arg_tys)
in
- warning
- (Syntax.string_of_term @{context}
- (defs_aux @{context} orules preds (@{term "even::nat\<Rightarrow>bool"}, [@{typ "nat"}])))
+ warning (Syntax.string_of_term lthy def);
+ lthy
end*}
-
text {*
The arguments of the main function for the definitions are
the intro rules; the predicates and their names, their syntax
@@ -108,6 +119,23 @@
subsection {* Induction Principles *}
+text {* Recall the proof for the induction principle for @{term "even"}: *}
+
+lemma
+ assumes prems: "even n"
+ shows "P 0 \<Longrightarrow>
+ (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
+apply(atomize (full))
+apply(cut_tac prems)
+apply(unfold even_def)
+apply(drule spec[where x=P])
+apply(drule spec[where x=Q])
+apply(assumption)
+done
+
+
+text {* We need to be able to instantiate universal quantifiers. *}
+
ML{*fun inst_spec ct =
Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*}
@@ -120,40 +148,30 @@
*}
lemma "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \<Longrightarrow> True"
-apply (tactic {* EVERY' (map (dtac o inst_spec)
- [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*})
+apply (tactic {*
+ let
+ val ctrms = [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]
+ in
+ EVERY1 (map (dtac o inst_spec) ctrms)
+ end *})
txt {* \begin{minipage}{\textwidth}
@{subgoals}
\end{minipage}*}
(*<*)oops(*>*)
-
-lemma
- assumes "even n"
- shows "P 0 \<Longrightarrow>
- (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
-apply(atomize (full))
-apply(cut_tac prems)
-apply(unfold even_def)
-apply(drule spec[where x=P])
-apply(drule spec[where x=Q])
-apply(assumption)
-done
-
text {*
- The tactic for proving the induction rules:
+ Now the tactic for proving the induction rules:
*}
ML{*fun induction_tac defs prems insts =
- EVERY1 [K (print_tac "start"),
- ObjectLogic.full_atomize_tac,
+ EVERY1 [ObjectLogic.full_atomize_tac,
cut_facts_tac prems,
K (rewrite_goals_tac defs),
EVERY' (map (dtac o inst_spec) insts),
assume_tac]*}
lemma
- assumes "even n"
+ assumes prems: "even n"
shows "P 0 \<Longrightarrow>
(\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
apply(tactic {*
@@ -165,6 +183,7 @@
end *})
done
+
text {*
While the generic proof is relatively simple, it is a bit harder to
set up the goals for the induction principles.
@@ -209,12 +228,13 @@
@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
val defs = [@{thm even_def}, @{thm odd_def}]
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
- val tyss = [[@{typ "nat"}],[@{typ "nat"}]]
+ val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
in
inductions rules defs preds tyss @{context}
end
*}
+
subsection {* Introduction Rules *}
ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
@@ -266,7 +286,6 @@
end *})
done
-
ML{*fun introductions rules preds defs lthy =
let
fun prove_intro (i, goal) =
@@ -276,6 +295,8 @@
map_index prove_intro rules
end*}
+text {* main internal function *}
+
ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy =
let
val syns = map snd pred_specs
@@ -308,10 +329,9 @@
|> snd
end*}
-
ML{*fun read_specification' vars specs lthy =
let
- val specs' = map (fn (a, s) => [(a, [s])]) specs
+ val specs' = map (fn (a, s) => (a, [s])) specs
val ((varst, specst), _) =
Specification.read_specification vars specs' lthy
val specst' = map (apsnd the_single) specst
--- a/CookBook/Package/Ind_Interface.thy Fri Mar 13 12:21:44 2009 +0100
+++ b/CookBook/Package/Ind_Interface.thy Fri Mar 13 16:57:16 2009 +0100
@@ -277,7 +277,7 @@
@{ML [display] "Specification.read_specification:
(Binding.binding * string option * mixfix) list -> (*{variables}*)
- (Attrib.binding * string list) list list -> (*{rules}*)
+ (Attrib.binding * string list) list -> (*{rules}*)
local_theory ->
(((Binding.binding * typ) * mixfix) list *
(Attrib.binding * term list) list) *
@@ -315,8 +315,8 @@
"Specification.read_specification
[(Binding.name \"trcl\", NONE, NoSyn),
(Binding.name \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)]
- [[((Binding.name \"base\", []), [\"trcl r x x\"])],
- [((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]]
+ [((Binding.name \"base\", []), [\"trcl r x x\"]),
+ ((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]
@{context}"
"((\<dots>,
[(\<dots>,
--- a/CookBook/Package/simple_inductive_package.ML Fri Mar 13 12:21:44 2009 +0100
+++ b/CookBook/Package/simple_inductive_package.ML Fri Mar 13 16:57:16 2009 +0100
@@ -198,7 +198,7 @@
(* @chunk read_specification *)
fun read_specification' vars specs lthy =
let
- val specs' = map (fn (a, s) => [(a, [s])]) specs
+ val specs' = map (fn (a, s) => (a, [s])) specs
val ((varst, specst), _) =
Specification.read_specification vars specs' lthy
val specst' = map (apsnd the_single) specst
--- a/CookBook/chunks.ML Fri Mar 13 12:21:44 2009 +0100
+++ b/CookBook/chunks.ML Fri Mar 13 16:57:16 2009 +0100
@@ -49,7 +49,7 @@
fun declare_chunk name thy =
(Sign.full_bname thy name,
- ChunkData.map (snd o NameSpace.bind (Sign.naming_of thy)
+ ChunkData.map (snd o NameSpace.define (Sign.naming_of thy)
(Binding.name name, ([], stamp ()))) thy
handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name));
Binary file cookbook.pdf has changed