--- a/CookBook/Appendix.thy Sun Mar 08 20:53:00 2009 +0000
+++ b/CookBook/Appendix.thy Tue Mar 10 13:20:46 2009 +0000
@@ -18,6 +18,12 @@
user space type systems (in the form that already exists)
unification and typing algorithms
+
+ useful datastructures:
+
+ discrimination nets
+
+ association lists
*}
end
--- a/CookBook/Package/Ind_Code.thy Sun Mar 08 20:53:00 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy Tue Mar 10 13:20:46 2009 +0000
@@ -1,26 +1,178 @@
theory Ind_Code
-imports "../Base" Simple_Inductive_Package
+imports "../Base" Simple_Inductive_Package Ind_Prelims
begin
+section {* Code *}
+
+subsection {* Definitions *}
+
+text {*
+ If we give it a term and a constant name, it will define the
+ constant as the term.
+*}
+
+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
+in
+ (thm, lthy)
+end*}
+
+text {*
+ Returns the definition and the local theory in which this definition has
+ been made. What is @{ML Thm.internalK}?
+*}
+
+ML {*let
+ val lthy = TheoryTarget.init NONE @{theory}
+in
+ make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy
+end*}
+
+text {*
+ Why is the output of MyTrue blue?
+*}
+
+text {*
+ Constructs the term for the definition: the main arguments are a predicate
+ and the types of the arguments, it also expects orules which are the
+ intro rules in the object logic; preds which are all predicates. returns the
+ term.
+*}
+
+ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_types) =
+let
+ fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
+
+ val fresh_args =
+ arg_types
+ |> map (pair "z")
+ |> Variable.variant_frees lthy orules
+ |> map Free
+in
+ list_comb (pred, fresh_args)
+ |> fold_rev (curry HOLogic.mk_imp) orules
+ |> fold_rev mk_all preds
+ |> fold_rev lambda fresh_args
+end*}
+
+text {*
+ The lines 5-9 produce fresh arguments with which the predicate can be applied.
+ For this it pairs every type with a string @{text [quotes] "z"} (Line 7); then
+ generates variants for all these strings (names) so that they are unique w.r.t.~to
+ the intro rules; in Line 9 it generates the corresponding variable terms for these
+ unique names.
+
+ The unique free variables are applied to the predicate (Line 11); then
+ the intro rules are attached as preconditions (Line 12); in Line 13 we
+ quantify over all predicates; and in line 14 we just abstract over all
+ the (fresh) arguments of the predicate.
+*}
+
text {*
- What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK?
+ The arguments of the main function for the definitions are
+ the intro rules; the predicates and their names, their syntax
+ annotations and the argument types of each predicate. It
+ returns a theorem list (the definitions) and a local
+ theory where the definitions are made
+*}
+
+ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
+let
+ val thy = ProofContext.theory_of lthy
+ val orules = map (ObjectLogic.atomize_term thy) rules
+ val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss)
+in
+ fold_map make_defs (prednames ~~ syns ~~ defs) lthy
+end*}
+
+text {*
+ In line 4 we generate the intro rules in the object logic; for this we have to
+ obtain the theory behind the local theory (Line 3); with this we can
+ call @{ML defs_aux} to generate the terms for the left-hand sides.
+ The actual definitions are made in Line 7.
+*}
+
+subsection {* Introduction Rules *}
+
+ML{*fun inst_spec ct =
+ Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*}
+
+text {*
+ Instantiates the @{text "x"} in @{thm spec[no_vars]} with a @{ML_type cterm}.
+*}
+
+text {*
+ Instantiates universal qantifications in the premises
+*}
+
+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*})
+(*<*)oops(*>*)
+
+text {*
+ The tactic for proving the induction rules:
*}
+ML{*fun induction_tac defs prems insts =
+ 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 asm: "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 {* induction_tac [@{thm even_def}, @{thm odd_def}] [@{thm asm}]
+ [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})
+done
+
+ML %linenosgray{*fun inductions rules defs preds Tss lthy1 =
+let
+ val Ps = replicate (length preds) "P"
+ val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1
+
+ val thy = ProofContext.theory_of lthy2
+
+ val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss
+ val newpreds = map Free (newprednames ~~ Tss')
+ val cnewpreds = map (cterm_of thy) newpreds
+ val rules' = map (subst_free (preds ~~ newpreds)) rules
+
+ fun prove_induction ((pred, newpred), Ts) =
+ let
+ val zs = replicate (length Ts) "z"
+ val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
+ val newargs = map Free (newargnames ~~ Ts)
+
+ 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 ~~ Tss)
+end*}
+
+ML {* Goal.prove *}
+ML {* singleton *}
+ML {* ProofContext.export *}
text {*
- @{ML_chunk [display,gray] definitions_aux}
- @{ML_chunk [display,gray,linenos] definitions}
-
*}
text {*
-
- @{ML_chunk [display,gray] induction_rules}
+ @{ML_chunk [display,gray] subproof1}
-*}
-
-text {*
+ @{ML_chunk [display,gray] subproof2}
@{ML_chunk [display,gray] intro_rules}
--- a/CookBook/Package/Simple_Inductive_Package.thy Sun Mar 08 20:53:00 2009 +0000
+++ b/CookBook/Package/Simple_Inductive_Package.thy Tue Mar 10 13:20:46 2009 +0000
@@ -1,8 +1,62 @@
theory Simple_Inductive_Package
-imports Main
-uses ("simple_inductive_package.ML")
+imports Main "../Base"
+uses "simple_inductive_package.ML"
begin
+(*
+simple_inductive
+ trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ base: "trcl R x x"
+| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
+
+thm trcl_def
+thm trcl.induct
+thm trcl.intros
+
+simple_inductive
+ even and odd
+where
+ even0: "even 0"
+| evenS: "odd n \<Longrightarrow> even (Suc n)"
+| oddS: "even n \<Longrightarrow> odd (Suc n)"
+
+thm even_def odd_def
+thm even.induct odd.induct
+thm even0
+thm evenS
+thm oddS
+thm even_odd.intros
+
+simple_inductive
+ accpart for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ accpartI: "(\<forall>y. r y x \<longrightarrow> accpart r y) \<Longrightarrow> accpart r x"
+
+thm accpart_def
+thm accpart.induct
+thm accpartI
+
+locale rel =
+ fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+
+simple_inductive (in rel) accpart'
+where
+ accpartI': "\<And>x. (\<And>y. r y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
+
+
+context rel
+begin
+ thm accpartI'
+ thm accpart'.induct
+end
+
+thm rel.accpartI'
+thm rel.accpart'.induct
+
+
+lemma "True" by simp
+*)
use_chunks "simple_inductive_package.ML"
--- a/CookBook/Package/simple_inductive_package.ML Sun Mar 08 20:53:00 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Tue Mar 10 13:20:46 2009 +0000
@@ -18,107 +18,143 @@
structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
struct
-fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
-
-(* @chunk definitions_aux *)
-fun definitions_aux ((binding, syn), trm) lthy =
+(* @chunk make_definitions *)
+fun make_defs ((binding, syn), trm) lthy =
let
- val ((_, (_, thm)), lthy) =
- LocalTheory.define Thm.internalK ((binding, syn), (Attrib.empty_binding, trm)) lthy
+ val arg = ((binding, syn), (Attrib.empty_binding, trm))
+ val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy
in
(thm, lthy)
end
(* @end *)
+(* @chunk definitions_aux *)
+fun defs_aux lthy orules preds params (pred, arg_types) =
+let
+ fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
+
+ val fresh_args =
+ arg_types
+ |> map (pair "z")
+ |> Variable.variant_frees lthy orules
+ |> map Free
+in
+ list_comb (pred, fresh_args)
+ |> fold_rev (curry HOLogic.mk_imp) orules
+ |> fold_rev mk_all preds
+ |> fold_rev lambda (params @ fresh_args)
+end
+(* @end *)
+
(* @chunk definitions *)
-fun definitions params rules preds preds' Tss lthy =
+fun definitions rules params preds prednames syns arg_typess lthy =
let
val thy = ProofContext.theory_of lthy
- val rules' = map (ObjectLogic.atomize_term thy) rules
+ val orules = map (ObjectLogic.atomize_term thy) rules
+ val defs =
+ map (defs_aux lthy orules preds params) (preds ~~ arg_typess)
in
- fold_map (fn ((((R, _), syn), pred), Ts) =>
- let
- val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts))
-
- val t0 = list_comb (pred, zs);
- val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0;
- val t2 = fold_rev mk_all preds' t1;
- val t3 = fold_rev lambda (params @ zs) t2;
- in
- definitions_aux ((R, syn), t3)
- end) (preds ~~ preds' ~~ Tss) lthy
+ fold_map make_defs (prednames ~~ syns ~~ defs) lthy
end
(* @end *)
fun inst_spec ct =
Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
+(* @chunk induction_tac *)
+fun induction_tac defs prems insts =
+ EVERY1 [ObjectLogic.full_atomize_tac,
+ cut_facts_tac prems,
+ K (rewrite_goals_tac defs),
+ EVERY' (map (dtac o inst_spec) insts),
+ assume_tac]
+(* @end *)
+
+(* @chunk induction_rules *)
+fun inductions rules defs parnames preds Tss lthy1 =
+let
+ val (_, lthy2) = Variable.add_fixes parnames lthy1
+
+ val Ps = replicate (length preds) "P"
+ val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2
+
+ val thy = ProofContext.theory_of lthy3
+
+ val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss
+ val newpreds = map Free (newprednames ~~ Tss')
+ val cnewpreds = map (cterm_of thy) newpreds
+ val rules' = map (subst_free (preds ~~ newpreds)) rules
+
+ fun prove_induction ((pred, newpred), Ts) =
+ let
+ val (newargnames, lthy4) =
+ Variable.variant_fixes (replicate (length Ts) "z") lthy3;
+ val newargs = map Free (newargnames ~~ Ts)
+
+ 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 lthy4 [] [prem] goal
+ (fn {prems, ...} => induction_tac defs prems cnewpreds)
+ |> singleton (ProofContext.export lthy4 lthy1)
+ end
+in
+ map prove_induction (preds ~~ newpreds ~~ Tss)
+end
+(* @end *)
+
val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp});
-(* @chunk induction_rules *)
-fun INDUCTION rules preds' Tss defs lthy1 lthy2 =
-let
- val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2;
- val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss);
- val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps;
- val rules'' = map (subst_free (preds' ~~ Ps)) rules;
-
- fun prove_indrule ((R, P), Ts) =
+(* @chunk subproof1 *)
+fun subproof2 prem params2 prems2 =
+ SUBPROOF (fn {prems, ...} =>
let
- val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3;
- val zs = map Free (znames ~~ Ts)
+ val prem' = prems MRS prem;
+ val prem'' =
+ case prop_of prem' of
+ _ $ (Const (@{const_name All}, _) $ _) =>
+ prem' |> all_elims params2
+ |> imp_elims prems2
+ | _ => prem';
+ in
+ rtac prem'' 1
+ end)
+(* @end *)
- val prem = HOLogic.mk_Trueprop (list_comb (R, zs))
- val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs)))
+(* @chunk subproof2 *)
+fun subproof1 rules preds i =
+ SUBPROOF (fn {params, prems, context = ctxt', ...} =>
+ let
+ val (prems1, prems2) = chop (length prems - length rules) prems;
+ val (params1, params2) = chop (length params - length preds) params;
in
- Goal.prove lthy4 [] [prem] goal
- (fn {prems, ...} => EVERY1
- ([ObjectLogic.full_atomize_tac,
- cut_facts_tac prems,
- K (rewrite_goals_tac defs)] @
- map (fn ct => dtac (inst_spec ct)) cPs @
- [assume_tac])) |>
- singleton (ProofContext.export lthy4 lthy1)
- end;
-in
- map prove_indrule (preds' ~~ Ps ~~ Tss)
- end
+ rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ THEN
+ EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
+ end)
(* @end *)
(* @chunk intro_rules *)
-fun INTROS rules preds' defs lthy1 lthy2 =
+fun INTROS rules parnames preds defs lthy1 =
let
- fun prove_intro (i, r) =
- Goal.prove lthy2 [] [] r
- (fn {prems, context = ctxt} => EVERY
- [ObjectLogic.rulify_tac 1,
- rewrite_goals_tac defs,
- REPEAT (resolve_tac [@{thm allI},@{thm impI}] 1),
- SUBPROOF (fn {params, prems, context = ctxt', ...} =>
- let
- val (prems1, prems2) = chop (length prems - length rules) prems;
- val (params1, params2) = chop (length params - length preds') params;
- in
- rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
- THEN
- EVERY1 (map (fn prem =>
- SUBPROOF (fn {prems = prems', concl, ...} =>
- let
-
- val prem' = prems' MRS prem;
- val prem'' = case prop_of prem' of
- _ $ (Const (@{const_name All}, _) $ _) =>
- prem' |> all_elims params2
- |> imp_elims prems2
- | _ => prem';
- in rtac prem'' 1 end) ctxt') prems1)
- end) ctxt 1]) |>
- singleton (ProofContext.export lthy2 lthy1)
+ val (_, lthy2) = Variable.add_fixes parnames lthy1
+
+ fun prove_intro (i, goal) =
+ Goal.prove lthy2 [] [] goal
+ (fn {context = ctxt, ...} =>
+ EVERY1
+ [ObjectLogic.rulify_tac,
+ K (rewrite_goals_tac defs),
+ REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
+ subproof1 rules preds i ctxt])
+ |> singleton (ProofContext.export lthy2 lthy1)
in
map_index prove_intro rules
end
+
(* @end *)
(* @chunk add_inductive_i *)
@@ -129,12 +165,15 @@
val Tss = map (binder_types o fastype_of) preds';
val (ass,rules) = split_list specs;
- val (defs, lthy1) = definitions params' rules preds preds' Tss lthy
- val (_, lthy2) = Variable.add_fixes (map (Binding.name_of o fst) params) lthy1;
+ val prednames = map (fst o fst) preds
+ val syns = map snd preds
+ val parnames = map (Binding.name_of o fst) params
+
+ val (defs, lthy1) = definitions rules params' preds' prednames syns Tss lthy;
- val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
-
- val intros = INTROS rules preds' defs lthy1 lthy2
+ val inducts = inductions rules defs parnames preds' Tss lthy1
+
+ val intros = INTROS rules parnames preds' defs lthy1
val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds);
val case_names = map (Binding.name_of o fst o fst) specs
Binary file cookbook.pdf has changed