isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:a0b280dd4bc7
+:520127b708e6
 theory Essential
-imports Base FirstSteps
+imports Base First_Steps
 begin
 (*<*)
 setup{*
 open_file_with_prelude
 "Essential_Code.thy"
-["theory Essential", "imports Base FirstSteps", "begin"]
+["theory Essential", "imports Base First_Steps", "begin"]
 *}
 (*>*)
 chapter {* Isabelle Essentials *}
 "let
 val v1 = Var ((\"x\", 3), @{typ bool})
 val v2 = Var ((\"x1\", 3), @{typ bool})
 val v3 = Free (\"x\", @{typ bool})
 in
-string_of_terms @{context} [v1, v2, v3]
+pretty_terms @{context} [v1, v2, v3]
-|> tracing
+|> pwriteln
 end"
 "?x3, ?x1.3, x"}
 When constructing terms, you are usually concerned with free variables (as
 mentioned earlier, you cannot construct schematic variables using the
 @{ML_response_fake [display,gray]
 "let
 val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
 in
-tracing (string_of_term @{context} omega)
+pwriteln (pretty_term @{context} omega)
 end"
 "x x"}
 Sometimes the internal representation of terms can be surprisingly different
 from what you see at the user-level, because the layers of
 @{ML_response_fake [display, gray, linenos]
 "let
 val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
 in
 subst_bounds (rev vrs, trm)
-|> string_of_term @{context}
+|> pretty_term @{context}
-|> tracing
+|> pwriteln
 end"
 "x = y"}
 Note that in Line 4 we had to reverse the list of variables that @{ML
 strip_alls} returned. The reason is that the head of the list the function
 @{ML_response_fake [gray,display]
 "let
 val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
-string_of_term @{context} eq
+eq |> pretty_term @{context}
-|> tracing
+|> pwriteln
 end"
 "True = False"}
 \begin{readmore}
 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}*}
 ML{*fun pretty_helper aux env =
 env |> Vartab.dest
-|> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux)
+|> map ((fn (s1, s2) => Pretty.block [s1, Pretty.str ";=", s2]) o aux)
-|> commas
+|> Pretty.commas
-|> enclose "[" "]"
+|> Pretty.enum "" "[" "]"
-|> tracing
+|> pwriteln
 fun pretty_tyenv ctxt tyenv =
 let
 fun get_typs (v, (s, T)) = (TVar (v, s), T)
-val print = pairself (Syntax.string_of_typ ctxt)
+val print = pairself (pretty_typ ctxt)
 in
 pretty_helper (print o get_typs) tyenv
 end*}
 text_raw {*
 \end{isabelle}
 *}
 ML{*fun pretty_env ctxt env =
 let
 fun get_trms (v, (T, t)) = (Var (v, T), t)
-val print = pairself (string_of_term ctxt)
+val print = pairself (pretty_term ctxt)
 in
 pretty_helper (print o get_trms) env
 end*}
 text {*
 @{ML_response_fake [display, gray]
 "let
 val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}
 in
 Envir.subst_term (Vartab.empty, fo_env) trm
-|> string_of_term @{context}
+|> pretty_term @{context}
-|> tracing
+|> pwriteln
 end"
 "P (\<lambda>a b. Q b a)"}
 First-order matching is useful for matching against applications and
 variables. It can also deal with abstractions and a limited form of
 "Envir.term_env"} pulls out the term environment from the result record. The
 corresponding function for type environment is @{ML_ind
 "Envir.type_env"}. An assumption of this function is that the terms to be
 unified have already the same type. In case of failure, the exceptions that
 are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}.
-*}
-(*
-ML {*
-fun patunif_in_emptyenv (t, u) =
-let
-val init = Envir.empty 0;
-val env = Pattern.unify @{theory} (t, u) init;
-in
-(env |> Envir.term_env |> Vartab.dest,
-env |> Envir.type_env |> Vartab.dest)
-end
-*}
-text {*
-@{ML_response [display, gray]
-"val t1 = @{term_pat \"(% x y. ?f y x)\"};
-val u1 = @{term_pat \"z::bool\"};
-(* type conflict isnt noticed *)
-patunif_in_emptyenv (t1, u1);"
-"check missing"
-*}
-@{ML_response [display, gray]
-"val t2 = @{term_pat \"(% y. ?f y)\"} |> Term.strip_abs_body;
-val u2 = @{term_pat \"z::bool\"};
-(* fails because of loose bounds *)
-(* patunif_in_emptyenv (t2, u2) *)"
-"check missing"
-*}
-@{ML_response [display, gray]
-"val t3 = @{term_pat \"(% y. plu (?f y) (% x. g x))\"};
-val u3 = @{term_pat \"(% y. plu y (% x. g x))\"};
-(* eta redexe im term egal, hidden polym wird inst *)
-patunif_in_emptyenv (t3, u3)"
-"check missing"
-*}
-@{ML_response [display, gray]
-"val t4 = @{term_pat \"(% y. plu (?f y) ((% x. g x) k))\"};
-val u4 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};
-(* beta redexe are largely ignored, hidden polymorphism is instantiated *)
-patunif_in_emptyenv (t4, u4)"
-"check missing"
-*}
-@{ML_response [display, gray]
-"val t5 = @{term_pat \"(% y. plu ((% x. ?f) y) ((% x. g x) k))\"};
-val u5 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};
-(* fails: can't have beta redexes which seperate a var from its arguments *)
-(* patunif_in_emptyenv (t5, u5) *)"
-*}
-@{ML_response [display, gray]
-"val t6 = @{term_pat \"(% x y. ?f x y) a b\"};
-val u6 = @{term_pat \"c\"};
-(* Pattern.pattern assumes argument is beta-normal *)
-Pattern.pattern t6;
-(* fails: can't have beta redexes which seperate a var from its arguments,
-otherwise this would be general unification for general a,b,c *)
-(* patunif_in_emptyenv (t6, u6) *)"
-*}
-@{ML_response [display, gray]
-"val t7 = @{term_pat \"(% y. plu ((% x. ?f x) y) ((% x. g x) k))\"};
-val u7 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};
-(* eta redexe die Pattern trennen brauchen nicht normalisiert sein *)
-patunif_in_emptyenv (t7, u7)"
-*}
-@{ML_response [display, gray]
-"val t8 = @{term_pat \"(% y. ?f y)\"};
-val u8 = @{term_pat \"(% y. y ?f)\"};
-(* variables of the same name are identified *)
-(* patunif_in_emptyenv (t8, u8) *)"
-*}
-@{ML_response [display, gray]
-"val t9 = @{term_pat \"(% y. ?f y)\"};
-val u9 = @{term_pat \"(% y. ?f y)\"};
-(* trivial solutions are empty and don't contain ?f = ?f etc *)
-patunif_in_emptyenv (t9, u9)"
-*}
-@{ML_response [display, gray]
-"val t10 = @{term_pat \"(% y. (% x. ?f x) y)\"};
-val u10 = @{term_pat \"(% y. ?f y)\"};
-(* trivial solutions are empty and don't contain ?f = ?f etc *)
-patunif_in_emptyenv (t10, u10)"
-*}
-@{ML_response [display, gray]
-"val t11 = @{term_pat \"(% z. ?f z)\"};
-val u11 = @{term_pat \"(% z. k (?f z))\"};
-(* fails: occurs check *)
-(* patunif_in_emptyenv (t11, u11) *)"
-*}
-@{ML_response [display, gray]
-"val t12 = @{term_pat \"(% z. ?f z)\"};
-val u12 = @{term_pat \"?g a\"};
-(* fails: *both* terme have to be higher-order patterns *)
-(* patunif_in_emptyenv (t12, u12) *)"
-*}
-*}
-*)
-text {*
 As mentioned before, unrestricted higher-order unification, respectively
 unrestricted higher-order matching, is in general undecidable and might also
 not posses a single most general solution. Therefore Isabelle implements the
 unification function @{ML_ind unifiers in Unify} so that it returns a lazy
 @{ML_response_fake [display,gray]
 "let
 val eq = @{thm True_def}
 in
 (Thm.lhs_of eq, Thm.rhs_of eq)
-|> pairself (string_of_cterm @{context})
+|> pairself (Pretty.string_of o (pretty_cterm @{context}))
 end"
 "(True, (\<lambda>x. x) = (\<lambda>x. x))"}
 Other function produce terms that can be pattern-matched.
 Suppose the following two theorems.
 @{ML_response_fake [display,gray]
 "let
 val ctxt = @{context}
 fun prems_and_concl thm =
-[\"Premises: \"   ^ (string_of_terms ctxt (Thm.prems_of thm))] @
+[[Pretty.str \"Premises:\", pretty_terms ctxt (Thm.prems_of thm)],
-[\"Conclusion: \" ^ (string_of_term ctxt (Thm.concl_of thm))]
+[Pretty.str \"Conclusion:\", pretty_term ctxt (Thm.concl_of thm)]]
-|> cat_lines
+|> map Pretty.block
-|> tracing
+|> Pretty.chunks
+|> pwriteln
 in
 prems_and_concl @{thm foo_test1};
 prems_and_concl @{thm foo_test2}
 end"
 "Premises: ?A, ?B

changeset 441	520127b708e6
parent 440	a0b280dd4bc7
child 446	4c32349b9875