--- a/CookBook/Package/Ind_Code.thy Sat Mar 14 00:48:22 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy Mon Mar 16 00:12:32 2009 +0100
@@ -7,35 +7,72 @@
subsection {* Definitions *}
text {*
- If we give it a term and a constant name, it will define the
- constant as the term.
+ @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
+
+ @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
+
+ @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
+
+ @{text [display] "ind ::= \<And>zs. pred zs \<Longrightarrow> rules[preds::=Ps] \<Longrightarrow> P zs"}
+
+ @{text [display] "oind ::= \<forall>zs. pred zs \<longrightarrow> orules[preds::=Ps] \<longrightarrow> P zs"}
+
+ So we have @{text "pred zs"} and @{text "orules[preds::=Ps]"}; have to show
+ @{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\<forall>preds. orules \<longrightarrow> pred zs"}.
+ Instantiating the @{text "preds"} with @{text "Ps"} gives
+ @{text "orules[preds::=Ps] \<longrightarrow> P zs"}. So we can conclude with @{text "P zs"}.
+
+ We have to show @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"};
+ expanding the defs
+
+ @{text [display]
+ "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ts"}
+
+ so we have @{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},
+ @{text "orules"}; and have to show @{text "pred ts"}
+
+ the @{text "orules"} are of the form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}.
+
+ using the @{text "As"} we ????
*}
-ML{*fun make_defs ((binding, syn), trm) lthy =
+
+text {*
+ First we have to produce for each predicate its definitions of the form
+
+ @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
+
+ We use the following wrapper function to actually make the definition via
+ @{ML LocalTheory.define}. The function takes a predicate name, a syntax
+ annotation and a term representing the right-hand side of the definition.
+*}
+
+ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy =
let
- val arg = ((binding, syn), (Attrib.empty_binding, trm))
+ val arg = ((predname, syn), (Attrib.empty_binding, trm))
val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
in
(thm, lthy')
end*}
text {*
- Returns the definition and the local theory in which this definition has
- been made. The @{ML internalK in Thm} is just a flag attached to the
+ Returns the definition (as theorem) and the local theory in which this definition has
+ been made. The @{ML internalK in Thm} in Line 4 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.
+ for tools such as finding theorems in the theorem database. We also
+ use @{ML empty_binding in Attrib} in Line 3, since the definition does not need any
+ theorem attributes.
*}
-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
-*}
+local_setup %gray {* fn lthy =>
+let
+ val arg = ((Binding.name "MyTrue", NoSyn), @{term True})
+ val (def, lthy') = make_defs arg lthy
+ val _ = warning (str_of_thm lthy' def)
+in
+ lthy'
+end *}
text {*
Prints out the theorem @{prop "MyTrue \<equiv> True"}.
@@ -89,8 +126,7 @@
val arg_tys = [@{typ "nat"}]
val def = defs_aux lthy orules preds (pred, arg_tys)
in
- warning (Syntax.string_of_term lthy def);
- lthy
+ warning (Syntax.string_of_term lthy def); lthy
end*}
text {*
@@ -117,6 +153,22 @@
The actual definitions are made in Line 7.
*}
+local_setup {*
+fn lthy =>
+let
+ val rules = [@{prop "even 0"},
+ @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+ @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
+ val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+ val prednames = [Binding.name "even", Binding.name "odd"]
+ val syns = [NoSyn, NoSyn]
+ val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
+ val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
+in
+ warning (str_of_thms lthy' defs); lthy
+end*}
+
+
subsection {* Induction Principles *}
text {* Recall the proof for the induction principle for @{term "even"}: *}
@@ -189,8 +241,22 @@
set up the goals for the induction principles.
*}
-ML {* singleton *}
-ML {* ProofContext.export *}
+ML {*
+fun prove_induction lthy2 defs rules cnewpreds ((pred, newpred), tys) =
+let
+ val zs = replicate (length tys) "z"
+ val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
+ val newargs = map Free (newargnames ~~ tys)
+
+ val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
+ val goal = Logic.list_implies
+ (rules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
+in
+ Goal.prove lthy3 [] [prem] goal
+ (fn {prems, ...} => induction_tac defs prems cnewpreds)
+ |> singleton (ProofContext.export lthy3 lthy2)
+end
+*}
ML %linenosgray{*fun inductions rules defs preds tyss lthy1 =
let
@@ -204,23 +270,10 @@
val cnewpreds = map (cterm_of thy) newpreds
val rules' = map (subst_free (preds ~~ newpreds)) rules
-
- fun prove_induction ((pred, newpred), tys) =
- let
- val zs = replicate (length tys) "z"
- val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
- val newargs = map Free (newargnames ~~ tys)
-
- val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
- val goal = Logic.list_implies
- (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
- in
- Goal.prove lthy3 [] [prem] goal
- (fn {prems, ...} => induction_tac defs prems cnewpreds)
- |> singleton (ProofContext.export lthy3 lthy1)
- end
in
- map prove_induction (preds ~~ newpreds ~~ tyss)
+ map (prove_induction lthy2 defs rules' cnewpreds)
+ (preds ~~ newpreds ~~ tyss)
+ |> ProofContext.export lthy2 lthy1
end*}
ML {*