recdef (permissive);
authorwenzelm
Fri Sep 28 19:17:01 2001 +0200 (2001-09-28)
changeset 116260dbfb578bf75
parent 11625 74cdf24724ea
child 11627 abf9cda4a4d2
recdef (permissive);
doc-src/TutorialI/Advanced/Partial.thy
doc-src/TutorialI/Advanced/WFrec.thy
doc-src/TutorialI/Recdef/Nested1.thy
doc-src/TutorialI/Recdef/termination.thy
src/HOL/Library/While_Combinator.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/ex/Recdefs.thy
     1.1 --- a/doc-src/TutorialI/Advanced/Partial.thy	Fri Sep 28 18:55:37 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Advanced/Partial.thy	Fri Sep 28 19:17:01 2001 +0200
     1.3 @@ -62,9 +62,9 @@
     1.4  *}
     1.5  
     1.6  consts divi :: "nat \<times> nat \<Rightarrow> nat"
     1.7 -recdef divi "measure(\<lambda>(m,n). m)"
     1.8 +recdef (permissive) divi "measure(\<lambda>(m,n). m)"
     1.9    "divi(m,n) = (if n = 0 then arbitrary else
    1.10 -                if m < n then 0 else divi(m-n,n)+1)"
    1.11 +                if m < n then 0 else divi(m-n,n)+1)"  (* FIXME permissive!? *)
    1.12  
    1.13  text{*\noindent Of course we could also have defined
    1.14  @{term"divi(m,0)"} to be some specific number, for example 0. The
     2.1 --- a/doc-src/TutorialI/Advanced/WFrec.thy	Fri Sep 28 18:55:37 2001 +0200
     2.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy	Fri Sep 28 19:17:01 2001 +0200
     2.3 @@ -8,11 +8,11 @@
     2.4  can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:
     2.5  *}
     2.6  
     2.7 -consts ack :: "nat\<times>nat \<Rightarrow> nat";
     2.8 +consts ack :: "nat\<times>nat \<Rightarrow> nat"
     2.9  recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
    2.10    "ack(0,n)         = Suc n"
    2.11    "ack(Suc m,0)     = ack(m, 1)"
    2.12 -  "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
    2.13 +  "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"
    2.14  
    2.15  text{*\noindent
    2.16  The lexicographic product decreases if either its first component
    2.17 @@ -67,8 +67,8 @@
    2.18  *}
    2.19  
    2.20  consts f :: "nat \<Rightarrow> nat"
    2.21 -recdef f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
    2.22 -"f i = (if #10 \<le> i then 0 else i * f(Suc i))";
    2.23 +recdef (*<*)(permissive)(*<*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
    2.24 +"f i = (if #10 \<le> i then 0 else i * f(Suc i))"
    2.25  
    2.26  text{*\noindent
    2.27  Since \isacommand{recdef} is not prepared for the relation supplied above,
    2.28 @@ -81,9 +81,9 @@
    2.29  txt{*\noindent
    2.30  The proof is by showing that our relation is a subset of another well-founded
    2.31  relation: one given by a measure function.\index{*wf_subset (theorem)}
    2.32 -*};
    2.33 +*}
    2.34  
    2.35 -apply (rule wf_subset [of "measure (\<lambda>k::nat. N-k)"], blast);
    2.36 +apply (rule wf_subset [of "measure (\<lambda>k::nat. N-k)"], blast)
    2.37  
    2.38  txt{*
    2.39  @{subgoals[display,indent=0,margin=65]}
    2.40 @@ -91,7 +91,7 @@
    2.41  \noindent
    2.42  The inclusion remains to be proved. After unfolding some definitions, 
    2.43  we are left with simple arithmetic:
    2.44 -*};
    2.45 +*}
    2.46  
    2.47  apply (clarify, simp add: measure_def inv_image_def)
    2.48  
    2.49 @@ -100,9 +100,9 @@
    2.50  
    2.51  \noindent
    2.52  And that is dispatched automatically:
    2.53 -*};
    2.54 +*}
    2.55  
    2.56 -by arith;
    2.57 +by arith
    2.58  
    2.59  text{*\noindent
    2.60  
    2.61 @@ -114,7 +114,7 @@
    2.62  recdef g "{(i,j). j<i \<and> i \<le> (#10::nat)}"
    2.63  "g i = (if #10 \<le> i then 0 else i * g(Suc i))"
    2.64  (*>*)
    2.65 -(hints recdef_wf: wf_greater);
    2.66 +(hints recdef_wf: wf_greater)
    2.67  
    2.68  text{*\noindent
    2.69  Alternatively, we could have given @{text "measure (\<lambda>k::nat. #10-k)"} for the
     3.1 --- a/doc-src/TutorialI/Recdef/Nested1.thy	Fri Sep 28 18:55:37 2001 +0200
     3.2 +++ b/doc-src/TutorialI/Recdef/Nested1.thy	Fri Sep 28 19:17:01 2001 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  (*<*)
     3.5 -theory Nested1 = Nested0:;
     3.6 +theory Nested1 = Nested0:
     3.7  (*>*)
     3.8  
     3.9  text{*\noindent
    3.10 @@ -11,11 +11,11 @@
    3.11  Defining @{term trev} by \isacommand{recdef} rather than \isacommand{primrec}
    3.12  simplifies matters because we are now free to use the recursion equation
    3.13  suggested at the end of \S\ref{sec:nested-datatype}:
    3.14 -*};
    3.15 +*}
    3.16  
    3.17 -recdef trev "measure size"
    3.18 +recdef (*<*)(permissive)(*<*)trev "measure size"
    3.19   "trev (Var x)    = Var x"
    3.20 - "trev (App f ts) = App f (rev(map trev ts))";
    3.21 + "trev (App f ts) = App f (rev(map trev ts))"
    3.22  
    3.23  text{*\noindent
    3.24  Remember that function @{term size} is defined for each \isacommand{datatype}.
    3.25 @@ -34,8 +34,8 @@
    3.26  which equals @{term"Suc(term_list_size ts)"}.  We will now prove the termination condition and
    3.27  continue with our definition.  Below we return to the question of how
    3.28  \isacommand{recdef} knows about @{term map}.
    3.29 -*};
    3.30 +*}
    3.31  
    3.32  (*<*)
    3.33 -end;
    3.34 +end
    3.35  (*>*)
     4.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 28 18:55:37 2001 +0200
     4.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 28 19:17:01 2001 +0200
     4.3 @@ -16,9 +16,9 @@
     4.4  Isabelle may fail to prove the termination condition for some
     4.5  recursive call.  Let us try the following artificial function:*}
     4.6  
     4.7 -consts f :: "nat\<times>nat \<Rightarrow> nat";
     4.8 -recdef f "measure(\<lambda>(x,y). x-y)"
     4.9 -  "f(x,y) = (if x \<le> y then x else f(x,y+1))";
    4.10 +consts f :: "nat\<times>nat \<Rightarrow> nat"
    4.11 +recdef (*<*)(permissive)(*<*)f "measure(\<lambda>(x,y). x-y)"
    4.12 +  "f(x,y) = (if x \<le> y then x else f(x,y+1))"
    4.13  
    4.14  text{*\noindent
    4.15  Isabelle prints a
    4.16 @@ -28,14 +28,14 @@
    4.17  of your function once more. In our case the required lemma is the obvious one:
    4.18  *}
    4.19  
    4.20 -lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
    4.21 +lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y"
    4.22  
    4.23  txt{*\noindent
    4.24  It was not proved automatically because of the awkward behaviour of subtraction
    4.25  on type @{typ"nat"}. This requires more arithmetic than is tried by default:
    4.26  *}
    4.27  
    4.28 -apply(arith);
    4.29 +apply(arith)
    4.30  done
    4.31  
    4.32  text{*\noindent
    4.33 @@ -45,7 +45,7 @@
    4.34  a simplification rule.  
    4.35  *}
    4.36  
    4.37 -consts g :: "nat\<times>nat \<Rightarrow> nat";
    4.38 +consts g :: "nat\<times>nat \<Rightarrow> nat"
    4.39  recdef g "measure(\<lambda>(x,y). x-y)"
    4.40    "g(x,y) = (if x \<le> y then x else g(x,y+1))"
    4.41  (hints recdef_simp: termi_lem)
    4.42 @@ -56,8 +56,8 @@
    4.43  simplification rule.  Thus we can automatically prove results such as this one:
    4.44  *}
    4.45  
    4.46 -theorem "g(1,0) = g(1,1)";
    4.47 -apply(simp);
    4.48 +theorem "g(1,0) = g(1,1)"
    4.49 +apply(simp)
    4.50  done
    4.51  
    4.52  text{*\noindent
     5.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Sep 28 18:55:37 2001 +0200
     5.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Sep 28 19:17:01 2001 +0200
     5.3 @@ -19,7 +19,7 @@
     5.4  *}
     5.5  
     5.6  consts while_aux :: "('a => bool) \<times> ('a => 'a) \<times> 'a => 'a"
     5.7 -recdef while_aux
     5.8 +recdef (permissive) while_aux
     5.9    "same_fst (\<lambda>b. True) (\<lambda>b. same_fst (\<lambda>c. True) (\<lambda>c.
    5.10        {(t, s).  b s \<and> c s = t \<and>
    5.11          \<not> (\<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))}))"
     6.1 --- a/src/HOL/NanoJava/TypeRel.thy	Fri Sep 28 18:55:37 2001 +0200
     6.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Fri Sep 28 19:17:01 2001 +0200
     6.3 @@ -105,7 +105,7 @@
     6.4  
     6.5  consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<leadsto> 'b)"
     6.6  
     6.7 -recdef class_rec "subcls1\<inverse>"
     6.8 +recdef (permissive) class_rec "subcls1\<inverse>"
     6.9        "class_rec C = (\<lambda>f. case class C of None   \<Rightarrow> arbitrary 
    6.10                                          | Some m \<Rightarrow> if wf (subcls1\<inverse>) 
    6.11         then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m)
     7.1 --- a/src/HOL/ex/Recdefs.thy	Fri Sep 28 18:55:37 2001 +0200
     7.2 +++ b/src/HOL/ex/Recdefs.thy	Fri Sep 28 19:17:01 2001 +0200
     7.3 @@ -33,7 +33,7 @@
     7.4  
     7.5  text {* Not handled automatically: too complicated. *}
     7.6  consts variant :: "nat * nat list => nat"
     7.7 -recdef variant  "measure (\<lambda>(n::nat, ns). size (filter (\<lambda>y. n \<le> y) ns))"
     7.8 +recdef (permissive) variant  "measure (\<lambda>(n::nat, ns). size (filter (\<lambda>y. n \<le> y) ns))"
     7.9    "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
    7.10  
    7.11  consts gcd :: "nat * nat => nat"
    7.12 @@ -51,7 +51,7 @@
    7.13   *}
    7.14  
    7.15  consts g :: "nat => nat"
    7.16 -recdef g  less_than
    7.17 +recdef (permissive) g  less_than
    7.18    "g 0 = 0"
    7.19    "g (Suc x) = g (g x)"
    7.20  
    7.21 @@ -80,7 +80,7 @@
    7.22  *}
    7.23  
    7.24  consts k :: "nat => nat"
    7.25 -recdef k  less_than
    7.26 +recdef (permissive) k  less_than
    7.27    "k 0 = 0"
    7.28    "k (Suc n) =
    7.29     (let x = k 1
    7.30 @@ -94,7 +94,7 @@
    7.31      else part (P, rst, l1, h # l2))"
    7.32  
    7.33  consts fqsort :: "('a => 'a => bool) * 'a list => 'a list"
    7.34 -recdef fqsort  "measure (size o snd)"
    7.35 +recdef (permissive) fqsort  "measure (size o snd)"
    7.36    "fqsort (ord, []) = []"
    7.37    "fqsort (ord, x # rst) =
    7.38    (let (less, more) = part ((\<lambda>y. ord y x), rst, ([], []))
    7.39 @@ -109,7 +109,7 @@
    7.40  *}
    7.41  
    7.42  consts mapf :: "nat => nat list"
    7.43 -recdef mapf  "measure (\<lambda>m. m)"
    7.44 +recdef (permissive) mapf  "measure (\<lambda>m. m)"
    7.45    "mapf 0 = []"
    7.46    "mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
    7.47    (hints cong: map_cong)