diff -r fb6c29a90003 -r d8c376662bb4 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Mon Apr 30 12:36:32 2012 +0100 +++ b/ProgTutorial/Essential.thy Mon Apr 30 14:43:52 2012 +0100 @@ -2,15 +2,6 @@ imports Base First_Steps begin -(*<*) -setup{* -open_file_with_prelude - "Essential_Code.thy" - ["theory Essential", "imports Base First_Steps", "begin"] -*} -(*>*) - - chapter {* Isabelle Essentials *} text {* @@ -229,7 +220,7 @@ detail in Section~\ref{sec:pretty}). *} -ML{*local +ML %grayML{*local fun pp_pair (x, y) = Pretty.list "(" ")" [x, y] fun pp_list xs = Pretty.list "[" "]" xs fun pp_str s = Pretty.str s @@ -251,7 +242,7 @@ @{ML_ind addPrettyPrinter in PolyML} as follows. *} -ML{*PolyML.addPrettyPrinter +ML %grayML{*PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*} text {* @@ -281,7 +272,7 @@ with the code *} -ML{*PolyML.addPrettyPrinter +ML %grayML{*PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*} text {* @@ -312,7 +303,7 @@ *} -ML{*fun make_imp P Q = +ML %grayML{*fun make_imp P Q = let val x = Free ("x", @{typ nat}) in @@ -325,7 +316,7 @@ the following does \emph{not} work. *} -ML{*fun make_wrong_imp P Q = @{prop "\(x::nat). P x \ Q x"} *} +ML %grayML{*fun make_wrong_imp P Q = @{prop "\(x::nat). P x \ Q x"} *} text {* To see this, apply @{text "@{term S}"} and @{text "@{term T}"} @@ -427,7 +418,7 @@ function that strips off the outermost forall quantifiers in a term. *} -ML{*fun strip_alls t = +ML %grayML{*fun strip_alls t = let fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T)) in @@ -450,7 +441,7 @@ builds the quantification from a body and a list of (free) variables. *} -ML{*fun build_alls ([], t) = t +ML %grayML{*fun build_alls ([], t) = t | build_alls (Free (x, T) :: vs, t) = Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool}) $ Abs (x, T, build_alls (vs, t))*} @@ -549,7 +540,7 @@ @{text is_true} as follows *} -ML{*fun is_true @{term True} = true +ML %grayML{*fun is_true @{term True} = true | is_true _ = false*} text {* @@ -557,7 +548,7 @@ the function *} -ML{*fun is_all (@{term All} $ _) = true +ML %grayML{*fun is_all (@{term All} $ _) = true | is_all _ = false*} text {* @@ -571,7 +562,7 @@ for this function is *} -ML{*fun is_all (Const ("HOL.All", _) $ _) = true +ML %grayML{*fun is_all (Const ("HOL.All", _) $ _) = true | is_all _ = false*} text {* @@ -586,7 +577,7 @@ attempts to pick out @{text "Nil"}-terms: *} -ML{*fun is_nil (Const ("Nil", _)) = true +ML %grayML{*fun is_nil (Const ("Nil", _)) = true | is_nil _ = false *} text {* @@ -622,7 +613,7 @@ be written as follows. *} -ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true +ML %grayML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true | is_nil_or_all _ = false *} @@ -640,18 +631,18 @@ *} -ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *} +ML %grayML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *} text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *} -ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *} +ML %grayML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *} text {* If you want to construct a function type with more than one argument type, then you can use @{ML_ind "--->" in Term}. *} -ML{*fun make_fun_types tys ty = tys ---> ty *} +ML %grayML{*fun make_fun_types tys ty = tys ---> ty *} text {* A handy function for manipulating terms is @{ML_ind map_types in Term}: it takes a @@ -659,7 +650,7 @@ change every @{typ nat} in a term into an @{typ int} using the function: *} -ML{*fun nat_to_int ty = +ML %grayML{*fun nat_to_int ty = (case ty of @{typ nat} => @{typ int} | Type (s, tys) => Type (s, map nat_to_int tys) @@ -802,7 +793,7 @@ \begin{figure}[t] \begin{minipage}{\textwidth} \begin{isabelle}*} -ML{*fun pretty_helper aux env = +ML %grayML{*fun pretty_helper aux env = env |> Vartab.dest |> map aux |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2]) @@ -864,7 +855,7 @@ class s1 class s2 -ML{*val (tyenv, index) = let +ML %grayML{*val (tyenv, index) = let val ty1 = @{typ_pat "?'a::s1"} val ty2 = @{typ_pat "?'b::s2"} in @@ -916,7 +907,7 @@ of failure. For example *} -ML{*val tyenv_match = let +ML %grayML{*val tyenv_match = let val pat = @{typ_pat "?'a * ?'b"} and ty = @{typ_pat "bool list * nat"} in @@ -944,7 +935,7 @@ following matcher: *} -ML{*val tyenv_match' = let +ML %grayML{*val tyenv_match' = let val pat = @{typ_pat "?'a * ?'b"} and ty = @{typ_pat "?'b list * nat"} in @@ -989,7 +980,7 @@ the function @{text "pretty_env"}: *} -ML{*fun pretty_env ctxt env = +ML %grayML{*fun pretty_env ctxt env = let fun get_trms (v, (T, t)) = (Var (v, T), t) val print = pairself (pretty_term ctxt) @@ -1004,7 +995,7 @@ @{text "?X ?Y"}. *} -ML{*val (_, fo_env) = let +ML %grayML{*val (_, fo_env) = let val fo_pat = @{term_pat "(?X::(nat\nat\nat)\bool) ?Y"} val trm_a = @{term "P::(nat\nat\nat)\bool"} val trm_b = @{term "\a b. (Q::nat\nat\nat) b a"} @@ -1123,7 +1114,7 @@ list of potentially infinite unifiers. An example is as follows *} -ML{*val uni_seq = +ML %grayML{*val uni_seq = let val trm1 = @{term_pat "?X ?Y"} val trm2 = @{term "f a"} @@ -1138,7 +1129,7 @@ unifiers @{text "un1\un3"}. *} -ML{*val SOME ((un1, _), next1) = Seq.pull uni_seq; +ML %grayML{*val SOME ((un1, _), next1) = Seq.pull uni_seq; val SOME ((un2, _), next2) = Seq.pull next1; val SOME ((un3, _), next3) = Seq.pull next2; val NONE = Seq.pull next3 *} @@ -1226,14 +1217,14 @@ @{ML_type ctyp}-pairs with the function *} -ML{*fun prep_trm thy (x, (T, t)) = +ML %grayML{*fun prep_trm thy (x, (T, t)) = (cterm_of thy (Var (x, T)), cterm_of thy t)*} text {* and into proper @{ML_type cterm}-pairs with *} -ML{*fun prep_ty thy (x, (S, ty)) = +ML %grayML{*fun prep_ty thy (x, (S, ty)) = (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*} text {* @@ -1628,7 +1619,7 @@ To see how it works let us assume we defined our own theorem list @{text MyThmList}. *} -ML{*structure MyThmList = Generic_Data +ML %grayML{*structure MyThmList = Generic_Data (type T = thm list val empty = [] val extend = I @@ -1809,7 +1800,7 @@ following function for atomizing a theorem. *} -ML{*fun atomize_thm thm = +ML %grayML{*fun atomize_thm thm = let val thm' = forall_intr_vars thm val thm'' = Object_Logic.atomize (cprop_of thm') @@ -1850,7 +1841,7 @@ following three helper functions. *} -ML{*fun rep_goals i = replicate i @{prop "f x = f x"} +ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"} fun rep_tacs i = replicate i (rtac @{thm refl}) fun multi_test ctxt i = @@ -1871,7 +1862,7 @@ using @{ML map} and @{ML prove in Goal}. *} -ML{*let +ML %grayML{*let fun test_prove ctxt thm = Goal.prove ctxt ["P", "x"] [] thm (K (rtac @{thm refl} 1)) in @@ -2040,7 +2031,7 @@ and uses them as name in the outermost abstractions. *} -ML{*fun rename_allq [] t = t +ML %grayML{*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) = @@ -2117,7 +2108,7 @@ this attribute is *} -ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*} +ML %grayML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*} text {* where the function @{ML_ind rule_attribute in Thm} expects a function taking a @@ -2164,7 +2155,7 @@ attribute as follows: *} -ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric) +ML %grayML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric) "applying the sym rule" *} text {* @@ -2178,7 +2169,7 @@ after another). The code for this attribute is *} -ML{*fun MY_THEN thms = +ML %grayML{*fun MY_THEN thms = let fun RS_rev thm1 thm2 = thm2 RS thm1 in @@ -2237,7 +2228,7 @@ let us introduce a theorem list. *} -ML{*structure MyThms = Named_Thms +ML %grayML{*structure MyThms = Named_Thms (val name = @{binding "attr_thms"} val description = "Theorems for an Attribute") *} @@ -2248,7 +2239,7 @@ with the code *} -ML{*val my_add = Thm.declaration_attribute MyThms.add_thm +ML %grayML{*val my_add = Thm.declaration_attribute MyThms.add_thm val my_del = Thm.declaration_attribute MyThms.del_thm *} text {* @@ -2342,7 +2333,7 @@ type: *} -ML{*fun pprint prt = tracing (Pretty.string_of prt)*} +ML %grayML{*fun pprint prt = tracing (Pretty.string_of prt)*} text {* The point of the pretty-printing infrastructure is to give hints about how to @@ -2351,13 +2342,13 @@ following function that replicates a string n times: *} -ML{*fun rep n str = implode (replicate n str) *} +ML %grayML{*fun rep n str = implode (replicate n str) *} text {* and suppose we want to print out the string: *} -ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*} +ML %grayML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*} text {* We deliberately chose a large string so that it spans over more than one line.