--- a/src/HOL/Auth/Guard/Extensions.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Wed Sep 08 19:21:46 2010 +0200
@@ -31,10 +31,8 @@
subsubsection{*"remove l x" erase the first element of "l" equal to "x"*}
-consts remove :: "'a list => 'a => 'a list"
-
-primrec
-"remove [] y = []"
+primrec remove :: "'a list => 'a => 'a list" where
+"remove [] y = []" |
"remove (x#xs) y = (if x=y then xs else x # remove xs y)"
lemma set_remove: "set (remove l x) <= set l"
@@ -348,13 +346,9 @@
subsubsection{*knows without initState*}
-consts knows' :: "agent => event list => msg set"
-
-primrec
-knows'_Nil:
- "knows' A [] = {}"
-
-knows'_Cons0:
+primrec knows' :: "agent => event list => msg set" where
+ knows'_Nil: "knows' A [] = {}" |
+ knows'_Cons0:
"knows' A (ev # evs) = (
if A = Spy then (
case ev of
@@ -426,10 +420,8 @@
subsubsection{*maximum knowledge an agent can have
includes messages sent to the agent*}
-consts knows_max' :: "agent => event list => msg set"
-
-primrec
-knows_max'_def_Nil: "knows_max' A [] = {}"
+primrec knows_max' :: "agent => event list => msg set" where
+knows_max'_def_Nil: "knows_max' A [] = {}" |
knows_max'_def_Cons: "knows_max' A (ev # evs) = (
if A=Spy then (
case ev of
@@ -498,10 +490,8 @@
subsubsection{*used without initState*}
-consts used' :: "event list => msg set"
-
-primrec
-"used' [] = {}"
+primrec used' :: "event list => msg set" where
+"used' [] = {}" |
"used' (ev # evs) = (
case ev of
Says A B X => parts {X} Un used' evs
--- a/src/HOL/Auth/Public.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Public.thy Wed Sep 08 19:21:46 2010 +0200
@@ -199,24 +199,32 @@
knowledge of the Spy. All other agents are automata, merely following the
protocol.*}
-primrec
+term initState_Server
+
+overloading
+ initState \<equiv> initState
+begin
+
+primrec initState where
(*Agents know their private key and all public keys*)
initState_Server:
"initState Server =
{Key (priEK Server), Key (priSK Server)} \<union>
(Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)"
- initState_Friend:
+| initState_Friend:
"initState (Friend i) =
{Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union>
(Key ` range pubEK) \<union> (Key ` range pubSK)"
- initState_Spy:
+| initState_Spy:
"initState Spy =
(Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union>
(Key ` shrK ` bad) \<union>
(Key ` range pubEK) \<union> (Key ` range pubSK)"
+end
+
text{*These lemmas allow reasoning about @{term "used evs"} rather than
@{term "knows Spy evs"}, which is useful when there are private Notes.
--- a/src/HOL/Auth/Shared.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Shared.thy Wed Sep 08 19:21:46 2010 +0200
@@ -22,10 +22,17 @@
done
text{*Server knows all long-term keys; other agents know only their own*}
-primrec
+
+overloading
+ initState \<equiv> initState
+begin
+
+primrec initState where
initState_Server: "initState Server = Key ` range shrK"
- initState_Friend: "initState (Friend i) = {Key (shrK (Friend i))}"
- initState_Spy: "initState Spy = Key`shrK`bad"
+| initState_Friend: "initState (Friend i) = {Key (shrK (Friend i))}"
+| initState_Spy: "initState Spy = Key`shrK`bad"
+
+end
subsection{*Basic properties of shrK*}
--- a/src/HOL/Auth/Smartcard/EventSC.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Wed Sep 08 19:21:46 2010 +0200
@@ -19,7 +19,6 @@
consts
bad :: "agent set" (*compromised agents*)
- knows :: "agent => event list => msg set" (*agents' knowledge*)
stolen :: "card set" (* stolen smart cards *)
cloned :: "card set" (* cloned smart cards*)
secureM :: "bool"(*assumption of secure means between agents and their cards*)
@@ -50,7 +49,8 @@
primrec (*This definition is extended over the new events, subject to the
assumption of secure means*)
- knows_Nil: "knows A [] = initState A"
+ knows :: "agent => event list => msg set" (*agents' knowledge*) where
+ knows_Nil: "knows A [] = initState A" |
knows_Cons: "knows A (ev # evs) =
(case ev of
Says A' B X =>
@@ -78,13 +78,11 @@
-consts
+primrec
(*The set of items that might be visible to someone is easily extended
over the new events*)
- used :: "event list => msg set"
-
-primrec
- used_Nil: "used [] = (UN B. parts (initState B))"
+ used :: "event list => msg set" where
+ used_Nil: "used [] = (UN B. parts (initState B))" |
used_Cons: "used (ev # evs) =
(case ev of
Says A B X => parts {X} \<union> (used evs)
@@ -98,7 +96,6 @@
Likewise, @{term C_Gets} will always have to follow @{term Inputs}
and @{term A_Gets} will always have to follow @{term Outpts}*}
-
lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> used evs"
apply (induct_tac evs)
apply (auto split: event.split)
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Wed Sep 08 19:21:46 2010 +0200
@@ -51,16 +51,21 @@
text{*initState must be defined with care*}
-primrec
+
+overloading
+ initState \<equiv> initState
+begin
+
+primrec initState where
(*Server knows all long-term keys; adding cards' keys may be redundant but
helps prove crdK_in_initState and crdK_in_used to distinguish cards' keys
from fresh (session) keys*)
initState_Server: "initState Server =
(Key`(range shrK \<union> range crdK \<union> range pin \<union> range pairK)) \<union>
- (Nonce`(range Pairkey))"
+ (Nonce`(range Pairkey))" |
(*Other agents know only their own*)
- initState_Friend: "initState (Friend i) = {Key (pin (Friend i))}"
+ initState_Friend: "initState (Friend i) = {Key (pin (Friend i))}" |
(*Spy knows bad agents' pins, cloned cards' keys, pairKs, and Pairkeys *)
initState_Spy: "initState Spy =
@@ -70,6 +75,7 @@
(pairK`{(X,A). Card A \<in> cloned})))
\<union> (Nonce`(Pairkey`{(A,B). Card A \<in> cloned & Card B \<in> cloned}))"
+end
text{*Still relying on axioms*}
axioms
--- a/src/HOL/Decision_Procs/Cooper.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Sep 08 19:21:46 2010 +0200
@@ -67,27 +67,26 @@
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
-consts Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"
-primrec
+primrec Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool" where
"Ifm bbs bs T = True"
- "Ifm bbs bs F = False"
- "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
- "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
- "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
- "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
- "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
- "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
- "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
- "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
- "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
- "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
- "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
- "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
- "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
- "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
- "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
- "Ifm bbs bs (Closed n) = bbs!n"
- "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
+| "Ifm bbs bs F = False"
+| "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
+| "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
+| "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
+| "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
+| "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
+| "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
+| "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
+| "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
+| "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
+| "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
+| "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
+| "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
+| "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
+| "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
+| "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
+| "Ifm bbs bs (Closed n) = bbs!n"
+| "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
consts prep :: "fm \<Rightarrow> fm"
recdef prep "measure fmsize"
@@ -132,50 +131,47 @@
"qfree p = True"
(* Boundedness and substitution *)
-consts
- numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
- bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
- subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *)
-primrec
+
+primrec numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where
"numbound0 (C c) = True"
- "numbound0 (Bound n) = (n>0)"
- "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
- "numbound0 (Neg a) = numbound0 a"
- "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
- "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
- "numbound0 (Mul i a) = numbound0 a"
+| "numbound0 (Bound n) = (n>0)"
+| "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
+| "numbound0 (Neg a) = numbound0 a"
+| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
+| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
+| "numbound0 (Mul i a) = numbound0 a"
lemma numbound0_I:
assumes nb: "numbound0 a"
shows "Inum (b#bs) a = Inum (b'#bs) a"
using nb
-by (induct a rule: numbound0.induct) (auto simp add: gr0_conv_Suc)
+by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
-primrec
+primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
"bound0 T = True"
- "bound0 F = True"
- "bound0 (Lt a) = numbound0 a"
- "bound0 (Le a) = numbound0 a"
- "bound0 (Gt a) = numbound0 a"
- "bound0 (Ge a) = numbound0 a"
- "bound0 (Eq a) = numbound0 a"
- "bound0 (NEq a) = numbound0 a"
- "bound0 (Dvd i a) = numbound0 a"
- "bound0 (NDvd i a) = numbound0 a"
- "bound0 (NOT p) = bound0 p"
- "bound0 (And p q) = (bound0 p \<and> bound0 q)"
- "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
- "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
- "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
- "bound0 (E p) = False"
- "bound0 (A p) = False"
- "bound0 (Closed P) = True"
- "bound0 (NClosed P) = True"
+| "bound0 F = True"
+| "bound0 (Lt a) = numbound0 a"
+| "bound0 (Le a) = numbound0 a"
+| "bound0 (Gt a) = numbound0 a"
+| "bound0 (Ge a) = numbound0 a"
+| "bound0 (Eq a) = numbound0 a"
+| "bound0 (NEq a) = numbound0 a"
+| "bound0 (Dvd i a) = numbound0 a"
+| "bound0 (NDvd i a) = numbound0 a"
+| "bound0 (NOT p) = bound0 p"
+| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
+| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (E p) = False"
+| "bound0 (A p) = False"
+| "bound0 (Closed P) = True"
+| "bound0 (NClosed P) = True"
lemma bound0_I:
assumes bp: "bound0 p"
shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
-by (induct p rule: bound0.induct) (auto simp add: gr0_conv_Suc)
+by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
fun numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
"numsubst0 t (C c) = (C c)"
@@ -195,24 +191,24 @@
"numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
by (induct t rule: numsubst0.induct, auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
-primrec
+primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
"subst0 t T = T"
- "subst0 t F = F"
- "subst0 t (Lt a) = Lt (numsubst0 t a)"
- "subst0 t (Le a) = Le (numsubst0 t a)"
- "subst0 t (Gt a) = Gt (numsubst0 t a)"
- "subst0 t (Ge a) = Ge (numsubst0 t a)"
- "subst0 t (Eq a) = Eq (numsubst0 t a)"
- "subst0 t (NEq a) = NEq (numsubst0 t a)"
- "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
- "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
- "subst0 t (NOT p) = NOT (subst0 t p)"
- "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
- "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
- "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
- "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
- "subst0 t (Closed P) = (Closed P)"
- "subst0 t (NClosed P) = (NClosed P)"
+| "subst0 t F = F"
+| "subst0 t (Lt a) = Lt (numsubst0 t a)"
+| "subst0 t (Le a) = Le (numsubst0 t a)"
+| "subst0 t (Gt a) = Gt (numsubst0 t a)"
+| "subst0 t (Ge a) = Ge (numsubst0 t a)"
+| "subst0 t (Eq a) = Eq (numsubst0 t a)"
+| "subst0 t (NEq a) = NEq (numsubst0 t a)"
+| "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
+| "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
+| "subst0 t (NOT p) = NOT (subst0 t p)"
+| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
+| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
+| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
+| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
+| "subst0 t (Closed P) = (Closed P)"
+| "subst0 t (NClosed P) = (NClosed P)"
lemma subst0_I: assumes qfp: "qfree p"
shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p"
@@ -280,14 +276,14 @@
lemma numsubst0_numbound0: assumes nb: "numbound0 t"
shows "numbound0 (numsubst0 t a)"
-using nb apply (induct a rule: numbound0.induct)
+using nb apply (induct a)
apply simp_all
-apply (case_tac n, simp_all)
+apply (case_tac nat, simp_all)
done
lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"
shows "bound0 (subst0 t p)"
-using qf numsubst0_numbound0[OF nb] by (induct p rule: subst0.induct, auto)
+using qf numsubst0_numbound0[OF nb] by (induct p) auto
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
by (induct p, simp_all)
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Sep 08 19:21:46 2010 +0200
@@ -16,26 +16,24 @@
| Neg tm | Sub tm tm | CNP nat poly tm
(* A size for poly to make inductive proofs simpler*)
-consts tmsize :: "tm \<Rightarrow> nat"
-primrec
+primrec tmsize :: "tm \<Rightarrow> nat" where
"tmsize (CP c) = polysize c"
- "tmsize (Bound n) = 1"
- "tmsize (Neg a) = 1 + tmsize a"
- "tmsize (Add a b) = 1 + tmsize a + tmsize b"
- "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
- "tmsize (Mul c a) = 1 + polysize c + tmsize a"
- "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
+| "tmsize (Bound n) = 1"
+| "tmsize (Neg a) = 1 + tmsize a"
+| "tmsize (Add a b) = 1 + tmsize a + tmsize b"
+| "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
+| "tmsize (Mul c a) = 1 + polysize c + tmsize a"
+| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
(* Semantics of terms tm *)
-consts Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
-primrec
+primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" where
"Itm vs bs (CP c) = (Ipoly vs c)"
- "Itm vs bs (Bound n) = bs!n"
- "Itm vs bs (Neg a) = -(Itm vs bs a)"
- "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
- "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
- "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
- "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"
+| "Itm vs bs (Bound n) = bs!n"
+| "Itm vs bs (Neg a) = -(Itm vs bs a)"
+| "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
+| "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
+| "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
+| "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"
fun allpolys:: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool" where
@@ -47,51 +45,48 @@
| "allpolys P (Sub p q) = (allpolys P p \<and> allpolys P q)"
| "allpolys P p = True"
-consts
- tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool"
- tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *)
- tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *)
- incrtm0:: "tm \<Rightarrow> tm"
- incrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm"
- decrtm0:: "tm \<Rightarrow> tm"
- decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm"
-primrec
+primrec tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool" where
"tmboundslt n (CP c) = True"
- "tmboundslt n (Bound m) = (m < n)"
- "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
- "tmboundslt n (Neg a) = tmboundslt n a"
- "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
- "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)"
- "tmboundslt n (Mul i a) = tmboundslt n a"
-primrec
+| "tmboundslt n (Bound m) = (m < n)"
+| "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
+| "tmboundslt n (Neg a) = tmboundslt n a"
+| "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
+| "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)"
+| "tmboundslt n (Mul i a) = tmboundslt n a"
+
+primrec tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *) where
"tmbound0 (CP c) = True"
- "tmbound0 (Bound n) = (n>0)"
- "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
- "tmbound0 (Neg a) = tmbound0 a"
- "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
- "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)"
- "tmbound0 (Mul i a) = tmbound0 a"
+| "tmbound0 (Bound n) = (n>0)"
+| "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
+| "tmbound0 (Neg a) = tmbound0 a"
+| "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
+| "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)"
+| "tmbound0 (Mul i a) = tmbound0 a"
lemma tmbound0_I:
assumes nb: "tmbound0 a"
shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
using nb
-by (induct a rule: tmbound0.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto simp add: nth_pos2)
-primrec
+primrec tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) where
"tmbound n (CP c) = True"
- "tmbound n (Bound m) = (n \<noteq> m)"
- "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
- "tmbound n (Neg a) = tmbound n a"
- "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
- "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)"
- "tmbound n (Mul i a) = tmbound n a"
+| "tmbound n (Bound m) = (n \<noteq> m)"
+| "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
+| "tmbound n (Neg a) = tmbound n a"
+| "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
+| "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)"
+| "tmbound n (Mul i a) = tmbound n a"
lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t" by (induct t, auto)
lemma tmbound_I:
assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound n t" and le: "n \<le> length bs"
shows "Itm vs (bs[n:=x]) t = Itm vs bs t"
using nb le bnd
- by (induct t rule: tmbound.induct , auto)
+ by (induct t rule: tm.induct , auto)
+
+consts
+ incrtm0:: "tm \<Rightarrow> tm"
+ decrtm0:: "tm \<Rightarrow> tm"
recdef decrtm0 "measure size"
"decrtm0 (Bound n) = Bound (n - 1)"
@@ -101,6 +96,7 @@
"decrtm0 (Mul c a) = Mul c (decrtm0 a)"
"decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
"decrtm0 a = a"
+
recdef incrtm0 "measure size"
"incrtm0 (Bound n) = Bound (n + 1)"
"incrtm0 (Neg a) = Neg (incrtm0 a)"
@@ -109,25 +105,26 @@
"incrtm0 (Mul c a) = Mul c (incrtm0 a)"
"incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
"incrtm0 a = a"
+
lemma decrtm0: assumes nb: "tmbound0 t"
shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
using nb by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
+
lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
-primrec
+primrec decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" where
"decrtm m (CP c) = (CP c)"
- "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
- "decrtm m (Neg a) = Neg (decrtm m a)"
- "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
- "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
- "decrtm m (Mul c a) = Mul c (decrtm m a)"
- "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
+| "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
+| "decrtm m (Neg a) = Neg (decrtm m a)"
+| "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
+| "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
+| "decrtm m (Mul c a) = Mul c (decrtm m a)"
+| "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
-consts removen:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-primrec
+primrec removen:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"removen n [] = []"
- "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
+| "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
lemma removen_same: "n \<ge> length xs \<Longrightarrow> removen n xs = xs"
by (induct xs arbitrary: n, auto)
@@ -172,50 +169,47 @@
and nle: "m \<le> length bs"
shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
using bnd nb nle
- by (induct t rule: decrtm.induct, auto simp add: removen_nth)
+ by (induct t rule: tm.induct, auto simp add: removen_nth)
-consts tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm"
-primrec
+primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where
"tmsubst0 t (CP c) = CP c"
- "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
- "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
- "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
- "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
- "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)"
- "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
+| "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
+| "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
+| "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
+| "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
+| "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)"
+| "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
lemma tmsubst0:
shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
-by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto simp add: nth_pos2)
lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
-by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto simp add: nth_pos2)
-consts tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm"
-
-primrec
+primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
"tmsubst n t (CP c) = CP c"
- "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
- "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a)
+| "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
+| "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a)
else CNP m c (tmsubst n t a))"
- "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
- "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
- "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)"
- "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
+| "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
+| "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
+| "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)"
+| "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
lemma tmsubst: assumes nb: "tmboundslt (length bs) a" and nlt: "n \<le> length bs"
shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
using nb nlt
-by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto simp add: nth_pos2)
lemma tmsubst_nb0: assumes tnb: "tmbound0 t"
shows "tmbound0 (tmsubst 0 t a)"
using tnb
-by (induct a rule: tmsubst.induct, auto)
+by (induct a rule: tm.induct, auto)
lemma tmsubst_nb: assumes tnb: "tmbound m t"
shows "tmbound m (tmsubst m t a)"
using tnb
-by (induct a rule: tmsubst.induct, auto)
+by (induct a rule: tm.induct, auto)
lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"
by (induct t, auto)
(* Simplification *)
@@ -447,21 +441,20 @@
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
-consts Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
-primrec
+primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" where
"Ifm vs bs T = True"
- "Ifm vs bs F = False"
- "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
- "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
- "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
- "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
- "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
- "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
- "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
- "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
- "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
- "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
- "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
+| "Ifm vs bs F = False"
+| "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
+| "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
+| "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
+| "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
+| "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
+| "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
+| "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
+| "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
+| "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
+| "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
+| "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
consts not:: "fm \<Rightarrow> fm"
recdef not "measure size"
@@ -516,27 +509,24 @@
(* Boundedness and substitution *)
-consts boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool"
-primrec
+primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool" where
"boundslt n T = True"
- "boundslt n F = True"
- "boundslt n (Lt t) = (tmboundslt n t)"
- "boundslt n (Le t) = (tmboundslt n t)"
- "boundslt n (Eq t) = (tmboundslt n t)"
- "boundslt n (NEq t) = (tmboundslt n t)"
- "boundslt n (NOT p) = boundslt n p"
- "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
- "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
- "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
- "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
- "boundslt n (E p) = boundslt (Suc n) p"
- "boundslt n (A p) = boundslt (Suc n) p"
+| "boundslt n F = True"
+| "boundslt n (Lt t) = (tmboundslt n t)"
+| "boundslt n (Le t) = (tmboundslt n t)"
+| "boundslt n (Eq t) = (tmboundslt n t)"
+| "boundslt n (NEq t) = (tmboundslt n t)"
+| "boundslt n (NOT p) = boundslt n p"
+| "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
+| "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
+| "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
+| "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
+| "boundslt n (E p) = boundslt (Suc n) p"
+| "boundslt n (A p) = boundslt (Suc n) p"
consts
bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
- bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *)
decr0 :: "fm \<Rightarrow> fm"
- decr :: "nat \<Rightarrow> fm \<Rightarrow> fm"
recdef bound0 "measure size"
"bound0 T = True"
"bound0 F = True"
@@ -556,26 +546,26 @@
using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
by (induct p rule: bound0.induct,auto simp add: nth_pos2)
-primrec
+primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *) where
"bound m T = True"
- "bound m F = True"
- "bound m (Lt t) = tmbound m t"
- "bound m (Le t) = tmbound m t"
- "bound m (Eq t) = tmbound m t"
- "bound m (NEq t) = tmbound m t"
- "bound m (NOT p) = bound m p"
- "bound m (And p q) = (bound m p \<and> bound m q)"
- "bound m (Or p q) = (bound m p \<and> bound m q)"
- "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
- "bound m (Iff p q) = (bound m p \<and> bound m q)"
- "bound m (E p) = bound (Suc m) p"
- "bound m (A p) = bound (Suc m) p"
+| "bound m F = True"
+| "bound m (Lt t) = tmbound m t"
+| "bound m (Le t) = tmbound m t"
+| "bound m (Eq t) = tmbound m t"
+| "bound m (NEq t) = tmbound m t"
+| "bound m (NOT p) = bound m p"
+| "bound m (And p q) = (bound m p \<and> bound m q)"
+| "bound m (Or p q) = (bound m p \<and> bound m q)"
+| "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
+| "bound m (Iff p q) = (bound m p \<and> bound m q)"
+| "bound m (E p) = bound (Suc m) p"
+| "bound m (A p) = bound (Suc m) p"
lemma bound_I:
assumes bnd: "boundslt (length bs) p" and nb: "bound n p" and le: "n \<le> length bs"
shows "Ifm vs (bs[n:=x]) p = Ifm vs bs p"
using bnd nb le tmbound_I[where bs=bs and vs = vs]
-proof(induct p arbitrary: bs n rule: bound.induct)
+proof(induct p arbitrary: bs n rule: fm.induct)
case (E p bs n)
{fix y
from prems have bnd: "boundslt (length (y#bs)) p"
@@ -607,26 +597,26 @@
using nb
by (induct p rule: decr0.induct, simp_all add: decrtm0)
-primrec
+primrec decr :: "nat \<Rightarrow> fm \<Rightarrow> fm" where
"decr m T = T"
- "decr m F = F"
- "decr m (Lt t) = (Lt (decrtm m t))"
- "decr m (Le t) = (Le (decrtm m t))"
- "decr m (Eq t) = (Eq (decrtm m t))"
- "decr m (NEq t) = (NEq (decrtm m t))"
- "decr m (NOT p) = NOT (decr m p)"
- "decr m (And p q) = conj (decr m p) (decr m q)"
- "decr m (Or p q) = disj (decr m p) (decr m q)"
- "decr m (Imp p q) = imp (decr m p) (decr m q)"
- "decr m (Iff p q) = iff (decr m p) (decr m q)"
- "decr m (E p) = E (decr (Suc m) p)"
- "decr m (A p) = A (decr (Suc m) p)"
+| "decr m F = F"
+| "decr m (Lt t) = (Lt (decrtm m t))"
+| "decr m (Le t) = (Le (decrtm m t))"
+| "decr m (Eq t) = (Eq (decrtm m t))"
+| "decr m (NEq t) = (NEq (decrtm m t))"
+| "decr m (NOT p) = NOT (decr m p)"
+| "decr m (And p q) = conj (decr m p) (decr m q)"
+| "decr m (Or p q) = disj (decr m p) (decr m q)"
+| "decr m (Imp p q) = imp (decr m p) (decr m q)"
+| "decr m (Iff p q) = iff (decr m p) (decr m q)"
+| "decr m (E p) = E (decr (Suc m) p)"
+| "decr m (A p) = A (decr (Suc m) p)"
lemma decr: assumes bnd: "boundslt (length bs) p" and nb: "bound m p"
and nle: "m < length bs"
shows "Ifm vs (removen m bs) (decr m p) = Ifm vs bs p"
using bnd nb nle
-proof(induct p arbitrary: bs m rule: decr.induct)
+proof(induct p arbitrary: bs m rule: fm.induct)
case (E p bs m)
{fix x
from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p"
@@ -642,55 +632,51 @@
} thus ?case by auto
qed (auto simp add: decrtm removen_nth)
-consts
- subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm"
-
-primrec
+primrec subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm" where
"subst0 t T = T"
- "subst0 t F = F"
- "subst0 t (Lt a) = Lt (tmsubst0 t a)"
- "subst0 t (Le a) = Le (tmsubst0 t a)"
- "subst0 t (Eq a) = Eq (tmsubst0 t a)"
- "subst0 t (NEq a) = NEq (tmsubst0 t a)"
- "subst0 t (NOT p) = NOT (subst0 t p)"
- "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
- "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
- "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
- "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
- "subst0 t (E p) = E p"
- "subst0 t (A p) = A p"
+| "subst0 t F = F"
+| "subst0 t (Lt a) = Lt (tmsubst0 t a)"
+| "subst0 t (Le a) = Le (tmsubst0 t a)"
+| "subst0 t (Eq a) = Eq (tmsubst0 t a)"
+| "subst0 t (NEq a) = NEq (tmsubst0 t a)"
+| "subst0 t (NOT p) = NOT (subst0 t p)"
+| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
+| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
+| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
+| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
+| "subst0 t (E p) = E p"
+| "subst0 t (A p) = A p"
lemma subst0: assumes qf: "qfree p"
shows "Ifm vs (x#bs) (subst0 t p) = Ifm vs ((Itm vs (x#bs) t)#bs) p"
using qf tmsubst0[where x="x" and bs="bs" and t="t"]
-by (induct p rule: subst0.induct, auto)
+by (induct p rule: fm.induct, auto)
lemma subst0_nb:
assumes bp: "tmbound0 t" and qf: "qfree p"
shows "bound0 (subst0 t p)"
using qf tmsubst0_nb[OF bp] bp
-by (induct p rule: subst0.induct, auto)
+by (induct p rule: fm.induct, auto)
-consts subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm"
-primrec
+primrec subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" where
"subst n t T = T"
- "subst n t F = F"
- "subst n t (Lt a) = Lt (tmsubst n t a)"
- "subst n t (Le a) = Le (tmsubst n t a)"
- "subst n t (Eq a) = Eq (tmsubst n t a)"
- "subst n t (NEq a) = NEq (tmsubst n t a)"
- "subst n t (NOT p) = NOT (subst n t p)"
- "subst n t (And p q) = And (subst n t p) (subst n t q)"
- "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
- "subst n t (Imp p q) = Imp (subst n t p) (subst n t q)"
- "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
- "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
- "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
+| "subst n t F = F"
+| "subst n t (Lt a) = Lt (tmsubst n t a)"
+| "subst n t (Le a) = Le (tmsubst n t a)"
+| "subst n t (Eq a) = Eq (tmsubst n t a)"
+| "subst n t (NEq a) = NEq (tmsubst n t a)"
+| "subst n t (NOT p) = NOT (subst n t p)"
+| "subst n t (And p q) = And (subst n t p) (subst n t q)"
+| "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
+| "subst n t (Imp p q) = Imp (subst n t p) (subst n t q)"
+| "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
+| "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
+| "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
lemma subst: assumes nb: "boundslt (length bs) p" and nlm: "n \<le> length bs"
shows "Ifm vs bs (subst n t p) = Ifm vs (bs[n:= Itm vs bs t]) p"
using nb nlm
-proof (induct p arbitrary: bs n t rule: subst0.induct)
+proof (induct p arbitrary: bs n t rule: fm.induct)
case (E p bs n)
{fix x
from prems have bn: "boundslt (length (x#bs)) p" by simp
@@ -713,7 +699,7 @@
lemma subst_nb: assumes tnb: "tmbound m t"
shows "bound m (subst m t p)"
using tnb tmsubst_nb incrtm0_tmbound
-by (induct p arbitrary: m t rule: subst.induct, auto)
+by (induct p arbitrary: m t rule: fm.induct, auto)
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
by (induct p rule: not.induct, auto)
@@ -2475,10 +2461,9 @@
text {* Rest of the implementation *}
-consts alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list"
-primrec
+primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
"alluopairs [] = []"
- "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
+| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
by (induct xs, auto)
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Wed Sep 08 19:21:46 2010 +0200
@@ -10,60 +10,52 @@
text{* Application of polynomial as a real function. *}
-consts poly :: "'a list => 'a => ('a::{comm_ring})"
-primrec
+primrec poly :: "'a list => 'a => ('a::{comm_ring})" where
poly_Nil: "poly [] x = 0"
- poly_Cons: "poly (h#t) x = h + x * poly t x"
+| poly_Cons: "poly (h#t) x = h + x * poly t x"
subsection{*Arithmetic Operations on Polynomials*}
text{*addition*}
-consts padd :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "+++" 65)
-primrec
+primrec padd :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "+++" 65) where
padd_Nil: "[] +++ l2 = l2"
- padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
+| padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
else (h + hd l2)#(t +++ tl l2))"
text{*Multiplication by a constant*}
-consts cmult :: "['a :: comm_ring_1, 'a list] => 'a list" (infixl "%*" 70)
-primrec
- cmult_Nil: "c %* [] = []"
- cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
+primrec cmult :: "['a :: comm_ring_1, 'a list] => 'a list" (infixl "%*" 70) where
+ cmult_Nil: "c %* [] = []"
+| cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
text{*Multiplication by a polynomial*}
-consts pmult :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "***" 70)
-primrec
- pmult_Nil: "[] *** l2 = []"
- pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
+primrec pmult :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "***" 70) where
+ pmult_Nil: "[] *** l2 = []"
+| pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
else (h %* l2) +++ ((0) # (t *** l2)))"
text{*Repeated multiplication by a polynomial*}
-consts mulexp :: "[nat, 'a list, 'a list] => ('a ::comm_ring_1) list"
-primrec
- mulexp_zero: "mulexp 0 p q = q"
- mulexp_Suc: "mulexp (Suc n) p q = p *** mulexp n p q"
+primrec mulexp :: "[nat, 'a list, 'a list] => ('a ::comm_ring_1) list" where
+ mulexp_zero: "mulexp 0 p q = q"
+| mulexp_Suc: "mulexp (Suc n) p q = p *** mulexp n p q"
text{*Exponential*}
-consts pexp :: "['a list, nat] => ('a::comm_ring_1) list" (infixl "%^" 80)
-primrec
- pexp_0: "p %^ 0 = [1]"
- pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
+primrec pexp :: "['a list, nat] => ('a::comm_ring_1) list" (infixl "%^" 80) where
+ pexp_0: "p %^ 0 = [1]"
+| pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
text{*Quotient related value of dividing a polynomial by x + a*}
(* Useful for divisor properties in inductive proofs *)
-consts "pquot" :: "['a list, 'a::field] => 'a list"
-primrec
- pquot_Nil: "pquot [] a= []"
- pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
+primrec pquot :: "['a list, 'a::field] => 'a list" where
+ pquot_Nil: "pquot [] a= []"
+| pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
text{*normalization of polynomials (remove extra 0 coeff)*}
-consts pnormalize :: "('a::comm_ring_1) list => 'a list"
-primrec
- pnormalize_Nil: "pnormalize [] = []"
- pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
+primrec pnormalize :: "('a::comm_ring_1) list => 'a list" where
+ pnormalize_Nil: "pnormalize [] = []"
+| pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
then (if (h = 0) then [] else [h])
else (h#(pnormalize p)))"
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Sep 08 19:21:46 2010 +0200
@@ -19,38 +19,35 @@
abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
subsection{* Boundedness, substitution and all that *}
-consts polysize:: "poly \<Rightarrow> nat"
-primrec
+primrec polysize:: "poly \<Rightarrow> nat" where
"polysize (C c) = 1"
- "polysize (Bound n) = 1"
- "polysize (Neg p) = 1 + polysize p"
- "polysize (Add p q) = 1 + polysize p + polysize q"
- "polysize (Sub p q) = 1 + polysize p + polysize q"
- "polysize (Mul p q) = 1 + polysize p + polysize q"
- "polysize (Pw p n) = 1 + polysize p"
- "polysize (CN c n p) = 4 + polysize c + polysize p"
+| "polysize (Bound n) = 1"
+| "polysize (Neg p) = 1 + polysize p"
+| "polysize (Add p q) = 1 + polysize p + polysize q"
+| "polysize (Sub p q) = 1 + polysize p + polysize q"
+| "polysize (Mul p q) = 1 + polysize p + polysize q"
+| "polysize (Pw p n) = 1 + polysize p"
+| "polysize (CN c n p) = 4 + polysize c + polysize p"
-consts
- polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *)
- polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *)
-primrec
+primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where
"polybound0 (C c) = True"
- "polybound0 (Bound n) = (n>0)"
- "polybound0 (Neg a) = polybound0 a"
- "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
- "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)"
- "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
- "polybound0 (Pw p n) = (polybound0 p)"
- "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
-primrec
+| "polybound0 (Bound n) = (n>0)"
+| "polybound0 (Neg a) = polybound0 a"
+| "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
+| "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)"
+| "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
+| "polybound0 (Pw p n) = (polybound0 p)"
+| "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
+
+primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) where
"polysubst0 t (C c) = (C c)"
- "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
- "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
- "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
- "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"
- "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
- "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
- "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
+| "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
+| "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
+| "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
+| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"
+| "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
+| "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
+| "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
else CN (polysubst0 t c) n (polysubst0 t p))"
consts
@@ -195,11 +192,10 @@
definition shift1 :: "poly \<Rightarrow> poly" where
"shift1 p \<equiv> CN 0\<^sub>p 0 p"
-consts funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
-primrec
- "funpow 0 f x = x"
- "funpow (Suc n) f x = funpow n f (f x)"
+abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
+ "funpow \<equiv> compow"
+
function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)"
where
"polydivide_aux (a,n,p,k,s) =
@@ -211,7 +207,6 @@
else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
by pat_completeness auto
-
definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
"polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)"
@@ -230,16 +225,16 @@
subsection{* Semantics of the polynomial representation *}
-consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}"
-primrec
+primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
"Ipoly bs (C c) = INum c"
- "Ipoly bs (Bound n) = bs!n"
- "Ipoly bs (Neg a) = - Ipoly bs a"
- "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
- "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
- "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
- "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
- "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
+| "Ipoly bs (Bound n) = bs!n"
+| "Ipoly bs (Neg a) = - Ipoly bs a"
+| "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
+| "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
+| "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
+| "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
+| "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
+
abbreviation
Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
@@ -729,7 +724,7 @@
by (simp add: shift1_def)
lemma funpow_shift1_isnpoly:
"\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)"
- by (induct n arbitrary: p, auto simp add: shift1_isnpoly)
+ by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
lemma funpow_isnpolyh:
assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n"
@@ -767,7 +762,7 @@
subsection{* Miscilanious lemmas about indexes, decrementation, substitution etc ... *}
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
-proof(induct p arbitrary: n rule: polybound0.induct, auto)
+proof(induct p arbitrary: n rule: poly.induct, auto)
case (goal1 c n p n')
hence "n = Suc (n - 1)" by simp
hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp
@@ -793,7 +788,7 @@
assumes nb: "polybound0 a"
shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
using nb
-by (induct a rule: polybound0.induct) auto
+by (induct a rule: poly.induct) auto
lemma polysubst0_I:
shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
by (induct t) simp_all
@@ -809,12 +804,12 @@
lemma polysubst0_polybound0: assumes nb: "polybound0 t"
shows "polybound0 (polysubst0 t a)"
-using nb by (induct a rule: polysubst0.induct, auto)
+using nb by (induct a rule: poly.induct, auto)
lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)
-fun maxindex :: "poly \<Rightarrow> nat" where
+primrec maxindex :: "poly \<Rightarrow> nat" where
"maxindex (Bound n) = n + 1"
| "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))"
| "maxindex (Add p q) = max (maxindex p) (maxindex q)"
@@ -1183,7 +1178,7 @@
case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
and "head (shift1 p) = head p" by (simp_all add: shift1_head)
- thus ?case by simp
+ thus ?case by (simp add: funpow_swap1)
qed auto
lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
@@ -1641,8 +1636,8 @@
lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
unfolding pnormal_def
- apply (induct p rule: pnormalize.induct, simp_all)
- apply (case_tac "p=[]", simp_all)
+ apply (induct p)
+ apply (simp_all, case_tac "p=[]", simp_all)
done
lemma degree_degree: assumes inc: "isnonconstant p"
@@ -1668,16 +1663,15 @@
qed
section{* Swaps ; Division by a certain variable *}
-consts swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
-primrec
+primrec swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where
"swap n m (C x) = C x"
- "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
- "swap n m (Neg t) = Neg (swap n m t)"
- "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
- "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
- "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
- "swap n m (Pw t k) = Pw (swap n m t) k"
- "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)
+| "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
+| "swap n m (Neg t) = Neg (swap n m t)"
+| "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
+| "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
+| "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
+| "swap n m (Pw t k) = Pw (swap n m t) k"
+| "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)
(swap n m p)"
lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs"
--- a/src/HOL/Hoare_Parallel/OG_Com.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy Wed Sep 08 19:21:46 2010 +0200
@@ -32,24 +32,21 @@
text {* The function @{text pre} extracts the precondition of an
annotated command: *}
-consts
- pre ::"'a ann_com \<Rightarrow> 'a assn"
-primrec
+primrec pre ::"'a ann_com \<Rightarrow> 'a assn" where
"pre (AnnBasic r f) = r"
- "pre (AnnSeq c1 c2) = pre c1"
- "pre (AnnCond1 r b c1 c2) = r"
- "pre (AnnCond2 r b c) = r"
- "pre (AnnWhile r b i c) = r"
- "pre (AnnAwait r b c) = r"
+| "pre (AnnSeq c1 c2) = pre c1"
+| "pre (AnnCond1 r b c1 c2) = r"
+| "pre (AnnCond2 r b c) = r"
+| "pre (AnnWhile r b i c) = r"
+| "pre (AnnAwait r b c) = r"
text {* Well-formedness predicate for atomic programs: *}
-consts atom_com :: "'a com \<Rightarrow> bool"
-primrec
+primrec atom_com :: "'a com \<Rightarrow> bool" where
"atom_com (Parallel Ts) = False"
- "atom_com (Basic f) = True"
- "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
- "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
- "atom_com (While b i c) = atom_com c"
+| "atom_com (Basic f) = True"
+| "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
+| "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
+| "atom_com (While b i c) = atom_com c"
end
\ No newline at end of file
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Sep 08 19:21:46 2010 +0200
@@ -3,29 +3,27 @@
theory OG_Hoare imports OG_Tran begin
-consts assertions :: "'a ann_com \<Rightarrow> ('a assn) set"
-primrec
+primrec assertions :: "'a ann_com \<Rightarrow> ('a assn) set" where
"assertions (AnnBasic r f) = {r}"
- "assertions (AnnSeq c1 c2) = assertions c1 \<union> assertions c2"
- "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2"
- "assertions (AnnCond2 r b c) = {r} \<union> assertions c"
- "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c"
- "assertions (AnnAwait r b c) = {r}"
+| "assertions (AnnSeq c1 c2) = assertions c1 \<union> assertions c2"
+| "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2"
+| "assertions (AnnCond2 r b c) = {r} \<union> assertions c"
+| "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c"
+| "assertions (AnnAwait r b c) = {r}"
-consts atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set"
-primrec
+primrec atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set" where
"atomics (AnnBasic r f) = {(r, Basic f)}"
- "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2"
- "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2"
- "atomics (AnnCond2 r b c) = atomics c"
- "atomics (AnnWhile r b i c) = atomics c"
- "atomics (AnnAwait r b c) = {(r \<inter> b, c)}"
+| "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2"
+| "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2"
+| "atomics (AnnCond2 r b c) = atomics c"
+| "atomics (AnnWhile r b i c) = atomics c"
+| "atomics (AnnAwait r b c) = {(r \<inter> b, c)}"
-consts com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op"
-primrec "com (c, q) = c"
+primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
+ "com (c, q) = c"
-consts post :: "'a ann_triple_op \<Rightarrow> 'a assn"
-primrec "post (c, q) = q"
+primrec post :: "'a ann_triple_op \<Rightarrow> 'a assn" where
+ "post (c, q) = q"
definition interfree_aux :: "('a ann_com_op \<times> 'a assn \<times> 'a ann_com_op) \<Rightarrow> bool" where
"interfree_aux \<equiv> \<lambda>(co, q, co'). co'= None \<or>
@@ -466,4 +464,4 @@
apply(auto simp add: SEM_def sem_def)
done
-end
\ No newline at end of file
+end
--- a/src/HOL/IMP/Compiler0.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/IMP/Compiler0.thy Wed Sep 08 19:21:46 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/IMP/Compiler.thy
- ID: $Id$
Author: Tobias Nipkow, TUM
Copyright 1996 TUM
@@ -49,14 +48,13 @@
subsection "The compiler"
-consts compile :: "com \<Rightarrow> instr list"
-primrec
-"compile \<SKIP> = []"
-"compile (x:==a) = [ASIN x a]"
-"compile (c1;c2) = compile c1 @ compile c2"
+primrec compile :: "com \<Rightarrow> instr list" where
+"compile \<SKIP> = []" |
+"compile (x:==a) = [ASIN x a]" |
+"compile (c1;c2) = compile c1 @ compile c2" |
"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
[JMPF b (length(compile c1) + 2)] @ compile c1 @
- [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
+ [JMPF (%x. False) (length(compile c2)+1)] @ compile c2" |
"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
[JMPB (length(compile c)+1)]"
--- a/src/HOL/Import/HOL4Compat.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Wed Sep 08 19:21:46 2010 +0200
@@ -33,17 +33,13 @@
(*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
by simp*)
-consts
- ISL :: "'a + 'b => bool"
- ISR :: "'a + 'b => bool"
-
-primrec ISL_def:
+primrec ISL :: "'a + 'b => bool" where
"ISL (Inl x) = True"
- "ISL (Inr x) = False"
+| "ISL (Inr x) = False"
-primrec ISR_def:
+primrec ISR :: "'a + 'b => bool" where
"ISR (Inl x) = False"
- "ISR (Inr x) = True"
+| "ISR (Inr x) = True"
lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))"
by simp
@@ -51,14 +47,10 @@
lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))"
by simp
-consts
- OUTL :: "'a + 'b => 'a"
- OUTR :: "'a + 'b => 'b"
-
-primrec OUTL_def:
+primrec OUTL :: "'a + 'b => 'a" where
"OUTL (Inl x) = x"
-primrec OUTR_def:
+primrec OUTR :: "'a + 'b => 'b" where
"OUTR (Inr x) = x"
lemma OUTL: "OUTL (Inl x) = x"
@@ -79,17 +71,13 @@
lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
by simp
-consts
- IS_SOME :: "'a option => bool"
- IS_NONE :: "'a option => bool"
-
-primrec IS_SOME_def:
+primrec IS_SOME :: "'a option => bool" where
"IS_SOME (Some x) = True"
- "IS_SOME None = False"
+| "IS_SOME None = False"
-primrec IS_NONE_def:
+primrec IS_NONE :: "'a option => bool" where
"IS_NONE (Some x) = False"
- "IS_NONE None = True"
+| "IS_NONE None = True"
lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)"
by simp
@@ -97,15 +85,12 @@
lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)"
by simp
-consts
- OPTION_JOIN :: "'a option option => 'a option"
-
-primrec OPTION_JOIN_def:
+primrec OPTION_JOIN :: "'a option option => 'a option" where
"OPTION_JOIN None = None"
- "OPTION_JOIN (Some x) = x"
+| "OPTION_JOIN (Some x) = x"
lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)"
- by simp;
+ by simp
lemma PAIR: "(fst x,snd x) = x"
by simp
@@ -261,14 +246,11 @@
lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
by simp
-consts
- list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat"
+primrec list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
+ "list_size f [] = 0"
+| "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
-primrec
- "list_size f [] = 0"
- "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
-
-lemma list_size_def: "(!f. list_size f [] = 0) &
+lemma list_size_def': "(!f. list_size f [] = 0) &
(!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
by simp
@@ -377,12 +359,9 @@
lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
by simp
-consts
- map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list"
-
-primrec
+primrec map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list" where
map2_Nil: "map2 f [] l2 = []"
- map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
+| map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)"
by simp
@@ -419,12 +398,9 @@
lemma [hol4rew]: "ZIP (a,b) = zip a b"
by (simp add: ZIP_def)
-consts
- unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list"
-
-primrec
+primrec unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list" where
unzip_Nil: "unzip [] = ([],[])"
- unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
+| unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
lemma UNZIP: "(unzip [] = ([],[])) &
(!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"
--- a/src/HOL/Induct/ABexp.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Induct/ABexp.thy Wed Sep 08 19:21:46 2010 +0200
@@ -20,38 +20,32 @@
text {* \medskip Evaluation of arithmetic and boolean expressions *}
-consts
- evala :: "('a => nat) => 'a aexp => nat"
- evalb :: "('a => nat) => 'a bexp => bool"
-
-primrec
+primrec evala :: "('a => nat) => 'a aexp => nat"
+ and evalb :: "('a => nat) => 'a bexp => bool" where
"evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
- "evala env (Sum a1 a2) = evala env a1 + evala env a2"
- "evala env (Diff a1 a2) = evala env a1 - evala env a2"
- "evala env (Var v) = env v"
- "evala env (Num n) = n"
+| "evala env (Sum a1 a2) = evala env a1 + evala env a2"
+| "evala env (Diff a1 a2) = evala env a1 - evala env a2"
+| "evala env (Var v) = env v"
+| "evala env (Num n) = n"
- "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
- "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
- "evalb env (Neg b) = (\<not> evalb env b)"
+| "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
+| "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
+| "evalb env (Neg b) = (\<not> evalb env b)"
text {* \medskip Substitution on arithmetic and boolean expressions *}
-consts
- substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
- substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
-
-primrec
+primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
+ and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" where
"substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
- "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
- "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
- "substa f (Var v) = f v"
- "substa f (Num n) = Num n"
+| "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
+| "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
+| "substa f (Var v) = f v"
+| "substa f (Num n) = Num n"
- "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
- "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
- "substb f (Neg b) = Neg (substb f b)"
+| "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
+| "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
+| "substb f (Neg b) = Neg (substb f b)"
lemma subst1_aexp:
"evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
--- a/src/HOL/Induct/Ordinals.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Induct/Ordinals.thy Wed Sep 08 19:21:46 2010 +0200
@@ -17,18 +17,13 @@
| Succ ordinal
| Limit "nat => ordinal"
-consts
- pred :: "ordinal => nat => ordinal option"
-primrec
+primrec pred :: "ordinal => nat => ordinal option" where
"pred Zero n = None"
- "pred (Succ a) n = Some a"
- "pred (Limit f) n = Some (f n)"
+| "pred (Succ a) n = Some a"
+| "pred (Limit f) n = Some (f n)"
-consts
- iter :: "('a => 'a) => nat => ('a => 'a)"
-primrec
- "iter f 0 = id"
- "iter f (Suc n) = f \<circ> (iter f n)"
+abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)" where
+ "iter f n \<equiv> f ^^ n"
definition
OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" where
@@ -38,30 +33,24 @@
OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<Squnion>") where
"\<Squnion>f = OpLim (iter f)"
-consts
- cantor :: "ordinal => ordinal => ordinal"
-primrec
+primrec cantor :: "ordinal => ordinal => ordinal" where
"cantor a Zero = Succ a"
- "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
- "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
+| "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
+| "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
-consts
- Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<nabla>")
-primrec
+primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<nabla>") where
"\<nabla>f Zero = f Zero"
- "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
- "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
+| "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
+| "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
definition
deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" where
"deriv f = \<nabla>(\<Squnion>f)"
-consts
- veblen :: "ordinal => ordinal => ordinal"
-primrec
+primrec veblen :: "ordinal => ordinal => ordinal" where
"veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
- "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
- "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
+| "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
+| "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
definition "veb a = veblen a Zero"
definition "\<epsilon>\<^isub>0 = veb Zero"
--- a/src/HOL/Induct/PropLog.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Induct/PropLog.thy Wed Sep 08 19:21:46 2010 +0200
@@ -41,25 +41,20 @@
subsubsection {* Semantics of propositional logic. *}
-consts
- eval :: "['a set, 'a pl] => bool" ("_[[_]]" [100,0] 100)
-
-primrec "tt[[false]] = False"
- "tt[[#v]] = (v \<in> tt)"
- eval_imp: "tt[[p->q]] = (tt[[p]] --> tt[[q]])"
+primrec eval :: "['a set, 'a pl] => bool" ("_[[_]]" [100,0] 100) where
+ "tt[[false]] = False"
+| "tt[[#v]] = (v \<in> tt)"
+| eval_imp: "tt[[p->q]] = (tt[[p]] --> tt[[q]])"
text {*
A finite set of hypotheses from @{text t} and the @{text Var}s in
@{text p}.
*}
-consts
- hyps :: "['a pl, 'a set] => 'a pl set"
-
-primrec
+primrec hyps :: "['a pl, 'a set] => 'a pl set" where
"hyps false tt = {}"
- "hyps (#v) tt = {if v \<in> tt then #v else #v->false}"
- "hyps (p->q) tt = hyps p tt Un hyps q tt"
+| "hyps (#v) tt = {if v \<in> tt then #v else #v->false}"
+| "hyps (p->q) tt = hyps p tt Un hyps q tt"
subsubsection {* Logical consequence *}
--- a/src/HOL/Induct/QuoDataType.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Wed Sep 08 19:21:46 2010 +0200
@@ -58,14 +58,11 @@
text{*A function to return the set of nonces present in a message. It will
be lifted to the initial algrebra, to serve as an example of that process.*}
-consts
- freenonces :: "freemsg \<Rightarrow> nat set"
-
-primrec
- "freenonces (NONCE N) = {N}"
- "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
- "freenonces (CRYPT K X) = freenonces X"
- "freenonces (DECRYPT K X) = freenonces X"
+primrec freenonces :: "freemsg \<Rightarrow> nat set" where
+ "freenonces (NONCE N) = {N}"
+| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
+| "freenonces (CRYPT K X) = freenonces X"
+| "freenonces (DECRYPT K X) = freenonces X"
text{*This theorem lets us prove that the nonces function respects the
equivalence relation. It also helps us prove that Nonce
@@ -78,12 +75,11 @@
text{*A function to return the left part of the top pair in a message. It will
be lifted to the initial algrebra, to serve as an example of that process.*}
-consts freeleft :: "freemsg \<Rightarrow> freemsg"
-primrec
- "freeleft (NONCE N) = NONCE N"
- "freeleft (MPAIR X Y) = X"
- "freeleft (CRYPT K X) = freeleft X"
- "freeleft (DECRYPT K X) = freeleft X"
+primrec freeleft :: "freemsg \<Rightarrow> freemsg" where
+ "freeleft (NONCE N) = NONCE N"
+| "freeleft (MPAIR X Y) = X"
+| "freeleft (CRYPT K X) = freeleft X"
+| "freeleft (DECRYPT K X) = freeleft X"
text{*This theorem lets us prove that the left function respects the
equivalence relation. It also helps us prove that MPair
@@ -96,12 +92,11 @@
subsubsection{*The Right Projection*}
text{*A function to return the right part of the top pair in a message.*}
-consts freeright :: "freemsg \<Rightarrow> freemsg"
-primrec
- "freeright (NONCE N) = NONCE N"
- "freeright (MPAIR X Y) = Y"
- "freeright (CRYPT K X) = freeright X"
- "freeright (DECRYPT K X) = freeright X"
+primrec freeright :: "freemsg \<Rightarrow> freemsg" where
+ "freeright (NONCE N) = NONCE N"
+| "freeright (MPAIR X Y) = Y"
+| "freeright (CRYPT K X) = freeright X"
+| "freeright (DECRYPT K X) = freeright X"
text{*This theorem lets us prove that the right function respects the
equivalence relation. It also helps us prove that MPair
@@ -114,12 +109,11 @@
subsubsection{*The Discriminator for Constructors*}
text{*A function to distinguish nonces, mpairs and encryptions*}
-consts freediscrim :: "freemsg \<Rightarrow> int"
-primrec
- "freediscrim (NONCE N) = 0"
- "freediscrim (MPAIR X Y) = 1"
- "freediscrim (CRYPT K X) = freediscrim X + 2"
- "freediscrim (DECRYPT K X) = freediscrim X - 2"
+primrec freediscrim :: "freemsg \<Rightarrow> int" where
+ "freediscrim (NONCE N) = 0"
+| "freediscrim (MPAIR X Y) = 1"
+| "freediscrim (CRYPT K X) = freediscrim X + 2"
+| "freediscrim (DECRYPT K X) = freediscrim X - 2"
text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
theorem msgrel_imp_eq_freediscrim:
--- a/src/HOL/Induct/QuoNestedDataType.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Sep 08 19:21:46 2010 +0200
@@ -72,17 +72,14 @@
be lifted to the initial algrebra, to serve as an example of that process.
Note that the "free" refers to the free datatype rather than to the concept
of a free variable.*}
-consts
- freevars :: "freeExp \<Rightarrow> nat set"
- freevars_list :: "freeExp list \<Rightarrow> nat set"
+primrec freevars :: "freeExp \<Rightarrow> nat set"
+ and freevars_list :: "freeExp list \<Rightarrow> nat set" where
+ "freevars (VAR N) = {N}"
+| "freevars (PLUS X Y) = freevars X \<union> freevars Y"
+| "freevars (FNCALL F Xs) = freevars_list Xs"
-primrec
- "freevars (VAR N) = {N}"
- "freevars (PLUS X Y) = freevars X \<union> freevars Y"
- "freevars (FNCALL F Xs) = freevars_list Xs"
-
- "freevars_list [] = {}"
- "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
+| "freevars_list [] = {}"
+| "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
text{*This theorem lets us prove that the vars function respects the
equivalence relation. It also helps us prove that Variable
@@ -98,11 +95,10 @@
subsubsection{*Functions for Freeness*}
text{*A discriminator function to distinguish vars, sums and function calls*}
-consts freediscrim :: "freeExp \<Rightarrow> int"
-primrec
- "freediscrim (VAR N) = 0"
- "freediscrim (PLUS X Y) = 1"
- "freediscrim (FNCALL F Xs) = 2"
+primrec freediscrim :: "freeExp \<Rightarrow> int" where
+ "freediscrim (VAR N) = 0"
+| "freediscrim (PLUS X Y) = 1"
+| "freediscrim (FNCALL F Xs) = 2"
theorem exprel_imp_eq_freediscrim:
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
@@ -111,12 +107,10 @@
text{*This function, which returns the function name, is used to
prove part of the injectivity property for FnCall.*}
-consts freefun :: "freeExp \<Rightarrow> nat"
-
-primrec
- "freefun (VAR N) = 0"
- "freefun (PLUS X Y) = 0"
- "freefun (FNCALL F Xs) = F"
+primrec freefun :: "freeExp \<Rightarrow> nat" where
+ "freefun (VAR N) = 0"
+| "freefun (PLUS X Y) = 0"
+| "freefun (FNCALL F Xs) = F"
theorem exprel_imp_eq_freefun:
"U \<sim> V \<Longrightarrow> freefun U = freefun V"
@@ -125,11 +119,10 @@
text{*This function, which returns the list of function arguments, is used to
prove part of the injectivity property for FnCall.*}
-consts freeargs :: "freeExp \<Rightarrow> freeExp list"
-primrec
- "freeargs (VAR N) = []"
- "freeargs (PLUS X Y) = []"
- "freeargs (FNCALL F Xs) = Xs"
+primrec freeargs :: "freeExp \<Rightarrow> freeExp list" where
+ "freeargs (VAR N) = []"
+| "freeargs (PLUS X Y) = []"
+| "freeargs (FNCALL F Xs) = Xs"
theorem exprel_imp_eqv_freeargs:
"U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
@@ -285,10 +278,9 @@
by (simp add: congruent_def exprel_imp_eq_freevars)
text{*The extension of the function @{term vars} to lists*}
-consts vars_list :: "exp list \<Rightarrow> nat set"
-primrec
- "vars_list [] = {}"
- "vars_list(E#Es) = vars E \<union> vars_list Es"
+primrec vars_list :: "exp list \<Rightarrow> nat set" where
+ "vars_list [] = {}"
+| "vars_list(E#Es) = vars E \<union> vars_list Es"
text{*Now prove the three equations for @{term vars}*}
--- a/src/HOL/Induct/SList.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Induct/SList.thy Wed Sep 08 19:21:46 2010 +0200
@@ -133,10 +133,9 @@
map :: "('a=>'b) => ('a list => 'b list)" where
"map f xs = list_rec xs [] (%x l r. f(x)#r)"
-consts take :: "['a list,nat] => 'a list"
-primrec
+primrec take :: "['a list,nat] => 'a list" where
take_0: "take xs 0 = []"
- take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
+| take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
lemma ListI: "x : list (range Leaf) ==> x : List"
by (simp add: List_def)
--- a/src/HOL/Induct/Tree.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Induct/Tree.thy Wed Sep 08 19:21:46 2010 +0200
@@ -95,15 +95,15 @@
text{*Example of a general function*}
function
- add2 :: "(brouwer*brouwer) => brouwer"
+ add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
where
- "add2 (i, Zero) = i"
-| "add2 (i, (Succ j)) = Succ (add2 (i, j))"
-| "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
+ "add2 i Zero = i"
+| "add2 i (Succ j) = Succ (add2 i j)"
+| "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))"
by pat_completeness auto
termination by (relation "inv_image brouwer_order snd") auto
-lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
+lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)"
by (induct k) auto
end
--- a/src/HOL/Lattice/Orders.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Lattice/Orders.thy Wed Sep 08 19:21:46 2010 +0200
@@ -48,9 +48,7 @@
datatype 'a dual = dual 'a
-consts
- undual :: "'a dual \<Rightarrow> 'a"
-primrec
+primrec undual :: "'a dual \<Rightarrow> 'a" where
undual_dual: "undual (dual x) = x"
instantiation dual :: (leq) leq
--- a/src/HOL/Metis_Examples/BT.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy Wed Sep 08 19:21:46 2010 +0200
@@ -15,53 +15,41 @@
Lf
| Br 'a "'a bt" "'a bt"
-consts
- n_nodes :: "'a bt => nat"
- n_leaves :: "'a bt => nat"
- depth :: "'a bt => nat"
- reflect :: "'a bt => 'a bt"
- bt_map :: "('a => 'b) => ('a bt => 'b bt)"
- preorder :: "'a bt => 'a list"
- inorder :: "'a bt => 'a list"
- postorder :: "'a bt => 'a list"
- appnd :: "'a bt => 'a bt => 'a bt"
+primrec n_nodes :: "'a bt => nat" where
+ "n_nodes Lf = 0"
+| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+
+primrec n_leaves :: "'a bt => nat" where
+ "n_leaves Lf = Suc 0"
+| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
-primrec
- "n_nodes Lf = 0"
- "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+primrec depth :: "'a bt => nat" where
+ "depth Lf = 0"
+| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
-primrec
- "n_leaves Lf = Suc 0"
- "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
-
-primrec
- "depth Lf = 0"
- "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
+primrec reflect :: "'a bt => 'a bt" where
+ "reflect Lf = Lf"
+| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
-primrec
- "reflect Lf = Lf"
- "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
-
-primrec
+primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
"bt_map f Lf = Lf"
- "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
+| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
-primrec
+primrec preorder :: "'a bt => 'a list" where
"preorder Lf = []"
- "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
+| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
-primrec
+primrec inorder :: "'a bt => 'a list" where
"inorder Lf = []"
- "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
+| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
-primrec
+primrec postorder :: "'a bt => 'a list" where
"postorder Lf = []"
- "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
-primrec
- "appnd Lf t = t"
- "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)"
-
+primrec append :: "'a bt => 'a bt => 'a bt" where
+ "append Lf t = t"
+| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
text {* \medskip BT simplification *}
@@ -135,12 +123,12 @@
apply (metis bt_map.simps(1))
by (metis bt_map.simps(2))
-declare [[ sledgehammer_problem_prefix = "BT__bt_map_appnd" ]]
+declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
-lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)"
+lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)"
apply (induct t)
- apply (metis appnd.simps(1) bt_map.simps(1))
-by (metis appnd.simps(2) bt_map.simps(2))
+ apply (metis append.simps(1) bt_map.simps(1))
+by (metis append.simps(2) bt_map.simps(2))
declare [[ sledgehammer_problem_prefix = "BT__bt_map_compose" ]]
@@ -219,8 +207,8 @@
apply (induct t)
apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
reflect.simps(1))
-by (metis append.simps(1) append.simps(2) postorder.simps(2) preorder.simps(2)
- reflect.simps(2) rev.simps(2) rev_append rev_swap)
+apply simp
+done
declare [[ sledgehammer_problem_prefix = "BT__inorder_reflect" ]]
@@ -245,44 +233,44 @@
Analogues of the standard properties of the append function for lists.
*}
-declare [[ sledgehammer_problem_prefix = "BT__appnd_assoc" ]]
+declare [[ sledgehammer_problem_prefix = "BT__append_assoc" ]]
-lemma appnd_assoc [simp]: "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
+lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)"
apply (induct t1)
- apply (metis appnd.simps(1))
-by (metis appnd.simps(2))
+ apply (metis append.simps(1))
+by (metis append.simps(2))
-declare [[ sledgehammer_problem_prefix = "BT__appnd_Lf2" ]]
+declare [[ sledgehammer_problem_prefix = "BT__append_Lf2" ]]
-lemma appnd_Lf2 [simp]: "appnd t Lf = t"
+lemma append_Lf2 [simp]: "append t Lf = t"
apply (induct t)
- apply (metis appnd.simps(1))
-by (metis appnd.simps(2))
+ apply (metis append.simps(1))
+by (metis append.simps(2))
declare max_add_distrib_left [simp]
-declare [[ sledgehammer_problem_prefix = "BT__depth_appnd" ]]
+declare [[ sledgehammer_problem_prefix = "BT__depth_append" ]]
-lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
+lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
apply (induct t1)
- apply (metis appnd.simps(1) depth.simps(1) plus_nat.simps(1))
+ apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1))
by simp
-declare [[ sledgehammer_problem_prefix = "BT__n_leaves_appnd" ]]
+declare [[ sledgehammer_problem_prefix = "BT__n_leaves_append" ]]
-lemma n_leaves_appnd [simp]:
- "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
+lemma n_leaves_append [simp]:
+ "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
apply (induct t1)
- apply (metis appnd.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
+ apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
semiring_norm(111))
by (simp add: left_distrib)
-declare [[ sledgehammer_problem_prefix = "BT__bt_map_appnd" ]]
+declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
-lemma (*bt_map_appnd:*)
- "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
+lemma (*bt_map_append:*)
+ "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
apply (induct t1)
- apply (metis appnd.simps(1) bt_map.simps(1))
-by (metis bt_map_appnd)
+ apply (metis append.simps(1) bt_map.simps(1))
+by (metis bt_map_append)
end
--- a/src/HOL/Nominal/Examples/Class3.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Nominal/Examples/Class3.thy Wed Sep 08 19:21:46 2010 +0200
@@ -5956,17 +5956,13 @@
done
qed
-consts
- "idn" :: "(name\<times>ty) list\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list"
-primrec
+primrec "idn" :: "(name\<times>ty) list\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list" where
"idn [] a = []"
- "idn (p#\<Gamma>) a = ((fst p),a,Ax (fst p) a)#(idn \<Gamma> a)"
-
-consts
- "idc" :: "(coname\<times>ty) list\<Rightarrow>name\<Rightarrow>(coname\<times>name\<times>trm) list"
-primrec
+| "idn (p#\<Gamma>) a = ((fst p),a,Ax (fst p) a)#(idn \<Gamma> a)"
+
+primrec "idc" :: "(coname\<times>ty) list\<Rightarrow>name\<Rightarrow>(coname\<times>name\<times>trm) list" where
"idc [] x = []"
- "idc (p#\<Delta>) x = ((fst p),x,Ax x (fst p))#(idc \<Delta> x)"
+| "idc (p#\<Delta>) x = ((fst p),x,Ax x (fst p))#(idc \<Delta> x)"
lemma idn_eqvt[eqvt]:
fixes pi1::"name prm"
--- a/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 08 19:21:46 2010 +0200
@@ -107,17 +107,17 @@
| "vrs_of (TVarB x y) = {}"
by auto
-consts
+primrec
"ty_dom" :: "env \<Rightarrow> tyvrs set"
-primrec
+where
"ty_dom [] = {}"
- "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)"
+| "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)"
-consts
+primrec
"trm_dom" :: "env \<Rightarrow> vrs set"
-primrec
+where
"trm_dom [] = {}"
- "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)"
+| "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)"
lemma vrs_of_eqvt[eqvt]:
fixes pi ::"tyvrs prm"
@@ -475,12 +475,9 @@
by (induct B rule: binding.induct)
(simp_all add: fresh_atm type_subst_identity)
-consts
- subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100)
-
-primrec
-"([])[Y \<mapsto> T]\<^sub>e= []"
-"(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
+primrec subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100) where
+ "([])[Y \<mapsto> T]\<^sub>e= []"
+| "(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
lemma ctxt_subst_fresh':
fixes X::"tyvrs"
@@ -686,13 +683,13 @@
have fresh_cond: "X\<sharp>\<Gamma>" by fact
hence fresh_ty_dom: "X\<sharp>(ty_dom \<Gamma>)" by (simp add: fresh_dom)
have "(\<forall>X<:T\<^isub>2. T\<^isub>1) closed_in \<Gamma>" by fact
- 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>)"
+ 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>)"
by (auto simp add: closed_in_def ty.supp abs_supp)
have ok: "\<turnstile> \<Gamma> ok" by fact
- hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_ty_dom by simp
- have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp
+ hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T2 fresh_ty_dom by simp
+ have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T2 ok by simp
moreover
- 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
+ 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
ultimately show "\<Gamma> \<turnstile> (\<forall>X<:T\<^isub>2. T\<^isub>1) <: (\<forall>X<:T\<^isub>2. T\<^isub>1)" using fresh_cond
by (simp add: subtype_of.SA_all)
qed (auto simp add: closed_in_def ty.supp supp_atm)
@@ -783,10 +780,10 @@
have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
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
have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
- hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed)
+ hence closed\<^isub>T1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed)
have ok: "\<turnstile> \<Delta> ok" by fact
have ext: "\<Delta> extends \<Gamma>" by fact
- have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
+ have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T1 by (simp only: extends_closed)
hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force
moreover
have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
@@ -811,10 +808,10 @@
have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
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
have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
- hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed)
+ hence closed\<^isub>T1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed)
have ok: "\<turnstile> \<Delta> ok" by fact
have ext: "\<Delta> extends \<Gamma>" by fact
- have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
+ have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T1 by (simp only: extends_closed)
hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force
moreover
have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
@@ -903,7 +900,7 @@
case (SA_arrow \<Gamma> Q\<^isub>1 S\<^isub>1 S\<^isub>2 Q\<^isub>2)
then have rh_drv: "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T" by simp
from `Q\<^isub>1 \<rightarrow> Q\<^isub>2 = Q`
- 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
+ have Q\<^isub>12_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" by auto
have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
have lh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact
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)"
@@ -921,10 +918,10 @@
and rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1"
and rh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
from IH_trans[of "Q\<^isub>1"]
- 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
+ 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
moreover
from IH_trans[of "Q\<^isub>2"]
- 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
+ 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
ultimately have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
then have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" using T_inst by simp
}
@@ -954,15 +951,15 @@
and rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1"
and rh_drv_prm\<^isub>2:"((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
have "(\<forall>X<:Q\<^isub>1. Q\<^isub>2) = Q" by fact
- then have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q"
+ then have Q\<^isub>12_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q"
using fresh_cond by auto
from IH_trans[of "Q\<^isub>1"]
- 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
+ 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
moreover
from IH_narrow[of "Q\<^isub>1" "[]"]
- 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
+ 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
with IH_trans[of "Q\<^isub>2"]
- 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
+ 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
ultimately have "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:T\<^isub>1. T\<^isub>2)"
using fresh_cond by (simp add: subtype_of.SA_all)
hence "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T" using T_inst by simp
@@ -1005,16 +1002,16 @@
with IH_inner show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" by (simp add: subtype_of.SA_trans_TVar)
next
case True
- have memb\<^isub>X\<^isub>Q: "(TVarB X Q)\<in>set (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp
- have memb\<^isub>X\<^isub>P: "(TVarB X P)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" by simp
+ have memb\<^isub>XQ: "(TVarB X Q)\<in>set (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp
+ have memb\<^isub>XP: "(TVarB X P)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" by simp
have eq: "X=Y" by fact
- hence "S=Q" using ok\<^isub>Q lh_drv_prm memb\<^isub>X\<^isub>Q by (simp only: uniqueness_of_ctxt)
+ hence "S=Q" using ok\<^isub>Q lh_drv_prm memb\<^isub>XQ by (simp only: uniqueness_of_ctxt)
hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp
moreover
have "(\<Delta>@[(TVarB X P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def)
hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv ok\<^isub>P by (simp only: weakening)
ultimately have "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_lemma)
- then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto
+ then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>XP eq by auto
qed
next
case (SA_refl_TVar Y \<Gamma> X \<Delta>)
@@ -1049,7 +1046,7 @@
| 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"
| T_Sub[intro]: "\<lbrakk> \<Gamma> \<turnstile> t : S; \<Gamma> \<turnstile> S <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t : T"
| 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)"
-| 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>)"
+| 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>)"
equivariance typing
@@ -1164,10 +1161,10 @@
inductive
eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60)
where
- 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]"
+ 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]"
| E_App1 [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u"
| E_App2 [intro]: "\<lbrakk> val v; t \<longmapsto> t' \<rbrakk> \<Longrightarrow> v \<cdot> t \<longmapsto> v \<cdot> t'"
-| 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]"
+| 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]"
| E_TApp [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot>\<^sub>\<tau> T \<longmapsto> t' \<cdot>\<^sub>\<tau> T"
lemma better_E_Abs[intro]:
@@ -1315,7 +1312,7 @@
case (T_Var x T)
then show ?case by auto
next
- case (T_App X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
+ case (T_App X t\<^isub>1 T\<^isub>2 T\<^isub>11 T\<^isub>12)
then show ?case by force
next
case (T_Abs y T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
@@ -1744,68 +1741,68 @@
assumes H: "\<Gamma> \<turnstile> t : T"
shows "t \<longmapsto> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : T" using H
proof (nominal_induct avoiding: t' rule: typing.strong_induct)
- case (T_App \<Gamma> t\<^isub>1 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2 t\<^isub>2 t')
+ case (T_App \<Gamma> t\<^isub>1 T\<^isub>11 T\<^isub>12 t\<^isub>2 t')
obtain x::vrs where x_fresh: "x \<sharp> (\<Gamma>, t\<^isub>1 \<cdot> t\<^isub>2, t')"
by (rule exists_fresh) (rule fin_supp)
obtain X::tyvrs where "X \<sharp> (t\<^isub>1 \<cdot> t\<^isub>2, t')"
by (rule exists_fresh) (rule fin_supp)
with `t\<^isub>1 \<cdot> t\<^isub>2 \<longmapsto> t'` show ?case
proof (cases rule: eval.strong_cases [where x=x and X=X])
- case (E_Abs v\<^isub>2 T\<^isub>1\<^isub>1' t\<^isub>1\<^isub>2)
- 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"
+ case (E_Abs v\<^isub>2 T\<^isub>11' t\<^isub>12)
+ 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"
by (simp add: trm.inject fresh_prod)
moreover from x_fresh have "x \<sharp> \<Gamma>" by simp
ultimately obtain S'
- where T\<^isub>1\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1\<^isub>1 <: T\<^isub>1\<^isub>1'"
- and t\<^isub>1\<^isub>2: "(VarB x T\<^isub>1\<^isub>1') # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : S'"
- and S': "\<Gamma> \<turnstile> S' <: T\<^isub>1\<^isub>2"
+ where T\<^isub>11: "\<Gamma> \<turnstile> T\<^isub>11 <: T\<^isub>11'"
+ and t\<^isub>12: "(VarB x T\<^isub>11') # \<Gamma> \<turnstile> t\<^isub>12 : S'"
+ and S': "\<Gamma> \<turnstile> S' <: T\<^isub>12"
by (rule Abs_type') blast
- from `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1`
- have "\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1'" using T\<^isub>1\<^isub>1 by (rule T_Sub)
- with t\<^isub>1\<^isub>2 have "\<Gamma> \<turnstile> t\<^isub>1\<^isub>2[x \<mapsto> t\<^isub>2] : S'"
+ from `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11`
+ have "\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11'" using T\<^isub>11 by (rule T_Sub)
+ with t\<^isub>12 have "\<Gamma> \<turnstile> t\<^isub>12[x \<mapsto> t\<^isub>2] : S'"
by (rule subst_type [where \<Delta>="[]", simplified])
- hence "\<Gamma> \<turnstile> t\<^isub>1\<^isub>2[x \<mapsto> t\<^isub>2] : T\<^isub>1\<^isub>2" using S' by (rule T_Sub)
+ hence "\<Gamma> \<turnstile> t\<^isub>12[x \<mapsto> t\<^isub>2] : T\<^isub>12" using S' by (rule T_Sub)
with E_Abs and x_fresh show ?thesis by (simp add: trm.inject fresh_prod)
next
case (E_App1 t''' t'' u)
hence "t\<^isub>1 \<longmapsto> t''" by (simp add:trm.inject)
- hence "\<Gamma> \<turnstile> t'' : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2" by (rule T_App)
- hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^isub>2 : T\<^isub>1\<^isub>2" using `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1`
+ hence "\<Gamma> \<turnstile> t'' : T\<^isub>11 \<rightarrow> T\<^isub>12" by (rule T_App)
+ hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^isub>2 : T\<^isub>12" using `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11`
by (rule typing.T_App)
with E_App1 show ?thesis by (simp add:trm.inject)
next
case (E_App2 v t''' t'')
hence "t\<^isub>2 \<longmapsto> t''" by (simp add:trm.inject)
- hence "\<Gamma> \<turnstile> t'' : T\<^isub>1\<^isub>1" by (rule T_App)
- with T_App(1) have "\<Gamma> \<turnstile> t\<^isub>1 \<cdot> t'' : T\<^isub>1\<^isub>2"
+ hence "\<Gamma> \<turnstile> t'' : T\<^isub>11" by (rule T_App)
+ with T_App(1) have "\<Gamma> \<turnstile> t\<^isub>1 \<cdot> t'' : T\<^isub>12"
by (rule typing.T_App)
with E_App2 show ?thesis by (simp add:trm.inject)
qed (simp_all add: fresh_prod)
next
- case (T_TApp X \<Gamma> t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2 t')
+ case (T_TApp X \<Gamma> t\<^isub>1 T\<^isub>2 T\<^isub>11 T\<^isub>12 t')
obtain x::vrs where "x \<sharp> (t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2, t')"
by (rule exists_fresh) (rule fin_supp)
with `t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 \<longmapsto> t'`
show ?case
proof (cases rule: eval.strong_cases [where X=X and x=x])
- case (E_TAbs T\<^isub>1\<^isub>1' T\<^isub>2' t\<^isub>1\<^isub>2)
- 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'"
+ case (E_TAbs T\<^isub>11' T\<^isub>2' t\<^isub>12)
+ 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'"
by (simp_all add: trm.inject)
- moreover from `\<Gamma>\<turnstile>T\<^isub>2<:T\<^isub>1\<^isub>1` and `X \<sharp> \<Gamma>` have "X \<sharp> T\<^isub>1\<^isub>1"
+ moreover from `\<Gamma>\<turnstile>T\<^isub>2<:T\<^isub>11` and `X \<sharp> \<Gamma>` have "X \<sharp> T\<^isub>11"
by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed)
ultimately obtain S'
- where "TVarB X T\<^isub>1\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : S'"
- and "(TVarB X T\<^isub>1\<^isub>1 # \<Gamma>) \<turnstile> S' <: T\<^isub>1\<^isub>2"
+ where "TVarB X T\<^isub>11 # \<Gamma> \<turnstile> t\<^isub>12 : S'"
+ and "(TVarB X T\<^isub>11 # \<Gamma>) \<turnstile> S' <: T\<^isub>12"
by (rule TAbs_type') blast
- hence "TVarB X T\<^isub>1\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : T\<^isub>1\<^isub>2" by (rule T_Sub)
- 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`
+ hence "TVarB X T\<^isub>11 # \<Gamma> \<turnstile> t\<^isub>12 : T\<^isub>12" by (rule T_Sub)
+ 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`
by (rule substT_type [where D="[]", simplified])
with T_TApp and E_TAbs show ?thesis by (simp add: trm.inject)
next
case (E_TApp t''' t'' T)
from E_TApp have "t\<^isub>1 \<longmapsto> t''" by (simp add: trm.inject)
- then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2)" by (rule T_TApp)
- 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`
+ then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^isub>11. T\<^isub>12)" by (rule T_TApp)
+ 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`
by (rule better_T_TApp)
with E_TApp show ?thesis by (simp add: trm.inject)
qed (simp_all add: fresh_prod)
@@ -1845,7 +1842,7 @@
shows "val t \<or> (\<exists>t'. t \<longmapsto> t')"
using assms
proof (induct "[]::env" t T)
- case (T_App t\<^isub>1 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2 t\<^isub>2)
+ case (T_App t\<^isub>1 T\<^isub>11 T\<^isub>12 t\<^isub>2)
hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
thus ?case
proof
@@ -1871,7 +1868,7 @@
thus ?case by auto
qed
next
- case (T_TApp X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
+ case (T_TApp X t\<^isub>1 T\<^isub>2 T\<^isub>11 T\<^isub>12)
hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
thus ?case
proof
--- a/src/HOL/Nominal/Examples/W.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Nominal/Examples/W.thy Wed Sep 08 19:21:46 2010 +0200
@@ -150,12 +150,9 @@
equivariance valid
text {* General *}
-consts
- gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS"
-
-primrec
+primrec gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS" where
"gen T [] = Ty T"
- "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
+| "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
lemma gen_eqvt[eqvt]:
fixes pi::"tvar prm"
--- a/src/HOL/UNITY/Comp/AllocBase.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Wed Sep 08 19:21:46 2010 +0200
@@ -15,17 +15,11 @@
NbT_pos: "0 < NbT"
(*This function merely sums the elements of a list*)
-consts tokens :: "nat list => nat"
-primrec
+primrec tokens :: "nat list => nat" where
"tokens [] = 0"
- "tokens (x#xs) = x + tokens xs"
+| "tokens (x#xs) = x + tokens xs"
-consts
- bag_of :: "'a list => 'a multiset"
-
-primrec
- "bag_of [] = {#}"
- "bag_of (x#xs) = {#x#} + bag_of xs"
+abbreviation (input) "bag_of \<equiv> multiset_of"
lemma setsum_fun_mono [rule_format]:
"!!f :: nat=>nat.
--- a/src/HOL/ZF/HOLZF.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/ZF/HOLZF.thy Wed Sep 08 19:21:46 2010 +0200
@@ -402,12 +402,9 @@
done
qed
-consts
- nat2Nat :: "nat \<Rightarrow> ZF"
-
-primrec
-nat2Nat_0[intro]: "nat2Nat 0 = Empty"
-nat2Nat_Suc[intro]: "nat2Nat (Suc n) = SucNat (nat2Nat n)"
+primrec nat2Nat :: "nat \<Rightarrow> ZF" where
+ nat2Nat_0[intro]: "nat2Nat 0 = Empty"
+| nat2Nat_Suc[intro]: "nat2Nat (Suc n) = SucNat (nat2Nat n)"
definition Nat2nat :: "ZF \<Rightarrow> nat" where
"Nat2nat == inv nat2Nat"
@@ -500,12 +497,9 @@
apply auto
done
-consts
- NatInterval :: "nat \<Rightarrow> nat \<Rightarrow> ZF"
-
-primrec
+primrec NatInterval :: "nat \<Rightarrow> nat \<Rightarrow> ZF" where
"NatInterval n 0 = Singleton (nat2Nat n)"
- "NatInterval n (Suc m) = union (NatInterval n m) (Singleton (nat2Nat (n+m+1)))"
+| "NatInterval n (Suc m) = union (NatInterval n m) (Singleton (nat2Nat (n+m+1)))"
lemma n_Elem_NatInterval[rule_format]: "! q. q <= m \<longrightarrow> Elem (nat2Nat (n+q)) (NatInterval n m)"
apply (induct m)
@@ -729,12 +723,9 @@
apply (simp add: Ext_def)
done
-consts
- Ext_ZF_n :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> nat \<Rightarrow> ZF"
-
-primrec
+primrec Ext_ZF_n :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> nat \<Rightarrow> ZF" where
"Ext_ZF_n R s 0 = Ext_ZF R s"
- "Ext_ZF_n R s (Suc n) = Sum (Repl (Ext_ZF_n R s n) (Ext_ZF R))"
+| "Ext_ZF_n R s (Suc n) = Sum (Repl (Ext_ZF_n R s n) (Ext_ZF R))"
definition Ext_ZF_hull :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> ZF" where
"Ext_ZF_hull R s == SeqSum (Ext_ZF_n R s)"
--- a/src/HOL/ex/BT.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/ex/BT.thy Wed Sep 08 19:21:46 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/ex/BT.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -14,53 +13,41 @@
Lf
| Br 'a "'a bt" "'a bt"
-consts
- n_nodes :: "'a bt => nat"
- n_leaves :: "'a bt => nat"
- depth :: "'a bt => nat"
- reflect :: "'a bt => 'a bt"
- bt_map :: "('a => 'b) => ('a bt => 'b bt)"
- preorder :: "'a bt => 'a list"
- inorder :: "'a bt => 'a list"
- postorder :: "'a bt => 'a list"
- append :: "'a bt => 'a bt => 'a bt"
+primrec n_nodes :: "'a bt => nat" where
+ "n_nodes Lf = 0"
+| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+
+primrec n_leaves :: "'a bt => nat" where
+ "n_leaves Lf = Suc 0"
+| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
-primrec
- "n_nodes Lf = 0"
- "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+primrec depth :: "'a bt => nat" where
+ "depth Lf = 0"
+| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
-primrec
- "n_leaves Lf = Suc 0"
- "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
-
-primrec
- "depth Lf = 0"
- "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
+primrec reflect :: "'a bt => 'a bt" where
+ "reflect Lf = Lf"
+| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
-primrec
- "reflect Lf = Lf"
- "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
-
-primrec
+primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
"bt_map f Lf = Lf"
- "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
+| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
-primrec
+primrec preorder :: "'a bt => 'a list" where
"preorder Lf = []"
- "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
+| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
-primrec
+primrec inorder :: "'a bt => 'a list" where
"inorder Lf = []"
- "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
+| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
-primrec
+primrec postorder :: "'a bt => 'a list" where
"postorder Lf = []"
- "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
-primrec
+primrec append :: "'a bt => 'a bt => 'a bt" where
"append Lf t = t"
- "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
-
+| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
text {* \medskip BT simplification *}
--- a/src/HOL/ex/Chinese.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/ex/Chinese.thy Wed Sep 08 19:21:46 2010 +0200
@@ -1,5 +1,4 @@
(* -*- coding: utf-8 -*- :encoding=utf-8:
- ID: $Id$
Author: Ning Zhang and Christian Urban
Example theory involving Unicode characters (UTF-8 encoding) -- both
@@ -30,20 +29,17 @@
| Nine ("九")
| Ten ("十")
-consts
- translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100)
-
-primrec
+primrec translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100) where
"|一| = 1"
- "|二| = 2"
- "|三| = 3"
- "|四| = 4"
- "|五| = 5"
- "|六| = 6"
- "|七| = 7"
- "|八| = 8"
- "|九| = 9"
- "|十| = 10"
+|"|二| = 2"
+|"|三| = 3"
+|"|四| = 4"
+|"|五| = 5"
+|"|六| = 6"
+|"|七| = 7"
+|"|八| = 8"
+|"|九| = 9"
+|"|十| = 10"
thm translate.simps
--- a/src/HOL/ex/Hebrew.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/ex/Hebrew.thy Wed Sep 08 19:21:46 2010 +0200
@@ -1,5 +1,4 @@
(* -*- coding: utf-8 -*- :encoding=utf-8:
- ID: $Id$
Author: Makarius
Example theory involving Unicode characters (UTF-8 encoding) -- both
@@ -43,31 +42,29 @@
text {* Interpreting Hebrew letters as numbers. *}
-consts
- mispar :: "alef_bet => nat"
-primrec
+primrec mispar :: "alef_bet => nat" where
"mispar א = 1"
- "mispar ב = 2"
- "mispar ג = 3"
- "mispar ד = 4"
- "mispar ה = 5"
- "mispar ו = 6"
- "mispar ז = 7"
- "mispar ח = 8"
- "mispar ט = 9"
- "mispar י = 10"
- "mispar כ = 20"
- "mispar ל = 30"
- "mispar מ = 40"
- "mispar נ = 50"
- "mispar ס = 60"
- "mispar ע = 70"
- "mispar פ = 80"
- "mispar צ = 90"
- "mispar ק = 100"
- "mispar ר = 200"
- "mispar ש = 300"
- "mispar ת = 400"
+| "mispar ב = 2"
+| "mispar ג = 3"
+| "mispar ד = 4"
+| "mispar ה = 5"
+| "mispar ו = 6"
+| "mispar ז = 7"
+| "mispar ח = 8"
+| "mispar ט = 9"
+| "mispar י = 10"
+| "mispar כ = 20"
+| "mispar ל = 30"
+| "mispar מ = 40"
+| "mispar נ = 50"
+| "mispar ס = 60"
+| "mispar ע = 70"
+| "mispar פ = 80"
+| "mispar צ = 90"
+| "mispar ק = 100"
+| "mispar ר = 200"
+| "mispar ש = 300"
+| "mispar ת = 400"
thm mispar.simps
--- a/src/HOL/ex/ReflectionEx.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/ex/ReflectionEx.thy Wed Sep 08 19:21:46 2010 +0200
@@ -46,14 +46,13 @@
datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
-consts Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
-primrec
+primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool" where
"Ifm (At n) vs = vs!n"
- "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
- "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
- "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
- "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
- "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
+| "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
+| "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
+| "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
+| "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
+| "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
apply (reify Ifm.simps)
@@ -399,7 +398,7 @@
| "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)"
| "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)"
| "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs"
-consts prodmul:: "prod \<times> prod \<Rightarrow> prod"
+
datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F
| Or sgn sgn | And sgn sgn