1 theory First_Steps

     1 theory First_Steps

     2 imports Base

     2 imports Base

     3 begin

     3 begin

     4                                                   

     4                                                   

     5 chapter \<open>First Steps\label{chp:firststeps}\<close>

     5 chapter \<open>First Steps\label{chp:firststeps}\<close>

     7 

     6 

     8 text \<open>

     7 text \<open>

     9   \begin{flushright}

     8   \begin{flushright}

    10   {\em ``The most effective debugging tool is still careful thought,\\ 

     9   {\em ``The most effective debugging tool is still careful thought,\\ 

    11   coupled with judiciously placed print statements.''} \\[1ex]

    10   coupled with judiciously placed print statements.''} \\[1ex]

   107   is converted is monomorphic and not a function. 

   106   is converted is monomorphic and not a function. 

   108 

   107 

   109   You can print out error messages with the function @{ML_ind error in Library}; 

   108   You can print out error messages with the function @{ML_ind error in Library}; 

   110   for example:

   109   for example:

   111 

   110 

   113   \<open>if 0 = 1 then true else (error "foo")\<close> 

   112   \<open>if 0 = 1 then true else (error "foo")\<close> 

   116 

   114 

   117   This function raises the exception \<open>ERROR\<close>, which will then 

   115   This function raises the exception \<open>ERROR\<close>, which will then 

   118   be displayed by the infrastructure indicating that it is an error by

   116   be displayed by the infrastructure indicating that it is an error by

   119   painting the output red. Note that this exception is meant 

   117   painting the output red. Note that this exception is meant 

   120   for ``user-level'' error messages seen by the ``end-user''. 

   118   for ``user-level'' error messages seen by the ``end-user''. 

   130   @{ML_structure Syntax}. For more convenience, we bind them to the toplevel.

   128   @{ML_structure Syntax}. For more convenience, we bind them to the toplevel.

   131 \<close>

   129 \<close>

   132 

   130 

   133 ML %grayML\<open>val pretty_term = Syntax.pretty_term

   131 ML %grayML\<open>val pretty_term = Syntax.pretty_term

   134 val pwriteln = Pretty.writeln\<close>

   132 val pwriteln = Pretty.writeln\<close>

   136 text \<open>

   137 text \<open>

   137   They can be used as follows

   138   They can be used as follows

   138 

   139 

   140   \<open>pwriteln (pretty_term @{context} @{term "1::nat"})\<close>

   141   \<open>pwriteln (pretty_term @{context} @{term "1::nat"})\<close>

   141   \<open>"1"\<close>}

   142   \<open>"1"\<close>}

   142 

   143 

   143   If there is more than one term to be printed, you can use the 

   144   If there is more than one term to be printed, you can use the 

   144   function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} 

   145   function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} 

   157 ML %grayML\<open>val show_types_ctxt = Config.put show_types true @{context}\<close>

   158 ML %grayML\<open>val show_types_ctxt = Config.put show_types true @{context}\<close>

   158 

   159 

   159 text \<open>

   160 text \<open>

   160   Now by using this context @{ML pretty_term} prints out

   161   Now by using this context @{ML pretty_term} prints out

   161 

   162 

   163   \<open>pwriteln (pretty_term show_types_ctxt @{term "(1::nat, x)"})\<close>

   164   \<open>pwriteln (pretty_term show_types_ctxt @{term "(1::nat, x)"})\<close>

   164   \<open>(1::nat, x::'a)\<close>}

   165   \<open>(1::nat, x::'a)\<close>}

   165 

   166 

   166   where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.

   167   where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.

   167   Other configuration values that influence

   168   Other configuration values that influence

   201   \<open>?Q\<close> and so on. They are instantiated by Isabelle when a theorem is applied.

   202   \<open>?Q\<close> and so on. They are instantiated by Isabelle when a theorem is applied.

   202   For example, the theorem 

   203   For example, the theorem 

   203   @{thm [source] conjI} shown below can be used for any (typable) 

   204   @{thm [source] conjI} shown below can be used for any (typable) 

   204   instantiation of \<open>?P\<close> and \<open>?Q\<close>. 

   205   instantiation of \<open>?P\<close> and \<open>?Q\<close>. 

   205 

   206 

   207   \<open>pwriteln (pretty_thm @{context} @{thm conjI})\<close>

   208   \<open>pwriteln (pretty_thm @{context} @{thm conjI})\<close>

   208   \<open>\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\<close>}

   209   \<open>\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\<close>}

   209 

   210 

   210   However, to improve the readability when printing theorems, we

   211   However, to improve the readability when printing theorems, we

   211   can switch off the question marks as follows:

   212   can switch off the question marks as follows:

   219 end\<close>

   220 end\<close>

   220 

   221 

   221 text \<open>

   222 text \<open>

   222   With this function, theorem @{thm [source] conjI} is now printed as follows:

   223   With this function, theorem @{thm [source] conjI} is now printed as follows:

   223 

   224 

   225   \<open>pwriteln (pretty_thm_no_vars @{context} @{thm conjI})\<close>

   226   \<open>pwriteln (pretty_thm_no_vars @{context} @{thm conjI})\<close>

   226   \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close>}

   227   \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close>}

   227   

   228   

   228   Again the functions @{ML commas} and @{ML block in Pretty} help 

   229   Again the functions @{ML commas} and @{ML block in Pretty} help 

   229   with printing more than one theorem. 

   230   with printing more than one theorem. 

   265   \emph{not} print out information as

   266   \emph{not} print out information as

   266 

   267 

   267 @{ML_matchresult_fake [display,gray]

   268 @{ML_matchresult_fake [display,gray]

   268 \<open>pwriteln (Pretty.str "First half,"); 

   269 \<open>pwriteln (Pretty.str "First half,"); 

   269 pwriteln (Pretty.str "and second half.")\<close>

   270 pwriteln (Pretty.str "and second half.")\<close>

   272 

   273 

   273   but as a single string with appropriate formatting. For example

   274   but as a single string with appropriate formatting. For example

   274 

   275 

   276 \<open>pwriteln (Pretty.str ("First half," ^ "\\n" ^ "and second half."))\<close>

   277 \<open>pwriteln (Pretty.str ("First half," ^ "\\n" ^ "and second half."))\<close>

   277 \<open>First half,

   278 \<open>First half,

   278 and second half.\<close>}

   279 and second half.\<close>}

   279   

   280   

   280   To ease this kind of string manipulations, there are a number

   281   To ease this kind of string manipulations, there are a number

   281   of library functions in Isabelle. For example,  the function 

   282   of library functions in Isabelle. For example,  the function 

   282   @{ML_ind cat_lines in Library} concatenates a list of strings 

   283   @{ML_ind cat_lines in Library} concatenates a list of strings 

   283   and inserts newlines in between each element. 

   284   and inserts newlines in between each element. 

   284 

   285 

   286   \<open>pwriteln (Pretty.str (cat_lines ["foo", "bar"]))\<close>

   287   \<open>pwriteln (Pretty.str (cat_lines ["foo", "bar"]))\<close>

   287   \<open>foo

   288   \<open>foo

   288 bar\<close>}

   289 bar\<close>}

   289 

   290 

   290   Section \ref{sec:pretty} will explain the infrastructure that Isabelle 

   291   Section \ref{sec:pretty} will explain the infrastructure that Isabelle 

   385   This function takes a term and a context as arguments. If the term is of function

   386   This function takes a term and a context as arguments. If the term is of function

   386   type, then @{ML \<open>apply_fresh_args\<close>} returns the term with distinct variables 

   387   type, then @{ML \<open>apply_fresh_args\<close>} returns the term with distinct variables 

   387   applied to it. For example, below three variables are applied to the term 

   388   applied to it. For example, below three variables are applied to the term 

   388   @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:

   389   @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:

   389 

   390 

   391 \<open>let

   392 \<open>let

   392   val trm = @{term "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}

   393   val trm = @{term "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}

   393   val ctxt = @{context}

   394   val ctxt = @{context}

   394 in 

   395 in 

   395   apply_fresh_args trm ctxt

   396   apply_fresh_args trm ctxt

   412   

   413   

   413   Functions like @{ML apply_fresh_args} are often needed when constructing

   414   Functions like @{ML apply_fresh_args} are often needed when constructing

   414   terms involving fresh variables. For this the infrastructure helps

   415   terms involving fresh variables. For this the infrastructure helps

   415   tremendously to avoid any name clashes. Consider for example:

   416   tremendously to avoid any name clashes. Consider for example:

   416 

   417 

   418 \<open>let

   419 \<open>let

   419   val trm = @{term "za::'a \<Rightarrow> 'b \<Rightarrow> 'c"}

   420   val trm = @{term "za::'a \<Rightarrow> 'b \<Rightarrow> 'c"}

   420   val ctxt = @{context}

   421   val ctxt = @{context}

   421 in

   422 in

   422   apply_fresh_args trm ctxt 

   423   apply_fresh_args trm ctxt 

   597   \<open>acc_incs 1 ||>> (fn x => (x, x + 2))\<close>

   598   \<open>acc_incs 1 ||>> (fn x => (x, x + 2))\<close>

   598   \<open>((((("", 1), 2), 3), 4), 6)\<close>}

   599   \<open>((((("", 1), 2), 3), 4), 6)\<close>}

   599 

   600 

   600   An example where this combinator is useful is as follows

   601   An example where this combinator is useful is as follows

   601 

   602 

   603   \<open>let

   604   \<open>let

   604   val ((names1, names2), _) =

   605   val ((names1, names2), _) =

   605     @{context}

   606     @{context}

   606     |> Variable.variant_fixes (replicate 4 "x")

   607     |> Variable.variant_fixes (replicate 4 "x")

   607     ||>> Variable.variant_fixes (replicate 5 "x")

   608     ||>> Variable.variant_fixes (replicate 5 "x")

   637   augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing 

   638   augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing 

   638   information about the definitions---the function @{ML_ind define in Local_Defs} returns

   639   information about the definitions---the function @{ML_ind define in Local_Defs} returns

   639   both as pairs. We can use this information for example to print out the definiens and 

   640   both as pairs. We can use this information for example to print out the definiens and 

   640   the theorem corresponding to the definitions. For example for the first definition:

   641   the theorem corresponding to the definitions. For example for the first definition:

   641 

   642 

   643   \<open>let 

   644   \<open>let 

   644   val (one_trm, (_, one_thm)) = one_def

   645   val (one_trm, (_, one_thm)) = one_def

   645 in

   646 in

   648 end\<close>

   649 end\<close>

   649   \<open>One

   650   \<open>One

   650 One \<equiv> 1\<close>}

   651 One \<equiv> 1\<close>}

   651   Recall that @{ML \<open>|>\<close>} is the reverse function application. Recall also that

   652   Recall that @{ML \<open>|>\<close>} is the reverse function application. Recall also that

   652   the related reverse function composition is @{ML \<open>#>\<close>}. In fact all the

   653   the related reverse function composition is @{ML \<open>#>\<close>}. In fact all the

   671   plumbing is also needed in situations where a function operates over lists, 

   672   plumbing is also needed in situations where a function operates over lists, 

   672   but one calculates only with a single element. An example is the function 

   673   but one calculates only with a single element. An example is the function 

   673   @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check 

   674   @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check 

   674   a list of terms. Consider the code:

   675   a list of terms. Consider the code:

   675 

   676 

   677   \<open>let

   678   \<open>let

   678   val ctxt = @{context}

   679   val ctxt = @{context}

   679 in

   680 in

   680   map (Syntax.parse_term ctxt) ["m + n", "m * n", "m - (n::nat)"] 

   681   map (Syntax.parse_term ctxt) ["m + n", "m * n", "m - (n::nat)"] 

   681   |> Syntax.check_terms ctxt

   682   |> Syntax.check_terms ctxt

   692   check_terms in Syntax} needs plumbing. This can be done with the function

   693   check_terms in Syntax} needs plumbing. This can be done with the function

   693   @{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in

   694   @{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in

   694   Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented 

   695   Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented 

   695   in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example

   696   in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example

   696 

   697 

   698   \<open>let 

   699   \<open>let 

   699   val ctxt = @{context}

   700   val ctxt = @{context}

   700 in

   701 in

   701   Syntax.parse_term ctxt "m - (n::nat)" 

   702   Syntax.parse_term ctxt "m - (n::nat)" 

   702   |> singleton (Syntax.check_terms ctxt)

   703   |> singleton (Syntax.check_terms ctxt)

   772   defined abbreviations. For example

   773   defined abbreviations. For example

   773 

   774 

   774   @{ML_matchresult_fake [display, gray]

   775   @{ML_matchresult_fake [display, gray]

   775   \<open>Proof_Context.print_abbrevs false @{context}\<close>

   776   \<open>Proof_Context.print_abbrevs false @{context}\<close>

   776 \<open>\<dots>

   777 \<open>\<dots>

   778 Inter \<equiv> Inf

   779 Inter \<equiv> Inf

   779 \<dots>\<close>}

   780 \<dots>\<close>}

   780 

   781 

   781   The precise output of course depends on the abbreviations that are

   782   The precise output of course depends on the abbreviations that are

   782   currently defined; this can change over time.

   783   currently defined; this can change over time.

   783   You can also use antiquotations to refer to proved theorems: 

   784   You can also use antiquotations to refer to proved theorems: 

   784   \<open>@{thm \<dots>}\<close> for a single theorem

   785   \<open>@{thm \<dots>}\<close> for a single theorem

   785 

   786 

   787 

   788 

   788   and \<open>@{thms \<dots>}\<close> for more than one

   789   and \<open>@{thms \<dots>}\<close> for more than one

   789 

   790 

   791   \<open>@{thms conj_ac}\<close> 

   793   \<open>@{thms conj_ac}\<close> 

   795 

   797 

   796   The thm-antiquotations can also be used for manipulating theorems. For 

   798   The thm-antiquotations can also be used for manipulating theorems. For 

   797   example, if you need the version of the theorem @{thm [source] refl} that 

   799   example, if you need the version of the theorem @{thm [source] refl} that 

   798   has a meta-equality instead of an equality, you can write

   800   has a meta-equality instead of an equality, you can write

   799 

   801 

   801   \<open>@{thm refl[THEN eq_reflection]}\<close>

   803   \<open>@{thm refl[THEN eq_reflection]}\<close>

   802   \<open>?x \<equiv> ?x\<close>}

   804   \<open>?x \<equiv> ?x\<close>}

   803 

   805 

   804   The point of these antiquotations is that referring to theorems in this way

   806   The point of these antiquotations is that referring to theorems in this way

   805   makes your code independent from what theorems the user might have stored

   807   makes your code independent from what theorems the user might have stored

   814 ML %grayML\<open>val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all}\<close>

   816 ML %grayML\<open>val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all}\<close>

   815 

   817 

   816 text \<open>

   818 text \<open>

   817   The result can be printed out as follows.

   819   The result can be printed out as follows.

   818 

   820 

   820 \<open>foo_thms |> pretty_thms_no_vars @{context}

   822 \<open>foo_thms |> pretty_thms_no_vars @{context}

   821          |> pwriteln\<close>

   823          |> pwriteln\<close>

   822   \<open>True, False \<Longrightarrow> P\<close>}

   824   \<open>True, False \<Longrightarrow> P\<close>}

   823 

   825 

   824   You can also refer to the current simpset via an antiquotation. To illustrate 

   826   You can also refer to the current simpset via an antiquotation. To illustrate 

   838   The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all

   840   The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all

   839   information stored in the simpset, but here we are only interested in the names of the

   841   information stored in the simpset, but here we are only interested in the names of the

   840   simp-rules. Now you can feed in the current simpset into this function. 

   842   simp-rules. Now you can feed in the current simpset into this function. 

   841   The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.

   843   The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.

   842 

   844 

   844   \<open>get_thm_names_from_ss @{context}\<close> 

   846   \<open>get_thm_names_from_ss @{context}\<close> 

   846 

   848 

   847   Again, this way of referencing simpsets makes you independent from additions

   849   Again, this way of referencing simpsets makes you independent from additions

   848   of lemmas to the simpset by the user, which can potentially cause loops in your

   850   of lemmas to the simpset by the user, which can potentially cause loops in your

   849   code.

   851   code.

   850 

   852 

   882   transformed into a term using the function @{ML_ind read_term_pattern in

   884   transformed into a term using the function @{ML_ind read_term_pattern in

   883   Proof_Context} (Line 5); the next two lines transform the term into a string

   885   Proof_Context} (Line 5); the next two lines transform the term into a string

   884   so that the ML-system can understand it. (All these functions will be explained

   886   so that the ML-system can understand it. (All these functions will be explained

   885   in more detail in later sections.) An example for this antiquotation is:

   887   in more detail in later sections.) An example for this antiquotation is:

   886 

   888 

   888   \<open>@{term_pat "Suc (?x::nat)"}\<close>

   890   \<open>@{term_pat "Suc (?x::nat)"}\<close>

   890 

   892 

   891   which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly

   893   which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly

   892   we can write an antiquotation for type patterns. Its code is

   894   we can write an antiquotation for type patterns. Its code is

   893 \<close>

   895 \<close>

   894 

   896 

   978 end\<close>

   980 end\<close>

   979 

   981 

   980 text \<open>

   982 text \<open>

   981   The data can be retrieved with the projection functions defined above.

   983   The data can be retrieved with the projection functions defined above.

   982   

   984   

   987 true\<close>}

   989 true\<close>}

   988 

   990 

   989   Notice that we access the integer as an integer and the boolean as

   991   Notice that we access the integer as an integer and the boolean as

   990   a boolean. If we attempt to access the integer as a boolean, then we get 

   992   a boolean. If we attempt to access the integer as a boolean, then we get 

   991   a runtime error. 

   993   a runtime error. 

   992 

   994 

   994 \<open>project_bool (nth foo_list 0)\<close>  

   996 \<open>project_bool (nth foo_list 0)\<close>  

   996 

   998 

   997   This runtime error is the reason why ML is still type-sound despite

   999   This runtime error is the reason why ML is still type-sound despite

   998   containing a universal type.

  1000   containing a universal type.

   999 

  1001 

  1000   Now, Isabelle heavily uses this mechanism for storing all sorts of

  1002   Now, Isabelle heavily uses this mechanism for storing all sorts of

  1060 text \<open>

  1062 text \<open>

  1061   The use of the command \isacommand{setup} makes sure the table in the 

  1063   The use of the command \isacommand{setup} makes sure the table in the 

  1062   \emph{current} theory is updated (this is explained further in 

  1064   \emph{current} theory is updated (this is explained further in 

  1063   Section~\ref{sec:theories}). The lookup can now be performed as follows.

  1065   Section~\ref{sec:theories}). The lookup can now be performed as follows.

  1064 

  1066 

  1066 \<open>lookup @{theory} "conj"\<close>

  1068 \<open>lookup @{theory} "conj"\<close>

  1067 \<open>SOME "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"\<close>}

  1069 \<open>SOME "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"\<close>}

  1068 

  1070 

  1069   An important point to note is that these tables (and data in general)

  1071   An important point to note is that these tables (and data in general)

  1070   need to be treated in a purely functional fashion. Although

  1072   need to be treated in a purely functional fashion. Although

  1071   we can update the table as follows

  1073   we can update the table as follows

  1072 \<close>

  1074 \<close>

  1073 

  1075 

  1074 setup %gray \<open>update "conj" @{thm TrueI}\<close>

  1076 setup %gray \<open>update "conj" @{thm TrueI}\<close>

  1075 

  1077 

  1076 text \<open>

  1079 text \<open>

  1077   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}

  1080   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}

  1078   

  1081   

  1080 \<open>lookup @{theory} "conj"\<close>

  1083 \<open>lookup @{theory} "conj"\<close>

  1081 \<open>SOME "True"\<close>}

  1084 \<open>SOME "True"\<close>}

  1082 

  1085 

  1083   there are no references involved. This is one of the most fundamental

  1086   there are no references involved. This is one of the most fundamental

  1084   coding conventions for programming in Isabelle. References  

  1087   coding conventions for programming in Isabelle. References  

  1269 

  1272 

  1270 text \<open>

  1273 text \<open>

  1271   The rules in the list can be retrieved using the function 

  1274   The rules in the list can be retrieved using the function 

  1272   @{ML FooRules.get}:

  1275   @{ML FooRules.get}:

  1273 

  1276 

  1275   \<open>FooRules.get @{context}\<close> 

  1278   \<open>FooRules.get @{context}\<close> 

  1277 

  1280 

  1278   Note that this function takes a proof context as argument. This might be 

  1281   Note that this function takes a proof context as argument. This might be 

  1279   confusing, since the theorem list is stored as theory data. It becomes clear by knowing

  1282   confusing, since the theorem list is stored as theory data. It becomes clear by knowing

  1280   that the proof context contains the information about the current theory and so the function

  1283   that the proof context contains the information about the current theory and so the function

  1281   can access the theorem list in the theory via the context. 

  1284   can access the theorem list in the theory via the context.