--- a/doc-src/TutorialI/Advanced/Partial.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy Fri Sep 28 19:17:01 2001 +0200
@@ -62,9 +62,9 @@
*}
consts divi :: "nat \<times> nat \<Rightarrow> nat"
-recdef divi "measure(\<lambda>(m,n). m)"
+recdef (permissive) divi "measure(\<lambda>(m,n). m)"
"divi(m,n) = (if n = 0 then arbitrary else
- if m < n then 0 else divi(m-n,n)+1)"
+ if m < n then 0 else divi(m-n,n)+1)" (* FIXME permissive!? *)
text{*\noindent Of course we could also have defined
@{term"divi(m,0)"} to be some specific number, for example 0. The
--- a/doc-src/TutorialI/Advanced/WFrec.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Fri Sep 28 19:17:01 2001 +0200
@@ -8,11 +8,11 @@
can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:
*}
-consts ack :: "nat\<times>nat \<Rightarrow> nat";
+consts ack :: "nat\<times>nat \<Rightarrow> nat"
recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
"ack(0,n) = Suc n"
"ack(Suc m,0) = ack(m, 1)"
- "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
+ "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"
text{*\noindent
The lexicographic product decreases if either its first component
@@ -67,8 +67,8 @@
*}
consts f :: "nat \<Rightarrow> nat"
-recdef f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
-"f i = (if #10 \<le> i then 0 else i * f(Suc i))";
+recdef (*<*)(permissive)(*<*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
+"f i = (if #10 \<le> i then 0 else i * f(Suc i))"
text{*\noindent
Since \isacommand{recdef} is not prepared for the relation supplied above,
@@ -81,9 +81,9 @@
txt{*\noindent
The proof is by showing that our relation is a subset of another well-founded
relation: one given by a measure function.\index{*wf_subset (theorem)}
-*};
+*}
-apply (rule wf_subset [of "measure (\<lambda>k::nat. N-k)"], blast);
+apply (rule wf_subset [of "measure (\<lambda>k::nat. N-k)"], blast)
txt{*
@{subgoals[display,indent=0,margin=65]}
@@ -91,7 +91,7 @@
\noindent
The inclusion remains to be proved. After unfolding some definitions,
we are left with simple arithmetic:
-*};
+*}
apply (clarify, simp add: measure_def inv_image_def)
@@ -100,9 +100,9 @@
\noindent
And that is dispatched automatically:
-*};
+*}
-by arith;
+by arith
text{*\noindent
@@ -114,7 +114,7 @@
recdef g "{(i,j). j<i \<and> i \<le> (#10::nat)}"
"g i = (if #10 \<le> i then 0 else i * g(Suc i))"
(*>*)
-(hints recdef_wf: wf_greater);
+(hints recdef_wf: wf_greater)
text{*\noindent
Alternatively, we could have given @{text "measure (\<lambda>k::nat. #10-k)"} for the
--- a/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 28 19:17:01 2001 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Nested1 = Nested0:;
+theory Nested1 = Nested0:
(*>*)
text{*\noindent
@@ -11,11 +11,11 @@
Defining @{term trev} by \isacommand{recdef} rather than \isacommand{primrec}
simplifies matters because we are now free to use the recursion equation
suggested at the end of \S\ref{sec:nested-datatype}:
-*};
+*}
-recdef trev "measure size"
+recdef (*<*)(permissive)(*<*)trev "measure size"
"trev (Var x) = Var x"
- "trev (App f ts) = App f (rev(map trev ts))";
+ "trev (App f ts) = App f (rev(map trev ts))"
text{*\noindent
Remember that function @{term size} is defined for each \isacommand{datatype}.
@@ -34,8 +34,8 @@
which equals @{term"Suc(term_list_size ts)"}. We will now prove the termination condition and
continue with our definition. Below we return to the question of how
\isacommand{recdef} knows about @{term map}.
-*};
+*}
(*<*)
-end;
+end
(*>*)
--- a/doc-src/TutorialI/Recdef/termination.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Fri Sep 28 19:17:01 2001 +0200
@@ -16,9 +16,9 @@
Isabelle may fail to prove the termination condition for some
recursive call. Let us try the following artificial function:*}
-consts f :: "nat\<times>nat \<Rightarrow> nat";
-recdef f "measure(\<lambda>(x,y). x-y)"
- "f(x,y) = (if x \<le> y then x else f(x,y+1))";
+consts f :: "nat\<times>nat \<Rightarrow> nat"
+recdef (*<*)(permissive)(*<*)f "measure(\<lambda>(x,y). x-y)"
+ "f(x,y) = (if x \<le> y then x else f(x,y+1))"
text{*\noindent
Isabelle prints a
@@ -28,14 +28,14 @@
of your function once more. In our case the required lemma is the obvious one:
*}
-lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
+lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y"
txt{*\noindent
It was not proved automatically because of the awkward behaviour of subtraction
on type @{typ"nat"}. This requires more arithmetic than is tried by default:
*}
-apply(arith);
+apply(arith)
done
text{*\noindent
@@ -45,7 +45,7 @@
a simplification rule.
*}
-consts g :: "nat\<times>nat \<Rightarrow> nat";
+consts g :: "nat\<times>nat \<Rightarrow> nat"
recdef g "measure(\<lambda>(x,y). x-y)"
"g(x,y) = (if x \<le> y then x else g(x,y+1))"
(hints recdef_simp: termi_lem)
@@ -56,8 +56,8 @@
simplification rule. Thus we can automatically prove results such as this one:
*}
-theorem "g(1,0) = g(1,1)";
-apply(simp);
+theorem "g(1,0) = g(1,1)"
+apply(simp)
done
text{*\noindent
--- a/src/HOL/Library/While_Combinator.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/src/HOL/Library/While_Combinator.thy Fri Sep 28 19:17:01 2001 +0200
@@ -19,7 +19,7 @@
*}
consts while_aux :: "('a => bool) \<times> ('a => 'a) \<times> 'a => 'a"
-recdef while_aux
+recdef (permissive) while_aux
"same_fst (\<lambda>b. True) (\<lambda>b. same_fst (\<lambda>c. True) (\<lambda>c.
{(t, s). b s \<and> c s = t \<and>
\<not> (\<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))}))"
--- a/src/HOL/NanoJava/TypeRel.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy Fri Sep 28 19:17:01 2001 +0200
@@ -105,7 +105,7 @@
consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<leadsto> 'b)"
-recdef class_rec "subcls1\<inverse>"
+recdef (permissive) class_rec "subcls1\<inverse>"
"class_rec C = (\<lambda>f. case class C of None \<Rightarrow> arbitrary
| Some m \<Rightarrow> if wf (subcls1\<inverse>)
then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m)
--- a/src/HOL/ex/Recdefs.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/src/HOL/ex/Recdefs.thy Fri Sep 28 19:17:01 2001 +0200
@@ -33,7 +33,7 @@
text {* Not handled automatically: too complicated. *}
consts variant :: "nat * nat list => nat"
-recdef variant "measure (\<lambda>(n::nat, ns). size (filter (\<lambda>y. n \<le> y) ns))"
+recdef (permissive) variant "measure (\<lambda>(n::nat, ns). size (filter (\<lambda>y. n \<le> y) ns))"
"variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
consts gcd :: "nat * nat => nat"
@@ -51,7 +51,7 @@
*}
consts g :: "nat => nat"
-recdef g less_than
+recdef (permissive) g less_than
"g 0 = 0"
"g (Suc x) = g (g x)"
@@ -80,7 +80,7 @@
*}
consts k :: "nat => nat"
-recdef k less_than
+recdef (permissive) k less_than
"k 0 = 0"
"k (Suc n) =
(let x = k 1
@@ -94,7 +94,7 @@
else part (P, rst, l1, h # l2))"
consts fqsort :: "('a => 'a => bool) * 'a list => 'a list"
-recdef fqsort "measure (size o snd)"
+recdef (permissive) fqsort "measure (size o snd)"
"fqsort (ord, []) = []"
"fqsort (ord, x # rst) =
(let (less, more) = part ((\<lambda>y. ord y x), rst, ([], []))
@@ -109,7 +109,7 @@
*}
consts mapf :: "nat => nat list"
-recdef mapf "measure (\<lambda>m. m)"
+recdef (permissive) mapf "measure (\<lambda>m. m)"
"mapf 0 = []"
"mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
(hints cong: map_cong)