diff -r aec7073d4645 -r daf404920ab9 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Fri Jun 03 15:15:17 2016 +0100 +++ b/ProgTutorial/Essential.thy Tue May 14 11:10:53 2019 +0200 @@ -253,12 +253,13 @@ 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 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*} - +ML %grayML{*ML_system_pp + (fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)*} + +ML \@{typ "bool"}\ text {* Now the type bool is printed out in full detail. @@ -286,8 +287,8 @@ with the code *} -ML %grayML{*PolyML.addPrettyPrinter - (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*} +ML %grayML{*ML_system_pp + (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 @@ -817,7 +818,7 @@ 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*} @@ -997,7 +998,7 @@ 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*} @@ -1080,8 +1081,8 @@ val trm_list = [@{term_pat \"?X\"}, @{term_pat \"a\"}, @{term_pat \"f (\a b. ?X a b) c\"}, - @{term_pat \"\a b. (op +) a b\"}, - @{term_pat \"\a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"}, + @{term_pat \"\a b. (+) a b\"}, + @{term_pat \"\a. (+) a ?Y\"}, @{term_pat \"?X ?Y\"}, @{term_pat \"\a b. ?X a b ?Y\"}, @{term_pat \"\a. ?X a a\"}, @{term_pat \"?X a\"}] in @@ -1106,7 +1107,7 @@ val trm1 = @{term_pat \"\x y. g (?X y x) (f (?Y x))\"} val trm2 = @{term_pat \"\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" @@ -1134,7 +1135,7 @@ 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 {* @@ -1171,7 +1172,7 @@ 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"} @@ -1215,12 +1216,12 @@ @{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} - and @{ML_type cterm} pairs: + that this function expects the instantiations as lists of @{ML_type "((indexname * sort) * ctyp)"} + 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 @@ -1231,30 +1232,31 @@ @{ML_type ctyp}-pairs with the function *} -ML %grayML{*fun prep_trm thy (x, (T, t)) = - (cterm_of thy (Var (x, T)), cterm_of thy t)*} +ML %grayML{*fun prep_trm ctxt (x, (T, 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)) = - (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*} +ML %grayML{*fun prep_ty ctxt (x, (S, 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 \Context.get_generic_context\ 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 @@ -1268,9 +1270,9 @@ @{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" @@ -1429,11 +1431,11 @@ 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: @@ -1457,7 +1459,7 @@ 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"} @@ -1466,7 +1468,7 @@ 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 \ bool"} or with the antiquotation: @@ -1575,8 +1577,18 @@ 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 @@ -1590,7 +1602,7 @@ 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, @@ -1720,7 +1732,7 @@ 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, (\x. x) = (\x. x))"} @@ -1795,7 +1807,7 @@ @{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" @@ -1819,7 +1831,7 @@ 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*} @@ -1839,7 +1851,7 @@ @{ML_response_fake [display,gray] "let val trm = @{term \"P \ P::bool\"} - val tac = K (atac 1) + val tac = K (assume_tac @{context} 1) in Goal.prove @{context} [\"P\"] [] trm tac end" @@ -1853,15 +1865,15 @@ 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 {* @@ -1872,7 +1884,7 @@ "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}. @@ -1880,7 +1892,7 @@ 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*} @@ -1991,8 +2003,8 @@ *} ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms -val get_names = map #1 o pthms_of -val get_pbodies = map (Future.join o #3) o pthms_of *} +val get_names = (map Proofterm.thm_node_name) 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. @@ -2248,7 +2260,7 @@ 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 @@ -2313,7 +2325,7 @@ 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 {* @@ -2715,8 +2727,8 @@ and type. For example: @{ML_response_fake [display,gray] - "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}" - "The term \"op = (op = (op = (op = (op = op =))))\" has type + "tell_type @{context} @{term \"(=) ((=) ((=) ((=) ((=) (=)))))\"}" + "The term \"(=) ((=) ((=) ((=) ((=) (=)))))\" has type \"((((('a \ 'a \ bool) \ bool) \ bool) \ bool) \ bool) \ bool\"."} \begin{readmore}