--- a/ProgTutorial/Essential.thy Tue Jul 20 13:34:44 2010 +0100
+++ b/ProgTutorial/Essential.thy Wed Jul 28 19:09:49 2010 +0200
@@ -1,12 +1,12 @@
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"]
*}
(*>*)
@@ -84,8 +84,8 @@
val v2 = Var ((\"x1\", 3), @{typ bool})
val v3 = Free (\"x\", @{typ bool})
in
- string_of_terms @{context} [v1, v2, v3]
- |> tracing
+ pretty_terms @{context} [v1, v2, v3]
+ |> pwriteln
end"
"?x3, ?x1.3, x"}
@@ -118,7 +118,7 @@
"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"}
@@ -423,8 +423,8 @@
val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
in
subst_bounds (rev vrs, trm)
- |> string_of_term @{context}
- |> tracing
+ |> pretty_term @{context}
+ |> pwriteln
end"
"x = y"}
@@ -457,8 +457,8 @@
"let
val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
in
- string_of_term @{context} eq
- |> tracing
+ eq |> pretty_term @{context}
+ |> pwriteln
end"
"True = False"}
@@ -713,15 +713,15 @@
\begin{isabelle}*}
ML{*fun pretty_helper aux env =
env |> Vartab.dest
- |> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux)
- |> commas
- |> enclose "[" "]"
- |> tracing
+ |> map ((fn (s1, s2) => Pretty.block [s1, Pretty.str ";=", s2]) o aux)
+ |> Pretty.commas
+ |> Pretty.enum "" "[" "]"
+ |> 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*}
@@ -901,7 +901,7 @@
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*}
@@ -942,8 +942,8 @@
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}
- |> tracing
+ |> pretty_term @{context}
+ |> pwriteln
end"
"P (\<lambda>a b. Q b a)"}
@@ -1024,106 +1024,6 @@
"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
@@ -1719,7 +1619,7 @@
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))"}
@@ -1738,10 +1638,11 @@
"let
val ctxt = @{context}
fun prems_and_concl thm =
- [\"Premises: \" ^ (string_of_terms ctxt (Thm.prems_of thm))] @
- [\"Conclusion: \" ^ (string_of_term ctxt (Thm.concl_of thm))]
- |> cat_lines
- |> tracing
+ [[Pretty.str \"Premises:\", pretty_terms ctxt (Thm.prems_of thm)],
+ [Pretty.str \"Conclusion:\", pretty_term ctxt (Thm.concl_of thm)]]
+ |> map Pretty.block
+ |> Pretty.chunks
+ |> pwriteln
in
prems_and_concl @{thm foo_test1};
prems_and_concl @{thm foo_test2}