# HG changeset patch # User Christian Urban # Date 1387151345 0 # Node ID 82c482467d75dd529ec65367ad3be722233e2a97 # Parent be361e980acf0bf62ed03bf59ab66052aced572c updated to latest isabelle diff -r be361e980acf -r 82c482467d75 ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Sat Aug 31 08:07:45 2013 +0100 +++ b/ProgTutorial/Advanced.thy Sun Dec 15 23:49:05 2013 +0000 @@ -546,7 +546,7 @@ The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as *} -ML %grayML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*} +ML %grayML{*val identity = Morphism.morphism "" {binding = [], typ = [], term = [], fact = []}*} text {* Morphisms can be composed with the function @{ML_ind "$>" in Morphism} @@ -557,7 +557,7 @@ | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s) | trm_phi t = t*} -ML %grayML{*val phi = Morphism.term_morphism trm_phi*} +ML %grayML{*val phi = Morphism.term_morphism "foo" trm_phi*} ML %grayML{*Morphism.term phi @{term "P x y"}*} diff -r be361e980acf -r 82c482467d75 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Sat Aug 31 08:07:45 2013 +0100 +++ b/ProgTutorial/Essential.thy Sun Dec 15 23:49:05 2013 +0000 @@ -1769,7 +1769,7 @@ @{ML_response_fake [display,gray,linenos] "Thm.reflexive @{cterm \"True\"} - |> Simplifier.rewrite_rule [@{thm True_def}] + |> Simplifier.rewrite_rule @{context} [@{thm True_def}] |> pretty_thm @{context} |> pwriteln" "(\x. x) = (\x. x) \ (\x. x) = (\x. x)"} @@ -1785,7 +1785,7 @@ replaces all object connectives by equivalents in the meta logic. For example @{ML_response_fake [display, gray] - "Object_Logic.rulify @{thm foo_test2}" + "Object_Logic.rulify @{context} @{thm foo_test2}" "\?A; ?B\ \ ?C"} The transformation in the other direction can be achieved with function @@ -1794,9 +1794,9 @@ @{ML_response_fake [display,gray] "let val thm = @{thm foo_test1} - val meta_eq = Object_Logic.atomize (cprop_of thm) + val meta_eq = Object_Logic.atomize @{context} (cprop_of thm) in - Raw_Simplifier.rewrite_rule [meta_eq] thm + Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm end" "?A \ ?B \ ?C"} @@ -1815,19 +1815,19 @@ following function for atomizing a theorem. *} -ML %grayML{*fun atomize_thm thm = +ML %grayML{*fun atomize_thm ctxt thm = let val thm' = forall_intr_vars thm - val thm'' = Object_Logic.atomize (cprop_of thm') + val thm'' = Object_Logic.atomize ctxt (cprop_of thm') in - Raw_Simplifier.rewrite_rule [thm''] thm' + Raw_Simplifier.rewrite_rule ctxt [thm''] thm' end*} text {* This function produces for the theorem @{thm [source] list.induct} @{ML_response_fake [display, gray] - "atomize_thm @{thm list.induct}" + "atomize_thm @{context} @{thm list.induct}" "\P list. P [] \ (\a list. P list \ P (a # list)) \ P list"} Theorems can also be produced from terms by giving an explicit proof. diff -r be361e980acf -r 82c482467d75 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Sat Aug 31 08:07:45 2013 +0100 +++ b/ProgTutorial/Package/Ind_Code.thy Sun Dec 15 23:49:05 2013 +0000 @@ -253,10 +253,10 @@ be implemented as follows: *} -ML %linenosgray{*fun ind_tac defs prem insts = - EVERY1 [Object_Logic.full_atomize_tac, +ML %linenosgray{*fun ind_tac ctxt defs prem insts = + EVERY1 [Object_Logic.full_atomize_tac ctxt, cut_facts_tac prem, - rewrite_goal_tac defs, + rewrite_goal_tac ctxt defs, inst_spec_tac insts, assume_tac]*} @@ -277,7 +277,7 @@ lemma automatic_ind_prin_even: assumes prem: "even z" shows "P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P z" -by (tactic {* ind_tac eo_defs @{thms prem} +by (tactic {* ind_tac @{context} eo_defs @{thms prem} [@{cterm "P::nat\bool"}, @{cterm "Q::nat\bool"}] *}) lemma automatic_ind_prin_fresh: @@ -286,7 +286,7 @@ (\a t s. \P a t; P a s\ \ P a (App t s)) \ (\a t. P a (Lam a t)) \ (\a b t. \a \ b; P a t\ \ P a (Lam b t)) \ P z za" -by (tactic {* ind_tac @{thms fresh_def} @{thms prem} +by (tactic {* ind_tac @{context} @{thms fresh_def} @{thms prem} [@{cterm "P::string\trm\bool"}] *}) @@ -340,7 +340,7 @@ (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs))) in Goal.prove lthy' [] [prem] goal - (fn {prems, ...} => ind_tac defs prems cnewpreds) + (fn {prems, context, ...} => ind_tac context defs prems cnewpreds) |> singleton (Proof_Context.export lthy' lthy) end *} @@ -539,9 +539,9 @@ will use the tactic *} -ML %linenosgray{*fun expand_tac defs = - Object_Logic.rulify_tac 1 - THEN rewrite_goal_tac defs 1 +ML %linenosgray{*fun expand_tac ctxt defs = + Object_Logic.rulify_tac ctxt 1 + THEN rewrite_goal_tac ctxt defs 1 THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *} text {* @@ -554,7 +554,7 @@ lemma fresh_Lam: shows "\a b t. \a \ b; fresh a t\ \ fresh a (Lam b t)" (*>*) -apply(tactic {* expand_tac @{thms fresh_def} *}) +apply(tactic {* expand_tac @{context} @{thms fresh_def} *}) txt {* gives us the goal state @@ -645,7 +645,7 @@ (*<*) lemma fresh_Lam: shows "\a b t. \a \ b; fresh a t\ \ fresh a (Lam b t)" -apply(tactic {* expand_tac @{thms fresh_def} *}) +apply(tactic {* expand_tac @{context} @{thms fresh_def} *}) (*>*) apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} 1 *}) (*<*)oops(*>*) @@ -692,7 +692,7 @@ val (params1, params2) = chop (length cparams - length preds) cparams val (prems1, prems2) = chop (length prems - length rules) prems in - rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 + rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1 end) *} text {* @@ -706,7 +706,7 @@ (*<*) lemma fresh_Lam: shows "\a b t. \a \ b; fresh a t\ \ fresh a (Lam b t)" -apply(tactic {* expand_tac @{thms fresh_def} *}) +apply(tactic {* expand_tac @{context} @{thms fresh_def} *}) (*>*) apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} 1 *}) (*<*)oops(*>*) @@ -759,13 +759,13 @@ *} ML %grayML{*fun prove_intro_tac i preds rules = - SUBPROOF (fn {params, prems, ...} => + SUBPROOF (fn {params, prems, context, ...} => let val cparams = map snd params val (params1, params2) = chop (length cparams - length preds) cparams val (prems1, prems2) = chop (length prems - length rules) prems in - rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 + rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1 THEN EVERY1 (map (prepare_prem params2 prems2) prems1) end) *} @@ -776,7 +776,7 @@ lemma fresh_Lam: shows "\a b t. \a \ b; fresh a t\ \ fresh a (Lam b t)" -apply(tactic {* expand_tac @{thms fresh_def} *}) +apply(tactic {* expand_tac @{context} @{thms fresh_def} *}) apply(tactic {* prove_intro_tac 3 [fresh_pred] fresh_rules @{context} 1 *}) done @@ -793,7 +793,7 @@ lemma accpartI: shows "\R x. (\y. R y x \ accpart R y) \ accpart R x" -apply(tactic {* expand_tac @{thms accpart_def} *}) +apply(tactic {* expand_tac @{context} @{thms accpart_def} *}) apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} 1 *}) apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} 1 *}) @@ -864,7 +864,7 @@ val (params1, params2) = chop (length cparams - length preds) cparams val (prems1, prems2) = chop (length prems - length rules) prems in - rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 + rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1 THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1) end) *} @@ -875,7 +875,7 @@ lemma accpartI: shows "\R x. (\y. R y x \ accpart R y) \ accpart R x" -apply(tactic {* expand_tac @{thms accpart_def} *}) +apply(tactic {* expand_tac @{context} @{thms accpart_def} *}) apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *}) done @@ -885,8 +885,8 @@ *} ML %linenosgray{*fun intro_tac defs rules preds i ctxt = - EVERY1 [Object_Logic.rulify_tac, - rewrite_goal_tac defs, + EVERY1 [Object_Logic.rulify_tac ctxt, + rewrite_goal_tac ctxt defs, REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]), prove_intro_tac i preds rules ctxt]*} diff -r be361e980acf -r 82c482467d75 ProgTutorial/Package/simple_inductive_package.ML --- a/ProgTutorial/Package/simple_inductive_package.ML Sat Aug 31 08:07:45 2013 +0100 +++ b/ProgTutorial/Package/simple_inductive_package.ML Sun Dec 15 23:49:05 2013 +0000 @@ -62,10 +62,10 @@ Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; (* @chunk induction_tac *) -fun induction_tac defs prems insts = - EVERY1 [Object_Logic.full_atomize_tac, +fun induction_tac ctxt defs prems insts = + EVERY1 [Object_Logic.full_atomize_tac ctxt, cut_facts_tac prems, - rewrite_goal_tac defs, + rewrite_goal_tac ctxt defs, EVERY' (map (dtac o inst_spec) insts), assume_tac] (* @end *) @@ -96,7 +96,7 @@ (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) in Goal.prove lthy4 [] [prem] goal - (fn {prems, ...} => induction_tac defs prems cnewpreds) + (fn {prems, context, ...} => induction_tac context defs prems cnewpreds) |> singleton (Proof_Context.export lthy4 lthy1) end in @@ -131,15 +131,15 @@ val (prems1, prems2) = chop (length prems - length rules) prems; val (params1, params2) = chop (length params - length preds) (map snd params); in - rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 + rtac (Object_Logic.rulify ctxt' (all_elims params1 (nth prems2 i))) 1 THEN EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) end) (* @end *) fun introductions_tac defs rules preds i ctxt = - EVERY1 [Object_Logic.rulify_tac, - rewrite_goal_tac defs, + EVERY1 [Object_Logic.rulify_tac ctxt, + rewrite_goal_tac ctxt defs, REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), subproof1 rules preds i ctxt] diff -r be361e980acf -r 82c482467d75 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Sat Aug 31 08:07:45 2013 +0100 +++ b/ProgTutorial/Tactical.thy Sun Dec 15 23:49:05 2013 +0000 @@ -1574,7 +1574,7 @@ lemma shows "MyTrue \ True" -apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *}) +apply(tactic {* rewrite_goal_tac @{context} @{thms MyTrue_def} 1 *}) txt{* producing the goal state \begin{isabelle} @{subgoals [display]} diff -r be361e980acf -r 82c482467d75 progtutorial.pdf Binary file progtutorial.pdf has changed