--- a/ProgTutorial/Essential.thy Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Essential.thy Sun Mar 07 21:15:05 2010 +0100
@@ -39,7 +39,7 @@
@{ML_response [display,gray]
"@{term \"(a::nat) + b = c\"}"
"Const (\"op =\", \<dots>) $
- (Const (\"Algebras.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+ (Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using
the internal representation corresponding to the datatype @{ML_type_ind "term"},
@@ -533,8 +533,8 @@
\mbox{@{text "(op *)"}}:
@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})"
- "(Const (\"Algebras.zero_class.zero\", \<dots>),
- Const (\"Algebras.times_class.times\", \<dots>))"}
+ "(Const (\"Groups.zero_class.zero\", \<dots>),
+ Const (\"Groups.times_class.times\", \<dots>))"}
While you could use the complete name, for example
@{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
@@ -770,6 +770,9 @@
assumption about the sorts, they are incomparable.
*}
+class s1
+class s2
+
ML{*val (tyenv, index) = let
val ty1 = @{typ_pat "?'a::s1"}
val ty2 = @{typ_pat "?'b::s2"}
@@ -1639,26 +1642,26 @@
stated using object logic connectives, while theorems using the connectives
from the meta logic are more convenient for reasoning. Therefore there are
some build in functions which help with these transformations. The function
- @{ML_ind rulify in ObjectLogic}
+ @{ML_ind rulify in Object_Logic}
replaces all object connectives by equivalents in the meta logic. For example
@{ML_response_fake [display, gray]
- "ObjectLogic.rulify @{thm foo_test2}"
+ "Object_Logic.rulify @{thm foo_test2}"
"\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}
The transformation in the other direction can be achieved with function
- @{ML_ind atomize in ObjectLogic} and the following code.
+ @{ML_ind atomize in Object_Logic} and the following code.
@{ML_response_fake [display,gray]
"let
val thm = @{thm foo_test1}
- val meta_eq = ObjectLogic.atomize (cprop_of thm)
+ val meta_eq = Object_Logic.atomize (cprop_of thm)
in
MetaSimplifier.rewrite_rule [meta_eq] thm
end"
"?A \<longrightarrow> ?B \<longrightarrow> ?C"}
- In this code the function @{ML atomize in ObjectLogic} produces
+ In this code the function @{ML atomize in Object_Logic} produces
a meta-equation between the given theorem and the theorem transformed
into the object logic. The result is the theorem with object logic
connectives. However, in order to completely transform a theorem
@@ -1676,7 +1679,7 @@
ML{*fun atomize_thm thm =
let
val thm' = forall_intr_vars thm
- val thm'' = ObjectLogic.atomize (cprop_of thm')
+ val thm'' = Object_Logic.atomize (cprop_of thm')
in
MetaSimplifier.rewrite_rule [thm''] thm'
end*}
@@ -1688,8 +1691,6 @@
"atomize_thm @{thm list.induct}"
"\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
- \footnote{\bf FIXME: say someting about @{ML_ind standard in Drule}.}
-
Theorems can also be produced from terms by giving an explicit proof.
One way to achieve this is by using the function @{ML_ind prove in Goal}
in the structure @{ML_struct Goal}. For example below we use this function
--- a/ProgTutorial/Package/Ind_Code.thy Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy Sun Mar 07 21:15:05 2010 +0100
@@ -137,7 +137,7 @@
ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy =
let
val thy = ProofContext.theory_of lthy
- val orules = map (ObjectLogic.atomize_term thy) rules
+ val orules = map (Object_Logic.atomize_term thy) rules
val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss)
in
fold_map make_defn (prednames ~~ mxs ~~ defs) lthy
@@ -150,7 +150,7 @@
meta-connectives). To do this transformation we have to obtain the theory
behind the local theory using the function @{ML_ind theory_of in ProofContext}
(Line 3); with this theory we can use the function
- @{ML_ind atomize_term in ObjectLogic} to make the transformation (Line 4). The call
+ @{ML_ind atomize_term in Object_Logic} to make the transformation (Line 4). The call
to @{ML defn_aux} in Line 5 produces all right-hand sides of the
definitions. The actual definitions are then made in Line 7. The result of
the function is a list of theorems and a local theory (the theorems are
@@ -254,7 +254,7 @@
*}
ML %linenosgray{*fun ind_tac defs prem insts =
- EVERY1 [ObjectLogic.full_atomize_tac,
+ EVERY1 [Object_Logic.full_atomize_tac,
cut_facts_tac prem,
rewrite_goal_tac defs,
inst_spec_tac insts,
@@ -540,7 +540,7 @@
*}
ML %linenosgray{*fun expand_tac defs =
- ObjectLogic.rulify_tac 1
+ Object_Logic.rulify_tac 1
THEN rewrite_goal_tac defs 1
THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
@@ -679,7 +679,7 @@
To use this premise with @{ML rtac}, we need to instantiate its
quantifiers (with @{text params1}) and transform it into rule
- format (using @{ML_ind rulify in ObjectLogic}). So we can modify the
+ format (using @{ML_ind rulify in Object_Logic}). So we can modify the
code as follows:
*}
@@ -690,7 +690,7 @@
val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
- rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1
end) *}
text {*
@@ -763,7 +763,7 @@
val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
- rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1
THEN EVERY1 (map (prepare_prem params2 prems2) prems1)
end) *}
@@ -861,7 +861,7 @@
val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
- rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1
THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1)
end) *}
@@ -882,7 +882,7 @@
*}
ML %linenosgray{*fun intro_tac defs rules preds i ctxt =
- EVERY1 [ObjectLogic.rulify_tac,
+ EVERY1 [Object_Logic.rulify_tac,
rewrite_goal_tac defs,
REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
prove_intro_tac i preds rules ctxt]*}
--- a/ProgTutorial/Package/simple_inductive_package.ML Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML Sun Mar 07 21:15:05 2010 +0100
@@ -50,7 +50,7 @@
fun definitions rules params preds prednames syns arg_typess lthy =
let
val thy = ProofContext.theory_of lthy
- val orules = map (ObjectLogic.atomize_term thy) rules
+ val orules = map (Object_Logic.atomize_term thy) rules
val defs =
map (defs_aux lthy orules preds params) (preds ~~ arg_typess)
in
@@ -63,7 +63,7 @@
(* @chunk induction_tac *)
fun induction_tac defs prems insts =
- EVERY1 [ObjectLogic.full_atomize_tac,
+ EVERY1 [Object_Logic.full_atomize_tac,
cut_facts_tac prems,
rewrite_goal_tac defs,
EVERY' (map (dtac o inst_spec) insts),
@@ -131,14 +131,14 @@
val (prems1, prems2) = chop (length prems - length rules) prems;
val (params1, params2) = chop (length params - length preds) (map snd params);
in
- rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ rtac (Object_Logic.rulify (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 [ObjectLogic.rulify_tac,
+ EVERY1 [Object_Logic.rulify_tac,
rewrite_goal_tac defs,
REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
subproof1 rules preds i ctxt]
--- a/ProgTutorial/Recipes/ExternalSolver.thy Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Recipes/ExternalSolver.thy Sun Mar 07 21:15:05 2010 +0100
@@ -10,7 +10,7 @@
You want to use an external application.
\smallskip
- {\bf Solution:} The function @{ML system_out} might be the right thing for
+ {\bf Solution:} The function @{ML bash_output} might be the right thing for
you.
\smallskip
@@ -20,7 +20,7 @@
For example, consider running an ordinary shell commands:
@{ML_response [display,gray]
- "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
+ "bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
on Page~\pageref{rec:timeout}), i.e. external applications are killed
@@ -28,10 +28,10 @@
one second:
@{ML_response_fake [display,gray]
- "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"
+ "TimeLimit.timeLimit (Time.fromSeconds 1) bash_output \"sleep 30\"
handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
- The function @{ML system_out} can also be used for more reasonable
+ The function @{ML bash_output} can also be used for more reasonable
applications, e.g. coupling external solvers with Isabelle. In that case,
one has to make sure that Isabelle can find the particular executable.
One way to ensure this is by adding a Bash-like variable binding into
@@ -46,7 +46,7 @@
In Isabelle, this application may now be executed by
- @{ML_response_fake [display,gray] "system_out \"$FOO\"" "\<dots>"}
+ @{ML_response_fake [display,gray] "bash_output \"$FOO\"" "\<dots>"}
*}
--- a/ProgTutorial/Tactical.thy Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Tactical.thy Sun Mar 07 21:15:05 2010 +0100
@@ -2178,7 +2178,7 @@
end"
"Const (\"==\",\<dots>) $
(Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $
- (Const (\"Algebras.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"}
+ (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"}
The argument @{ML true} in @{ML beta_conversion in Thm} indicates that
the right-hand side should be fully beta-normalised. If instead
Binary file progtutorial.pdf has changed