--- 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"}*}
--- 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"
"(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>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}"
"\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?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 \<longrightarrow> ?B \<longrightarrow> ?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}"
"\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
Theorems can also be produced from terms by giving an explicit proof.
--- 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 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"
-by (tactic {* ind_tac eo_defs @{thms prem}
+by (tactic {* ind_tac @{context} eo_defs @{thms prem}
[@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})
lemma automatic_ind_prin_fresh:
@@ -286,7 +286,7 @@
(\<And>a t s. \<lbrakk>P a t; P a s\<rbrakk> \<Longrightarrow> P a (App t s)) \<Longrightarrow>
(\<And>a t. P a (Lam a t)) \<Longrightarrow>
(\<And>a b t. \<lbrakk>a \<noteq> b; P a t\<rbrakk> \<Longrightarrow> P a (Lam b t)) \<Longrightarrow> 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\<Rightarrow>trm\<Rightarrow>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 "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> 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 "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> 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 "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> 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 "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> 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 "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> 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 "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> 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]*}
--- 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]
--- 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 \<Longrightarrow> 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]}
Binary file progtutorial.pdf has changed