# HG changeset patch
# User wenzelm
# Date 1001697421 -7200
# Node ID 0dbfb578bf7571dd9e6c4a7971496e246c33d7a7
# Parent  74cdf24724ea5a95264880d596661b58c619e8b5
recdef (permissive);

diff -r 74cdf24724ea -r 0dbfb578bf75 doc-src/TutorialI/Advanced/Partial.thy
--- 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
diff -r 74cdf24724ea -r 0dbfb578bf75 doc-src/TutorialI/Advanced/WFrec.thy
--- 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
diff -r 74cdf24724ea -r 0dbfb578bf75 doc-src/TutorialI/Recdef/Nested1.thy
--- 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
 (*>*)
diff -r 74cdf24724ea -r 0dbfb578bf75 doc-src/TutorialI/Recdef/termination.thy
--- 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
diff -r 74cdf24724ea -r 0dbfb578bf75 src/HOL/Library/While_Combinator.thy
--- 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)))}))"
diff -r 74cdf24724ea -r 0dbfb578bf75 src/HOL/NanoJava/TypeRel.thy
--- 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)
diff -r 74cdf24724ea -r 0dbfb578bf75 src/HOL/ex/Recdefs.thy
--- 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)