modernized primrec
authorhaftmann
Wed Sep 08 19:21:46 2010 +0200 (2010-09-08)
changeset 392469e58f0499f57
parent 39215 7b2631c91a95
child 39247 3a15ee47c610
modernized primrec
src/HOL/Auth/Guard/Extensions.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Smartcard/EventSC.thy
src/HOL/Auth/Smartcard/Smartcard.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Hoare_Parallel/OG_Com.thy
src/HOL/Hoare_Parallel/OG_Hoare.thy
src/HOL/IMP/Compiler0.thy
src/HOL/Import/HOL4Compat.thy
src/HOL/Induct/ABexp.thy
src/HOL/Induct/Ordinals.thy
src/HOL/Induct/PropLog.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Induct/SList.thy
src/HOL/Induct/Tree.thy
src/HOL/Lattice/Orders.thy
src/HOL/Metis_Examples/BT.thy
src/HOL/Nominal/Examples/Class3.thy
src/HOL/Nominal/Examples/Fsub.thy
src/HOL/Nominal/Examples/W.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/ZF/HOLZF.thy
src/HOL/ex/BT.thy
src/HOL/ex/Chinese.thy
src/HOL/ex/Hebrew.thy
src/HOL/ex/ReflectionEx.thy
     1.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Wed Sep 08 13:25:22 2010 +0200
     1.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Wed Sep 08 19:21:46 2010 +0200
     1.3 @@ -31,10 +31,8 @@
     1.4  
     1.5  subsubsection{*"remove l x" erase the first element of "l" equal to "x"*}
     1.6  
     1.7 -consts remove :: "'a list => 'a => 'a list"
     1.8 -
     1.9 -primrec
    1.10 -"remove [] y = []"
    1.11 +primrec remove :: "'a list => 'a => 'a list" where
    1.12 +"remove [] y = []" |
    1.13  "remove (x#xs) y = (if x=y then xs else x # remove xs y)"
    1.14  
    1.15  lemma set_remove: "set (remove l x) <= set l"
    1.16 @@ -348,13 +346,9 @@
    1.17  
    1.18  subsubsection{*knows without initState*}
    1.19  
    1.20 -consts knows' :: "agent => event list => msg set"
    1.21 -
    1.22 -primrec
    1.23 -knows'_Nil:
    1.24 - "knows' A [] = {}"
    1.25 -
    1.26 -knows'_Cons0:
    1.27 +primrec knows' :: "agent => event list => msg set" where
    1.28 +  knows'_Nil: "knows' A [] = {}" |
    1.29 +  knows'_Cons0:
    1.30   "knows' A (ev # evs) = (
    1.31     if A = Spy then (
    1.32       case ev of
    1.33 @@ -426,10 +420,8 @@
    1.34  subsubsection{*maximum knowledge an agent can have
    1.35  includes messages sent to the agent*}
    1.36  
    1.37 -consts knows_max' :: "agent => event list => msg set"
    1.38 -
    1.39 -primrec
    1.40 -knows_max'_def_Nil: "knows_max' A [] = {}"
    1.41 +primrec knows_max' :: "agent => event list => msg set" where
    1.42 +knows_max'_def_Nil: "knows_max' A [] = {}" |
    1.43  knows_max'_def_Cons: "knows_max' A (ev # evs) = (
    1.44    if A=Spy then (
    1.45      case ev of
    1.46 @@ -498,10 +490,8 @@
    1.47  
    1.48  subsubsection{*used without initState*}
    1.49  
    1.50 -consts used' :: "event list => msg set"
    1.51 -
    1.52 -primrec
    1.53 -"used' [] = {}"
    1.54 +primrec used' :: "event list => msg set" where
    1.55 +"used' [] = {}" |
    1.56  "used' (ev # evs) = (
    1.57    case ev of
    1.58      Says A B X => parts {X} Un used' evs
     2.1 --- a/src/HOL/Auth/Public.thy	Wed Sep 08 13:25:22 2010 +0200
     2.2 +++ b/src/HOL/Auth/Public.thy	Wed Sep 08 19:21:46 2010 +0200
     2.3 @@ -199,24 +199,32 @@
     2.4  knowledge of the Spy.  All other agents are automata, merely following the
     2.5  protocol.*}
     2.6  
     2.7 -primrec
     2.8 +term initState_Server
     2.9 +
    2.10 +overloading
    2.11 +  initState \<equiv> initState
    2.12 +begin
    2.13 +
    2.14 +primrec initState where
    2.15          (*Agents know their private key and all public keys*)
    2.16    initState_Server:
    2.17      "initState Server     =    
    2.18         {Key (priEK Server), Key (priSK Server)} \<union> 
    2.19         (Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)"
    2.20  
    2.21 -  initState_Friend:
    2.22 +| initState_Friend:
    2.23      "initState (Friend i) =    
    2.24         {Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union> 
    2.25         (Key ` range pubEK) \<union> (Key ` range pubSK)"
    2.26  
    2.27 -  initState_Spy:
    2.28 +| initState_Spy:
    2.29      "initState Spy        =    
    2.30         (Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union> 
    2.31         (Key ` shrK ` bad) \<union> 
    2.32         (Key ` range pubEK) \<union> (Key ` range pubSK)"
    2.33  
    2.34 +end
    2.35 +
    2.36  
    2.37  text{*These lemmas allow reasoning about @{term "used evs"} rather than
    2.38     @{term "knows Spy evs"}, which is useful when there are private Notes. 
     3.1 --- a/src/HOL/Auth/Shared.thy	Wed Sep 08 13:25:22 2010 +0200
     3.2 +++ b/src/HOL/Auth/Shared.thy	Wed Sep 08 19:21:46 2010 +0200
     3.3 @@ -22,10 +22,17 @@
     3.4     done
     3.5  
     3.6  text{*Server knows all long-term keys; other agents know only their own*}
     3.7 -primrec
     3.8 +
     3.9 +overloading
    3.10 +  initState \<equiv> initState
    3.11 +begin
    3.12 +
    3.13 +primrec initState where
    3.14    initState_Server:  "initState Server     = Key ` range shrK"
    3.15 -  initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
    3.16 -  initState_Spy:     "initState Spy        = Key`shrK`bad"
    3.17 +| initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
    3.18 +| initState_Spy:     "initState Spy        = Key`shrK`bad"
    3.19 +
    3.20 +end
    3.21  
    3.22  
    3.23  subsection{*Basic properties of shrK*}
     4.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy	Wed Sep 08 13:25:22 2010 +0200
     4.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy	Wed Sep 08 19:21:46 2010 +0200
     4.3 @@ -19,7 +19,6 @@
     4.4      
     4.5  consts 
     4.6   bad     :: "agent set"  (*compromised agents*)
     4.7 - knows   :: "agent => event list => msg set" (*agents' knowledge*)
     4.8   stolen    :: "card set" (* stolen smart cards *)
     4.9   cloned  :: "card set"   (* cloned smart cards*)
    4.10   secureM :: "bool"(*assumption of secure means between agents and their cards*)
    4.11 @@ -50,7 +49,8 @@
    4.12  
    4.13  primrec (*This definition is extended over the new events, subject to the 
    4.14            assumption of secure means*)
    4.15 -  knows_Nil:   "knows A [] = initState A"
    4.16 +  knows   :: "agent => event list => msg set" (*agents' knowledge*) where
    4.17 +  knows_Nil:   "knows A [] = initState A" |
    4.18    knows_Cons:  "knows A (ev # evs) =
    4.19           (case ev of
    4.20              Says A' B X => 
    4.21 @@ -78,13 +78,11 @@
    4.22  
    4.23  
    4.24  
    4.25 -consts
    4.26 +primrec
    4.27    (*The set of items that might be visible to someone is easily extended 
    4.28      over the new events*)
    4.29 -  used :: "event list => msg set"
    4.30 -
    4.31 -primrec
    4.32 -  used_Nil:   "used []         = (UN B. parts (initState B))"
    4.33 +  used :: "event list => msg set" where
    4.34 +  used_Nil:   "used []         = (UN B. parts (initState B))" |
    4.35    used_Cons:  "used (ev # evs) =
    4.36                   (case ev of
    4.37                      Says A B X => parts {X} \<union> (used evs)
    4.38 @@ -98,7 +96,6 @@
    4.39         Likewise, @{term C_Gets} will always have to follow @{term Inputs}
    4.40         and @{term A_Gets} will always have to follow @{term Outpts}*}
    4.41  
    4.42 -
    4.43  lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> used evs"
    4.44  apply (induct_tac evs)
    4.45  apply (auto split: event.split) 
     5.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Sep 08 13:25:22 2010 +0200
     5.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Sep 08 19:21:46 2010 +0200
     5.3 @@ -51,16 +51,21 @@
     5.4  
     5.5  
     5.6  text{*initState must be defined with care*}
     5.7 -primrec
     5.8 +
     5.9 +overloading
    5.10 +  initState \<equiv> initState
    5.11 +begin
    5.12 +
    5.13 +primrec initState where
    5.14  (*Server knows all long-term keys; adding cards' keys may be redundant but
    5.15    helps prove crdK_in_initState and crdK_in_used to distinguish cards' keys
    5.16    from fresh (session) keys*)
    5.17    initState_Server:  "initState Server = 
    5.18          (Key`(range shrK \<union> range crdK \<union> range pin \<union> range pairK)) \<union> 
    5.19 -        (Nonce`(range Pairkey))"
    5.20 +        (Nonce`(range Pairkey))" |
    5.21  
    5.22  (*Other agents know only their own*)
    5.23 -  initState_Friend:  "initState (Friend i) = {Key (pin (Friend i))}"
    5.24 +  initState_Friend:  "initState (Friend i) = {Key (pin (Friend i))}" |
    5.25  
    5.26  (*Spy knows bad agents' pins, cloned cards' keys, pairKs, and Pairkeys *)
    5.27    initState_Spy: "initState Spy  = 
    5.28 @@ -70,6 +75,7 @@
    5.29                          (pairK`{(X,A). Card A \<in> cloned})))
    5.30             \<union> (Nonce`(Pairkey`{(A,B). Card A \<in> cloned & Card B \<in> cloned}))"
    5.31  
    5.32 +end
    5.33  
    5.34  text{*Still relying on axioms*}
    5.35  axioms
     6.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 08 13:25:22 2010 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 08 19:21:46 2010 +0200
     6.3 @@ -67,27 +67,26 @@
     6.4    by (induct p rule: fmsize.induct) simp_all
     6.5  
     6.6    (* Semantics of formulae (fm) *)
     6.7 -consts Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"
     6.8 -primrec
     6.9 +primrec Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool" where
    6.10    "Ifm bbs bs T = True"
    6.11 -  "Ifm bbs bs F = False"
    6.12 -  "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
    6.13 -  "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
    6.14 -  "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
    6.15 -  "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
    6.16 -  "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
    6.17 -  "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
    6.18 -  "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
    6.19 -  "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
    6.20 -  "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
    6.21 -  "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
    6.22 -  "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
    6.23 -  "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
    6.24 -  "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
    6.25 -  "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
    6.26 -  "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
    6.27 -  "Ifm bbs bs (Closed n) = bbs!n"
    6.28 -  "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
    6.29 +| "Ifm bbs bs F = False"
    6.30 +| "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
    6.31 +| "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
    6.32 +| "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
    6.33 +| "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
    6.34 +| "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
    6.35 +| "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
    6.36 +| "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
    6.37 +| "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
    6.38 +| "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
    6.39 +| "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
    6.40 +| "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
    6.41 +| "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
    6.42 +| "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
    6.43 +| "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
    6.44 +| "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
    6.45 +| "Ifm bbs bs (Closed n) = bbs!n"
    6.46 +| "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
    6.47  
    6.48  consts prep :: "fm \<Rightarrow> fm"
    6.49  recdef prep "measure fmsize"
    6.50 @@ -132,50 +131,47 @@
    6.51    "qfree p = True"
    6.52  
    6.53    (* Boundedness and substitution *)
    6.54 -consts 
    6.55 -  numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
    6.56 -  bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
    6.57 -  subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *)
    6.58 -primrec
    6.59 +    
    6.60 +primrec numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where
    6.61    "numbound0 (C c) = True"
    6.62 -  "numbound0 (Bound n) = (n>0)"
    6.63 -  "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
    6.64 -  "numbound0 (Neg a) = numbound0 a"
    6.65 -  "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
    6.66 -  "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
    6.67 -  "numbound0 (Mul i a) = numbound0 a"
    6.68 +| "numbound0 (Bound n) = (n>0)"
    6.69 +| "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
    6.70 +| "numbound0 (Neg a) = numbound0 a"
    6.71 +| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
    6.72 +| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
    6.73 +| "numbound0 (Mul i a) = numbound0 a"
    6.74  
    6.75  lemma numbound0_I:
    6.76    assumes nb: "numbound0 a"
    6.77    shows "Inum (b#bs) a = Inum (b'#bs) a"
    6.78  using nb
    6.79 -by (induct a rule: numbound0.induct) (auto simp add: gr0_conv_Suc)
    6.80 +by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
    6.81  
    6.82 -primrec
    6.83 +primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
    6.84    "bound0 T = True"
    6.85 -  "bound0 F = True"
    6.86 -  "bound0 (Lt a) = numbound0 a"
    6.87 -  "bound0 (Le a) = numbound0 a"
    6.88 -  "bound0 (Gt a) = numbound0 a"
    6.89 -  "bound0 (Ge a) = numbound0 a"
    6.90 -  "bound0 (Eq a) = numbound0 a"
    6.91 -  "bound0 (NEq a) = numbound0 a"
    6.92 -  "bound0 (Dvd i a) = numbound0 a"
    6.93 -  "bound0 (NDvd i a) = numbound0 a"
    6.94 -  "bound0 (NOT p) = bound0 p"
    6.95 -  "bound0 (And p q) = (bound0 p \<and> bound0 q)"
    6.96 -  "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
    6.97 -  "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
    6.98 -  "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
    6.99 -  "bound0 (E p) = False"
   6.100 -  "bound0 (A p) = False"
   6.101 -  "bound0 (Closed P) = True"
   6.102 -  "bound0 (NClosed P) = True"
   6.103 +| "bound0 F = True"
   6.104 +| "bound0 (Lt a) = numbound0 a"
   6.105 +| "bound0 (Le a) = numbound0 a"
   6.106 +| "bound0 (Gt a) = numbound0 a"
   6.107 +| "bound0 (Ge a) = numbound0 a"
   6.108 +| "bound0 (Eq a) = numbound0 a"
   6.109 +| "bound0 (NEq a) = numbound0 a"
   6.110 +| "bound0 (Dvd i a) = numbound0 a"
   6.111 +| "bound0 (NDvd i a) = numbound0 a"
   6.112 +| "bound0 (NOT p) = bound0 p"
   6.113 +| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
   6.114 +| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
   6.115 +| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
   6.116 +| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
   6.117 +| "bound0 (E p) = False"
   6.118 +| "bound0 (A p) = False"
   6.119 +| "bound0 (Closed P) = True"
   6.120 +| "bound0 (NClosed P) = True"
   6.121  lemma bound0_I:
   6.122    assumes bp: "bound0 p"
   6.123    shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
   6.124  using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
   6.125 -by (induct p rule: bound0.induct) (auto simp add: gr0_conv_Suc)
   6.126 +by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
   6.127  
   6.128  fun numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
   6.129    "numsubst0 t (C c) = (C c)"
   6.130 @@ -195,24 +191,24 @@
   6.131    "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
   6.132  by (induct t rule: numsubst0.induct, auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
   6.133  
   6.134 -primrec
   6.135 +primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
   6.136    "subst0 t T = T"
   6.137 -  "subst0 t F = F"
   6.138 -  "subst0 t (Lt a) = Lt (numsubst0 t a)"
   6.139 -  "subst0 t (Le a) = Le (numsubst0 t a)"
   6.140 -  "subst0 t (Gt a) = Gt (numsubst0 t a)"
   6.141 -  "subst0 t (Ge a) = Ge (numsubst0 t a)"
   6.142 -  "subst0 t (Eq a) = Eq (numsubst0 t a)"
   6.143 -  "subst0 t (NEq a) = NEq (numsubst0 t a)"
   6.144 -  "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
   6.145 -  "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
   6.146 -  "subst0 t (NOT p) = NOT (subst0 t p)"
   6.147 -  "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   6.148 -  "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   6.149 -  "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
   6.150 -  "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   6.151 -  "subst0 t (Closed P) = (Closed P)"
   6.152 -  "subst0 t (NClosed P) = (NClosed P)"
   6.153 +| "subst0 t F = F"
   6.154 +| "subst0 t (Lt a) = Lt (numsubst0 t a)"
   6.155 +| "subst0 t (Le a) = Le (numsubst0 t a)"
   6.156 +| "subst0 t (Gt a) = Gt (numsubst0 t a)"
   6.157 +| "subst0 t (Ge a) = Ge (numsubst0 t a)"
   6.158 +| "subst0 t (Eq a) = Eq (numsubst0 t a)"
   6.159 +| "subst0 t (NEq a) = NEq (numsubst0 t a)"
   6.160 +| "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
   6.161 +| "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
   6.162 +| "subst0 t (NOT p) = NOT (subst0 t p)"
   6.163 +| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   6.164 +| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   6.165 +| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
   6.166 +| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   6.167 +| "subst0 t (Closed P) = (Closed P)"
   6.168 +| "subst0 t (NClosed P) = (NClosed P)"
   6.169  
   6.170  lemma subst0_I: assumes qfp: "qfree p"
   6.171    shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p"
   6.172 @@ -280,14 +276,14 @@
   6.173  
   6.174  lemma numsubst0_numbound0: assumes nb: "numbound0 t"
   6.175    shows "numbound0 (numsubst0 t a)"
   6.176 -using nb apply (induct a rule: numbound0.induct)
   6.177 +using nb apply (induct a)
   6.178  apply simp_all
   6.179 -apply (case_tac n, simp_all)
   6.180 +apply (case_tac nat, simp_all)
   6.181  done
   6.182  
   6.183  lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"
   6.184    shows "bound0 (subst0 t p)"
   6.185 -using qf numsubst0_numbound0[OF nb] by (induct p  rule: subst0.induct, auto)
   6.186 +using qf numsubst0_numbound0[OF nb] by (induct p) auto
   6.187  
   6.188  lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
   6.189  by (induct p, simp_all)
     7.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Sep 08 13:25:22 2010 +0200
     7.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Sep 08 19:21:46 2010 +0200
     7.3 @@ -16,26 +16,24 @@
     7.4    | Neg tm | Sub tm tm | CNP nat poly tm
     7.5    (* A size for poly to make inductive proofs simpler*)
     7.6  
     7.7 -consts tmsize :: "tm \<Rightarrow> nat"
     7.8 -primrec 
     7.9 +primrec tmsize :: "tm \<Rightarrow> nat" where
    7.10    "tmsize (CP c) = polysize c"
    7.11 -  "tmsize (Bound n) = 1"
    7.12 -  "tmsize (Neg a) = 1 + tmsize a"
    7.13 -  "tmsize (Add a b) = 1 + tmsize a + tmsize b"
    7.14 -  "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
    7.15 -  "tmsize (Mul c a) = 1 + polysize c + tmsize a"
    7.16 -  "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
    7.17 +| "tmsize (Bound n) = 1"
    7.18 +| "tmsize (Neg a) = 1 + tmsize a"
    7.19 +| "tmsize (Add a b) = 1 + tmsize a + tmsize b"
    7.20 +| "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
    7.21 +| "tmsize (Mul c a) = 1 + polysize c + tmsize a"
    7.22 +| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
    7.23  
    7.24    (* Semantics of terms tm *)
    7.25 -consts Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
    7.26 -primrec
    7.27 +primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" where
    7.28    "Itm vs bs (CP c) = (Ipoly vs c)"
    7.29 -  "Itm vs bs (Bound n) = bs!n"
    7.30 -  "Itm vs bs (Neg a) = -(Itm vs bs a)"
    7.31 -  "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
    7.32 -  "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
    7.33 -  "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
    7.34 -  "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"   
    7.35 +| "Itm vs bs (Bound n) = bs!n"
    7.36 +| "Itm vs bs (Neg a) = -(Itm vs bs a)"
    7.37 +| "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
    7.38 +| "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
    7.39 +| "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
    7.40 +| "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"   
    7.41  
    7.42  
    7.43  fun allpolys:: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool"  where
    7.44 @@ -47,51 +45,48 @@
    7.45  | "allpolys P (Sub p q) = (allpolys P p \<and> allpolys P q)"
    7.46  | "allpolys P p = True"
    7.47  
    7.48 -consts 
    7.49 -  tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool"
    7.50 -  tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *)
    7.51 -  tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *)
    7.52 -  incrtm0:: "tm \<Rightarrow> tm"
    7.53 -  incrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm"
    7.54 -  decrtm0:: "tm \<Rightarrow> tm" 
    7.55 -  decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" 
    7.56 -primrec
    7.57 +primrec tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool" where
    7.58    "tmboundslt n (CP c) = True"
    7.59 -  "tmboundslt n (Bound m) = (m < n)"
    7.60 -  "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
    7.61 -  "tmboundslt n (Neg a) = tmboundslt n a"
    7.62 -  "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
    7.63 -  "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 
    7.64 -  "tmboundslt n (Mul i a) = tmboundslt n a"
    7.65 -primrec
    7.66 +| "tmboundslt n (Bound m) = (m < n)"
    7.67 +| "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
    7.68 +| "tmboundslt n (Neg a) = tmboundslt n a"
    7.69 +| "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
    7.70 +| "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 
    7.71 +| "tmboundslt n (Mul i a) = tmboundslt n a"
    7.72 +
    7.73 +primrec tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *) where
    7.74    "tmbound0 (CP c) = True"
    7.75 -  "tmbound0 (Bound n) = (n>0)"
    7.76 -  "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
    7.77 -  "tmbound0 (Neg a) = tmbound0 a"
    7.78 -  "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
    7.79 -  "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 
    7.80 -  "tmbound0 (Mul i a) = tmbound0 a"
    7.81 +| "tmbound0 (Bound n) = (n>0)"
    7.82 +| "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
    7.83 +| "tmbound0 (Neg a) = tmbound0 a"
    7.84 +| "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
    7.85 +| "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 
    7.86 +| "tmbound0 (Mul i a) = tmbound0 a"
    7.87  lemma tmbound0_I:
    7.88    assumes nb: "tmbound0 a"
    7.89    shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
    7.90  using nb
    7.91 -by (induct a rule: tmbound0.induct,auto simp add: nth_pos2)
    7.92 +by (induct a rule: tm.induct,auto simp add: nth_pos2)
    7.93  
    7.94 -primrec
    7.95 +primrec tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) where
    7.96    "tmbound n (CP c) = True"
    7.97 -  "tmbound n (Bound m) = (n \<noteq> m)"
    7.98 -  "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
    7.99 -  "tmbound n (Neg a) = tmbound n a"
   7.100 -  "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
   7.101 -  "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)" 
   7.102 -  "tmbound n (Mul i a) = tmbound n a"
   7.103 +| "tmbound n (Bound m) = (n \<noteq> m)"
   7.104 +| "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
   7.105 +| "tmbound n (Neg a) = tmbound n a"
   7.106 +| "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
   7.107 +| "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)" 
   7.108 +| "tmbound n (Mul i a) = tmbound n a"
   7.109  lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t" by (induct t, auto)
   7.110  
   7.111  lemma tmbound_I: 
   7.112    assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound n t" and le: "n \<le> length bs"
   7.113    shows "Itm vs (bs[n:=x]) t = Itm vs bs t"
   7.114    using nb le bnd
   7.115 -  by (induct t rule: tmbound.induct , auto)
   7.116 +  by (induct t rule: tm.induct , auto)
   7.117 +
   7.118 +consts 
   7.119 +  incrtm0:: "tm \<Rightarrow> tm"
   7.120 +  decrtm0:: "tm \<Rightarrow> tm" 
   7.121  
   7.122  recdef decrtm0 "measure size"
   7.123    "decrtm0 (Bound n) = Bound (n - 1)"
   7.124 @@ -101,6 +96,7 @@
   7.125    "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
   7.126    "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
   7.127    "decrtm0 a = a"
   7.128 +
   7.129  recdef incrtm0 "measure size"
   7.130    "incrtm0 (Bound n) = Bound (n + 1)"
   7.131    "incrtm0 (Neg a) = Neg (incrtm0 a)"
   7.132 @@ -109,25 +105,26 @@
   7.133    "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
   7.134    "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
   7.135    "incrtm0 a = a"
   7.136 +
   7.137  lemma decrtm0: assumes nb: "tmbound0 t"
   7.138    shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
   7.139    using nb by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
   7.140 +
   7.141  lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
   7.142    by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
   7.143  
   7.144 -primrec
   7.145 +primrec decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" where
   7.146    "decrtm m (CP c) = (CP c)"
   7.147 -  "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
   7.148 -  "decrtm m (Neg a) = Neg (decrtm m a)"
   7.149 -  "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
   7.150 -  "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
   7.151 -  "decrtm m (Mul c a) = Mul c (decrtm m a)"
   7.152 -  "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
   7.153 +| "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
   7.154 +| "decrtm m (Neg a) = Neg (decrtm m a)"
   7.155 +| "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
   7.156 +| "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
   7.157 +| "decrtm m (Mul c a) = Mul c (decrtm m a)"
   7.158 +| "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
   7.159  
   7.160 -consts removen:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   7.161 -primrec
   7.162 +primrec removen:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   7.163    "removen n [] = []"
   7.164 -  "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
   7.165 +| "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
   7.166  
   7.167  lemma removen_same: "n \<ge> length xs \<Longrightarrow> removen n xs = xs"
   7.168    by (induct xs arbitrary: n, auto)
   7.169 @@ -172,50 +169,47 @@
   7.170    and nle: "m \<le> length bs" 
   7.171    shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
   7.172    using bnd nb nle
   7.173 -  by (induct t rule: decrtm.induct, auto simp add: removen_nth)
   7.174 +  by (induct t rule: tm.induct, auto simp add: removen_nth)
   7.175  
   7.176 -consts tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm"
   7.177 -primrec
   7.178 +primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where
   7.179    "tmsubst0 t (CP c) = CP c"
   7.180 -  "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   7.181 -  "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
   7.182 -  "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
   7.183 -  "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
   7.184 -  "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 
   7.185 -  "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
   7.186 +| "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   7.187 +| "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
   7.188 +| "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
   7.189 +| "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
   7.190 +| "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 
   7.191 +| "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
   7.192  lemma tmsubst0:
   7.193    shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
   7.194 -by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
   7.195 +by (induct a rule: tm.induct,auto simp add: nth_pos2)
   7.196  
   7.197  lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
   7.198 -by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
   7.199 +by (induct a rule: tm.induct,auto simp add: nth_pos2)
   7.200  
   7.201 -consts tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" 
   7.202 -
   7.203 -primrec
   7.204 +primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
   7.205    "tmsubst n t (CP c) = CP c"
   7.206 -  "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
   7.207 -  "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a) 
   7.208 +| "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
   7.209 +| "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a) 
   7.210               else CNP m c (tmsubst n t a))"
   7.211 -  "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
   7.212 -  "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
   7.213 -  "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 
   7.214 -  "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
   7.215 +| "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
   7.216 +| "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
   7.217 +| "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 
   7.218 +| "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
   7.219  
   7.220  lemma tmsubst: assumes nb: "tmboundslt (length bs) a" and nlt: "n \<le> length bs"
   7.221    shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
   7.222  using nb nlt
   7.223 -by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
   7.224 +by (induct a rule: tm.induct,auto simp add: nth_pos2)
   7.225  
   7.226  lemma tmsubst_nb0: assumes tnb: "tmbound0 t"
   7.227  shows "tmbound0 (tmsubst 0 t a)"
   7.228  using tnb
   7.229 -by (induct a rule: tmsubst.induct, auto)
   7.230 +by (induct a rule: tm.induct, auto)
   7.231  
   7.232  lemma tmsubst_nb: assumes tnb: "tmbound m t"
   7.233  shows "tmbound m (tmsubst m t a)"
   7.234  using tnb
   7.235 -by (induct a rule: tmsubst.induct, auto)
   7.236 +by (induct a rule: tm.induct, auto)
   7.237  lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"
   7.238    by (induct t, auto)
   7.239    (* Simplification *)
   7.240 @@ -447,21 +441,20 @@
   7.241  by (induct p rule: fmsize.induct) simp_all
   7.242  
   7.243    (* Semantics of formulae (fm) *)
   7.244 -consts Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
   7.245 -primrec
   7.246 +primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" where
   7.247    "Ifm vs bs T = True"
   7.248 -  "Ifm vs bs F = False"
   7.249 -  "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
   7.250 -  "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
   7.251 -  "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
   7.252 -  "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
   7.253 -  "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
   7.254 -  "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
   7.255 -  "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
   7.256 -  "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
   7.257 -  "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
   7.258 -  "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
   7.259 -  "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
   7.260 +| "Ifm vs bs F = False"
   7.261 +| "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
   7.262 +| "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
   7.263 +| "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
   7.264 +| "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
   7.265 +| "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
   7.266 +| "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
   7.267 +| "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
   7.268 +| "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
   7.269 +| "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
   7.270 +| "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
   7.271 +| "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
   7.272  
   7.273  consts not:: "fm \<Rightarrow> fm"
   7.274  recdef not "measure size"
   7.275 @@ -516,27 +509,24 @@
   7.276  
   7.277    (* Boundedness and substitution *)
   7.278  
   7.279 -consts boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool"
   7.280 -primrec
   7.281 +primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool" where
   7.282    "boundslt n T = True"
   7.283 -  "boundslt n F = True"
   7.284 -  "boundslt n (Lt t) = (tmboundslt n t)"
   7.285 -  "boundslt n (Le t) = (tmboundslt n t)"
   7.286 -  "boundslt n (Eq t) = (tmboundslt n t)"
   7.287 -  "boundslt n (NEq t) = (tmboundslt n t)"
   7.288 -  "boundslt n (NOT p) = boundslt n p"
   7.289 -  "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
   7.290 -  "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
   7.291 -  "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
   7.292 -  "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
   7.293 -  "boundslt n (E p) = boundslt (Suc n) p"
   7.294 -  "boundslt n (A p) = boundslt (Suc n) p"
   7.295 +| "boundslt n F = True"
   7.296 +| "boundslt n (Lt t) = (tmboundslt n t)"
   7.297 +| "boundslt n (Le t) = (tmboundslt n t)"
   7.298 +| "boundslt n (Eq t) = (tmboundslt n t)"
   7.299 +| "boundslt n (NEq t) = (tmboundslt n t)"
   7.300 +| "boundslt n (NOT p) = boundslt n p"
   7.301 +| "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
   7.302 +| "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
   7.303 +| "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
   7.304 +| "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
   7.305 +| "boundslt n (E p) = boundslt (Suc n) p"
   7.306 +| "boundslt n (A p) = boundslt (Suc n) p"
   7.307  
   7.308  consts 
   7.309    bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
   7.310 -  bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *)
   7.311    decr0 :: "fm \<Rightarrow> fm"
   7.312 -  decr :: "nat \<Rightarrow> fm \<Rightarrow> fm"
   7.313  recdef bound0 "measure size"
   7.314    "bound0 T = True"
   7.315    "bound0 F = True"
   7.316 @@ -556,26 +546,26 @@
   7.317  using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
   7.318  by (induct p rule: bound0.induct,auto simp add: nth_pos2)
   7.319  
   7.320 -primrec
   7.321 +primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *) where
   7.322    "bound m T = True"
   7.323 -  "bound m F = True"
   7.324 -  "bound m (Lt t) = tmbound m t"
   7.325 -  "bound m (Le t) = tmbound m t"
   7.326 -  "bound m (Eq t) = tmbound m t"
   7.327 -  "bound m (NEq t) = tmbound m t"
   7.328 -  "bound m (NOT p) = bound m p"
   7.329 -  "bound m (And p q) = (bound m p \<and> bound m q)"
   7.330 -  "bound m (Or p q) = (bound m p \<and> bound m q)"
   7.331 -  "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
   7.332 -  "bound m (Iff p q) = (bound m p \<and> bound m q)"
   7.333 -  "bound m (E p) = bound (Suc m) p"
   7.334 -  "bound m (A p) = bound (Suc m) p"
   7.335 +| "bound m F = True"
   7.336 +| "bound m (Lt t) = tmbound m t"
   7.337 +| "bound m (Le t) = tmbound m t"
   7.338 +| "bound m (Eq t) = tmbound m t"
   7.339 +| "bound m (NEq t) = tmbound m t"
   7.340 +| "bound m (NOT p) = bound m p"
   7.341 +| "bound m (And p q) = (bound m p \<and> bound m q)"
   7.342 +| "bound m (Or p q) = (bound m p \<and> bound m q)"
   7.343 +| "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
   7.344 +| "bound m (Iff p q) = (bound m p \<and> bound m q)"
   7.345 +| "bound m (E p) = bound (Suc m) p"
   7.346 +| "bound m (A p) = bound (Suc m) p"
   7.347  
   7.348  lemma bound_I:
   7.349    assumes bnd: "boundslt (length bs) p" and nb: "bound n p" and le: "n \<le> length bs"
   7.350    shows "Ifm vs (bs[n:=x]) p = Ifm vs bs p"
   7.351    using bnd nb le tmbound_I[where bs=bs and vs = vs]
   7.352 -proof(induct p arbitrary: bs n rule: bound.induct)
   7.353 +proof(induct p arbitrary: bs n rule: fm.induct)
   7.354    case (E p bs n) 
   7.355    {fix y
   7.356      from prems have bnd: "boundslt (length (y#bs)) p" 
   7.357 @@ -607,26 +597,26 @@
   7.358    using nb 
   7.359    by (induct p rule: decr0.induct, simp_all add: decrtm0)
   7.360  
   7.361 -primrec
   7.362 +primrec decr :: "nat \<Rightarrow> fm \<Rightarrow> fm" where
   7.363    "decr m T = T"
   7.364 -  "decr m F = F"
   7.365 -  "decr m (Lt t) = (Lt (decrtm m t))"
   7.366 -  "decr m (Le t) = (Le (decrtm m t))"
   7.367 -  "decr m (Eq t) = (Eq (decrtm m t))"
   7.368 -  "decr m (NEq t) = (NEq (decrtm m t))"
   7.369 -  "decr m (NOT p) = NOT (decr m p)" 
   7.370 -  "decr m (And p q) = conj (decr m p) (decr m q)"
   7.371 -  "decr m (Or p q) = disj (decr m p) (decr m q)"
   7.372 -  "decr m (Imp p q) = imp (decr m p) (decr m q)"
   7.373 -  "decr m (Iff p q) = iff (decr m p) (decr m q)"
   7.374 -  "decr m (E p) = E (decr (Suc m) p)"
   7.375 -  "decr m (A p) = A (decr (Suc m) p)"
   7.376 +| "decr m F = F"
   7.377 +| "decr m (Lt t) = (Lt (decrtm m t))"
   7.378 +| "decr m (Le t) = (Le (decrtm m t))"
   7.379 +| "decr m (Eq t) = (Eq (decrtm m t))"
   7.380 +| "decr m (NEq t) = (NEq (decrtm m t))"
   7.381 +| "decr m (NOT p) = NOT (decr m p)" 
   7.382 +| "decr m (And p q) = conj (decr m p) (decr m q)"
   7.383 +| "decr m (Or p q) = disj (decr m p) (decr m q)"
   7.384 +| "decr m (Imp p q) = imp (decr m p) (decr m q)"
   7.385 +| "decr m (Iff p q) = iff (decr m p) (decr m q)"
   7.386 +| "decr m (E p) = E (decr (Suc m) p)"
   7.387 +| "decr m (A p) = A (decr (Suc m) p)"
   7.388  
   7.389  lemma decr: assumes  bnd: "boundslt (length bs) p" and nb: "bound m p" 
   7.390    and nle: "m < length bs" 
   7.391    shows "Ifm vs (removen m bs) (decr m p) = Ifm vs bs p"
   7.392    using bnd nb nle
   7.393 -proof(induct p arbitrary: bs m rule: decr.induct)
   7.394 +proof(induct p arbitrary: bs m rule: fm.induct)
   7.395    case (E p bs m) 
   7.396    {fix x
   7.397      from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
   7.398 @@ -642,55 +632,51 @@
   7.399    } thus ?case by auto
   7.400  qed (auto simp add: decrtm removen_nth)
   7.401  
   7.402 -consts
   7.403 -  subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm"
   7.404 -
   7.405 -primrec
   7.406 +primrec subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm" where
   7.407    "subst0 t T = T"
   7.408 -  "subst0 t F = F"
   7.409 -  "subst0 t (Lt a) = Lt (tmsubst0 t a)"
   7.410 -  "subst0 t (Le a) = Le (tmsubst0 t a)"
   7.411 -  "subst0 t (Eq a) = Eq (tmsubst0 t a)"
   7.412 -  "subst0 t (NEq a) = NEq (tmsubst0 t a)"
   7.413 -  "subst0 t (NOT p) = NOT (subst0 t p)"
   7.414 -  "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   7.415 -  "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   7.416 -  "subst0 t (Imp p q) = Imp (subst0 t p)  (subst0 t q)"
   7.417 -  "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   7.418 -  "subst0 t (E p) = E p"
   7.419 -  "subst0 t (A p) = A p"
   7.420 +| "subst0 t F = F"
   7.421 +| "subst0 t (Lt a) = Lt (tmsubst0 t a)"
   7.422 +| "subst0 t (Le a) = Le (tmsubst0 t a)"
   7.423 +| "subst0 t (Eq a) = Eq (tmsubst0 t a)"
   7.424 +| "subst0 t (NEq a) = NEq (tmsubst0 t a)"
   7.425 +| "subst0 t (NOT p) = NOT (subst0 t p)"
   7.426 +| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   7.427 +| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   7.428 +| "subst0 t (Imp p q) = Imp (subst0 t p)  (subst0 t q)"
   7.429 +| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   7.430 +| "subst0 t (E p) = E p"
   7.431 +| "subst0 t (A p) = A p"
   7.432  
   7.433  lemma subst0: assumes qf: "qfree p"
   7.434    shows "Ifm vs (x#bs) (subst0 t p) = Ifm vs ((Itm vs (x#bs) t)#bs) p"
   7.435  using qf tmsubst0[where x="x" and bs="bs" and t="t"]
   7.436 -by (induct p rule: subst0.induct, auto)
   7.437 +by (induct p rule: fm.induct, auto)
   7.438  
   7.439  lemma subst0_nb:
   7.440    assumes bp: "tmbound0 t" and qf: "qfree p"
   7.441    shows "bound0 (subst0 t p)"
   7.442  using qf tmsubst0_nb[OF bp] bp
   7.443 -by (induct p rule: subst0.induct, auto)
   7.444 +by (induct p rule: fm.induct, auto)
   7.445  
   7.446 -consts   subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" 
   7.447 -primrec
   7.448 +primrec subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" where
   7.449    "subst n t T = T"
   7.450 -  "subst n t F = F"
   7.451 -  "subst n t (Lt a) = Lt (tmsubst n t a)"
   7.452 -  "subst n t (Le a) = Le (tmsubst n t a)"
   7.453 -  "subst n t (Eq a) = Eq (tmsubst n t a)"
   7.454 -  "subst n t (NEq a) = NEq (tmsubst n t a)"
   7.455 -  "subst n t (NOT p) = NOT (subst n t p)"
   7.456 -  "subst n t (And p q) = And (subst n t p) (subst n t q)"
   7.457 -  "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
   7.458 -  "subst n t (Imp p q) = Imp (subst n t p)  (subst n t q)"
   7.459 -  "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
   7.460 -  "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
   7.461 -  "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
   7.462 +| "subst n t F = F"
   7.463 +| "subst n t (Lt a) = Lt (tmsubst n t a)"
   7.464 +| "subst n t (Le a) = Le (tmsubst n t a)"
   7.465 +| "subst n t (Eq a) = Eq (tmsubst n t a)"
   7.466 +| "subst n t (NEq a) = NEq (tmsubst n t a)"
   7.467 +| "subst n t (NOT p) = NOT (subst n t p)"
   7.468 +| "subst n t (And p q) = And (subst n t p) (subst n t q)"
   7.469 +| "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
   7.470 +| "subst n t (Imp p q) = Imp (subst n t p)  (subst n t q)"
   7.471 +| "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
   7.472 +| "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
   7.473 +| "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
   7.474  
   7.475  lemma subst: assumes nb: "boundslt (length bs) p" and nlm: "n \<le> length bs"
   7.476    shows "Ifm vs bs (subst n t p) = Ifm vs (bs[n:= Itm vs bs t]) p"
   7.477    using nb nlm
   7.478 -proof (induct p arbitrary: bs n t rule: subst0.induct)
   7.479 +proof (induct p arbitrary: bs n t rule: fm.induct)
   7.480    case (E p bs n) 
   7.481    {fix x 
   7.482      from prems have bn: "boundslt (length (x#bs)) p" by simp 
   7.483 @@ -713,7 +699,7 @@
   7.484  lemma subst_nb: assumes tnb: "tmbound m t"
   7.485  shows "bound m (subst m t p)"
   7.486  using tnb tmsubst_nb incrtm0_tmbound
   7.487 -by (induct p arbitrary: m t rule: subst.induct, auto)
   7.488 +by (induct p arbitrary: m t rule: fm.induct, auto)
   7.489  
   7.490  lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
   7.491  by (induct p rule: not.induct, auto)
   7.492 @@ -2475,10 +2461,9 @@
   7.493  
   7.494  text {* Rest of the implementation *}
   7.495  
   7.496 -consts alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list"
   7.497 -primrec
   7.498 +primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
   7.499    "alluopairs [] = []"
   7.500 -  "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
   7.501 +| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
   7.502  
   7.503  lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
   7.504  by (induct xs, auto)
     8.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Sep 08 13:25:22 2010 +0200
     8.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Sep 08 19:21:46 2010 +0200
     8.3 @@ -10,60 +10,52 @@
     8.4  
     8.5  text{* Application of polynomial as a real function. *}
     8.6  
     8.7 -consts poly :: "'a list => 'a  => ('a::{comm_ring})"
     8.8 -primrec
     8.9 +primrec poly :: "'a list => 'a  => ('a::{comm_ring})" where
    8.10    poly_Nil:  "poly [] x = 0"
    8.11 -  poly_Cons: "poly (h#t) x = h + x * poly t x"
    8.12 +| poly_Cons: "poly (h#t) x = h + x * poly t x"
    8.13  
    8.14  
    8.15  subsection{*Arithmetic Operations on Polynomials*}
    8.16  
    8.17  text{*addition*}
    8.18 -consts padd :: "['a list, 'a list] => ('a::comm_ring_1) list"  (infixl "+++" 65)
    8.19 -primrec
    8.20 +primrec padd :: "['a list, 'a list] => ('a::comm_ring_1) list"  (infixl "+++" 65) where
    8.21    padd_Nil:  "[] +++ l2 = l2"
    8.22 -  padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
    8.23 +| padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
    8.24                              else (h + hd l2)#(t +++ tl l2))"
    8.25  
    8.26  text{*Multiplication by a constant*}
    8.27 -consts cmult :: "['a :: comm_ring_1, 'a list] => 'a list"  (infixl "%*" 70)
    8.28 -primrec
    8.29 -   cmult_Nil:  "c %* [] = []"
    8.30 -   cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
    8.31 +primrec cmult :: "['a :: comm_ring_1, 'a list] => 'a list"  (infixl "%*" 70) where
    8.32 +  cmult_Nil:  "c %* [] = []"
    8.33 +| cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
    8.34  
    8.35  text{*Multiplication by a polynomial*}
    8.36 -consts pmult :: "['a list, 'a list] => ('a::comm_ring_1) list"  (infixl "***" 70)
    8.37 -primrec
    8.38 -   pmult_Nil:  "[] *** l2 = []"
    8.39 -   pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
    8.40 +primrec pmult :: "['a list, 'a list] => ('a::comm_ring_1) list"  (infixl "***" 70) where
    8.41 +  pmult_Nil:  "[] *** l2 = []"
    8.42 +| pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
    8.43                                else (h %* l2) +++ ((0) # (t *** l2)))"
    8.44  
    8.45  text{*Repeated multiplication by a polynomial*}
    8.46 -consts mulexp :: "[nat, 'a list, 'a  list] => ('a ::comm_ring_1) list"
    8.47 -primrec
    8.48 -   mulexp_zero:  "mulexp 0 p q = q"
    8.49 -   mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"
    8.50 +primrec mulexp :: "[nat, 'a list, 'a  list] => ('a ::comm_ring_1) list" where
    8.51 +  mulexp_zero:  "mulexp 0 p q = q"
    8.52 +| mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"
    8.53  
    8.54  text{*Exponential*}
    8.55 -consts pexp :: "['a list, nat] => ('a::comm_ring_1) list"  (infixl "%^" 80)
    8.56 -primrec
    8.57 -   pexp_0:   "p %^ 0 = [1]"
    8.58 -   pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
    8.59 +primrec pexp :: "['a list, nat] => ('a::comm_ring_1) list"  (infixl "%^" 80) where
    8.60 +  pexp_0:   "p %^ 0 = [1]"
    8.61 +| pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
    8.62  
    8.63  text{*Quotient related value of dividing a polynomial by x + a*}
    8.64  (* Useful for divisor properties in inductive proofs *)
    8.65 -consts "pquot" :: "['a list, 'a::field] => 'a list"
    8.66 -primrec
    8.67 -   pquot_Nil:  "pquot [] a= []"
    8.68 -   pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
    8.69 +primrec pquot :: "['a list, 'a::field] => 'a list" where
    8.70 +  pquot_Nil:  "pquot [] a= []"
    8.71 +| pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
    8.72                     else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
    8.73  
    8.74  
    8.75  text{*normalization of polynomials (remove extra 0 coeff)*}
    8.76 -consts pnormalize :: "('a::comm_ring_1) list => 'a list"
    8.77 -primrec
    8.78 -   pnormalize_Nil:  "pnormalize [] = []"
    8.79 -   pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
    8.80 +primrec pnormalize :: "('a::comm_ring_1) list => 'a list" where
    8.81 +  pnormalize_Nil:  "pnormalize [] = []"
    8.82 +| pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
    8.83                                       then (if (h = 0) then [] else [h])
    8.84                                       else (h#(pnormalize p)))"
    8.85  
     9.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Sep 08 13:25:22 2010 +0200
     9.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Sep 08 19:21:46 2010 +0200
     9.3 @@ -19,38 +19,35 @@
     9.4  abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
     9.5  
     9.6  subsection{* Boundedness, substitution and all that *}
     9.7 -consts polysize:: "poly \<Rightarrow> nat"
     9.8 -primrec
     9.9 +primrec polysize:: "poly \<Rightarrow> nat" where
    9.10    "polysize (C c) = 1"
    9.11 -  "polysize (Bound n) = 1"
    9.12 -  "polysize (Neg p) = 1 + polysize p"
    9.13 -  "polysize (Add p q) = 1 + polysize p + polysize q"
    9.14 -  "polysize (Sub p q) = 1 + polysize p + polysize q"
    9.15 -  "polysize (Mul p q) = 1 + polysize p + polysize q"
    9.16 -  "polysize (Pw p n) = 1 + polysize p"
    9.17 -  "polysize (CN c n p) = 4 + polysize c + polysize p"
    9.18 +| "polysize (Bound n) = 1"
    9.19 +| "polysize (Neg p) = 1 + polysize p"
    9.20 +| "polysize (Add p q) = 1 + polysize p + polysize q"
    9.21 +| "polysize (Sub p q) = 1 + polysize p + polysize q"
    9.22 +| "polysize (Mul p q) = 1 + polysize p + polysize q"
    9.23 +| "polysize (Pw p n) = 1 + polysize p"
    9.24 +| "polysize (CN c n p) = 4 + polysize c + polysize p"
    9.25  
    9.26 -consts 
    9.27 -  polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *)
    9.28 -  polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *)
    9.29 -primrec
    9.30 +primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where
    9.31    "polybound0 (C c) = True"
    9.32 -  "polybound0 (Bound n) = (n>0)"
    9.33 -  "polybound0 (Neg a) = polybound0 a"
    9.34 -  "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
    9.35 -  "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" 
    9.36 -  "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
    9.37 -  "polybound0 (Pw p n) = (polybound0 p)"
    9.38 -  "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
    9.39 -primrec
    9.40 +| "polybound0 (Bound n) = (n>0)"
    9.41 +| "polybound0 (Neg a) = polybound0 a"
    9.42 +| "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
    9.43 +| "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" 
    9.44 +| "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
    9.45 +| "polybound0 (Pw p n) = (polybound0 p)"
    9.46 +| "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
    9.47 +
    9.48 +primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) where
    9.49    "polysubst0 t (C c) = (C c)"
    9.50 -  "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
    9.51 -  "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
    9.52 -  "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
    9.53 -  "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" 
    9.54 -  "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
    9.55 -  "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
    9.56 -  "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
    9.57 +| "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
    9.58 +| "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
    9.59 +| "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
    9.60 +| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" 
    9.61 +| "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
    9.62 +| "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
    9.63 +| "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
    9.64                               else CN (polysubst0 t c) n (polysubst0 t p))"
    9.65  
    9.66  consts 
    9.67 @@ -195,11 +192,10 @@
    9.68  
    9.69  definition shift1 :: "poly \<Rightarrow> poly" where
    9.70    "shift1 p \<equiv> CN 0\<^sub>p 0 p"
    9.71 -consts funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
    9.72  
    9.73 -primrec
    9.74 -  "funpow 0 f x = x"
    9.75 -  "funpow (Suc n) f x = funpow n f (f x)"
    9.76 +abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    9.77 +  "funpow \<equiv> compow"
    9.78 +
    9.79  function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)"
    9.80    where
    9.81    "polydivide_aux (a,n,p,k,s) = 
    9.82 @@ -211,7 +207,6 @@
    9.83    else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
    9.84    by pat_completeness auto
    9.85  
    9.86 -
    9.87  definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
    9.88    "polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)"
    9.89  
    9.90 @@ -230,16 +225,16 @@
    9.91  
    9.92  subsection{* Semantics of the polynomial representation *}
    9.93  
    9.94 -consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}"
    9.95 -primrec
    9.96 +primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
    9.97    "Ipoly bs (C c) = INum c"
    9.98 -  "Ipoly bs (Bound n) = bs!n"
    9.99 -  "Ipoly bs (Neg a) = - Ipoly bs a"
   9.100 -  "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
   9.101 -  "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
   9.102 -  "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
   9.103 -  "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
   9.104 -  "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
   9.105 +| "Ipoly bs (Bound n) = bs!n"
   9.106 +| "Ipoly bs (Neg a) = - Ipoly bs a"
   9.107 +| "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
   9.108 +| "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
   9.109 +| "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
   9.110 +| "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
   9.111 +| "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
   9.112 +
   9.113  abbreviation
   9.114    Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
   9.115    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
   9.116 @@ -729,7 +724,7 @@
   9.117    by (simp add: shift1_def)
   9.118  lemma funpow_shift1_isnpoly: 
   9.119    "\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)"
   9.120 -  by (induct n arbitrary: p, auto simp add: shift1_isnpoly)
   9.121 +  by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
   9.122  
   9.123  lemma funpow_isnpolyh: 
   9.124    assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n"
   9.125 @@ -767,7 +762,7 @@
   9.126  
   9.127  subsection{* Miscilanious lemmas about indexes, decrementation, substitution  etc ... *}
   9.128  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
   9.129 -proof(induct p arbitrary: n rule: polybound0.induct, auto)
   9.130 +proof(induct p arbitrary: n rule: poly.induct, auto)
   9.131    case (goal1 c n p n')
   9.132    hence "n = Suc (n - 1)" by simp
   9.133    hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
   9.134 @@ -793,7 +788,7 @@
   9.135    assumes nb: "polybound0 a"
   9.136    shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
   9.137  using nb
   9.138 -by (induct a rule: polybound0.induct) auto 
   9.139 +by (induct a rule: poly.induct) auto 
   9.140  lemma polysubst0_I:
   9.141    shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
   9.142    by (induct t) simp_all
   9.143 @@ -809,12 +804,12 @@
   9.144  
   9.145  lemma polysubst0_polybound0: assumes nb: "polybound0 t"
   9.146    shows "polybound0 (polysubst0 t a)"
   9.147 -using nb by (induct a rule: polysubst0.induct, auto)
   9.148 +using nb by (induct a rule: poly.induct, auto)
   9.149  
   9.150  lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
   9.151    by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)
   9.152  
   9.153 -fun maxindex :: "poly \<Rightarrow> nat" where
   9.154 +primrec maxindex :: "poly \<Rightarrow> nat" where
   9.155    "maxindex (Bound n) = n + 1"
   9.156  | "maxindex (CN c n p) = max  (n + 1) (max (maxindex c) (maxindex p))"
   9.157  | "maxindex (Add p q) = max (maxindex p) (maxindex q)"
   9.158 @@ -1183,7 +1178,7 @@
   9.159    case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   9.160    with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   9.161      and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
   9.162 -  thus ?case by simp
   9.163 +  thus ?case by (simp add: funpow_swap1)
   9.164  qed auto  
   9.165  
   9.166  lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
   9.167 @@ -1641,8 +1636,8 @@
   9.168  
   9.169  lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
   9.170    unfolding pnormal_def
   9.171 - apply (induct p rule: pnormalize.induct, simp_all)
   9.172 - apply (case_tac "p=[]", simp_all)
   9.173 + apply (induct p)
   9.174 + apply (simp_all, case_tac "p=[]", simp_all)
   9.175   done
   9.176  
   9.177  lemma degree_degree: assumes inc: "isnonconstant p"
   9.178 @@ -1668,16 +1663,15 @@
   9.179  qed
   9.180  
   9.181  section{* Swaps ; Division by a certain variable *}
   9.182 -consts swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
   9.183 -primrec
   9.184 +primrec swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where
   9.185    "swap n m (C x) = C x"
   9.186 -  "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
   9.187 -  "swap n m (Neg t) = Neg (swap n m t)"
   9.188 -  "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
   9.189 -  "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
   9.190 -  "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
   9.191 -  "swap n m (Pw t k) = Pw (swap n m t) k"
   9.192 -  "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k)
   9.193 +| "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
   9.194 +| "swap n m (Neg t) = Neg (swap n m t)"
   9.195 +| "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
   9.196 +| "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
   9.197 +| "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
   9.198 +| "swap n m (Pw t k) = Pw (swap n m t) k"
   9.199 +| "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k)
   9.200    (swap n m p)"
   9.201  
   9.202  lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs"
    10.1 --- a/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Sep 08 13:25:22 2010 +0200
    10.2 +++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Sep 08 19:21:46 2010 +0200
    10.3 @@ -32,24 +32,21 @@
    10.4  text {* The function @{text pre} extracts the precondition of an
    10.5  annotated command: *}
    10.6  
    10.7 -consts
    10.8 -  pre ::"'a ann_com \<Rightarrow> 'a assn" 
    10.9 -primrec 
   10.10 +primrec pre ::"'a ann_com \<Rightarrow> 'a assn"  where
   10.11    "pre (AnnBasic r f) = r"
   10.12 -  "pre (AnnSeq c1 c2) = pre c1"
   10.13 -  "pre (AnnCond1 r b c1 c2) = r"
   10.14 -  "pre (AnnCond2 r b c) = r"
   10.15 -  "pre (AnnWhile r b i c) = r"
   10.16 -  "pre (AnnAwait r b c) = r"
   10.17 +| "pre (AnnSeq c1 c2) = pre c1"
   10.18 +| "pre (AnnCond1 r b c1 c2) = r"
   10.19 +| "pre (AnnCond2 r b c) = r"
   10.20 +| "pre (AnnWhile r b i c) = r"
   10.21 +| "pre (AnnAwait r b c) = r"
   10.22  
   10.23  text {* Well-formedness predicate for atomic programs: *}
   10.24  
   10.25 -consts atom_com :: "'a com \<Rightarrow> bool"
   10.26 -primrec  
   10.27 +primrec atom_com :: "'a com \<Rightarrow> bool" where
   10.28    "atom_com (Parallel Ts) = False"
   10.29 -  "atom_com (Basic f) = True"
   10.30 -  "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
   10.31 -  "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
   10.32 -  "atom_com (While b i c) = atom_com c"
   10.33 +| "atom_com (Basic f) = True"
   10.34 +| "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
   10.35 +| "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
   10.36 +| "atom_com (While b i c) = atom_com c"
   10.37    
   10.38  end
   10.39 \ No newline at end of file
    11.1 --- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Sep 08 13:25:22 2010 +0200
    11.2 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Sep 08 19:21:46 2010 +0200
    11.3 @@ -3,29 +3,27 @@
    11.4  
    11.5  theory OG_Hoare imports OG_Tran begin
    11.6  
    11.7 -consts assertions :: "'a ann_com \<Rightarrow> ('a assn) set"
    11.8 -primrec
    11.9 +primrec assertions :: "'a ann_com \<Rightarrow> ('a assn) set" where
   11.10    "assertions (AnnBasic r f) = {r}"
   11.11 -  "assertions (AnnSeq c1 c2) = assertions c1 \<union> assertions c2"
   11.12 -  "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2"
   11.13 -  "assertions (AnnCond2 r b c) = {r} \<union> assertions c"
   11.14 -  "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c"
   11.15 -  "assertions (AnnAwait r b c) = {r}" 
   11.16 +| "assertions (AnnSeq c1 c2) = assertions c1 \<union> assertions c2"
   11.17 +| "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2"
   11.18 +| "assertions (AnnCond2 r b c) = {r} \<union> assertions c"
   11.19 +| "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c"
   11.20 +| "assertions (AnnAwait r b c) = {r}" 
   11.21  
   11.22 -consts atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set"       
   11.23 -primrec
   11.24 +primrec atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set" where
   11.25    "atomics (AnnBasic r f) = {(r, Basic f)}"
   11.26 -  "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2"
   11.27 -  "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2"
   11.28 -  "atomics (AnnCond2 r b c) = atomics c"
   11.29 -  "atomics (AnnWhile r b i c) = atomics c" 
   11.30 -  "atomics (AnnAwait r b c) = {(r \<inter> b, c)}"
   11.31 +| "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2"
   11.32 +| "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2"
   11.33 +| "atomics (AnnCond2 r b c) = atomics c"
   11.34 +| "atomics (AnnWhile r b i c) = atomics c" 
   11.35 +| "atomics (AnnAwait r b c) = {(r \<inter> b, c)}"
   11.36  
   11.37 -consts com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op"
   11.38 -primrec "com (c, q) = c"
   11.39 +primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
   11.40 +  "com (c, q) = c"
   11.41  
   11.42 -consts post :: "'a ann_triple_op \<Rightarrow> 'a assn"
   11.43 -primrec "post (c, q) = q"
   11.44 +primrec post :: "'a ann_triple_op \<Rightarrow> 'a assn" where
   11.45 +  "post (c, q) = q"
   11.46  
   11.47  definition interfree_aux :: "('a ann_com_op \<times> 'a assn \<times> 'a ann_com_op) \<Rightarrow> bool" where
   11.48    "interfree_aux \<equiv> \<lambda>(co, q, co'). co'= None \<or>  
   11.49 @@ -466,4 +464,4 @@
   11.50  apply(auto simp add: SEM_def sem_def)
   11.51  done
   11.52  
   11.53 -end
   11.54 \ No newline at end of file
   11.55 +end
    12.1 --- a/src/HOL/IMP/Compiler0.thy	Wed Sep 08 13:25:22 2010 +0200
    12.2 +++ b/src/HOL/IMP/Compiler0.thy	Wed Sep 08 19:21:46 2010 +0200
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      HOL/IMP/Compiler.thy
    12.5 -    ID:         $Id$
    12.6      Author:     Tobias Nipkow, TUM
    12.7      Copyright   1996 TUM
    12.8  
    12.9 @@ -49,14 +48,13 @@
   12.10  
   12.11  subsection "The compiler"
   12.12  
   12.13 -consts compile :: "com \<Rightarrow> instr list"
   12.14 -primrec
   12.15 -"compile \<SKIP> = []"
   12.16 -"compile (x:==a) = [ASIN x a]"
   12.17 -"compile (c1;c2) = compile c1 @ compile c2"
   12.18 +primrec compile :: "com \<Rightarrow> instr list" where
   12.19 +"compile \<SKIP> = []" |
   12.20 +"compile (x:==a) = [ASIN x a]" |
   12.21 +"compile (c1;c2) = compile c1 @ compile c2" |
   12.22  "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
   12.23   [JMPF b (length(compile c1) + 2)] @ compile c1 @
   12.24 - [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
   12.25 + [JMPF (%x. False) (length(compile c2)+1)] @ compile c2" |
   12.26  "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
   12.27   [JMPB (length(compile c)+1)]"
   12.28  
    13.1 --- a/src/HOL/Import/HOL4Compat.thy	Wed Sep 08 13:25:22 2010 +0200
    13.2 +++ b/src/HOL/Import/HOL4Compat.thy	Wed Sep 08 19:21:46 2010 +0200
    13.3 @@ -33,17 +33,13 @@
    13.4  (*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
    13.5    by simp*)
    13.6  
    13.7 -consts
    13.8 -  ISL :: "'a + 'b => bool"
    13.9 -  ISR :: "'a + 'b => bool"
   13.10 -
   13.11 -primrec ISL_def:
   13.12 +primrec ISL :: "'a + 'b => bool" where
   13.13    "ISL (Inl x) = True"
   13.14 -  "ISL (Inr x) = False"
   13.15 +| "ISL (Inr x) = False"
   13.16  
   13.17 -primrec ISR_def:
   13.18 +primrec ISR :: "'a + 'b => bool" where
   13.19    "ISR (Inl x) = False"
   13.20 -  "ISR (Inr x) = True"
   13.21 +| "ISR (Inr x) = True"
   13.22  
   13.23  lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))"
   13.24    by simp
   13.25 @@ -51,14 +47,10 @@
   13.26  lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))"
   13.27    by simp
   13.28  
   13.29 -consts
   13.30 -  OUTL :: "'a + 'b => 'a"
   13.31 -  OUTR :: "'a + 'b => 'b"
   13.32 -
   13.33 -primrec OUTL_def:
   13.34 +primrec OUTL :: "'a + 'b => 'a" where
   13.35    "OUTL (Inl x) = x"
   13.36  
   13.37 -primrec OUTR_def:
   13.38 +primrec OUTR :: "'a + 'b => 'b" where
   13.39    "OUTR (Inr x) = x"
   13.40  
   13.41  lemma OUTL: "OUTL (Inl x) = x"
   13.42 @@ -79,17 +71,13 @@
   13.43  lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
   13.44    by simp
   13.45  
   13.46 -consts
   13.47 -  IS_SOME :: "'a option => bool"
   13.48 -  IS_NONE :: "'a option => bool"
   13.49 -
   13.50 -primrec IS_SOME_def:
   13.51 +primrec IS_SOME :: "'a option => bool" where
   13.52    "IS_SOME (Some x) = True"
   13.53 -  "IS_SOME None = False"
   13.54 +| "IS_SOME None = False"
   13.55  
   13.56 -primrec IS_NONE_def:
   13.57 +primrec IS_NONE :: "'a option => bool" where
   13.58    "IS_NONE (Some x) = False"
   13.59 -  "IS_NONE None = True"
   13.60 +| "IS_NONE None = True"
   13.61  
   13.62  lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)"
   13.63    by simp
   13.64 @@ -97,15 +85,12 @@
   13.65  lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)"
   13.66    by simp
   13.67  
   13.68 -consts
   13.69 -  OPTION_JOIN :: "'a option option => 'a option"
   13.70 -
   13.71 -primrec OPTION_JOIN_def:
   13.72 +primrec OPTION_JOIN :: "'a option option => 'a option" where
   13.73    "OPTION_JOIN None = None"
   13.74 -  "OPTION_JOIN (Some x) = x"
   13.75 +| "OPTION_JOIN (Some x) = x"
   13.76  
   13.77  lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)"
   13.78 -  by simp;
   13.79 +  by simp
   13.80  
   13.81  lemma PAIR: "(fst x,snd x) = x"
   13.82    by simp
   13.83 @@ -261,14 +246,11 @@
   13.84  lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
   13.85    by simp
   13.86  
   13.87 -consts
   13.88 -  list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat"
   13.89 +primrec list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
   13.90 +  "list_size f [] = 0"
   13.91 +| "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
   13.92  
   13.93 -primrec
   13.94 -  "list_size f [] = 0"
   13.95 -  "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
   13.96 -
   13.97 -lemma list_size_def: "(!f. list_size f [] = 0) &
   13.98 +lemma list_size_def': "(!f. list_size f [] = 0) &
   13.99           (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
  13.100    by simp
  13.101  
  13.102 @@ -377,12 +359,9 @@
  13.103  lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
  13.104    by simp
  13.105  
  13.106 -consts
  13.107 -  map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list"
  13.108 -
  13.109 -primrec
  13.110 +primrec map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list" where
  13.111    map2_Nil: "map2 f [] l2 = []"
  13.112 -  map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
  13.113 +| map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
  13.114  
  13.115  lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)"
  13.116    by simp
  13.117 @@ -419,12 +398,9 @@
  13.118  lemma [hol4rew]: "ZIP (a,b) = zip a b"
  13.119    by (simp add: ZIP_def)
  13.120  
  13.121 -consts
  13.122 -  unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list"
  13.123 -
  13.124 -primrec
  13.125 +primrec unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list" where
  13.126    unzip_Nil: "unzip [] = ([],[])"
  13.127 -  unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
  13.128 +| unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
  13.129  
  13.130  lemma UNZIP: "(unzip [] = ([],[])) &
  13.131           (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"
    14.1 --- a/src/HOL/Induct/ABexp.thy	Wed Sep 08 13:25:22 2010 +0200
    14.2 +++ b/src/HOL/Induct/ABexp.thy	Wed Sep 08 19:21:46 2010 +0200
    14.3 @@ -20,38 +20,32 @@
    14.4  
    14.5  text {* \medskip Evaluation of arithmetic and boolean expressions *}
    14.6  
    14.7 -consts
    14.8 -  evala :: "('a => nat) => 'a aexp => nat"
    14.9 -  evalb :: "('a => nat) => 'a bexp => bool"
   14.10 -
   14.11 -primrec
   14.12 +primrec evala :: "('a => nat) => 'a aexp => nat"
   14.13 +  and evalb :: "('a => nat) => 'a bexp => bool" where
   14.14    "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
   14.15 -  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
   14.16 -  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
   14.17 -  "evala env (Var v) = env v"
   14.18 -  "evala env (Num n) = n"
   14.19 +| "evala env (Sum a1 a2) = evala env a1 + evala env a2"
   14.20 +| "evala env (Diff a1 a2) = evala env a1 - evala env a2"
   14.21 +| "evala env (Var v) = env v"
   14.22 +| "evala env (Num n) = n"
   14.23  
   14.24 -  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
   14.25 -  "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
   14.26 -  "evalb env (Neg b) = (\<not> evalb env b)"
   14.27 +| "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
   14.28 +| "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
   14.29 +| "evalb env (Neg b) = (\<not> evalb env b)"
   14.30  
   14.31  
   14.32  text {* \medskip Substitution on arithmetic and boolean expressions *}
   14.33  
   14.34 -consts
   14.35 -  substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
   14.36 -  substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
   14.37 -
   14.38 -primrec
   14.39 +primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
   14.40 +  and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" where
   14.41    "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
   14.42 -  "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
   14.43 -  "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
   14.44 -  "substa f (Var v) = f v"
   14.45 -  "substa f (Num n) = Num n"
   14.46 +| "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
   14.47 +| "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
   14.48 +| "substa f (Var v) = f v"
   14.49 +| "substa f (Num n) = Num n"
   14.50  
   14.51 -  "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
   14.52 -  "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
   14.53 -  "substb f (Neg b) = Neg (substb f b)"
   14.54 +| "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
   14.55 +| "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
   14.56 +| "substb f (Neg b) = Neg (substb f b)"
   14.57  
   14.58  lemma subst1_aexp:
   14.59    "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
    15.1 --- a/src/HOL/Induct/Ordinals.thy	Wed Sep 08 13:25:22 2010 +0200
    15.2 +++ b/src/HOL/Induct/Ordinals.thy	Wed Sep 08 19:21:46 2010 +0200
    15.3 @@ -17,18 +17,13 @@
    15.4    | Succ ordinal
    15.5    | Limit "nat => ordinal"
    15.6  
    15.7 -consts
    15.8 -  pred :: "ordinal => nat => ordinal option"
    15.9 -primrec
   15.10 +primrec pred :: "ordinal => nat => ordinal option" where
   15.11    "pred Zero n = None"
   15.12 -  "pred (Succ a) n = Some a"
   15.13 -  "pred (Limit f) n = Some (f n)"
   15.14 +| "pred (Succ a) n = Some a"
   15.15 +| "pred (Limit f) n = Some (f n)"
   15.16  
   15.17 -consts
   15.18 -  iter :: "('a => 'a) => nat => ('a => 'a)"
   15.19 -primrec
   15.20 -  "iter f 0 = id"
   15.21 -  "iter f (Suc n) = f \<circ> (iter f n)"
   15.22 +abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)" where
   15.23 +  "iter f n \<equiv> f ^^ n"
   15.24  
   15.25  definition
   15.26    OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" where
   15.27 @@ -38,30 +33,24 @@
   15.28    OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<Squnion>") where
   15.29    "\<Squnion>f = OpLim (iter f)"
   15.30  
   15.31 -consts
   15.32 -  cantor :: "ordinal => ordinal => ordinal"
   15.33 -primrec
   15.34 +primrec cantor :: "ordinal => ordinal => ordinal" where
   15.35    "cantor a Zero = Succ a"
   15.36 -  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
   15.37 -  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
   15.38 +| "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
   15.39 +| "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
   15.40  
   15.41 -consts
   15.42 -  Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>")
   15.43 -primrec
   15.44 +primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>") where
   15.45    "\<nabla>f Zero = f Zero"
   15.46 -  "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
   15.47 -  "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
   15.48 +| "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
   15.49 +| "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
   15.50  
   15.51  definition
   15.52    deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" where
   15.53    "deriv f = \<nabla>(\<Squnion>f)"
   15.54  
   15.55 -consts
   15.56 -  veblen :: "ordinal => ordinal => ordinal"
   15.57 -primrec
   15.58 +primrec veblen :: "ordinal => ordinal => ordinal" where
   15.59    "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
   15.60 -  "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
   15.61 -  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
   15.62 +| "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
   15.63 +| "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
   15.64  
   15.65  definition "veb a = veblen a Zero"
   15.66  definition "\<epsilon>\<^isub>0 = veb Zero"
    16.1 --- a/src/HOL/Induct/PropLog.thy	Wed Sep 08 13:25:22 2010 +0200
    16.2 +++ b/src/HOL/Induct/PropLog.thy	Wed Sep 08 19:21:46 2010 +0200
    16.3 @@ -41,25 +41,20 @@
    16.4  
    16.5  subsubsection {* Semantics of propositional logic. *}
    16.6  
    16.7 -consts
    16.8 -  eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100)
    16.9 -
   16.10 -primrec     "tt[[false]] = False"
   16.11 -            "tt[[#v]]    = (v \<in> tt)"
   16.12 -  eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
   16.13 +primrec eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100) where
   16.14 +            "tt[[false]] = False"
   16.15 +|            "tt[[#v]]    = (v \<in> tt)"
   16.16 +| eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
   16.17  
   16.18  text {*
   16.19    A finite set of hypotheses from @{text t} and the @{text Var}s in
   16.20    @{text p}.
   16.21  *}
   16.22  
   16.23 -consts
   16.24 -  hyps  :: "['a pl, 'a set] => 'a pl set"
   16.25 -
   16.26 -primrec
   16.27 +primrec hyps  :: "['a pl, 'a set] => 'a pl set" where
   16.28    "hyps false  tt = {}"
   16.29 -  "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
   16.30 -  "hyps (p->q) tt = hyps p tt Un hyps q tt"
   16.31 +| "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
   16.32 +| "hyps (p->q) tt = hyps p tt Un hyps q tt"
   16.33  
   16.34  subsubsection {* Logical consequence *}
   16.35  
    17.1 --- a/src/HOL/Induct/QuoDataType.thy	Wed Sep 08 13:25:22 2010 +0200
    17.2 +++ b/src/HOL/Induct/QuoDataType.thy	Wed Sep 08 19:21:46 2010 +0200
    17.3 @@ -58,14 +58,11 @@
    17.4  
    17.5  text{*A function to return the set of nonces present in a message.  It will
    17.6  be lifted to the initial algrebra, to serve as an example of that process.*}
    17.7 -consts
    17.8 -  freenonces :: "freemsg \<Rightarrow> nat set"
    17.9 -
   17.10 -primrec
   17.11 -   "freenonces (NONCE N) = {N}"
   17.12 -   "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
   17.13 -   "freenonces (CRYPT K X) = freenonces X"
   17.14 -   "freenonces (DECRYPT K X) = freenonces X"
   17.15 +primrec freenonces :: "freemsg \<Rightarrow> nat set" where
   17.16 +  "freenonces (NONCE N) = {N}"
   17.17 +| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
   17.18 +| "freenonces (CRYPT K X) = freenonces X"
   17.19 +| "freenonces (DECRYPT K X) = freenonces X"
   17.20  
   17.21  text{*This theorem lets us prove that the nonces function respects the
   17.22  equivalence relation.  It also helps us prove that Nonce
   17.23 @@ -78,12 +75,11 @@
   17.24  
   17.25  text{*A function to return the left part of the top pair in a message.  It will
   17.26  be lifted to the initial algrebra, to serve as an example of that process.*}
   17.27 -consts freeleft :: "freemsg \<Rightarrow> freemsg"
   17.28 -primrec
   17.29 -   "freeleft (NONCE N) = NONCE N"
   17.30 -   "freeleft (MPAIR X Y) = X"
   17.31 -   "freeleft (CRYPT K X) = freeleft X"
   17.32 -   "freeleft (DECRYPT K X) = freeleft X"
   17.33 +primrec freeleft :: "freemsg \<Rightarrow> freemsg" where
   17.34 +  "freeleft (NONCE N) = NONCE N"
   17.35 +| "freeleft (MPAIR X Y) = X"
   17.36 +| "freeleft (CRYPT K X) = freeleft X"
   17.37 +| "freeleft (DECRYPT K X) = freeleft X"
   17.38  
   17.39  text{*This theorem lets us prove that the left function respects the
   17.40  equivalence relation.  It also helps us prove that MPair
   17.41 @@ -96,12 +92,11 @@
   17.42  subsubsection{*The Right Projection*}
   17.43  
   17.44  text{*A function to return the right part of the top pair in a message.*}
   17.45 -consts freeright :: "freemsg \<Rightarrow> freemsg"
   17.46 -primrec
   17.47 -   "freeright (NONCE N) = NONCE N"
   17.48 -   "freeright (MPAIR X Y) = Y"
   17.49 -   "freeright (CRYPT K X) = freeright X"
   17.50 -   "freeright (DECRYPT K X) = freeright X"
   17.51 +primrec freeright :: "freemsg \<Rightarrow> freemsg" where
   17.52 +  "freeright (NONCE N) = NONCE N"
   17.53 +| "freeright (MPAIR X Y) = Y"
   17.54 +| "freeright (CRYPT K X) = freeright X"
   17.55 +| "freeright (DECRYPT K X) = freeright X"
   17.56  
   17.57  text{*This theorem lets us prove that the right function respects the
   17.58  equivalence relation.  It also helps us prove that MPair
   17.59 @@ -114,12 +109,11 @@
   17.60  subsubsection{*The Discriminator for Constructors*}
   17.61  
   17.62  text{*A function to distinguish nonces, mpairs and encryptions*}
   17.63 -consts freediscrim :: "freemsg \<Rightarrow> int"
   17.64 -primrec
   17.65 -   "freediscrim (NONCE N) = 0"
   17.66 -   "freediscrim (MPAIR X Y) = 1"
   17.67 -   "freediscrim (CRYPT K X) = freediscrim X + 2"
   17.68 -   "freediscrim (DECRYPT K X) = freediscrim X - 2"
   17.69 +primrec freediscrim :: "freemsg \<Rightarrow> int" where
   17.70 +  "freediscrim (NONCE N) = 0"
   17.71 +| "freediscrim (MPAIR X Y) = 1"
   17.72 +| "freediscrim (CRYPT K X) = freediscrim X + 2"
   17.73 +| "freediscrim (DECRYPT K X) = freediscrim X - 2"
   17.74  
   17.75  text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
   17.76  theorem msgrel_imp_eq_freediscrim:
    18.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Wed Sep 08 13:25:22 2010 +0200
    18.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Wed Sep 08 19:21:46 2010 +0200
    18.3 @@ -72,17 +72,14 @@
    18.4  be lifted to the initial algrebra, to serve as an example of that process.
    18.5  Note that the "free" refers to the free datatype rather than to the concept
    18.6  of a free variable.*}
    18.7 -consts
    18.8 -  freevars      :: "freeExp \<Rightarrow> nat set"
    18.9 -  freevars_list :: "freeExp list \<Rightarrow> nat set"
   18.10 +primrec freevars :: "freeExp \<Rightarrow> nat set" 
   18.11 +  and freevars_list :: "freeExp list \<Rightarrow> nat set" where
   18.12 +  "freevars (VAR N) = {N}"
   18.13 +| "freevars (PLUS X Y) = freevars X \<union> freevars Y"
   18.14 +| "freevars (FNCALL F Xs) = freevars_list Xs"
   18.15  
   18.16 -primrec
   18.17 -   "freevars (VAR N) = {N}"
   18.18 -   "freevars (PLUS X Y) = freevars X \<union> freevars Y"
   18.19 -   "freevars (FNCALL F Xs) = freevars_list Xs"
   18.20 -
   18.21 -   "freevars_list [] = {}"
   18.22 -   "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
   18.23 +| "freevars_list [] = {}"
   18.24 +| "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
   18.25  
   18.26  text{*This theorem lets us prove that the vars function respects the
   18.27  equivalence relation.  It also helps us prove that Variable
   18.28 @@ -98,11 +95,10 @@
   18.29  subsubsection{*Functions for Freeness*}
   18.30  
   18.31  text{*A discriminator function to distinguish vars, sums and function calls*}
   18.32 -consts freediscrim :: "freeExp \<Rightarrow> int"
   18.33 -primrec
   18.34 -   "freediscrim (VAR N) = 0"
   18.35 -   "freediscrim (PLUS X Y) = 1"
   18.36 -   "freediscrim (FNCALL F Xs) = 2"
   18.37 +primrec freediscrim :: "freeExp \<Rightarrow> int" where
   18.38 +  "freediscrim (VAR N) = 0"
   18.39 +| "freediscrim (PLUS X Y) = 1"
   18.40 +| "freediscrim (FNCALL F Xs) = 2"
   18.41  
   18.42  theorem exprel_imp_eq_freediscrim:
   18.43       "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
   18.44 @@ -111,12 +107,10 @@
   18.45  
   18.46  text{*This function, which returns the function name, is used to
   18.47  prove part of the injectivity property for FnCall.*}
   18.48 -consts  freefun :: "freeExp \<Rightarrow> nat"
   18.49 -
   18.50 -primrec
   18.51 -   "freefun (VAR N) = 0"
   18.52 -   "freefun (PLUS X Y) = 0"
   18.53 -   "freefun (FNCALL F Xs) = F"
   18.54 +primrec freefun :: "freeExp \<Rightarrow> nat" where
   18.55 +  "freefun (VAR N) = 0"
   18.56 +| "freefun (PLUS X Y) = 0"
   18.57 +| "freefun (FNCALL F Xs) = F"
   18.58  
   18.59  theorem exprel_imp_eq_freefun:
   18.60       "U \<sim> V \<Longrightarrow> freefun U = freefun V"
   18.61 @@ -125,11 +119,10 @@
   18.62  
   18.63  text{*This function, which returns the list of function arguments, is used to
   18.64  prove part of the injectivity property for FnCall.*}
   18.65 -consts  freeargs      :: "freeExp \<Rightarrow> freeExp list"
   18.66 -primrec
   18.67 -   "freeargs (VAR N) = []"
   18.68 -   "freeargs (PLUS X Y) = []"
   18.69 -   "freeargs (FNCALL F Xs) = Xs"
   18.70 +primrec freeargs :: "freeExp \<Rightarrow> freeExp list" where
   18.71 +  "freeargs (VAR N) = []"
   18.72 +| "freeargs (PLUS X Y) = []"
   18.73 +| "freeargs (FNCALL F Xs) = Xs"
   18.74  
   18.75  theorem exprel_imp_eqv_freeargs:
   18.76       "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
   18.77 @@ -285,10 +278,9 @@
   18.78  by (simp add: congruent_def exprel_imp_eq_freevars) 
   18.79  
   18.80  text{*The extension of the function @{term vars} to lists*}
   18.81 -consts vars_list :: "exp list \<Rightarrow> nat set"
   18.82 -primrec
   18.83 -   "vars_list []    = {}"
   18.84 -   "vars_list(E#Es) = vars E \<union> vars_list Es"
   18.85 +primrec vars_list :: "exp list \<Rightarrow> nat set" where
   18.86 +  "vars_list []    = {}"
   18.87 +| "vars_list(E#Es) = vars E \<union> vars_list Es"
   18.88  
   18.89  
   18.90  text{*Now prove the three equations for @{term vars}*}
    19.1 --- a/src/HOL/Induct/SList.thy	Wed Sep 08 13:25:22 2010 +0200
    19.2 +++ b/src/HOL/Induct/SList.thy	Wed Sep 08 19:21:46 2010 +0200
    19.3 @@ -133,10 +133,9 @@
    19.4    map       :: "('a=>'b) => ('a list => 'b list)" where
    19.5    "map f xs = list_rec xs [] (%x l r. f(x)#r)"
    19.6  
    19.7 -consts take      :: "['a list,nat] => 'a list"
    19.8 -primrec
    19.9 +primrec take :: "['a list,nat] => 'a list" where
   19.10    take_0:  "take xs 0 = []"
   19.11 -  take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
   19.12 +| take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
   19.13  
   19.14  lemma ListI: "x : list (range Leaf) ==> x : List"
   19.15  by (simp add: List_def)
    20.1 --- a/src/HOL/Induct/Tree.thy	Wed Sep 08 13:25:22 2010 +0200
    20.2 +++ b/src/HOL/Induct/Tree.thy	Wed Sep 08 19:21:46 2010 +0200
    20.3 @@ -95,15 +95,15 @@
    20.4  text{*Example of a general function*}
    20.5  
    20.6  function
    20.7 -  add2 :: "(brouwer*brouwer) => brouwer"
    20.8 +  add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
    20.9  where
   20.10 -  "add2 (i, Zero) = i"
   20.11 -| "add2 (i, (Succ j)) = Succ (add2 (i, j))"
   20.12 -| "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
   20.13 +  "add2 i Zero = i"
   20.14 +| "add2 i (Succ j) = Succ (add2 i j)"
   20.15 +| "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))"
   20.16  by pat_completeness auto
   20.17  termination by (relation "inv_image brouwer_order snd") auto
   20.18  
   20.19 -lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
   20.20 +lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)"
   20.21    by (induct k) auto
   20.22  
   20.23  end
    21.1 --- a/src/HOL/Lattice/Orders.thy	Wed Sep 08 13:25:22 2010 +0200
    21.2 +++ b/src/HOL/Lattice/Orders.thy	Wed Sep 08 19:21:46 2010 +0200
    21.3 @@ -48,9 +48,7 @@
    21.4  
    21.5  datatype 'a dual = dual 'a
    21.6  
    21.7 -consts
    21.8 -  undual :: "'a dual \<Rightarrow> 'a"
    21.9 -primrec
   21.10 +primrec undual :: "'a dual \<Rightarrow> 'a" where
   21.11    undual_dual: "undual (dual x) = x"
   21.12  
   21.13  instantiation dual :: (leq) leq
    22.1 --- a/src/HOL/Metis_Examples/BT.thy	Wed Sep 08 13:25:22 2010 +0200
    22.2 +++ b/src/HOL/Metis_Examples/BT.thy	Wed Sep 08 19:21:46 2010 +0200
    22.3 @@ -15,53 +15,41 @@
    22.4      Lf
    22.5    | Br 'a  "'a bt"  "'a bt"
    22.6  
    22.7 -consts
    22.8 -  n_nodes   :: "'a bt => nat"
    22.9 -  n_leaves  :: "'a bt => nat"
   22.10 -  depth     :: "'a bt => nat"
   22.11 -  reflect   :: "'a bt => 'a bt"
   22.12 -  bt_map    :: "('a => 'b) => ('a bt => 'b bt)"
   22.13 -  preorder  :: "'a bt => 'a list"
   22.14 -  inorder   :: "'a bt => 'a list"
   22.15 -  postorder :: "'a bt => 'a list"
   22.16 -  appnd    :: "'a bt => 'a bt => 'a bt"
   22.17 +primrec n_nodes :: "'a bt => nat" where
   22.18 +  "n_nodes Lf = 0"
   22.19 +| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
   22.20 +
   22.21 +primrec n_leaves :: "'a bt => nat" where
   22.22 +  "n_leaves Lf = Suc 0"
   22.23 +| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
   22.24  
   22.25 -primrec
   22.26 -  "n_nodes Lf = 0"
   22.27 -  "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
   22.28 +primrec depth :: "'a bt => nat" where
   22.29 +  "depth Lf = 0"
   22.30 +| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
   22.31  
   22.32 -primrec
   22.33 -  "n_leaves Lf = Suc 0"
   22.34 -  "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
   22.35 -
   22.36 -primrec
   22.37 -  "depth Lf = 0"
   22.38 -  "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
   22.39 +primrec reflect :: "'a bt => 'a bt" where
   22.40 +  "reflect Lf = Lf"
   22.41 +| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
   22.42  
   22.43 -primrec
   22.44 -  "reflect Lf = Lf"
   22.45 -  "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
   22.46 -
   22.47 -primrec
   22.48 +primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
   22.49    "bt_map f Lf = Lf"
   22.50 -  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
   22.51 +| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
   22.52  
   22.53 -primrec
   22.54 +primrec preorder :: "'a bt => 'a list" where
   22.55    "preorder Lf = []"
   22.56 -  "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
   22.57 +| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
   22.58  
   22.59 -primrec
   22.60 +primrec inorder :: "'a bt => 'a list" where
   22.61    "inorder Lf = []"
   22.62 -  "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
   22.63 +| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
   22.64  
   22.65 -primrec
   22.66 +primrec postorder :: "'a bt => 'a list" where
   22.67    "postorder Lf = []"
   22.68 -  "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
   22.69 +| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
   22.70  
   22.71 -primrec
   22.72 -  "appnd Lf t = t"
   22.73 -  "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)"
   22.74 -
   22.75 +primrec append :: "'a bt => 'a bt => 'a bt" where
   22.76 +  "append Lf t = t"
   22.77 +| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
   22.78  
   22.79  text {* \medskip BT simplification *}
   22.80  
   22.81 @@ -135,12 +123,12 @@
   22.82   apply (metis bt_map.simps(1))
   22.83  by (metis bt_map.simps(2))
   22.84  
   22.85 -declare [[ sledgehammer_problem_prefix = "BT__bt_map_appnd" ]]
   22.86 +declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
   22.87  
   22.88 -lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)"
   22.89 +lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)"
   22.90  apply (induct t)
   22.91 - apply (metis appnd.simps(1) bt_map.simps(1))
   22.92 -by (metis appnd.simps(2) bt_map.simps(2))
   22.93 + apply (metis append.simps(1) bt_map.simps(1))
   22.94 +by (metis append.simps(2) bt_map.simps(2))
   22.95  
   22.96  declare [[ sledgehammer_problem_prefix = "BT__bt_map_compose" ]]
   22.97  
   22.98 @@ -219,8 +207,8 @@
   22.99  apply (induct t)
  22.100   apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
  22.101                reflect.simps(1))
  22.102 -by (metis append.simps(1) append.simps(2) postorder.simps(2) preorder.simps(2)
  22.103 -          reflect.simps(2) rev.simps(2) rev_append rev_swap)
  22.104 +apply simp
  22.105 +done
  22.106  
  22.107  declare [[ sledgehammer_problem_prefix = "BT__inorder_reflect" ]]
  22.108  
  22.109 @@ -245,44 +233,44 @@
  22.110  Analogues of the standard properties of the append function for lists.
  22.111  *}
  22.112  
  22.113 -declare [[ sledgehammer_problem_prefix = "BT__appnd_assoc" ]]
  22.114 +declare [[ sledgehammer_problem_prefix = "BT__append_assoc" ]]
  22.115  
  22.116 -lemma appnd_assoc [simp]: "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
  22.117 +lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)"
  22.118  apply (induct t1)
  22.119 - apply (metis appnd.simps(1))
  22.120 -by (metis appnd.simps(2))
  22.121 + apply (metis append.simps(1))
  22.122 +by (metis append.simps(2))
  22.123  
  22.124 -declare [[ sledgehammer_problem_prefix = "BT__appnd_Lf2" ]]
  22.125 +declare [[ sledgehammer_problem_prefix = "BT__append_Lf2" ]]
  22.126  
  22.127 -lemma appnd_Lf2 [simp]: "appnd t Lf = t"
  22.128 +lemma append_Lf2 [simp]: "append t Lf = t"
  22.129  apply (induct t)
  22.130 - apply (metis appnd.simps(1))
  22.131 -by (metis appnd.simps(2))
  22.132 + apply (metis append.simps(1))
  22.133 +by (metis append.simps(2))
  22.134  
  22.135  declare max_add_distrib_left [simp]
  22.136  
  22.137 -declare [[ sledgehammer_problem_prefix = "BT__depth_appnd" ]]
  22.138 +declare [[ sledgehammer_problem_prefix = "BT__depth_append" ]]
  22.139  
  22.140 -lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
  22.141 +lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
  22.142  apply (induct t1)
  22.143 - apply (metis appnd.simps(1) depth.simps(1) plus_nat.simps(1))
  22.144 + apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1))
  22.145  by simp
  22.146  
  22.147 -declare [[ sledgehammer_problem_prefix = "BT__n_leaves_appnd" ]]
  22.148 +declare [[ sledgehammer_problem_prefix = "BT__n_leaves_append" ]]
  22.149  
  22.150 -lemma n_leaves_appnd [simp]:
  22.151 -     "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
  22.152 +lemma n_leaves_append [simp]:
  22.153 +     "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
  22.154  apply (induct t1)
  22.155 - apply (metis appnd.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
  22.156 + apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
  22.157                semiring_norm(111))
  22.158  by (simp add: left_distrib)
  22.159  
  22.160 -declare [[ sledgehammer_problem_prefix = "BT__bt_map_appnd" ]]
  22.161 +declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
  22.162  
  22.163 -lemma (*bt_map_appnd:*)
  22.164 -     "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
  22.165 +lemma (*bt_map_append:*)
  22.166 +     "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
  22.167  apply (induct t1)
  22.168 - apply (metis appnd.simps(1) bt_map.simps(1))
  22.169 -by (metis bt_map_appnd)
  22.170 + apply (metis append.simps(1) bt_map.simps(1))
  22.171 +by (metis bt_map_append)
  22.172  
  22.173  end
    23.1 --- a/src/HOL/Nominal/Examples/Class3.thy	Wed Sep 08 13:25:22 2010 +0200
    23.2 +++ b/src/HOL/Nominal/Examples/Class3.thy	Wed Sep 08 19:21:46 2010 +0200
    23.3 @@ -5956,17 +5956,13 @@
    23.4      done
    23.5  qed
    23.6  
    23.7 -consts
    23.8 -  "idn" :: "(name\<times>ty) list\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list"
    23.9 -primrec
   23.10 +primrec "idn" :: "(name\<times>ty) list\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list" where
   23.11    "idn [] a   = []"
   23.12 -  "idn (p#\<Gamma>) a = ((fst p),a,Ax (fst p) a)#(idn \<Gamma> a)"
   23.13 -
   23.14 -consts
   23.15 -  "idc" :: "(coname\<times>ty) list\<Rightarrow>name\<Rightarrow>(coname\<times>name\<times>trm) list"
   23.16 -primrec
   23.17 +| "idn (p#\<Gamma>) a = ((fst p),a,Ax (fst p) a)#(idn \<Gamma> a)"
   23.18 +
   23.19 +primrec "idc" :: "(coname\<times>ty) list\<Rightarrow>name\<Rightarrow>(coname\<times>name\<times>trm) list" where
   23.20    "idc [] x    = []"
   23.21 -  "idc (p#\<Delta>) x = ((fst p),x,Ax x (fst p))#(idc \<Delta> x)"
   23.22 +| "idc (p#\<Delta>) x = ((fst p),x,Ax x (fst p))#(idc \<Delta> x)"
   23.23  
   23.24  lemma idn_eqvt[eqvt]:
   23.25    fixes pi1::"name prm"
    24.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Sep 08 13:25:22 2010 +0200
    24.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Sep 08 19:21:46 2010 +0200
    24.3 @@ -107,17 +107,17 @@
    24.4  | "vrs_of (TVarB x y) = {}"
    24.5  by auto
    24.6  
    24.7 -consts
    24.8 +primrec
    24.9    "ty_dom" :: "env \<Rightarrow> tyvrs set"
   24.10 -primrec
   24.11 +where
   24.12    "ty_dom [] = {}"
   24.13 -  "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)" 
   24.14 +| "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)" 
   24.15  
   24.16 -consts
   24.17 +primrec
   24.18    "trm_dom" :: "env \<Rightarrow> vrs set"
   24.19 -primrec
   24.20 +where
   24.21    "trm_dom [] = {}"
   24.22 -  "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)" 
   24.23 +| "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)" 
   24.24  
   24.25  lemma vrs_of_eqvt[eqvt]:
   24.26    fixes pi ::"tyvrs prm"
   24.27 @@ -475,12 +475,9 @@
   24.28  by (induct B rule: binding.induct)
   24.29     (simp_all add: fresh_atm type_subst_identity)
   24.30  
   24.31 -consts 
   24.32 -  subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100)
   24.33 -
   24.34 -primrec
   24.35 -"([])[Y \<mapsto> T]\<^sub>e= []"
   24.36 -"(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
   24.37 +primrec subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100) where
   24.38 +  "([])[Y \<mapsto> T]\<^sub>e= []"
   24.39 +| "(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
   24.40  
   24.41  lemma ctxt_subst_fresh':
   24.42    fixes X::"tyvrs"
   24.43 @@ -686,13 +683,13 @@
   24.44    have fresh_cond: "X\<sharp>\<Gamma>" by fact
   24.45    hence fresh_ty_dom: "X\<sharp>(ty_dom \<Gamma>)" by (simp add: fresh_dom)
   24.46    have "(\<forall>X<:T\<^isub>2. T\<^isub>1) closed_in \<Gamma>" by fact
   24.47 -  hence closed\<^isub>T\<^isub>2: "T\<^isub>2 closed_in \<Gamma>" and closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in ((TVarB  X T\<^isub>2)#\<Gamma>)" 
   24.48 +  hence closed\<^isub>T2: "T\<^isub>2 closed_in \<Gamma>" and closed\<^isub>T1: "T\<^isub>1 closed_in ((TVarB  X T\<^isub>2)#\<Gamma>)" 
   24.49      by (auto simp add: closed_in_def ty.supp abs_supp)
   24.50    have ok: "\<turnstile> \<Gamma> ok" by fact  
   24.51 -  hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_ty_dom by simp
   24.52 -  have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp
   24.53 +  hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T2 fresh_ty_dom by simp
   24.54 +  have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T2 ok by simp
   24.55    moreover
   24.56 -  have "((TVarB X T\<^isub>2)#\<Gamma>) \<turnstile> T\<^isub>1 <: T\<^isub>1" using ih_T\<^isub>1 closed\<^isub>T\<^isub>1 ok' by simp
   24.57 +  have "((TVarB X T\<^isub>2)#\<Gamma>) \<turnstile> T\<^isub>1 <: T\<^isub>1" using ih_T\<^isub>1 closed\<^isub>T1 ok' by simp
   24.58    ultimately show "\<Gamma> \<turnstile> (\<forall>X<:T\<^isub>2. T\<^isub>1) <: (\<forall>X<:T\<^isub>2. T\<^isub>1)" using fresh_cond 
   24.59      by (simp add: subtype_of.SA_all)
   24.60  qed (auto simp add: closed_in_def ty.supp supp_atm)
   24.61 @@ -783,10 +780,10 @@
   24.62    have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   24.63    have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
   24.64    have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   24.65 -  hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   24.66 +  hence closed\<^isub>T1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   24.67    have ok: "\<turnstile> \<Delta> ok" by fact
   24.68    have ext: "\<Delta> extends \<Gamma>" by fact
   24.69 -  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
   24.70 +  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T1 by (simp only: extends_closed)
   24.71    hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force   
   24.72    moreover 
   24.73    have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
   24.74 @@ -811,10 +808,10 @@
   24.75    have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   24.76    have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
   24.77    have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   24.78 -  hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   24.79 +  hence closed\<^isub>T1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   24.80    have ok: "\<turnstile> \<Delta> ok" by fact
   24.81    have ext: "\<Delta> extends \<Gamma>" by fact
   24.82 -  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
   24.83 +  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T1 by (simp only: extends_closed)
   24.84    hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force   
   24.85    moreover
   24.86    have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
   24.87 @@ -903,7 +900,7 @@
   24.88        case (SA_arrow \<Gamma> Q\<^isub>1 S\<^isub>1 S\<^isub>2 Q\<^isub>2) 
   24.89        then have rh_drv: "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T" by simp
   24.90        from `Q\<^isub>1 \<rightarrow> Q\<^isub>2 = Q` 
   24.91 -      have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" by auto
   24.92 +      have Q\<^isub>12_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" by auto
   24.93        have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
   24.94        have lh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact      
   24.95        from rh_drv have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2)" 
   24.96 @@ -921,10 +918,10 @@
   24.97            and   rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1"
   24.98            and   rh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
   24.99          from IH_trans[of "Q\<^isub>1"] 
  24.100 -        have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>1 lh_drv_prm\<^isub>1 by simp 
  24.101 +        have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using Q\<^isub>12_less rh_drv_prm\<^isub>1 lh_drv_prm\<^isub>1 by simp 
  24.102          moreover
  24.103          from IH_trans[of "Q\<^isub>2"] 
  24.104 -        have "\<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 lh_drv_prm\<^isub>2 by simp
  24.105 +        have "\<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>12_less rh_drv_prm\<^isub>2 lh_drv_prm\<^isub>2 by simp
  24.106          ultimately have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
  24.107          then have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" using T_inst by simp
  24.108        }
  24.109 @@ -954,15 +951,15 @@
  24.110            and   rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1" 
  24.111            and   rh_drv_prm\<^isub>2:"((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
  24.112          have "(\<forall>X<:Q\<^isub>1. Q\<^isub>2) = Q" by fact 
  24.113 -        then have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" 
  24.114 +        then have Q\<^isub>12_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" 
  24.115            using fresh_cond by auto
  24.116          from IH_trans[of "Q\<^isub>1"] 
  24.117 -        have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using lh_drv_prm\<^isub>1 rh_drv_prm\<^isub>1 Q\<^isub>1\<^isub>2_less by blast
  24.118 +        have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using lh_drv_prm\<^isub>1 rh_drv_prm\<^isub>1 Q\<^isub>12_less by blast
  24.119          moreover
  24.120          from IH_narrow[of "Q\<^isub>1" "[]"] 
  24.121 -        have "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" using Q\<^isub>1\<^isub>2_less lh_drv_prm\<^isub>2 rh_drv_prm\<^isub>1 by simp
  24.122 +        have "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" using Q\<^isub>12_less lh_drv_prm\<^isub>2 rh_drv_prm\<^isub>1 by simp
  24.123          with IH_trans[of "Q\<^isub>2"] 
  24.124 -        have "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 by simp
  24.125 +        have "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>12_less rh_drv_prm\<^isub>2 by simp
  24.126          ultimately have "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:T\<^isub>1. T\<^isub>2)"
  24.127            using fresh_cond by (simp add: subtype_of.SA_all)
  24.128          hence "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T" using T_inst by simp
  24.129 @@ -1005,16 +1002,16 @@
  24.130          with IH_inner show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" by (simp add: subtype_of.SA_trans_TVar)
  24.131        next
  24.132          case True
  24.133 -        have memb\<^isub>X\<^isub>Q: "(TVarB X Q)\<in>set (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp
  24.134 -        have memb\<^isub>X\<^isub>P: "(TVarB X P)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" by simp
  24.135 +        have memb\<^isub>XQ: "(TVarB X Q)\<in>set (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp
  24.136 +        have memb\<^isub>XP: "(TVarB X P)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" by simp
  24.137          have eq: "X=Y" by fact 
  24.138 -        hence "S=Q" using ok\<^isub>Q lh_drv_prm memb\<^isub>X\<^isub>Q by (simp only: uniqueness_of_ctxt)
  24.139 +        hence "S=Q" using ok\<^isub>Q lh_drv_prm memb\<^isub>XQ by (simp only: uniqueness_of_ctxt)
  24.140          hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp
  24.141          moreover
  24.142          have "(\<Delta>@[(TVarB X P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def)
  24.143          hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv ok\<^isub>P by (simp only: weakening)
  24.144          ultimately have "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_lemma) 
  24.145 -        then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto
  24.146 +        then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>XP eq by auto
  24.147        qed
  24.148      next
  24.149        case (SA_refl_TVar Y \<Gamma> X \<Delta>)
  24.150 @@ -1049,7 +1046,7 @@
  24.151  | T_Abs[intro]: "\<lbrakk> VarB x T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> T\<^isub>2"
  24.152  | T_Sub[intro]: "\<lbrakk> \<Gamma> \<turnstile> t : S; \<Gamma> \<turnstile> S <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t : T"
  24.153  | T_TAbs[intro]:"\<lbrakk> TVarB X T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>1. t\<^isub>2) : (\<forall>X<:T\<^isub>1. T\<^isub>2)"
  24.154 -| T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^isub>1,T\<^isub>2); \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2); \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 : (T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>)" 
  24.155 +| T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^isub>1,T\<^isub>2); \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T\<^isub>11. T\<^isub>12); \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 : (T\<^isub>12[X \<mapsto> T\<^isub>2]\<^sub>\<tau>)" 
  24.156  
  24.157  equivariance typing
  24.158  
  24.159 @@ -1164,10 +1161,10 @@
  24.160  inductive 
  24.161    eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60)
  24.162  where
  24.163 -  E_Abs         : "\<lbrakk> x \<sharp> v\<^isub>2; val v\<^isub>2 \<rbrakk> \<Longrightarrow> (\<lambda>x:T\<^isub>1\<^isub>1. t\<^isub>1\<^isub>2) \<cdot> v\<^isub>2 \<longmapsto> t\<^isub>1\<^isub>2[x \<mapsto> v\<^isub>2]"
  24.164 +  E_Abs         : "\<lbrakk> x \<sharp> v\<^isub>2; val v\<^isub>2 \<rbrakk> \<Longrightarrow> (\<lambda>x:T\<^isub>11. t\<^isub>12) \<cdot> v\<^isub>2 \<longmapsto> t\<^isub>12[x \<mapsto> v\<^isub>2]"
  24.165  | E_App1 [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u"
  24.166  | E_App2 [intro]: "\<lbrakk> val v; t \<longmapsto> t' \<rbrakk> \<Longrightarrow> v \<cdot> t \<longmapsto> v \<cdot> t'"
  24.167 -| E_TAbs        : "X \<sharp> (T\<^isub>1\<^isub>1, T\<^isub>2) \<Longrightarrow> (\<lambda>X<:T\<^isub>1\<^isub>1. t\<^isub>1\<^isub>2) \<cdot>\<^sub>\<tau> T\<^isub>2 \<longmapsto> t\<^isub>1\<^isub>2[X \<mapsto>\<^sub>\<tau> T\<^isub>2]"
  24.168 +| E_TAbs        : "X \<sharp> (T\<^isub>11, T\<^isub>2) \<Longrightarrow> (\<lambda>X<:T\<^isub>11. t\<^isub>12) \<cdot>\<^sub>\<tau> T\<^isub>2 \<longmapsto> t\<^isub>12[X \<mapsto>\<^sub>\<tau> T\<^isub>2]"
  24.169  | E_TApp [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot>\<^sub>\<tau> T \<longmapsto> t' \<cdot>\<^sub>\<tau> T"
  24.170  
  24.171  lemma better_E_Abs[intro]:
  24.172 @@ -1315,7 +1312,7 @@
  24.173    case (T_Var x T)
  24.174    then show ?case by auto
  24.175  next
  24.176 -  case (T_App X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
  24.177 +  case (T_App X t\<^isub>1 T\<^isub>2 T\<^isub>11 T\<^isub>12)
  24.178    then show ?case by force
  24.179  next
  24.180    case (T_Abs y T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
  24.181 @@ -1744,68 +1741,68 @@
  24.182    assumes H: "\<Gamma> \<turnstile> t : T"
  24.183    shows "t \<longmapsto> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : T" using H
  24.184  proof (nominal_induct avoiding: t' rule: typing.strong_induct)
  24.185 -  case (T_App \<Gamma> t\<^isub>1 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2 t\<^isub>2 t')
  24.186 +  case (T_App \<Gamma> t\<^isub>1 T\<^isub>11 T\<^isub>12 t\<^isub>2 t')
  24.187    obtain x::vrs where x_fresh: "x \<sharp> (\<Gamma>, t\<^isub>1 \<cdot> t\<^isub>2, t')"
  24.188      by (rule exists_fresh) (rule fin_supp)
  24.189    obtain X::tyvrs where "X \<sharp> (t\<^isub>1 \<cdot> t\<^isub>2, t')"
  24.190      by (rule exists_fresh) (rule fin_supp)
  24.191    with `t\<^isub>1 \<cdot> t\<^isub>2 \<longmapsto> t'` show ?case
  24.192    proof (cases rule: eval.strong_cases [where x=x and X=X])
  24.193 -    case (E_Abs v\<^isub>2 T\<^isub>1\<^isub>1' t\<^isub>1\<^isub>2)
  24.194 -    with T_App and x_fresh have h: "\<Gamma> \<turnstile> (\<lambda>x:T\<^isub>1\<^isub>1'. t\<^isub>1\<^isub>2) : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2"
  24.195 +    case (E_Abs v\<^isub>2 T\<^isub>11' t\<^isub>12)
  24.196 +    with T_App and x_fresh have h: "\<Gamma> \<turnstile> (\<lambda>x:T\<^isub>11'. t\<^isub>12) : T\<^isub>11 \<rightarrow> T\<^isub>12"
  24.197        by (simp add: trm.inject fresh_prod)
  24.198      moreover from x_fresh have "x \<sharp> \<Gamma>" by simp
  24.199      ultimately obtain S'
  24.200 -      where T\<^isub>1\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1\<^isub>1 <: T\<^isub>1\<^isub>1'"
  24.201 -      and t\<^isub>1\<^isub>2: "(VarB x T\<^isub>1\<^isub>1') # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : S'"
  24.202 -      and S': "\<Gamma> \<turnstile> S' <: T\<^isub>1\<^isub>2"
  24.203 +      where T\<^isub>11: "\<Gamma> \<turnstile> T\<^isub>11 <: T\<^isub>11'"
  24.204 +      and t\<^isub>12: "(VarB x T\<^isub>11') # \<Gamma> \<turnstile> t\<^isub>12 : S'"
  24.205 +      and S': "\<Gamma> \<turnstile> S' <: T\<^isub>12"
  24.206        by (rule Abs_type') blast
  24.207 -    from `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1`
  24.208 -    have "\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1'" using T\<^isub>1\<^isub>1 by (rule T_Sub)
  24.209 -    with t\<^isub>1\<^isub>2 have "\<Gamma> \<turnstile> t\<^isub>1\<^isub>2[x \<mapsto> t\<^isub>2] : S'" 
  24.210 +    from `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11`
  24.211 +    have "\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11'" using T\<^isub>11 by (rule T_Sub)
  24.212 +    with t\<^isub>12 have "\<Gamma> \<turnstile> t\<^isub>12[x \<mapsto> t\<^isub>2] : S'" 
  24.213        by (rule subst_type [where \<Delta>="[]", simplified])
  24.214 -    hence "\<Gamma> \<turnstile> t\<^isub>1\<^isub>2[x \<mapsto> t\<^isub>2] : T\<^isub>1\<^isub>2" using S' by (rule T_Sub)
  24.215 +    hence "\<Gamma> \<turnstile> t\<^isub>12[x \<mapsto> t\<^isub>2] : T\<^isub>12" using S' by (rule T_Sub)
  24.216      with E_Abs and x_fresh show ?thesis by (simp add: trm.inject fresh_prod)
  24.217    next
  24.218      case (E_App1 t''' t'' u)
  24.219      hence "t\<^isub>1 \<longmapsto> t''" by (simp add:trm.inject) 
  24.220 -    hence "\<Gamma> \<turnstile> t'' : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2" by (rule T_App)
  24.221 -    hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^isub>2 : T\<^isub>1\<^isub>2" using `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1`
  24.222 +    hence "\<Gamma> \<turnstile> t'' : T\<^isub>11 \<rightarrow> T\<^isub>12" by (rule T_App)
  24.223 +    hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^isub>2 : T\<^isub>12" using `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11`
  24.224        by (rule typing.T_App)
  24.225      with E_App1 show ?thesis by (simp add:trm.inject)
  24.226    next
  24.227      case (E_App2 v t''' t'')
  24.228      hence "t\<^isub>2 \<longmapsto> t''" by (simp add:trm.inject) 
  24.229 -    hence "\<Gamma> \<turnstile> t'' : T\<^isub>1\<^isub>1" by (rule T_App)
  24.230 -    with T_App(1) have "\<Gamma> \<turnstile> t\<^isub>1 \<cdot> t'' : T\<^isub>1\<^isub>2"
  24.231 +    hence "\<Gamma> \<turnstile> t'' : T\<^isub>11" by (rule T_App)
  24.232 +    with T_App(1) have "\<Gamma> \<turnstile> t\<^isub>1 \<cdot> t'' : T\<^isub>12"
  24.233        by (rule typing.T_App)
  24.234      with E_App2 show ?thesis by (simp add:trm.inject) 
  24.235    qed (simp_all add: fresh_prod)
  24.236  next
  24.237 -  case (T_TApp X \<Gamma> t\<^isub>1 T\<^isub>2  T\<^isub>1\<^isub>1  T\<^isub>1\<^isub>2 t')
  24.238 +  case (T_TApp X \<Gamma> t\<^isub>1 T\<^isub>2  T\<^isub>11  T\<^isub>12 t')
  24.239    obtain x::vrs where "x \<sharp> (t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2, t')"
  24.240      by (rule exists_fresh) (rule fin_supp)
  24.241    with `t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 \<longmapsto> t'`
  24.242    show ?case
  24.243    proof (cases rule: eval.strong_cases [where X=X and x=x])
  24.244 -    case (E_TAbs T\<^isub>1\<^isub>1' T\<^isub>2' t\<^isub>1\<^isub>2)
  24.245 -    with T_TApp have "\<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>1\<^isub>1'. t\<^isub>1\<^isub>2) : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2)" and "X \<sharp> \<Gamma>" and "X \<sharp> T\<^isub>1\<^isub>1'"
  24.246 +    case (E_TAbs T\<^isub>11' T\<^isub>2' t\<^isub>12)
  24.247 +    with T_TApp have "\<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>11'. t\<^isub>12) : (\<forall>X<:T\<^isub>11. T\<^isub>12)" and "X \<sharp> \<Gamma>" and "X \<sharp> T\<^isub>11'"
  24.248        by (simp_all add: trm.inject)
  24.249 -    moreover from `\<Gamma>\<turnstile>T\<^isub>2<:T\<^isub>1\<^isub>1` and `X \<sharp> \<Gamma>` have "X \<sharp> T\<^isub>1\<^isub>1"
  24.250 +    moreover from `\<Gamma>\<turnstile>T\<^isub>2<:T\<^isub>11` and `X \<sharp> \<Gamma>` have "X \<sharp> T\<^isub>11"
  24.251        by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed)
  24.252      ultimately obtain S'
  24.253 -      where "TVarB X T\<^isub>1\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : S'"
  24.254 -      and "(TVarB X T\<^isub>1\<^isub>1 # \<Gamma>) \<turnstile> S' <: T\<^isub>1\<^isub>2"
  24.255 +      where "TVarB X T\<^isub>11 # \<Gamma> \<turnstile> t\<^isub>12 : S'"
  24.256 +      and "(TVarB X T\<^isub>11 # \<Gamma>) \<turnstile> S' <: T\<^isub>12"
  24.257        by (rule TAbs_type') blast
  24.258 -    hence "TVarB X T\<^isub>1\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : T\<^isub>1\<^isub>2" by (rule T_Sub)
  24.259 -    hence "\<Gamma> \<turnstile> t\<^isub>1\<^isub>2[X \<mapsto>\<^sub>\<tau> T\<^isub>2] : T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>" using `\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1`
  24.260 +    hence "TVarB X T\<^isub>11 # \<Gamma> \<turnstile> t\<^isub>12 : T\<^isub>12" by (rule T_Sub)
  24.261 +    hence "\<Gamma> \<turnstile> t\<^isub>12[X \<mapsto>\<^sub>\<tau> T\<^isub>2] : T\<^isub>12[X \<mapsto> T\<^isub>2]\<^sub>\<tau>" using `\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11`
  24.262        by (rule substT_type [where D="[]", simplified])
  24.263      with T_TApp and E_TAbs show ?thesis by (simp add: trm.inject)
  24.264    next
  24.265      case (E_TApp t''' t'' T)
  24.266      from E_TApp have "t\<^isub>1 \<longmapsto> t''" by (simp add: trm.inject)
  24.267 -    then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2)" by (rule T_TApp)
  24.268 -    then have "\<Gamma> \<turnstile> t'' \<cdot>\<^sub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>" using `\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1`
  24.269 +    then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^isub>11. T\<^isub>12)" by (rule T_TApp)
  24.270 +    then have "\<Gamma> \<turnstile> t'' \<cdot>\<^sub>\<tau> T\<^isub>2 : T\<^isub>12[X \<mapsto> T\<^isub>2]\<^sub>\<tau>" using `\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11`
  24.271        by (rule better_T_TApp)
  24.272      with E_TApp show ?thesis by (simp add: trm.inject)
  24.273    qed (simp_all add: fresh_prod)
  24.274 @@ -1845,7 +1842,7 @@
  24.275    shows "val t \<or> (\<exists>t'. t \<longmapsto> t')" 
  24.276  using assms
  24.277  proof (induct "[]::env" t T)
  24.278 -  case (T_App t\<^isub>1 T\<^isub>1\<^isub>1  T\<^isub>1\<^isub>2 t\<^isub>2)
  24.279 +  case (T_App t\<^isub>1 T\<^isub>11  T\<^isub>12 t\<^isub>2)
  24.280    hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
  24.281    thus ?case
  24.282    proof
  24.283 @@ -1871,7 +1868,7 @@
  24.284      thus ?case by auto
  24.285    qed
  24.286  next
  24.287 -  case (T_TApp X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
  24.288 +  case (T_TApp X t\<^isub>1 T\<^isub>2 T\<^isub>11 T\<^isub>12)
  24.289    hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
  24.290    thus ?case
  24.291    proof
    25.1 --- a/src/HOL/Nominal/Examples/W.thy	Wed Sep 08 13:25:22 2010 +0200
    25.2 +++ b/src/HOL/Nominal/Examples/W.thy	Wed Sep 08 19:21:46 2010 +0200
    25.3 @@ -150,12 +150,9 @@
    25.4  equivariance valid
    25.5  
    25.6  text {* General *}
    25.7 -consts
    25.8 -  gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS"
    25.9 -
   25.10 -primrec 
   25.11 +primrec gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS" where
   25.12    "gen T [] = Ty T"
   25.13 -  "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
   25.14 +| "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
   25.15  
   25.16  lemma gen_eqvt[eqvt]:
   25.17    fixes pi::"tvar prm"
    26.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Wed Sep 08 13:25:22 2010 +0200
    26.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Sep 08 19:21:46 2010 +0200
    26.3 @@ -15,17 +15,11 @@
    26.4    NbT_pos:  "0 < NbT"
    26.5  
    26.6  (*This function merely sums the elements of a list*)
    26.7 -consts tokens     :: "nat list => nat"
    26.8 -primrec 
    26.9 +primrec tokens :: "nat list => nat" where
   26.10    "tokens [] = 0"
   26.11 -  "tokens (x#xs) = x + tokens xs"
   26.12 +| "tokens (x#xs) = x + tokens xs"
   26.13  
   26.14 -consts
   26.15 -  bag_of :: "'a list => 'a multiset"
   26.16 -
   26.17 -primrec
   26.18 -  "bag_of []     = {#}"
   26.19 -  "bag_of (x#xs) = {#x#} + bag_of xs"
   26.20 +abbreviation (input) "bag_of \<equiv> multiset_of"
   26.21  
   26.22  lemma setsum_fun_mono [rule_format]:
   26.23       "!!f :: nat=>nat.  
    27.1 --- a/src/HOL/ZF/HOLZF.thy	Wed Sep 08 13:25:22 2010 +0200
    27.2 +++ b/src/HOL/ZF/HOLZF.thy	Wed Sep 08 19:21:46 2010 +0200
    27.3 @@ -402,12 +402,9 @@
    27.4      done
    27.5  qed
    27.6  
    27.7 -consts
    27.8 -  nat2Nat :: "nat \<Rightarrow> ZF"
    27.9 -
   27.10 -primrec
   27.11 -nat2Nat_0[intro]:  "nat2Nat 0 = Empty"
   27.12 -nat2Nat_Suc[intro]:  "nat2Nat (Suc n) = SucNat (nat2Nat n)"
   27.13 +primrec nat2Nat :: "nat \<Rightarrow> ZF" where
   27.14 +  nat2Nat_0[intro]:  "nat2Nat 0 = Empty"
   27.15 +| nat2Nat_Suc[intro]:  "nat2Nat (Suc n) = SucNat (nat2Nat n)"
   27.16  
   27.17  definition Nat2nat :: "ZF \<Rightarrow> nat" where
   27.18    "Nat2nat == inv nat2Nat"
   27.19 @@ -500,12 +497,9 @@
   27.20    apply auto
   27.21    done
   27.22  
   27.23 -consts
   27.24 -  NatInterval :: "nat \<Rightarrow> nat \<Rightarrow> ZF"
   27.25 -
   27.26 -primrec
   27.27 +primrec NatInterval :: "nat \<Rightarrow> nat \<Rightarrow> ZF" where
   27.28    "NatInterval n 0 = Singleton (nat2Nat n)"
   27.29 -  "NatInterval n (Suc m) = union (NatInterval n m) (Singleton (nat2Nat (n+m+1)))"
   27.30 +| "NatInterval n (Suc m) = union (NatInterval n m) (Singleton (nat2Nat (n+m+1)))"
   27.31  
   27.32  lemma n_Elem_NatInterval[rule_format]: "! q. q <= m \<longrightarrow> Elem (nat2Nat (n+q)) (NatInterval n m)"
   27.33    apply (induct m)
   27.34 @@ -729,12 +723,9 @@
   27.35    apply (simp add: Ext_def)
   27.36    done
   27.37  
   27.38 -consts
   27.39 -  Ext_ZF_n :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> nat \<Rightarrow> ZF"
   27.40 -
   27.41 -primrec
   27.42 +primrec Ext_ZF_n :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> nat \<Rightarrow> ZF" where
   27.43    "Ext_ZF_n R s 0 = Ext_ZF R s"
   27.44 -  "Ext_ZF_n R s (Suc n) = Sum (Repl (Ext_ZF_n R s n) (Ext_ZF R))"
   27.45 +| "Ext_ZF_n R s (Suc n) = Sum (Repl (Ext_ZF_n R s n) (Ext_ZF R))"
   27.46  
   27.47  definition Ext_ZF_hull :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> ZF" where
   27.48    "Ext_ZF_hull R s == SeqSum (Ext_ZF_n R s)"
    28.1 --- a/src/HOL/ex/BT.thy	Wed Sep 08 13:25:22 2010 +0200
    28.2 +++ b/src/HOL/ex/BT.thy	Wed Sep 08 19:21:46 2010 +0200
    28.3 @@ -1,5 +1,4 @@
    28.4  (*  Title:      HOL/ex/BT.thy
    28.5 -    ID:         $Id$
    28.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    28.7      Copyright   1995  University of Cambridge
    28.8  
    28.9 @@ -14,53 +13,41 @@
   28.10      Lf
   28.11    | Br 'a  "'a bt"  "'a bt"
   28.12  
   28.13 -consts
   28.14 -  n_nodes   :: "'a bt => nat"
   28.15 -  n_leaves  :: "'a bt => nat"
   28.16 -  depth     :: "'a bt => nat"
   28.17 -  reflect   :: "'a bt => 'a bt"
   28.18 -  bt_map    :: "('a => 'b) => ('a bt => 'b bt)"
   28.19 -  preorder  :: "'a bt => 'a list"
   28.20 -  inorder   :: "'a bt => 'a list"
   28.21 -  postorder :: "'a bt => 'a list"
   28.22 -  append     :: "'a bt => 'a bt => 'a bt"
   28.23 +primrec n_nodes :: "'a bt => nat" where
   28.24 +  "n_nodes Lf = 0"
   28.25 +| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
   28.26 +
   28.27 +primrec n_leaves :: "'a bt => nat" where
   28.28 +  "n_leaves Lf = Suc 0"
   28.29 +| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
   28.30  
   28.31 -primrec
   28.32 -  "n_nodes Lf = 0"
   28.33 -  "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
   28.34 +primrec depth :: "'a bt => nat" where
   28.35 +  "depth Lf = 0"
   28.36 +| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
   28.37  
   28.38 -primrec
   28.39 -  "n_leaves Lf = Suc 0"
   28.40 -  "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
   28.41 -
   28.42 -primrec
   28.43 -  "depth Lf = 0"
   28.44 -  "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
   28.45 +primrec reflect :: "'a bt => 'a bt" where
   28.46 +  "reflect Lf = Lf"
   28.47 +| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
   28.48  
   28.49 -primrec
   28.50 -  "reflect Lf = Lf"
   28.51 -  "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
   28.52 -
   28.53 -primrec
   28.54 +primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
   28.55    "bt_map f Lf = Lf"
   28.56 -  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
   28.57 +| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
   28.58  
   28.59 -primrec
   28.60 +primrec preorder :: "'a bt => 'a list" where
   28.61    "preorder Lf = []"
   28.62 -  "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
   28.63 +| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
   28.64  
   28.65 -primrec
   28.66 +primrec inorder :: "'a bt => 'a list" where
   28.67    "inorder Lf = []"
   28.68 -  "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
   28.69 +| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
   28.70  
   28.71 -primrec
   28.72 +primrec postorder :: "'a bt => 'a list" where
   28.73    "postorder Lf = []"
   28.74 -  "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
   28.75 +| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
   28.76  
   28.77 -primrec
   28.78 +primrec append :: "'a bt => 'a bt => 'a bt" where
   28.79    "append Lf t = t"
   28.80 -  "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
   28.81 -
   28.82 +| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
   28.83  
   28.84  text {* \medskip BT simplification *}
   28.85  
    29.1 --- a/src/HOL/ex/Chinese.thy	Wed Sep 08 13:25:22 2010 +0200
    29.2 +++ b/src/HOL/ex/Chinese.thy	Wed Sep 08 19:21:46 2010 +0200
    29.3 @@ -1,5 +1,4 @@
    29.4  (* -*- coding: utf-8 -*- :encoding=utf-8:
    29.5 -    ID:         $Id$
    29.6      Author:     Ning Zhang and Christian Urban
    29.7  
    29.8  Example theory involving Unicode characters (UTF-8 encoding) -- both
    29.9 @@ -30,20 +29,17 @@
   29.10    | Nine  ("九")
   29.11    | Ten   ("十")
   29.12  
   29.13 -consts
   29.14 -  translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100)
   29.15 -
   29.16 -primrec
   29.17 +primrec translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100) where
   29.18   "|一| = 1"
   29.19 - "|二| = 2"
   29.20 - "|三| = 3"
   29.21 - "|四| = 4"
   29.22 - "|五| = 5"
   29.23 - "|六| = 6"
   29.24 - "|七| = 7"
   29.25 - "|八| = 8"
   29.26 - "|九| = 9"
   29.27 - "|十| = 10"
   29.28 +|"|二| = 2"
   29.29 +|"|三| = 3"
   29.30 +|"|四| = 4"
   29.31 +|"|五| = 5"
   29.32 +|"|六| = 6"
   29.33 +|"|七| = 7"
   29.34 +|"|八| = 8"
   29.35 +|"|九| = 9"
   29.36 +|"|十| = 10"
   29.37  
   29.38  thm translate.simps
   29.39  
    30.1 --- a/src/HOL/ex/Hebrew.thy	Wed Sep 08 13:25:22 2010 +0200
    30.2 +++ b/src/HOL/ex/Hebrew.thy	Wed Sep 08 19:21:46 2010 +0200
    30.3 @@ -1,5 +1,4 @@
    30.4  (* -*- coding: utf-8 -*- :encoding=utf-8:  
    30.5 -    ID:         $Id$
    30.6      Author:     Makarius
    30.7  
    30.8  Example theory involving Unicode characters (UTF-8 encoding) -- both
    30.9 @@ -43,31 +42,29 @@
   30.10  
   30.11  text {* Interpreting Hebrew letters as numbers. *}
   30.12  
   30.13 -consts
   30.14 -  mispar :: "alef_bet => nat"
   30.15 -primrec
   30.16 +primrec mispar :: "alef_bet => nat" where
   30.17    "mispar א = 1"
   30.18 -  "mispar ב = 2"
   30.19 -  "mispar ג = 3"
   30.20 -  "mispar ד = 4"
   30.21 -  "mispar ה = 5"
   30.22 -  "mispar ו = 6"
   30.23 -  "mispar ז = 7"
   30.24 -  "mispar ח = 8"
   30.25 -  "mispar ט = 9"
   30.26 -  "mispar י = 10"
   30.27 -  "mispar כ = 20"
   30.28 -  "mispar ל = 30"
   30.29 -  "mispar מ = 40"
   30.30 -  "mispar נ = 50"
   30.31 -  "mispar ס = 60"
   30.32 -  "mispar ע = 70"
   30.33 -  "mispar פ = 80"
   30.34 -  "mispar צ = 90"
   30.35 -  "mispar ק = 100"
   30.36 -  "mispar ר = 200"
   30.37 -  "mispar ש = 300"
   30.38 -  "mispar ת = 400"
   30.39 +| "mispar ב = 2"
   30.40 +| "mispar ג = 3"
   30.41 +| "mispar ד = 4"
   30.42 +| "mispar ה = 5"
   30.43 +| "mispar ו = 6"
   30.44 +| "mispar ז = 7"
   30.45 +| "mispar ח = 8"
   30.46 +| "mispar ט = 9"
   30.47 +| "mispar י = 10"
   30.48 +| "mispar כ = 20"
   30.49 +| "mispar ל = 30"
   30.50 +| "mispar מ = 40"
   30.51 +| "mispar נ = 50"
   30.52 +| "mispar ס = 60"
   30.53 +| "mispar ע = 70"
   30.54 +| "mispar פ = 80"
   30.55 +| "mispar צ = 90"
   30.56 +| "mispar ק = 100"
   30.57 +| "mispar ר = 200"
   30.58 +| "mispar ש = 300"
   30.59 +| "mispar ת = 400"
   30.60  
   30.61  thm mispar.simps
   30.62  
    31.1 --- a/src/HOL/ex/ReflectionEx.thy	Wed Sep 08 13:25:22 2010 +0200
    31.2 +++ b/src/HOL/ex/ReflectionEx.thy	Wed Sep 08 19:21:46 2010 +0200
    31.3 @@ -46,14 +46,13 @@
    31.4  
    31.5  datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
    31.6  
    31.7 -consts Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
    31.8 -primrec
    31.9 +primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool" where
   31.10    "Ifm (At n) vs = vs!n"
   31.11 -  "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
   31.12 -  "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
   31.13 -  "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
   31.14 -  "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
   31.15 -  "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
   31.16 +| "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
   31.17 +| "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
   31.18 +| "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
   31.19 +| "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
   31.20 +| "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
   31.21  
   31.22  lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
   31.23  apply (reify Ifm.simps)
   31.24 @@ -399,7 +398,7 @@
   31.25  | "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)"
   31.26  | "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)"
   31.27  | "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs"
   31.28 -consts prodmul:: "prod \<times> prod \<Rightarrow> prod"
   31.29 +
   31.30  datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   31.31    | Or sgn sgn | And sgn sgn
   31.32