Unified function syntax
authorkrauss
Wed Mar 21 16:06:15 2007 +0100 (2007-03-21)
changeset 2249243545e640877
parent 22491 535fbed859da
child 22493 db930e490fe5
Unified function syntax
src/HOL/Library/ExecutableRat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/SCT_Examples.thy
src/HOL/Library/SCT_Interpretation.thy
src/HOL/Library/State_Monad.thy
src/HOL/Nominal/Examples/Crary.thy
src/HOL/Nominal/Examples/Lam_Funs.thy
src/HOL/ex/CodeCollections.thy
src/HOL/ex/Fundefs.thy
     1.1 --- a/src/HOL/Library/ExecutableRat.thy	Wed Mar 21 13:58:36 2007 +0100
     1.2 +++ b/src/HOL/Library/ExecutableRat.thy	Wed Mar 21 16:06:15 2007 +0100
     1.3 @@ -34,9 +34,9 @@
     1.4  fun
     1.5    add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> bool * nat" where
     1.6    "add_sign (True, n) (True, m) = (True, n + m)"
     1.7 -  "add_sign (False, n) (False, m) = (False, n + m)"
     1.8 -  "add_sign (True, n) (False, m) = minus_sign n m"
     1.9 -  "add_sign (False, n) (True, m) = minus_sign m n"
    1.10 +| "add_sign (False, n) (False, m) = (False, n + m)"
    1.11 +| "add_sign (True, n) (False, m) = minus_sign n m"
    1.12 +| "add_sign (False, n) (True, m) = minus_sign m n"
    1.13  
    1.14  definition
    1.15    erat_of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where
     2.1 --- a/src/HOL/Library/ExecutableSet.thy	Wed Mar 21 13:58:36 2007 +0100
     2.2 +++ b/src/HOL/Library/ExecutableSet.thy	Wed Mar 21 16:06:15 2007 +0100
     2.3 @@ -64,7 +64,7 @@
     2.4  fun
     2.5    drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     2.6    "drop_first f [] = []"
     2.7 -  "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
     2.8 +| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
     2.9  declare drop_first.simps [code del]
    2.10  declare drop_first.simps [code target: List]
    2.11  
    2.12 @@ -150,7 +150,7 @@
    2.13  function unions :: "'a list list \<Rightarrow> 'a list"
    2.14  where
    2.15    "unions [] = []"
    2.16 -  "unions xs = foldr unionl xs []"
    2.17 +| "unions xs = foldr unionl xs []"
    2.18  by pat_completeness auto
    2.19  termination by lexicographic_order
    2.20  
     3.1 --- a/src/HOL/Library/SCT_Examples.thy	Wed Mar 21 13:58:36 2007 +0100
     3.2 +++ b/src/HOL/Library/SCT_Examples.thy	Wed Mar 21 16:06:15 2007 +0100
     3.3 @@ -47,9 +47,9 @@
     3.4  function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
     3.5  where
     3.6    "foo True (Suc n) m = foo True n (Suc m)"
     3.7 -  "foo True 0 m = foo False 0 m"
     3.8 -  "foo False n (Suc m) = foo False (Suc n) m"
     3.9 -  "foo False n 0 = n"
    3.10 +| "foo True 0 m = foo False 0 m"
    3.11 +| "foo False n (Suc m) = foo False (Suc n) m"
    3.12 +| "foo False n 0 = n"
    3.13  by pat_completeness auto
    3.14  
    3.15  termination
     4.1 --- a/src/HOL/Library/SCT_Interpretation.thy	Wed Mar 21 13:58:36 2007 +0100
     4.2 +++ b/src/HOL/Library/SCT_Interpretation.thy	Wed Mar 21 16:06:15 2007 +0100
     4.3 @@ -65,7 +65,7 @@
     4.4  fun mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
     4.5  where
     4.6    "mk_rel [] x y = False"
     4.7 -  "mk_rel (c#cs) x y =
     4.8 +| "mk_rel (c#cs) x y =
     4.9    (in_cdesc c x y \<or> mk_rel cs x y)"
    4.10  
    4.11  
     5.1 --- a/src/HOL/Library/State_Monad.thy	Wed Mar 21 13:58:36 2007 +0100
     5.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Mar 21 16:06:15 2007 +0100
     5.3 @@ -257,12 +257,12 @@
     5.4  fun
     5.5    list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
     5.6    "list f [] = id"
     5.7 -  "list f (x#xs) = (do f x; list f xs done)"
     5.8 +| "list f (x#xs) = (do f x; list f xs done)"
     5.9  lemmas [code] = list.simps
    5.10  
    5.11  fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
    5.12    "list_yield f [] = return []"
    5.13 -  "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
    5.14 +| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
    5.15  lemmas [code] = list_yield.simps
    5.16    
    5.17  text {* combinator properties *}
     6.1 --- a/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 21 13:58:36 2007 +0100
     6.2 +++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 21 16:06:15 2007 +0100
     6.3 @@ -340,7 +340,7 @@
     6.4    lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm"   
     6.5  where
     6.6    "lookup [] X        = Var X"
     6.7 -  "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"
     6.8 +| "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"
     6.9  
    6.10  lemma lookup_eqvt[eqvt]:
    6.11    fixes pi::"name prm"
     7.1 --- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Wed Mar 21 13:58:36 2007 +0100
     7.2 +++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Wed Mar 21 16:06:15 2007 +0100
     7.3 @@ -90,7 +90,7 @@
     7.4    lookup :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam"   
     7.5  where
     7.6    "lookup [] x        = Var x"
     7.7 -  "lookup ((y,T)#\<theta>) x = (if x=y then T else lookup \<theta> x)"
     7.8 +| "lookup ((y,T)#\<theta>) x = (if x=y then T else lookup \<theta> x)"
     7.9  
    7.10  lemma lookup_eqvt[eqvt]:
    7.11    fixes pi::"name prm"
     8.1 --- a/src/HOL/ex/CodeCollections.thy	Wed Mar 21 13:58:36 2007 +0100
     8.2 +++ b/src/HOL/ex/CodeCollections.thy	Wed Mar 21 16:06:15 2007 +0100
     8.3 @@ -11,8 +11,8 @@
     8.4  fun
     8.5    abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
     8.6    "abs_sorted cmp [] \<longleftrightarrow> True"
     8.7 -  "abs_sorted cmp [x] \<longleftrightarrow> True"
     8.8 -  "abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)"
     8.9 +| "abs_sorted cmp [x] \<longleftrightarrow> True"
    8.10 +| "abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)"
    8.11  
    8.12  abbreviation (in ord)
    8.13    "sorted \<equiv> abs_sorted less_eq"
    8.14 @@ -105,7 +105,7 @@
    8.15    product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
    8.16    where
    8.17    "product [] ys = []"
    8.18 -  "product (x#xs) ys = map (Pair x) ys @ product xs ys"
    8.19 +| "product (x#xs) ys = map (Pair x) ys @ product xs ys"
    8.20  
    8.21  lemma product_all:
    8.22    assumes "x \<in> set xs" "y \<in> set ys"
     9.1 --- a/src/HOL/ex/Fundefs.thy	Wed Mar 21 13:58:36 2007 +0100
     9.2 +++ b/src/HOL/ex/Fundefs.thy	Wed Mar 21 16:06:15 2007 +0100
     9.3 @@ -114,9 +114,9 @@
     9.4  function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
     9.5  where
     9.6    "gcd3 x 0 = x"
     9.7 -  "gcd3 0 y = y"
     9.8 -  "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
     9.9 -  "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
    9.10 +| "gcd3 0 y = y"
    9.11 +| "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
    9.12 +| "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
    9.13    apply (case_tac x, case_tac a, auto)
    9.14    apply (case_tac ba, auto)
    9.15    done
    9.16 @@ -131,7 +131,7 @@
    9.17  function ev :: "nat \<Rightarrow> bool"
    9.18  where
    9.19    "ev (2 * n) = True"
    9.20 -  "ev (2 * n + 1) = False"
    9.21 +| "ev (2 * n + 1) = False"
    9.22  proof -  -- {* completeness is more difficult here \dots *}
    9.23    fix P :: bool
    9.24      and x :: nat