# HG changeset patch # User Christian Urban # Date 1236545580 0 # Node ID 2319cff107f07bf7717cad9c8f1ffb6c05ed536c # Parent 3fb9f820a294630fb5158fcdd0c3858f74056b63 removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive diff -r 3fb9f820a294 -r 2319cff107f0 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Fri Mar 06 21:52:17 2009 +0000 +++ b/CookBook/FirstSteps.thy Sun Mar 08 20:53:00 2009 +0000 @@ -408,17 +408,14 @@ ML{*fun get_thm_names_from_ss simpset = let - val ({rules,...}, _) = MetaSimplifier.rep_ss simpset + val {simps,...} = MetaSimplifier.dest_ss simpset in - map #name (Net.entries rules) + map #1 simps end*} text {* - The function @{ML rep_ss in MetaSimplifier} returns a record containing all - information about the simpset. The rules of a simpset are stored in a - \emph{discrimination net} (a data structure for fast indexing). From this - net you can extract the entries using the function @{ML Net.entries}. - You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored + The function @{ML dest_ss in MetaSimplifier} returns a record containing all + information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored in the current simpset. This simpset can be referred to using the antiquotation @{text "@{simpset}"}. @@ -444,7 +441,6 @@ course of this chapter you will learn more about these antiquotations: they can simplify Isabelle programming since one can directly access all kinds of logical elements from th ML-level. - *} section {* Terms and Types *} @@ -710,12 +706,12 @@ text {* Occasional you have to calculate what the ``base'' name of a given constant is. For this you can use the function @{ML Sign.extern_const} or - @{ML NameSpace.base_name}. For example: + @{ML Long_Name.base_name}. For example: @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} The difference between both functions is that @{ML extern_const in Sign} returns - the smallest name that is still unique, whereas @{ML base_name in NameSpace} always + the smallest name that is still unique, whereas @{ML base_name in Long_Name} always strips off all qualifiers. \begin{readmore} @@ -1182,31 +1178,38 @@ (* FIXME: some code below *) (*<*) +(* setup {* - Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] + Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] *} - +*) lemma "bar = (1::nat)" oops +(* setup {* Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] #> PureThy.add_defs false [((Binding.name "foo_def", Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] #> snd *} - +*) +(* lemma "foo = (1::nat)" apply(simp add: foo_def) done thm foo_def +*) (*>*) section {* Pretty-Printing (TBD) *} text {* - @{ML Pretty.big_list} + @{ML Pretty.big_list}, + @{ML Pretty.brk}, + @{ML Pretty.block}, + @{ML Pretty.chunks} *} section {* Misc (TBD) *} diff -r 3fb9f820a294 -r 2319cff107f0 CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Fri Mar 06 21:52:17 2009 +0000 +++ b/CookBook/Package/Ind_Code.thy Sun Mar 08 20:53:00 2009 +0000 @@ -3,6 +3,11 @@ begin text {* + What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK? +*} + + +text {* @{ML_chunk [display,gray] definitions_aux} @{ML_chunk [display,gray,linenos] definitions} diff -r 3fb9f820a294 -r 2319cff107f0 CookBook/Package/simple_inductive_package.ML --- a/CookBook/Package/simple_inductive_package.ML Fri Mar 06 21:52:17 2009 +0000 +++ b/CookBook/Package/simple_inductive_package.ML Sun Mar 08 20:53:00 2009 +0000 @@ -21,10 +21,10 @@ fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P (* @chunk definitions_aux *) -fun definitions_aux s ((binding, syn), (attr, trm)) lthy = +fun definitions_aux ((binding, syn), trm) lthy = let val ((_, (_, thm)), lthy) = - LocalTheory.define s ((binding, syn), (attr, trm)) lthy + LocalTheory.define Thm.internalK ((binding, syn), (Attrib.empty_binding, trm)) lthy in (thm, lthy) end @@ -45,7 +45,7 @@ val t2 = fold_rev mk_all preds' t1; val t3 = fold_rev lambda (params @ zs) t2; in - definitions_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3)) + definitions_aux ((R, syn), t3) end) (preds ~~ preds' ~~ Tss) lthy end (* @end *) diff -r 3fb9f820a294 -r 2319cff107f0 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Fri Mar 06 21:52:17 2009 +0000 +++ b/CookBook/Tactical.thy Sun Mar 08 20:53:00 2009 +0000 @@ -1119,58 +1119,44 @@ text_raw {* \begin{figure}[tp] \begin{isabelle}*} -ML{*fun get_parts ss = -let - val ({rules, ...}, {congs, procs, ...}) = MetaSimplifier.rep_ss ss - - val rules_list = Net.entries rules - val rnames = map #name rules_list - val rthms = map #thm rules_list - - val congs_list = fst congs - val cnames = map fst congs_list - val cthms = map (#thm o snd) congs_list - - val proc_list = Net.entries procs -in - (rnames ~~ rthms, cnames ~~ cthms) -end - -fun print_parts ctxt ss = +ML{*fun print_ss ctxt ss = let - val (simps, congs) = get_parts ss + val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss fun name_thm (nm, thm) = " " ^ nm ^ ": " ^ (str_of_thm ctxt thm) + fun name_ctrm (nm, ctrm) = + " " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm) val s1 = ["Simplification rules:"] val s2 = map name_thm simps val s3 = ["Congruences rules:"] val s4 = map name_thm congs + val s5 = ["Simproc patterns:"] + val s6 = map name_ctrm procs in - (s1 @ s2 @ s3 @ s4) + (s1 @ s2 @ s3 @ s4 @ s5 @ s6) |> separate "\n" |> implode |> warning end*} text_raw {* \end{isabelle} -\caption{The function @{ML MetaSimplifier.rep_ss} returns a record containing - a simpset. We are here only interested in the simplifcation rules, congruence rules and - simprocs. The first and third are discrimination nets, which from which we extract - lists using @{ML Net.entries}. The congruence rules are stored in - an association list, associating a constant with a rule.\label{fig:prettyss}} +\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing + all printable information stored in a simpset. We are here only interested in the + simplifcation rules, congruence rules and simprocs.\label{fig:printss}} \end{figure} *} text {* - To see how they work, consider the two functions in Figure~\ref{fig:prettyss}, which + To see how they work, consider the two functions in Figure~\ref{fig:printss}, which print out some parts of a simpset. If you use them to print out the components of the empty simpset, in ML @{ML empty_ss} and the most primitive simpset @{ML_response_fake [display,gray] - "print_parts @{context} empty_ss" + "print_ss @{context} empty_ss" "Simplification rules: -Congruences rules:"} +Congruences rules: +Simproc patterns:"} you can see it contains nothing. This simpset is usually not useful, except as a building block to build bigger simpsets. For example you can add to @{ML empty_ss} @@ -1183,10 +1169,11 @@ Printing then out the components of the simpset gives: @{ML_response_fake [display,gray] - "print_parts @{context} ss1" + "print_ss @{context} ss1" "Simplification rules: ??.unknown: A - B \ C \ A - B \ (A - C) -Congruences rules:"} +Congruences rules: +Simproc patterns:"} (FIXME: Why does it print out ??.unknown) @@ -1199,11 +1186,12 @@ gives @{ML_response_fake [display,gray] - "print_parts @{context} ss2" + "print_ss @{context} ss2" "Simplification rules: ??.unknown: A - B \ C \ A - B \ (A - C) Congruences rules: - UNION: \A = B; \x. x \ B \ C x = D x\ \ \x\A. C x \ \x\B. D x"} + UNION: \A = B; \x. x \ B \ C x = D x\ \ \x\A. C x \ \x\B. D x +Simproc patterns:"} Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} expects this form of the simplification and congruence rules. However, even @@ -1213,9 +1201,10 @@ printing out the components of this simpset @{ML_response_fake [display,gray] - "print_parts @{context} HOL_basic_ss" + "print_ss @{context} HOL_basic_ss" "Simplification rules: -Congruences rules:"} +Congruences rules: +Simproc patterns:"} also produces ``nothing'', the printout is misleading. In fact the @{ML HOL_basic_ss} is setup so that it can solve goals of the @@ -1239,7 +1228,7 @@ connectives in HOL. @{ML_response_fake [display,gray] - "print_parts @{context} HOL_ss" + "print_ss @{context} HOL_ss" "Simplification rules: Pure.triv_forall_equality: (\x. PROP V) \ PROP V HOL.the_eq_trivial: THE x. x = y \ y @@ -1248,7 +1237,9 @@ Congruences rules: HOL.simp_implies: \ \ (PROP P =simp=> PROP Q) \ (PROP P' =simp=> PROP Q') - op -->: \P \ P'; P' \ Q \ Q'\ \ P \ Q \ P' \ Q'"} + op -->: \P \ P'; P' \ Q \ Q'\ \ P \ Q \ P' \ Q' +Simproc patterns: + \"} The simplifier is often used to unfold definitions in a proof. For this the @@ -1418,9 +1409,6 @@ (FIXME: Is it interesting to say something about @{term "op =simp=>"}?) - (FIXME: Unfortunately one cannot access any simproc, as there is - no @{text rep_proc} in function @{ML get_parts}.) - (FIXME: What are the second components of the congruence rules---something to do with weak congruence constants?) diff -r 3fb9f820a294 -r 2319cff107f0 cookbook.pdf Binary file cookbook.pdf has changed