isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:aec7073d4645
+:daf404920ab9
 pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
 end*}
 text {*
 We can install this pretty printer with the function
-@{ML_ind addPrettyPrinter in PolyML} as follows.
+@{ML_ind ML_system_pp} as follows.
 *}
-ML %grayML{*PolyML.addPrettyPrinter
+ML %grayML{*ML_system_pp
-(fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*}
+(fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)*}
+ML \<open>@{typ "bool"}\<close>
 text {*
 Now the type bool is printed out in full detail.
 @{ML_response [display,gray]
 "@{typ \"bool\"}"
 We can restore the usual behaviour of Isabelle's pretty printer
 with the code
 *}
-ML %grayML{*PolyML.addPrettyPrinter
+ML %grayML{*ML_system_pp
-(fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*}
+(fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)*}
 text {*
 After that the types for booleans, lists and so on are printed out again
 the standard Isabelle way.
 |> pwriteln
 fun pretty_tyenv ctxt tyenv =
 let
 fun get_typs (v, (s, T)) = (TVar (v, s), T)
-val print = pairself (pretty_typ ctxt)
+val print = apply2 (pretty_typ ctxt)
 in
 pretty_helper (print o get_typs) tyenv
 end*}
 text_raw {*
 \end{isabelle}
 *}
 ML %grayML{*fun pretty_env ctxt env =
 let
 fun get_trms (v, (T, t)) = (Var (v, T), t)
-val print = pairself (pretty_term ctxt)
+val print = apply2 (pretty_term ctxt)
 in
 pretty_helper (print o get_trms) env
 end*}
 text {*
 @{ML_response [display, gray]
 "let
 val trm_list =
 [@{term_pat \"?X\"}, @{term_pat \"a\"},
 @{term_pat \"f (\<lambda>a b. ?X a b) c\"},
-@{term_pat \"\<lambda>a b. (op +) a b\"},
+@{term_pat \"\<lambda>a b. (+) a b\"},
-@{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"},
+@{term_pat \"\<lambda>a. (+) a ?Y\"}, @{term_pat \"?X ?Y\"},
 @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"},
 @{term_pat \"?X a\"}]
 in
 map Pattern.pattern trm_list
 end"
 @{ML_response_fake [display, gray]
 "let
 val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
 val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
 val init = Envir.empty 0
-val env = Pattern.unify @{theory} (trm1, trm2) init
+val env = Pattern.unify (Context.Proof @{context}) (trm1, trm2) init (* FIXME: Reference to generic context *)
 in
 pretty_env @{context} (Envir.term_env env)
 end"
 "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}
 let
 val trm1 = @{term_pat "?X ?Y"}
 val trm2 = @{term "f a"}
 val init = Envir.empty 0
 in
-Unify.unifiers (@{theory}, init, [(trm1, trm2)])
+Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
 end *}
 text {*
 The unifiers can be extracted from the lazy sequence using the
 function @{ML_ind "Seq.pull"}. In the example we obtain three
 "let
 val trm1 = @{term \"a\"}
 val trm2 = @{term \"b\"}
 val init = Envir.empty 0
 in
-Unify.unifiers (@{theory}, init, [(trm1, trm2)])
+Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
 |> Seq.pull
 end"
 "NONE"}
 In order to find a reasonable solution for a unification problem, Isabelle
 behaviour since the unification has more than one solution. One way round
 this problem is to instantiate the schematic variables @{text "?P"} and
 @{text "?x"}.  Instantiation function for theorems is
 @{ML_ind instantiate_normalize in Drule} from the structure
 @{ML_struct Drule}. One problem, however, is
-that this function expects the instantiations as lists of @{ML_type ctyp}
+that this function expects the instantiations as lists of @{ML_type "((indexname * sort) * ctyp)"}
-and @{ML_type cterm} pairs:
+respective @{ML_type "(indexname * typ) * cterm"}:
 \begin{isabelle}
 @{ML instantiate_normalize in Drule}@{text ":"}
-@{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}
+@{ML_type "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm"}
 \end{isabelle}
 This means we have to transform the environment the higher-order matching
 function returns into such an instantiation. For this we use the functions
 @{ML_ind term_env in Envir} and @{ML_ind type_env in Envir}, which extract
 from an environment the corresponding variable mappings for schematic type
 and term variables. These mappings can be turned into proper
 @{ML_type ctyp}-pairs with the function
 *}
-ML %grayML{*fun prep_trm thy (x, (T, t)) =
+ML %grayML{*fun prep_trm ctxt (x, (T, t)) =
-(cterm_of thy (Var (x, T)), cterm_of thy t)*}
+((x, T), Thm.cterm_of ctxt t)*}
 text {*
 and into proper @{ML_type cterm}-pairs with
 *}
-ML %grayML{*fun prep_ty thy (x, (S, ty)) =
+ML %grayML{*fun prep_ty ctxt (x, (S, ty)) =
-(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*}
+((x, S), Thm.ctyp_of ctxt ty)*}
 text {*
 We can now calculate the instantiations from the matching function.
 *}
-ML %linenosgray{*fun matcher_inst thy pat trm i =
+ML %linenosgray{*fun matcher_inst ctxt pat trm i =
 let
-val univ = Unify.matchers thy [(pat, trm)]
+val univ = Unify.matchers (Context.Proof ctxt) [(pat, trm)]
 val env = nth (Seq.list_of univ) i
 val tenv = Vartab.dest (Envir.term_env env)
 val tyenv = Vartab.dest (Envir.type_env env)
 in
-(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+(map (prep_ty ctxt) tyenv, map (prep_trm ctxt) tenv)
 end*}
+ML \<open>Context.get_generic_context\<close>
 text {*
 In Line 3 we obtain the higher-order matcher. We assume there is a finite
 number of them and select the one we are interested in via the parameter
 @{text i} in the next line. In Lines 5 and 6 we destruct the resulting
 environments using the function @{ML_ind dest in Vartab}. Finally, we need
 @{term "Q True"}.
 @{ML_response_fake [gray,display,linenos]
 "let
-val pat = Logic.strip_imp_concl (prop_of @{thm spec})
+val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
 val trm = @{term \"Trueprop (Q True)\"}
-val inst = matcher_inst @{theory} pat trm 1
+val inst = matcher_inst @{context} pat trm 1
 in
 Drule.instantiate_normalize inst @{thm spec}
 end"
 "\<forall>x. Q x \<Longrightarrow> Q True"}
 converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
 term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
 abstract objects that are guaranteed to be type-correct, and they can only
 be constructed via ``official interfaces''.
-Certification is always relative to a theory context. For example you can
+Certification is always relative to a context. For example you can
 write:
 @{ML_response_fake [display,gray]
-"cterm_of @{theory} @{term \"(a::nat) + b = c\"}"
+"Thm.cterm_of @{context} @{term \"(a::nat) + b = c\"}"
 "a + b = c"}
 This can also be written with an antiquotation:
 @{ML_response_fake [display,gray]
 "let
 val natT = @{typ \"nat\"}
 val zero = @{term \"0::nat\"}
 val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
 in
-cterm_of @{theory} (plus $ zero $ zero)
+Thm.cterm_of @{context} (plus $ zero $ zero)
 end"
 "0 + 0"}
 In Isabelle not just terms need to be certified, but also types. For example,
 you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on
 the ML-level as follows:
 @{ML_response_fake [display,gray]
-"ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
+"Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})"
 "nat \<Rightarrow> bool"}
 or with the antiquotation:
 @{ML_response_fake [display,gray]
 @{ML_struct Local_Theory} (the Isabelle command
 \isacommand{local\_setup} will be explained in more detail in
 Section~\ref{sec:local}).
 *}
+(*FIXME: add forward reference to Proof_Context.export *)
+ML %linenosgray{*val my_thm_vars =
+let
+val ctxt0 = @{context}
+val (_, ctxt1) = Variable.add_fixes ["P", "Q", "t"] ctxt0
+in
+singleton (Proof_Context.export ctxt1 ctxt0) my_thm
+end*}
 local_setup %gray {*
-Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
+Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd *}
 text {*
 The third argument of @{ML note in Local_Theory} is the list of theorems we
 want to store under a name. We can store more than one under a single name.
 The first argument of @{ML note in Local_Theory} is the name under
 @{ML_ind simp_add in Simplifier}, for adding the theorem to the simpset:
 *}
 local_setup %gray {*
 Local_Theory.note ((@{binding "my_thm_simp"},
-[Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
+[Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd *}
 text {*
 Note that we have to use another name under which the theorem is stored,
 since Isabelle does not allow us to call  @{ML_ind note in Local_Theory} twice
 with the same name. The attribute needs to be wrapped inside the function @{ML_ind
 @{ML_response_fake [display,gray]
 "let
 val eq = @{thm True_def}
 in
 (Thm.lhs_of eq, Thm.rhs_of eq)
-|> pairself (Pretty.string_of o (pretty_cterm @{context}))
+|> apply2 (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_ind atomize in Object_Logic} and the following code.
 @{ML_response_fake [display,gray]
 "let
 val thm = @{thm foo_test1}
-val meta_eq = Object_Logic.atomize @{context} (cprop_of thm)
+val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
 in
 Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm
 end"
 "?A \<longrightarrow> ?B \<longrightarrow> ?C"}
 *}
 ML %grayML{*fun atomize_thm ctxt thm =
 let
 val thm' = forall_intr_vars thm
-val thm'' = Object_Logic.atomize ctxt (cprop_of thm')
+val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm')
 in
 Raw_Simplifier.rewrite_rule ctxt [thm''] thm'
 end*}
 text {*
 to prove the term @{term "P \<Longrightarrow> P"}.
 @{ML_response_fake [display,gray]
 "let
 val trm = @{term \"P \<Longrightarrow> P::bool\"}
-val tac = K (atac 1)
+val tac = K (assume_tac @{context} 1)
 in
 Goal.prove @{context} [\"P\"] [] trm tac
 end"
 "?P \<Longrightarrow> ?P"}
 proved. The fifth is a corresponding proof given in form of a tactic (we explain
 tactics in Chapter~\ref{chp:tactical}). In the code above, the tactic proves the
 theorem by assumption.
 There is also the possibility of proving multiple goals at the same time
-using the function @{ML_ind prove_multi in Goal}. For this let us define the
+using the function @{ML_ind prove_common in Goal}. For this let us define the
 following three helper functions.
 *}
 ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"}
-fun rep_tacs i = replicate i (rtac @{thm refl})
+fun rep_tacs i = replicate i (resolve_tac @{context} [@{thm refl}])
 fun multi_test ctxt i =
-Goal.prove_multi ctxt ["f", "x"] [] (rep_goals i)
+Goal.prove_common ctxt NONE ["f", "x"] [] (rep_goals i)
 (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))*}
 text {*
 With them we can now produce three theorem instances of the
 proposition.
 @{ML_response_fake [display, gray]
 "multi_test @{context} 3"
 "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
-However you should be careful with @{ML prove_multi in Goal} and very
+However you should be careful with @{ML prove_common in Goal} and very
 large goals. If you increase the counter in the code above to @{text 3000},
 you will notice that takes approximately ten(!) times longer than
 using @{ML map} and @{ML prove in Goal}.
 *}
 ML %grayML{*let
 fun test_prove ctxt thm =
-Goal.prove ctxt ["P", "x"] [] thm (K (rtac @{thm refl} 1))
+Goal.prove ctxt ["P", "x"] [] thm (K (resolve_tac  @{context} [@{thm refl}] 1))
 in
 map (test_prove @{context}) (rep_goals 3000)
 end*}
 text {*
 that analyse the @{ML_type_ind proof_body} data-structure from the
 structure @{ML_struct Proofterm}.
 *}
 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms
-val get_names = map #1 o pthms_of
+val get_names = (map Proofterm.thm_node_name) o pthms_of
-val get_pbodies = map (Future.join o #3) o pthms_of *}
+val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of *}
 text {*
 To see what their purpose is, consider the following three short proofs.
 *}
 version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
 to produce the ``symmetric'' version of an equation. The main function behind
 this attribute is
 *}
-ML %grayML{*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
 context (which we ignore in the code above) and a theorem (@{text thm}), and
 returns another theorem (namely @{text thm} resolved with the theorem
 ML %grayML{*fun MY_THEN thms =
 let
 fun RS_rev thm1 thm2 = thm2 RS thm1
 in
-Thm.rule_attribute (fn _ => fn thm => fold RS_rev thms thm)
+Thm.rule_attribute [] (fn _ => fn thm => fold RS_rev thms thm)
 end*}
 text {*
 where for convenience we define the reverse and curried version of @{ML RS}.
 The setup of this theorem attribute uses the parser @{ML thms in Attrib},
 To see the proper line breaking, you can try out the function on a bigger term
 and type. For example:
 @{ML_response_fake [display,gray]
-"tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
+"tell_type @{context} @{term \"(=) ((=) ((=) ((=) ((=) (=)))))\"}"
-"The term \"op = (op = (op = (op = (op = op =))))\" has type
+"The term \"(=) ((=) ((=) ((=) ((=) (=)))))\" has type
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 \begin{readmore}
 The general infrastructure for pretty-printing is implemented in the file
 @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}

changeset 562	daf404920ab9
parent 559	ffa5c4ec9611
child 565	cecd7a941885