# HG changeset patch # User Christian Urban # Date 1258900030 -3600 # Node ID 36d61044f9bf20d580d6dc205d135f447e4a9bc1 # Parent 7675427e311f4a9a316de22124c84ae844f84c59 updated to new Isabelle and clarified Skip_Proof diff -r 7675427e311f -r 36d61044f9bf ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Sun Nov 22 03:13:29 2009 +0100 +++ b/ProgTutorial/Advanced.thy Sun Nov 22 15:27:10 2009 +0100 @@ -6,7 +6,7 @@ setup{* open_file_with_prelude "Advanced_Code.thy" - ["theory General", "imports Base FirstSteps", "begin"] + ["theory Advanced", "imports Base FirstSteps", "begin"] *} (*>*) @@ -29,7 +29,7 @@ section {* Theories\label{sec:theories} (TBD) *} text {* - As said above, theories are the most basic layer in Isabelle. They contain + Theories, as said above, are the most basic layer in Isabelle. They contain definitions, syntax declarations, axioms, proofs etc. If a definition is stated, it must be stored in a theory in order to be usable later on. Similar with proofs: once a proof is finished, the proved theorem needs diff -r 7675427e311f -r 36d61044f9bf ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Sun Nov 22 03:13:29 2009 +0100 +++ b/ProgTutorial/Essential.thy Sun Nov 22 15:27:10 2009 +0100 @@ -6,7 +6,7 @@ setup{* open_file_with_prelude "Essential_Code.thy" - ["theory General", "imports Base FirstSteps", "begin"] + ["theory Essential", "imports Base FirstSteps", "begin"] *} (*>*) @@ -1644,9 +1644,6 @@ "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}" "True = False"} - The function @{ML make_thm in Skip_Proof} however only works if - the ``quick-and-dirty'' mode is switched on. - Theorems also contain auxiliary data, such as the name of the theorem, its kind, the names for cases and so on. This data is stored in a string-string list and can be retrieved with the function @{ML_ind get_tags in diff -r 7675427e311f -r 36d61044f9bf ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sun Nov 22 03:13:29 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Sun Nov 22 15:27:10 2009 +0100 @@ -893,7 +893,7 @@ *} local_setup %gray {* - Local_Theory.define "" ((@{binding "TrueConj"}, NoSyn), + Local_Theory.define ((@{binding "TrueConj"}, NoSyn), (Attrib.empty_binding, @{term "True \ True"})) #> snd *} text {* diff -r 7675427e311f -r 36d61044f9bf ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Sun Nov 22 03:13:29 2009 +0100 +++ b/ProgTutorial/Package/Ind_Code.thy Sun Nov 22 15:27:10 2009 +0100 @@ -28,43 +28,17 @@ ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy = let val arg = ((predname, mx), (Attrib.empty_binding, trm)) - val ((_, (_ , thm)), lthy') = Local_Theory.define "" arg lthy + val ((_, (_ , thm)), lthy') = Local_Theory.define arg lthy in (thm, lthy') end*} text {* It returns the definition (as a theorem) and the local theory in which the - definition has been made. In Line 4, the string @{ML "\"\""} is a flag - attached to the theorem (other possibile flags are @{ML_ind definitionK in Thm} - and @{ML_ind theoremK in Thm}).\footnote{\bf FIXME: move to theorem section.} - These flags just classify theorems and have no - significant meaning, except for tools that, for example, find theorems in - the theorem database.\footnote{FIXME: put in the section about theorems.} We - also use @{ML_ind empty_binding in Attrib} in Line 3, since the definitions for - our inductive predicates are not meant to be seen by the user and therefore - do not need to have any theorem attributes. A testcase for this function is -*} - -local_setup %gray {* fn lthy => -let - val arg = ((@{binding "My_True"}, NoSyn), @{term True}) - val (def, lthy') = make_defn arg lthy -in - tracing (string_of_thm_no_vars lthy' def); lthy' -end *} - -text {* - which introduces the definition @{thm My_True_def} and then prints it out. - Since we are testing the function inside \isacommand{local\_setup}, i.e., make - actual changes to the ambient theory, we can query the definition with the usual - command \isacommand{thm}: - - \begin{isabelle} - \isacommand{thm}~@{thm [source] "My_True_def"}\\ - @{text ">"}~@{thm "My_True_def"} - \end{isabelle} - + definition has been made. We use @{ML_ind empty_binding in Attrib} in Line 3, + since the definitions for our inductive predicates are not meant to be seen + by the user and therefore do not need to have any theorem attributes. + The next two functions construct the right-hand sides of the definitions, which are terms whose general form is: diff -r 7675427e311f -r 36d61044f9bf ProgTutorial/Package/simple_inductive_package.ML --- a/ProgTutorial/Package/simple_inductive_package.ML Sun Nov 22 03:13:29 2009 +0100 +++ b/ProgTutorial/Package/simple_inductive_package.ML Sun Nov 22 15:27:10 2009 +0100 @@ -22,7 +22,7 @@ fun make_defs ((binding, syn), trm) lthy = let val arg = ((binding, syn), (Attrib.empty_binding, trm)) - val ((_, (_ , thm)), lthy) = Local_Theory.define "" arg lthy + val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy in (thm, lthy) end diff -r 7675427e311f -r 36d61044f9bf ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Sun Nov 22 03:13:29 2009 +0100 +++ b/ProgTutorial/Tactical.thy Sun Nov 22 15:27:10 2009 +0100 @@ -429,15 +429,6 @@ (*<*)oops(*>*) text {* - This tactic works however only if the quick-and-dirty mode of Isabelle - is switched on. This is done automatically in the ``interactive - mode'' of Isabelle, but must be done manually in the ``batch mode'' - with the assignment -*} - -ML{*quick_and_dirty := true*} - -text {* Another simple tactic is the function @{ML_ind atac in Tactic}, which, as shown earlier, corresponds to the assumption method. *} diff -r 7675427e311f -r 36d61044f9bf progtutorial.pdf Binary file progtutorial.pdf has changed