# HG changeset patch # User Christian Urban # Date 1256480763 -3600 # Node ID 9cf3bc448210d1d0874833f2adc4e7af0157b859 # Parent 80b56d9b322f3c99cc5764f7ab4c964af73aa055 some polishing diff -r 80b56d9b322f -r 9cf3bc448210 ProgTutorial/General.thy --- a/ProgTutorial/General.thy Thu Oct 22 14:08:23 2009 +0200 +++ b/ProgTutorial/General.thy Sun Oct 25 15:26:03 2009 +0100 @@ -11,7 +11,7 @@ (*>*) -chapter {* Isabelle in More Detail *} +chapter {* Isabelle Essentials *} text {* Isabelle is build around a few central ideas. One central idea is the @@ -886,14 +886,13 @@ Recall that Isabelle does not let you call @{ML note in LocalTheory} twice with the same theorem name. In effect, once a theorem is stored under a name, - this association will be fixed. While this is a ``safety-net'' to make sure a + this association is fixed. While this is a ``safety-net'' to make sure a theorem name refers to a particular theorem or collection of theorems, it is also a bit too restrictive in cases where a theorem name should refer to a dynamically expanding list of theorems (like a simpset). Therefore Isabelle also implements a mechanism where a theorem name can refer to a custom theorem list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. - To see how it works let us assume we defined our own theorem list maintained - in the data storage @{text MyThmList}. + To see how it works let us assume we defined our own theorem list @{text MyThmList}. *} ML{*structure MyThmList = GenericDataFun @@ -945,8 +944,8 @@ @{text "> True"} \end{isabelle} - There is a multitude of functions that manage or manipulate theorems in the - structures @{ML_struct Thm} and @{ML_struct Drule}. For example + There is a multitude of functions in the structures @{ML_struct Thm} and @{ML_struct Drule} + for managing or manipulating theorems. For example we can test theorems for alpha equality. Suppose you proved the following three theorems. *} @@ -1008,8 +1007,7 @@ Note that in the second case, there is no premise. \begin{readmore} - For the functions @{text "assume"}, @{text "forall_elim"} etc - see \isccite{sec:thms}. The basic functions for theorems are defined in + The basic functions for theorems are defined in @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. \end{readmore} @@ -1191,10 +1189,10 @@ term stands for the theorem to be presented; the output can be constructed to ones wishes. Let us, for example, assume we want to quote theorems without leading @{text \}-quantifiers. For this we can implement the following function - that strips off meta-quantifiers. + that strips off @{text "\"}s. *} -ML %linenosgray {*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = +ML %linenosgray{*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = Term.dest_abs body |> snd |> strip_allq | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = strip_allq t @@ -1243,7 +1241,7 @@ and uses them as name in the outermost abstractions. *} -ML {*fun rename_allq [] t = t +ML{*fun rename_allq [] t = t | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t) | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) = @@ -1506,6 +1504,49 @@ \end{readmore} *} +section {* Theories\label{sec:theories} (TBD) *} + + +text {* + Theories are the most fundamental building blocks 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 to be stored in the theorem database of the theory in order to + be usable. All relevant data of a theort can be querried as follows. + + \begin{isabelle} + \isacommand{print\_theory}\\ + @{text "> names: Pure Code_Generator HOL \"}\\ + @{text "> classes: Inf < type \"}\\ + @{text "> default sort: type"}\\ + @{text "> syntactic types: #prop \"}\\ + @{text "> logical types: 'a \ 'b \"}\\ + @{text "> type arities: * :: (random, random) random \"}\\ + @{text "> logical constants: == :: 'a \ 'a \ prop \"}\\ + @{text "> abbreviations: \"}\\ + @{text "> axioms: \"}\\ + @{text "> oracles: \"}\\ + @{text "> definitions: \"}\\ + @{text "> theorems: \"} + \end{isabelle} + + \begin{center} + \begin{tikzpicture} + \node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A}; + \end{tikzpicture} + \end{center} + + + In contrast to an ordinary theory, which simply consists of a type + signature, as well as tables for constants, axioms and theorems, a local + theory contains additional context information, such as locally fixed + variables and local assumptions that may be used by the package. The type + @{ML_type local_theory} is identical to the type of \emph{proof contexts} + @{ML_type "Proof.context"}, although not every proof context constitutes a + valid local theory. +*} + section {* Setups (TBD) *} text {* @@ -1559,21 +1600,6 @@ the current simpset. *} -section {* Theories\label{sec:theories} (TBD) *} - -text {* - There are theories, proof contexts and local theories (in this order, if you - want to order them). - - In contrast to an ordinary theory, which simply consists of a type - signature, as well as tables for constants, axioms and theorems, a local - theory contains additional context information, such as locally fixed - variables and local assumptions that may be used by the package. The type - @{ML_type local_theory} is identical to the type of \emph{proof contexts} - @{ML_type "Proof.context"}, although not every proof context constitutes a - valid local theory. -*} - section {* Contexts (TBD) *} section {* Local Theories (TBD) *} diff -r 80b56d9b322f -r 9cf3bc448210 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Thu Oct 22 14:08:23 2009 +0200 +++ b/ProgTutorial/Intro.thy Sun Oct 25 15:26:03 2009 +0100 @@ -27,7 +27,7 @@ then this tutorial is for you. It will guide you through the first steps of Isabelle programming, and also explain tricks of the trade. We also hope the tutorial will encourage researchers to play with Isabelle and implement - new ideas. The sources of Isabelle can look intimidating, but beginners + new ideas. The source code of Isabelle can look intimidating, but beginners can get by with knowledge of only a small number functions and a few basic coding conventions. diff -r 80b56d9b322f -r 9cf3bc448210 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Thu Oct 22 14:08:23 2009 +0200 +++ b/ProgTutorial/Package/Ind_Code.thy Sun Oct 25 15:26:03 2009 +0100 @@ -135,8 +135,8 @@ local_setup %gray {* fn lthy => let - val def = defn_aux lthy fresh_orules - [fresh_pred] (fresh_pred, fresh_arg_tys) + val arg = (fresh_pred, fresh_arg_tys) + val def = defn_aux lthy fresh_orules [fresh_pred] arg in tracing (string_of_term lthy def); lthy end *} @@ -239,9 +239,12 @@ quantifiers. *} -ML{*fun inst_spec ctrm = - Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] - @{thm spec}*} +ML{*fun inst_spec ctrm = +let + val cty = ctyp_of_term ctrm +in + Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec} +end*} text {* This helper function uses the function @{ML_ind instantiate' in Drule} @@ -613,10 +616,10 @@ *} ML{*fun chop_print params1 params2 prems1 prems2 ctxt = let - val s = ["Params1 from the rule:", string_of_cterms ctxt params1] - @ ["Params2 from the predicate:", string_of_cterms ctxt params2] - @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) - @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) + val s = ["Params1 from the rule:", string_of_cterms ctxt params1] + @ ["Params2 from the predicate:", string_of_cterms ctxt params2] + @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) + @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) in s |> cat_lines |> tracing diff -r 80b56d9b322f -r 9cf3bc448210 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Thu Oct 22 14:08:23 2009 +0200 +++ b/ProgTutorial/Tactical.thy Sun Oct 25 15:26:03 2009 +0100 @@ -331,8 +331,30 @@ misinterpreted as open subgoals. While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion @{term C} intact, with the exception of possibly instantiating schematic - variables. If you use the predefined tactics, which we describe in the next - section, this will always be the case. + variables. The instantiations of schematic variables can even be observed + on the user level. For this consider the following definition and proof. +*} + +definition + EQ_TRUE +where + "EQ_TRUE X \ (X = True)" + +lemma test: + shows "EQ_TRUE ?X" + unfolding EQ_TRUE_def + by (rule refl) + +text {* + Although Isabelle issues a warning message when stating goals involving + meta-variables, it is possible to prove this theorem. The reason for the warning + message is that the proved theorem is not @{text "EQ_TRUE ?X"}, as one might + expect, but @{thm test}: + + \begin{isabelle} + \isacommand{thm}~@{thm [source] test}\\ + @{text ">"}~@{thm test} + \end{isabelle} \begin{readmore} For more information about the internals of goals see \isccite{sec:tactical-goals}. diff -r 80b56d9b322f -r 9cf3bc448210 ProgTutorial/document/root.tex --- a/ProgTutorial/document/root.tex Thu Oct 22 14:08:23 2009 +0200 +++ b/ProgTutorial/document/root.tex Sun Oct 25 15:26:03 2009 +0100 @@ -17,6 +17,8 @@ \usepackage{makeidx} \usepackage{index} \usepackage{tocbibind} +\usepackage{tikz} +\usetikzlibrary{shadows} \usepackage{pdfsetup} diff -r 80b56d9b322f -r 9cf3bc448210 progtutorial.pdf Binary file progtutorial.pdf has changed