--- a/NEWS Fri Sep 10 15:16:51 2010 +0200
+++ b/NEWS Fri Sep 10 15:17:44 2010 +0200
@@ -71,6 +71,8 @@
*** HOL ***
+* String.literal is a type, but not a datatype. INCOMPATIBILITY.
+
* Renamed lemmas: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff
* Renamed class eq and constant eq (for code generation) to class equal
--- a/src/HOL/Auth/Guard/Extensions.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Fri Sep 10 15:17:44 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/Kerberos_BAN.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Fri Sep 10 15:17:44 2010 +0200
@@ -171,21 +171,21 @@
text{*Lemmas for reasoning about predicate "before"*}
-lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)";
+lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)";
+lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs";
+lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Fri Sep 10 15:17:44 2010 +0200
@@ -157,10 +157,7 @@
lemma Gets_imp_knows:
"\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> knows B evs"
-apply (case_tac "B = Spy")
-apply (blast dest!: Gets_imp_knows_Spy)
-apply (blast dest!: Gets_imp_knows_agents)
-done
+by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
lemma Gets_imp_knows_analz:
"\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> analz (knows B evs)"
@@ -168,21 +165,21 @@
done
text{*Lemmas for reasoning about predicate "before"*}
-lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)";
+lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)";
+lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs";
+lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
--- a/src/HOL/Auth/OtwayReesBella.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy Fri Sep 10 15:17:44 2010 +0200
@@ -104,11 +104,7 @@
lemma Gets_imp_knows:
"\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk> \<Longrightarrow> X \<in> knows B evs"
-apply (case_tac "B = Spy")
-apply (blast dest!: Gets_imp_knows_Spy)
-apply (blast dest!: Gets_imp_knows_agents)
-done
-
+by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
lemma OR2_analz_knows_Spy:
"\<lbrakk>Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> orb\<rbrakk>
@@ -218,15 +214,8 @@
evs \<in> orb\<rbrakk>
\<Longrightarrow> (K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>)))
| X \<in> analz (knows Spy evs)"
-apply (case_tac "B \<in> bad")
-apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd,
- THEN analz.Decrypt, THEN analz.Fst])
-prefer 3 apply blast
-prefer 3 apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN
- parts.Snd, THEN B_trusts_OR3]
- Says_Server_message_form)
-apply simp_all
-done
+by (metis B_trusts_OR3 Crypt_Spy_analz_bad Gets_imp_Says MPair_analz MPair_parts
+ Says_Server_message_form Says_imp_analz_Spy Says_imp_parts_knows_Spy)
lemma unique_Na: "\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
Says A B' \<lbrace>Nonce M', Agent A, Agent B', Crypt (shrK A) \<lbrace>Nonce Na, Nonce M', Agent A, Agent B'\<rbrace>\<rbrace> \<in> set evs;
@@ -240,7 +229,7 @@
lemma analz_image_freshCryptK_lemma:
"(Crypt K X \<in> analz (Key`nE \<union> H)) \<longrightarrow> (Crypt K X \<in> analz H) \<Longrightarrow>
- (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)";
+ (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])
ML
@@ -376,8 +365,6 @@
apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
apply (drule analz_hard, assumption, assumption, assumption, assumption)
apply (drule OR4_imp_Gets, assumption, assumption)
-apply (erule exE)
-(*blast doesn't do because it can't infer that Key (shrK P) \<in> (knows P evs)*)
apply (fastsimp dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
done
--- a/src/HOL/Auth/Public.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Auth/Public.thy Fri Sep 10 15:17:44 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.
@@ -227,12 +235,10 @@
"\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
apply (induct evs)
prefer 2
- apply (simp add: used_Cons)
- apply (rule ballI)
- apply (case_tac a, auto)
-apply (auto dest!: parts_cut)
+ apply (simp add: used_Cons split: event.split)
+ apply (metis Un_iff empty_subsetI insert_subset le_supI1 le_supI2 parts_subset_iff)
txt{*Base case*}
-apply (simp add: used_Nil)
+apply (auto dest!: parts_cut simp add: used_Nil)
done
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
--- a/src/HOL/Auth/Shared.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Auth/Shared.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Fri Sep 10 15:17:44 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/Code_Evaluation.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Fri Sep 10 15:17:44 2010 +0200
@@ -159,6 +159,18 @@
*}
+instantiation String.literal :: term_of
+begin
+
+definition
+ "term_of s = App (Const (STR ''STR'')
+ (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
+ Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
+
+instance ..
+
+end
+
subsubsection {* Code generator setup *}
lemmas [code del] = term.recs term.cases term.size
--- a/src/HOL/Code_Numeral.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Code_Numeral.thy Fri Sep 10 15:17:44 2010 +0200
@@ -345,7 +345,7 @@
code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(SML "!((_ : Int.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
(Scala infixl 5 "==")
(Eval "!((_ : int) = _)")
--- a/src/HOL/Decision_Procs/Cooper.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Fri Sep 10 15:17:44 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/HOL.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/HOL.thy Fri Sep 10 15:17:44 2010 +0200
@@ -1942,10 +1942,10 @@
(Haskell "Eq")
code_const "HOL.equal"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
code_const HOL.eq
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
text {* undefined *}
--- a/src/HOL/Hoare_Parallel/OG_Com.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/IMP/Compiler0.thy Fri Sep 10 15:17:44 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/Imperative_HOL/Heap.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Fri Sep 10 15:17:44 2010 +0200
@@ -30,10 +30,6 @@
instance int :: heap ..
-instance String.literal :: countable
- by (rule countable_classI [of "String.literal_case to_nat"])
- (auto split: String.literal.splits)
-
instance String.literal :: heap ..
instance typerep :: heap ..
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Sep 10 15:17:44 2010 +0200
@@ -402,12 +402,15 @@
subsubsection {* Logical intermediate layer *}
-primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where
- [code del, code_post]: "raise' (STR s) = raise s"
+definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
+ [code del]: "raise' s = raise (explode s)"
+
+lemma [code_post]: "raise' (STR s) = raise s"
+unfolding raise'_def by (simp add: STR_inverse)
lemma raise_raise' [code_inline]:
"raise s = raise' (STR s)"
- by simp
+ unfolding raise'_def by (simp add: STR_inverse)
code_datatype raise' -- {* avoid @{const "Heap"} formally *}
--- a/src/HOL/Import/HOL4Compat.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Induct/ABexp.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Induct/Ordinals.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Induct/PropLog.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Induct/SList.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Induct/Tree.thy Fri Sep 10 15:17:44 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/IsaMakefile Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/IsaMakefile Fri Sep 10 15:17:44 2010 +0200
@@ -162,7 +162,6 @@
Power.thy \
Predicate.thy \
Product_Type.thy \
- Record.thy \
Relation.thy \
Rings.thy \
SAT.thy \
@@ -254,6 +253,7 @@
Random.thy \
Random_Sequence.thy \
Recdef.thy \
+ Record.thy \
Refute.thy \
Semiring_Normalization.thy \
SetInterval.thy \
--- a/src/HOL/Lattice/Orders.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Lattice/Orders.thy Fri Sep 10 15:17:44 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/Library/Code_Char.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy Fri Sep 10 15:17:44 2010 +0200
@@ -34,7 +34,7 @@
code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
(SML "!((_ : char) = _)")
(OCaml "!((_ : char) = _)")
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
(Scala infixl 5 "==")
code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
@@ -44,14 +44,6 @@
definition implode :: "string \<Rightarrow> String.literal" where
"implode = STR"
-primrec explode :: "String.literal \<Rightarrow> string" where
- "explode (STR s) = s"
-
-lemma [code]:
- "literal_case f s = f (explode s)"
- "literal_rec f s = f (explode s)"
- by (cases s, simp)+
-
code_reserved SML String
code_const implode
--- a/src/HOL/Library/Code_Integer.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy Fri Sep 10 15:17:44 2010 +0200
@@ -99,7 +99,7 @@
code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
(Scala infixl 5 "==")
(Eval infixl 6 "=")
--- a/src/HOL/Library/Code_Natural.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Fri Sep 10 15:17:44 2010 +0200
@@ -130,7 +130,7 @@
(Scala infixl 8 "/%")
code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
(Scala infixl 5 "==")
code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
--- a/src/HOL/Library/Countable.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Library/Countable.thy Fri Sep 10 15:17:44 2010 +0200
@@ -100,8 +100,8 @@
text {* Further *}
instance String.literal :: countable
- by (rule countable_classI [of "String.literal_case to_nat"])
- (auto split: String.literal.splits)
+ by (rule countable_classI [of "to_nat o explode"])
+ (auto simp add: explode_inject)
instantiation typerep :: countable
begin
--- a/src/HOL/Library/Efficient_Nat.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Sep 10 15:17:44 2010 +0200
@@ -443,7 +443,7 @@
code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
(Scala infixl 5 "==")
(Eval infixl 6 "=")
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy Fri Sep 10 15:17:44 2010 +0200
@@ -7,11 +7,11 @@
uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
begin
-setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
- Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_fs",
- Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs",
- Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
+ Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4)) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_fs",
+ Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4)) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_nofs",
+ Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4)) *}
end
\ No newline at end of file
--- a/src/HOL/Library/SML_Quickcheck.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy Fri Sep 10 15:17:44 2010 +0200
@@ -7,7 +7,7 @@
setup {*
Inductive_Codegen.quickcheck_setup #>
- Quickcheck.add_generator ("SML", Codegen.test_term)
+ Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term))
*}
end
--- a/src/HOL/List.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/List.thy Fri Sep 10 15:17:44 2010 +0200
@@ -4829,7 +4829,7 @@
(Haskell -)
code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
code_reserved SML
list
--- a/src/HOL/Metis_Examples/BT.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy Fri Sep 10 15:17:44 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/Metis_Examples/BigO.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Fri Sep 10 15:17:44 2010 +0200
@@ -253,10 +253,9 @@
apply (rule abs_triangle_ineq)
apply (metis add_nonneg_nonneg)
apply (rule add_mono)
-using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]]
-(*Found by SPASS; SLOW*)
-apply (metis le_maxI2 linorder_linear linorder_not_le min_max.sup_absorb1 mult_le_cancel_right order_trans)
-apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
+using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]]
+ apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
+ apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
done
declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]]
@@ -619,9 +618,25 @@
prefer 2
apply simp
apply (simp add: mult_assoc [symmetric] abs_mult)
- (*couldn't get this proof without the step above; SLOW*)
- apply (metis mult_assoc abs_ge_zero mult_left_mono)
-done
+ (* couldn't get this proof without the step above *)
+proof -
+ fix g :: "'b \<Rightarrow> 'a" and d :: 'a
+ assume A1: "c \<noteq> (0\<Colon>'a)"
+ assume A2: "\<forall>x\<Colon>'b. \<bar>g x\<bar> \<le> d * \<bar>f x\<bar>"
+ have F1: "inverse \<bar>c\<bar> = \<bar>inverse c\<bar>" using A1 by (metis nonzero_abs_inverse)
+ have F2: "(0\<Colon>'a) < \<bar>c\<bar>" using A1 by (metis zero_less_abs_iff)
+ have "(0\<Colon>'a) < \<bar>c\<bar> \<longrightarrow> (0\<Colon>'a) < \<bar>inverse c\<bar>" using F1 by (metis positive_imp_inverse_positive)
+ hence "(0\<Colon>'a) < \<bar>inverse c\<bar>" using F2 by metis
+ hence F3: "(0\<Colon>'a) \<le> \<bar>inverse c\<bar>" by (metis order_le_less)
+ have "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar>"
+ using A2 by metis
+ hence F4: "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<and> (0\<Colon>'a) \<le> \<bar>inverse c\<bar>"
+ using F3 by metis
+ hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^isub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^isub>7 (u * v))\<bar>)"
+ by (metis comm_mult_left_mono)
+ thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
+ using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
+qed
declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult6" ]]
--- a/src/HOL/Metis_Examples/Message.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Metis_Examples/Message.thy Fri Sep 10 15:17:44 2010 +0200
@@ -85,7 +85,7 @@
text{*Equations hold because constructors are injective.*}
lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
-by (metis agent.inject imageI image_iff)
+by (metis agent.inject image_iff)
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x \<in> A)"
by (metis image_iff msg.inject(4))
@@ -241,7 +241,7 @@
lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
by (blast dest: parts_mono);
-lemma parts_cut: "[|Y\<in> parts(insert X G); X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
+lemma parts_cut: "[|Y\<in> parts (insert X G); X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
@@ -745,15 +745,12 @@
by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un
analz_mono analz_synth_Un insert_absorb)
-(* Simpler problems? BUT METIS CAN'T PROVE THE LAST STEP
lemma Fake_analz_insert_simpler:
"X \<in> synth (analz G) ==>
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
apply (rule subsetI)
apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
apply (metis Un_commute analz_analz_Un analz_synth_Un)
-apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset)
-done
-*)
+by (metis Un_upper1 Un_upper2 analz_mono insert_absorb insert_subset)
end
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Sep 10 15:17:44 2010 +0200
@@ -96,7 +96,7 @@
fun invoke_quickcheck quickcheck_generator thy t =
TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
(fn _ =>
- case Quickcheck.gen_test_term (ProofContext.init_global thy) true true (SOME quickcheck_generator)
+ case Quickcheck.gen_test_term (ProofContext.init_global thy) true (SOME quickcheck_generator)
size iterations (preprocess thy [] t) of
(NONE, (time_report, report)) => (NoCex, (time_report, report))
| (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
--- a/src/HOL/Nominal/Examples/Class3.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Nominal/Examples/Class3.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Nominal/Examples/W.thy Fri Sep 10 15:17:44 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/Option.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Option.thy Fri Sep 10 15:17:44 2010 +0200
@@ -128,7 +128,7 @@
(Haskell -)
code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
code_reserved SML
option NONE SOME
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Sep 10 15:17:44 2010 +0200
@@ -27,7 +27,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 1, expect = counterexample]
+quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 10, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Sep 10 15:17:44 2010 +0200
@@ -30,7 +30,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 1]
+quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 10]
oops
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Sep 10 15:17:44 2010 +0200
@@ -30,7 +30,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
- quickcheck[generator = predicate_compile_ff_nofs, size=2, iterations=3, quiet = false, expect = counterexample]
+ quickcheck[generator = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Fri Sep 10 15:17:44 2010 +0200
@@ -1419,7 +1419,110 @@
values "{x. test_minus_bool x}"
-subsection {* Examples for detecting switches *}
+subsection {* Functions *}
+
+fun partial_hd :: "'a list => 'a option"
+where
+ "partial_hd [] = Option.None"
+| "partial_hd (x # xs) = Some x"
+
+inductive hd_predicate
+where
+ "partial_hd xs = Some x ==> hd_predicate xs x"
+
+code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate .
+
+thm hd_predicate.equation
+
+subsection {* Locales *}
+
+inductive hd_predicate2 :: "('a list => 'a option) => 'a list => 'a => bool"
+where
+ "partial_hd' xs = Some x ==> hd_predicate2 partial_hd' xs x"
+
+
+thm hd_predicate2.intros
+
+code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 .
+thm hd_predicate2.equation
+
+locale A = fixes partial_hd :: "'a list => 'a option" begin
+
+inductive hd_predicate_in_locale :: "'a list => 'a => bool"
+where
+ "partial_hd xs = Some x ==> hd_predicate_in_locale xs x"
+
+end
+
+text {* The global introduction rules must be redeclared as introduction rules and then
+ one could invoke code_pred. *}
+
+declare A.hd_predicate_in_locale.intros [unfolded Predicate.eq_is_eq[symmetric], code_pred_intro]
+
+code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
+unfolding eq_is_eq by (auto elim: A.hd_predicate_in_locale.cases)
+
+interpretation A partial_hd .
+thm hd_predicate_in_locale.intros
+text {* A locally compliant solution with a trivial interpretation fails, because
+the predicate compiler has very strict assumptions about the terms and their structure. *}
+
+(*code_pred hd_predicate_in_locale .*)
+
+section {* Integer example *}
+
+definition three :: int
+where "three = 3"
+
+inductive is_three
+where
+ "is_three three"
+
+code_pred is_three .
+
+thm is_three.equation
+
+section {* String.literal example *}
+
+definition Error_1
+where
+ "Error_1 = STR ''Error 1''"
+
+definition Error_2
+where
+ "Error_2 = STR ''Error 2''"
+
+inductive "is_error" :: "String.literal \<Rightarrow> bool"
+where
+ "is_error Error_1"
+| "is_error Error_2"
+
+code_pred is_error .
+
+thm is_error.equation
+
+inductive is_error' :: "String.literal \<Rightarrow> bool"
+where
+ "is_error' (STR ''Error1'')"
+| "is_error' (STR ''Error2'')"
+
+code_pred is_error' .
+
+thm is_error'.equation
+
+datatype ErrorObject = Error String.literal int
+
+inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
+where
+ "is_error'' (Error Error_1 3)"
+| "is_error'' (Error Error_2 4)"
+
+code_pred is_error'' .
+
+thm is_error''.equation
+
+
+section {* Examples for detecting switches *}
inductive detect_switches1 where
"detect_switches1 [] []"
--- a/src/HOL/Product_Type.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Product_Type.thy Fri Sep 10 15:17:44 2010 +0200
@@ -29,7 +29,7 @@
by (simp_all add: equal)
code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
code_instance bool :: equal
(Haskell -)
@@ -110,7 +110,7 @@
(Haskell -)
code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
code_reserved SML
unit
@@ -281,7 +281,7 @@
(Haskell -)
code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
types_code
"prod" ("(_ */ _)")
--- a/src/HOL/String.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/String.thy Fri Sep 10 15:17:44 2010 +0200
@@ -152,17 +152,37 @@
Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
-subsection {* Strings as dedicated datatype *}
+subsection {* Strings as dedicated type *}
+
+typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
+ morphisms explode STR ..
+
+instantiation literal :: size
+begin
-datatype literal = STR string
+definition size_literal :: "literal \<Rightarrow> nat"
+where
+ [code]: "size_literal (s\<Colon>literal) = 0"
-declare literal.cases [code del] literal.recs [code del]
+instance ..
+
+end
-lemma [code]: "size (s\<Colon>literal) = 0"
- by (cases s) simp_all
+instantiation literal :: equal
+begin
+
+definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
+where
+ "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
-lemma [code]: "literal_size (s\<Colon>literal) = 0"
- by (cases s) simp_all
+instance
+proof
+qed (auto simp add: equal_literal_def explode_inject)
+
+end
+
+lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
+by(simp add: STR_inject)
subsection {* Code generator *}
@@ -189,7 +209,7 @@
code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
(SML "!((_ : string) = _)")
(OCaml "!((_ : string) = _)")
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
(Scala infixl 5 "==")
types_code
@@ -231,4 +251,4 @@
code_modulename Haskell
String String
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Sep 10 15:17:44 2010 +0200
@@ -10,7 +10,8 @@
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
- MalformedInput | MalformedOutput | UnknownError
+ MalformedInput | MalformedOutput | Interrupted | InternalError |
+ UnknownError
type prover_config =
{exec: string * string,
@@ -42,7 +43,7 @@
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
- MalformedOutput | UnknownError
+ MalformedOutput | Interrupted | InternalError | UnknownError
type prover_config =
{exec: string * string,
@@ -85,6 +86,8 @@
"The ATP problem is malformed. Please report this to the Isabelle \
\developers."
| string_for_failure MalformedOutput = "The ATP output is malformed."
+ | string_for_failure Interrupted = "The ATP was interrupted."
+ | string_for_failure InternalError = "An internal ATP error occurred."
| string_for_failure UnknownError = "An unknown ATP error occurred."
fun known_failure_in_output output =
@@ -182,7 +185,8 @@
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
- (SpassTooOld, "tptp2dfg")],
+ (SpassTooOld, "tptp2dfg"),
+ (InternalError, "Please report this error")],
default_max_relevant = 350 (* FUDGE *),
explicit_forall = true,
use_conjecture_for_hypotheses = true}
@@ -211,7 +215,8 @@
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(Unprovable, "Termination reason: Satisfiable"),
- (VampireTooOld, "not a valid option")],
+ (VampireTooOld, "not a valid option"),
+ (Interrupted, "Aborted by signal SIGINT")],
default_max_relevant = 400 (* FUDGE *),
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -285,7 +290,7 @@
val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
val remote_vampire = remotify_prover vampire "Vampire" ["9.0", "1.0", "0.6"]
val remote_sine_e =
- remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
+ remote_prover "sine_e" "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
800 (* FUDGE *) true
val remote_snark =
remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
--- a/src/HOL/Tools/Function/fun.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML Fri Sep 10 15:17:44 2010 +0200
@@ -44,7 +44,7 @@
())
end
- val (_, qs, gs, args, _) = split_def ctxt geq
+ val (_, qs, gs, args, _) = split_def ctxt (K true) geq
val _ = if not (null gs) then err "Conditional equations" else ()
val _ = map check_constr_pattern args
@@ -76,7 +76,7 @@
end
fun add_catchall ctxt fixes spec =
- let val fqgars = map (split_def ctxt) spec
+ let val fqgars = map (split_def ctxt (K true)) spec
val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
|> AList.lookup (op =) #> the
in
--- a/src/HOL/Tools/Function/function_common.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Fri Sep 10 15:17:44 2010 +0200
@@ -215,7 +215,7 @@
(* Analyzing function equations *)
-fun split_def ctxt geq =
+fun split_def ctxt check_head geq =
let
fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
val qs = Term.strip_qnt_vars "all" geq
@@ -227,8 +227,8 @@
val (head, args) = strip_comb f_args
- val fname = fst (dest_Free head)
- handle TERM _ => error (input_error "Head symbol must not be a bound variable")
+ val fname = fst (dest_Free head) handle TERM _ => ""
+ val _ = check_head fname
in
(fname, qs, gs, args, rhs)
end
@@ -242,11 +242,11 @@
let
fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
- val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
+ fun check_head fname =
+ member (op =) fnames fname orelse
+ input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
- val _ = member (op =) fnames fname
- orelse input_error ("Head symbol of left hand side must be " ^
- plural "" "one out of " fnames ^ commas_quote fnames)
+ val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
val _ = length args > 0 orelse input_error "Function has no arguments:"
--- a/src/HOL/Tools/Function/mutual.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Fri Sep 10 15:17:44 2010 +0200
@@ -72,7 +72,7 @@
fun analyze_eqs ctxt defname fs eqs =
let
val num = length fs
- val fqgars = map (split_def ctxt) eqs
+ val fqgars = map (split_def ctxt (K true)) eqs
val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
|> AList.lookup (op =) #> the
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 10 15:17:44 2010 +0200
@@ -73,9 +73,12 @@
type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
val infer_modes :
- mode_analysis_options -> options -> compilation -> (string * typ) list -> (string * mode list) list ->
- string list -> (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list ->
- theory -> ((moded_clause list pred_mode_table * string list) * theory)
+ mode_analysis_options -> options ->
+ (string -> Predicate_Compile_Aux.mode list) * (string -> Predicate_Compile_Aux.mode list)
+ * (string -> Predicate_Compile_Aux.mode -> bool) -> Proof.context -> (string * typ) list ->
+ (string * mode list) list ->
+ string list -> (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list ->
+ ((moded_clause list pred_mode_table * (string * mode list) list) * string list)
end;
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
@@ -1498,13 +1501,13 @@
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_ext_mode ms)) modes))
else ()
-fun infer_modes mode_analysis_options options compilation preds all_modes param_vs clauses thy =
+fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
+ preds all_modes param_vs clauses =
let
- val ctxt = ProofContext.init_global thy
val collect_errors = false
fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
fun add_needs_random s (false, m) = ((false, m), false)
- | add_needs_random s (true, m) = ((true, m), needs_random ctxt s m)
+ | add_needs_random s (true, m) = ((true, m), needs_random s m)
fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms
val prednames = map fst preds
(* extramodes contains all modes of all constants, should we only use the necessary ones
@@ -1516,18 +1519,16 @@
| predname_of _ = I
val relevant_prednames = fold (fn (_, clauses') =>
fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
+ |> filter_out (fn name => member (op =) prednames name)
val extra_modes =
if #infer_pos_and_neg_modes mode_analysis_options then
let
val pos_extra_modes =
- map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
+ map_filter (fn name => Option.map (pair name) (try lookup_mode name))
relevant_prednames
- |> filter_out (fn (name, _) => member (op =) prednames name)
val neg_extra_modes =
- map_filter (fn name => Option.map (pair name)
- (try (modes_of (negative_compilation_of compilation) ctxt) name))
- relevant_prednames
- |> filter_out (fn (name, _) => member (op =) prednames name)
+ map_filter (fn name => Option.map (pair name) (try lookup_neg_mode name))
+ relevant_prednames
in
map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
@ add_polarity_and_random_bit s false (the (AList.lookup (op =) neg_extra_modes s))))
@@ -1535,9 +1536,8 @@
end
else
map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
- (map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
- relevant_prednames
- |> filter_out (fn (name, _) => member (op =) prednames name))
+ (map_filter (fn name => Option.map (pair name) (try lookup_mode name))
+ relevant_prednames)
val _ = print_extra_modes options extra_modes
val start_modes =
if #infer_pos_and_neg_modes mode_analysis_options then
@@ -1559,11 +1559,11 @@
(fixp (fn modes => map fst (iteration modes)) start_modes, []))
val moded_clauses = map (get_modes_pred' mode_analysis_options ctxt param_vs clauses
(modes @ extra_modes)) modes
- val thy' = fold (fn (s, ms) => if member (op =) (map fst preds) s then
- set_needs_random s (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms) else I)
- modes thy
+ val need_random = fold (fn (s, ms) => if member (op =) (map fst preds) s then
+ cons (s, (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms)) else I)
+ modes []
in
- ((moded_clauses, errors), thy')
+ ((moded_clauses, need_random), errors)
end;
(* term construction *)
@@ -2845,10 +2845,13 @@
val (preds, all_vs, param_vs, all_modes, clauses) =
prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames)
val _ = print_step options "Infering modes..."
- val ((moded_clauses, errors), thy') =
+ val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
+ modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)
+ val ((moded_clauses, needs_random), errors) =
Output.cond_timeit (!Quickcheck.timing) "Infering modes"
(fn _ => infer_modes mode_analysis_options
- options compilation preds all_modes param_vs clauses thy)
+ options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
+ val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
val _ = check_expected_modes preds options modes
val _ = check_proposed_modes preds options modes errors
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Sep 10 15:17:44 2010 +0200
@@ -17,7 +17,7 @@
val tracing : bool Unsynchronized.ref;
val quiet : bool Unsynchronized.ref;
val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
- Proof.context -> bool -> term -> int -> term list option * (bool list * bool);
+ Proof.context -> term -> int -> term list option * (bool list * bool);
(* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
val nrandom : int Unsynchronized.ref;
val debug : bool Unsynchronized.ref;
@@ -310,7 +310,7 @@
(* quickcheck interface functions *)
-fun compile_term' compilation options depth ctxt report t =
+fun compile_term' compilation options depth ctxt t =
let
val c = compile_term compilation options ctxt t
val dummy_report = ([], false)
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Sep 10 15:17:44 2010 +0200
@@ -241,9 +241,13 @@
let
val ctxt0 = Variable.global_thm_context th
val (nnf_th, ctxt) = to_nnf th ctxt0
- val def_th = (* FIXME: to_definitional_cnf_with_quantifiers thy *) nnf_th
- val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th)
- val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt
+ fun aux th =
+ Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th))
+ th ctxt
+ val (cnf_ths, ctxt) =
+ aux nnf_th
+ |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
+ | p => p)
in
cnf_ths |> map introduce_combinators_in_theorem
|> Variable.export ctxt ctxt0
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Sep 10 15:17:44 2010 +0200
@@ -432,21 +432,44 @@
(* INFERENCE RULE: RESOLVE *)
-(*Like RSN, but we rename apart only the type variables. Vars here typically have an index
- of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
- could then fail. See comment on mk_var.*)
-fun resolve_inc_tyvars(tha,i,thb) =
+(* Like RSN, but we rename apart only the type variables. Vars here typically
+ have an index of 1, and the use of RSN would increase this typically to 3.
+ Instantiations of those Vars could then fail. See comment on "mk_var". *)
+fun resolve_inc_tyvars thy tha i thb =
let
- val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
- val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
+ val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+ fun aux tha thb =
+ case Thm.bicompose false (false, tha, nprems_of tha) i thb
+ |> Seq.list_of |> distinct Thm.eq_thm of
+ [th] => th
+ | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
+ [tha, thb])
in
- case distinct Thm.eq_thm ths of
- [th] => th
- | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
+ aux tha thb
+ handle TERM z =>
+ (* The unifier, which is invoked from "Thm.bicompose", will sometimes
+ refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
+ "TERM" exception (with "add_ffpair" as first argument). We then
+ perform unification of the types of variables by hand and try
+ again. We could do this the first time around but this error
+ occurs seldom and we don't want to break existing proofs in subtle
+ ways or slow them down needlessly. *)
+ case [] |> fold (Term.add_vars o prop_of) [tha, thb]
+ |> AList.group (op =)
+ |> maps (fn ((s, _), T :: Ts) =>
+ map (fn T' => (Free (s, T), Free (s, T'))) Ts)
+ |> rpair (Envir.empty ~1)
+ |-> fold (Pattern.unify thy)
+ |> Envir.type_env |> Vartab.dest
+ |> map (fn (x, (S, T)) =>
+ pairself (ctyp_of thy) (TVar (x, S), T)) of
+ [] => raise TERM z
+ | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
end
fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
let
+ val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
@@ -466,7 +489,10 @@
val index_th2 = get_index i_atm prems_th2
handle Empty => raise Fail "Failed to find literal in th2"
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2)
- in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end
+ in
+ resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2
+ i_th2
+ end
end;
(* INFERENCE RULE: REFL *)
@@ -790,6 +816,13 @@
#> map Clausifier.introduce_combinators_in_theorem
#> Meson.finish_cnf
+fun preskolem_tac ctxt st0 =
+ (if exists (Meson.has_too_many_clauses ctxt)
+ (Logic.prems_of_goal (prop_of st0) 1) then
+ cnf.cnfx_rewrite_tac ctxt 1
+ else
+ all_tac) st0
+
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
@@ -802,8 +835,7 @@
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *)
- (maps neg_clausify)
+ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Sep 10 15:17:44 2010 +0200
@@ -162,7 +162,10 @@
output =
case known_failure_in_output output known_failures of
NONE => (case extract_proof proof_delims output of
- "" => ("", SOME MalformedOutput)
+ "" => ("", SOME (if res_code = 0 andalso output = "" then
+ Interrupted
+ else
+ UnknownError))
| proof => if res_code = 0 then (proof, NONE)
else ("", SOME UnknownError))
| SOME failure =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Sep 10 15:17:44 2010 +0200
@@ -91,12 +91,11 @@
val bracket =
implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
^ "]") args)
- val space_bracket = if bracket = "" then "" else " " ^ bracket
val name =
case xref of
- Facts.Fact s => "`" ^ s ^ "`" ^ space_bracket
+ Facts.Fact s => "`" ^ s ^ "`" ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
- | _ => Facts.string_of_ref xref ^ space_bracket
+ | _ => Facts.string_of_ref xref ^ bracket
val multi = length ths > 1
in
(ths, (1, []))
@@ -686,6 +685,26 @@
val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
+fun all_prefixes_of s =
+ map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
+
+(* This is a terrible hack. Free variables are sometimes code as "M__" when they
+ are displayed as "M" and we want to avoid clashes with these. But sometimes
+ it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all
+ free variables. In the worse case scenario, where the fact won't be resolved
+ correctly, the user can fix it manually, e.g., by naming the fact in
+ question. Ideally we would need nothing of it, but backticks just don't work
+ with schematic variables. *)
+fun close_form t =
+ (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
+ |> fold (fn ((s, i), T) => fn (t', taken) =>
+ let val s' = Name.variant taken s in
+ (Term.all T $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
+ s' :: taken)
+ end)
+ (Term.add_vars t [] |> sort_wrt (fst o fst))
+ |> fst
+
fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths =
let
val thy = ProofContext.theory_of ctxt
@@ -700,11 +719,8 @@
clasimpset_rules_of ctxt
else
(Termtab.empty, Termtab.empty, Termtab.empty)
- (* Unnamed nonchained formulas with schematic variables are omitted, because
- they are rejected by the backticks (`...`) parser for some reason. *)
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
- (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) andalso
forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
val unnamed_locals =
union Thm.eq_thm (Facts.props local_facts) chained_ths
@@ -724,8 +740,10 @@
let
val multi = length ths > 1
fun backquotify th =
- "`" ^ Print_Mode.setmp [Print_Mode.input]
- (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
+ "`" ^ Print_Mode.setmp (Print_Mode.input ::
+ filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ()))
+ (Syntax.string_of_term ctxt) (close_form (prop_of th)) ^ "`"
|> String.translate (fn c => if Char.isPrint c then str c else "")
|> simplify_spaces
fun check_thms a =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 10 15:17:44 2010 +0200
@@ -31,6 +31,7 @@
fun string_for_failure Unprovable = "Unprovable."
| string_for_failure TimedOut = "Timed out."
+ | string_for_failure Interrupted = "Interrupted."
| string_for_failure _ = "Unknown error."
fun n_theorems names =
--- a/src/HOL/Tools/hologic.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Sep 10 15:17:44 2010 +0200
@@ -596,9 +596,9 @@
val literalT = Type ("String.literal", []);
-fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
+fun mk_literal s = Const ("String.STR", stringT --> literalT)
$ mk_string s;
-fun dest_literal (Const ("String.literal.STR", _) $ t) =
+fun dest_literal (Const ("String.STR", _) $ t) =
dest_string t
| dest_literal t = raise TERM ("dest_literal", [t]);
--- a/src/HOL/Tools/inductive.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Sep 10 15:17:44 2010 +0200
@@ -789,14 +789,12 @@
val xs = map Free (Variable.variant_frees lthy intr_ts
(mk_names "x" (length Ts) ~~ Ts))
in
- (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
+ (name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs)
(list_comb (rec_const, params @ make_bool_args' bs i @
make_args argTs (xs ~~ Ts)))))
end) (cnames_syn ~~ cs);
val (consts_defs, lthy'') = lthy'
- |> Local_Theory.conceal
- |> fold_map Local_Theory.define specs
- ||> Local_Theory.restore_naming lthy';
+ |> fold_map Local_Theory.define specs;
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
--- a/src/HOL/Tools/inductive_codegen.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Sep 10 15:17:44 2010 +0200
@@ -9,7 +9,7 @@
val add : string option -> int option -> attribute
val test_fn : (int * int * int -> term list option) Unsynchronized.ref
val test_term:
- Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
+ Proof.context -> term -> int -> term list option * (bool list * bool)
val setup : theory -> theory
val quickcheck_setup : theory -> theory
end;
@@ -799,7 +799,7 @@
val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
-fun test_term ctxt report t =
+fun test_term ctxt t =
let
val thy = ProofContext.theory_of ctxt;
val (xs, p) = strip_abs t;
@@ -853,6 +853,6 @@
setup_depth_start #>
setup_random_values #>
setup_size_offset #>
- Quickcheck.add_generator ("SML_inductive", test_term);
+ Context.theory_map (Quickcheck.add_generator ("SML_inductive", test_term));
end;
--- a/src/HOL/Tools/meson.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Sep 10 15:17:44 2010 +0200
@@ -11,7 +11,8 @@
val term_pair_of: indexname * (typ * 'a) -> term * 'a
val flexflex_first_order: thm -> thm
val size_of_subgoals: thm -> int
- val too_many_clauses: Proof.context option -> term -> bool
+ val estimated_num_clauses: Proof.context -> int -> term -> int
+ val has_too_many_clauses: Proof.context -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
val finish_cnf: thm list -> thm list
val presimplify: thm -> thm
@@ -26,8 +27,8 @@
val gocls: thm list -> thm list
val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic
val MESON:
- (int -> tactic) -> (thm list -> thm list) -> (thm list -> tactic)
- -> Proof.context -> int -> tactic
+ tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context
+ -> int -> tactic
val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
val safe_best_meson_tac: Proof.context -> int -> tactic
val depth_meson_tac: Proof.context -> int -> tactic
@@ -262,13 +263,10 @@
(*** The basic CNF transformation ***)
-fun too_many_clauses ctxto t =
+fun estimated_num_clauses ctxt bound t =
let
- val max_cl = case ctxto of SOME ctxt => Config.get ctxt max_clauses
- | NONE => max_clauses_default
-
- fun sum x y = if x < max_cl andalso y < max_cl then x+y else max_cl;
- fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
+ fun sum x y = if x < bound andalso y < bound then x+y else bound
+ fun prod x y = if x < bound andalso y < bound then x*y else bound
(*Estimate the number of clauses in order to detect infeasible theorems*)
fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
@@ -292,9 +290,12 @@
| signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t
| signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t
| signed_nclauses _ _ = 1; (* literal *)
- in
- signed_nclauses true t >= max_cl
- end;
+ in signed_nclauses true t end
+
+fun has_too_many_clauses ctxt t =
+ let val max_cl = Config.get ctxt max_clauses in
+ estimated_num_clauses ctxt (max_cl + 1) t > max_cl
+ end
(*Replaces universally quantified variables by FREE variables -- because
assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
@@ -355,8 +356,8 @@
in Seq.list_of (tac (th RS disj_forward)) @ ths end
| _ => nodups ctxt th :: ths (*no work to do*)
and cnf_nil th = cnf_aux (th,[])
- val cls =
- if too_many_clauses (SOME ctxt) (concl_of th)
+ val cls =
+ if has_too_many_clauses ctxt (concl_of th)
then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
else cnf_aux (th,ths)
in (cls, !ctxtr) end;
@@ -604,9 +605,9 @@
SELECT_GOAL
(EVERY [Object_Logic.atomize_prems_tac 1,
rtac ccontr 1,
+ preskolem_tac,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
- EVERY1 [preskolem_tac,
- skolemize_prems_tac ctxt negs,
+ EVERY1 [skolemize_prems_tac ctxt negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
@@ -615,7 +616,7 @@
(*ths is a list of additional clauses (HOL disjunctions) to use.*)
fun best_meson_tac sizef =
- MESON (K all_tac) make_clauses
+ MESON all_tac make_clauses
(fn cls =>
THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
(has_fewer_prems 1, sizef)
@@ -629,7 +630,7 @@
(** Depth-first search version **)
val depth_meson_tac =
- MESON (K all_tac) make_clauses
+ MESON all_tac make_clauses
(fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
@@ -649,7 +650,7 @@
fun iter_deepen_prolog_tac horns =
ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
-fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON (K all_tac) make_clauses
+fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses
(fn cls =>
(case (gocls (cls @ ths)) of
[] => no_tac (*no goal clauses*)
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Sep 10 15:17:44 2010 +0200
@@ -14,7 +14,7 @@
-> (string * sort -> string * sort) option
val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
- theory -> bool -> term -> int -> term list option * (bool list * bool)
+ Proof.context -> term -> int -> term list option * (bool list * bool)
val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
val eval_report_ref:
(unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref
@@ -380,10 +380,11 @@
Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
end
-fun compile_generator_expr thy report t =
+fun compile_generator_expr ctxt t =
let
val Ts = (map snd o fst o strip_abs) t;
- in if report then
+ val thy = ProofContext.theory_of ctxt
+ in if Quickcheck.report ctxt then
let
val t' = mk_reporting_generator_expr thy t Ts;
val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
@@ -404,6 +405,7 @@
val setup =
Datatype.interpretation ensure_random_datatype
#> Code_Target.extend_target (target, (Code_Eval.target, K I))
- #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of);
+ #> Context.theory_map
+ (Quickcheck.add_generator ("code", compile_generator_expr));
end;
--- a/src/HOL/UNITY/Comp/AllocBase.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/ZF/HOLZF.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/ex/BT.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/ex/Chinese.thy Fri Sep 10 15:17:44 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 Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/ex/Hebrew.thy Fri Sep 10 15:17:44 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/Numeral.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Fri Sep 10 15:17:44 2010 +0200
@@ -1086,7 +1086,7 @@
code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
(Scala infixl 5 "==")
(Eval infixl 6 "=")
--- a/src/HOL/ex/ReflectionEx.thy Fri Sep 10 15:16:51 2010 +0200
+++ b/src/HOL/ex/ReflectionEx.thy Fri Sep 10 15:17:44 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
--- a/src/Pure/codegen.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/Pure/codegen.ML Fri Sep 10 15:17:44 2010 +0200
@@ -76,7 +76,7 @@
val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
val test_fn: (int -> term list option) Unsynchronized.ref
- val test_term: Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
+ val test_term: Proof.context -> term -> int -> term list option * (bool list * bool)
val eval_result: (unit -> term) Unsynchronized.ref
val eval_term: theory -> term -> term
val evaluation_conv: cterm -> thm
@@ -869,7 +869,7 @@
val test_fn : (int -> term list option) Unsynchronized.ref =
Unsynchronized.ref (fn _ => NONE);
-fun test_term ctxt report t =
+fun test_term ctxt t =
let
val thy = ProofContext.theory_of ctxt;
val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
--- a/src/Tools/quickcheck.ML Fri Sep 10 15:16:51 2010 +0200
+++ b/src/Tools/quickcheck.ML Fri Sep 10 15:17:44 2010 +0200
@@ -17,12 +17,14 @@
datatype test_params = Test_Params of
{ size: int, iterations: int, default_type: typ list, no_assms: bool,
expect : expectation, report: bool, quiet : bool};
- val test_params_of: theory -> test_params
+ val test_params_of: Proof.context -> test_params
+ val report : Proof.context -> bool
+ val set_reporting : bool -> Proof.context -> Proof.context
val add_generator:
- string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
- -> theory -> theory
+ string * (Proof.context -> term -> int -> term list option * (bool list * bool))
+ -> Context.generic -> Context.generic
(* testing terms and proof states *)
- val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term ->
+ val gen_test_term: Proof.context -> bool -> string option -> int -> int -> term ->
(string * term) list option * ((string * int) list * ((int * report list) list) option)
val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
(string * term) list option
@@ -99,10 +101,10 @@
((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2)));
-structure Data = Theory_Data
+structure Data = Generic_Data
(
type T =
- (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
+ (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
* test_params;
val empty = ([], Test_Params
{ size = 10, iterations = 100, default_type = [], no_assms = false,
@@ -113,25 +115,32 @@
merge_test_params (params1, params2));
);
-val test_params_of = snd o Data.get;
+val test_params_of = snd o Data.get o Context.Proof;
+
+val report = snd o fst o snd o snd o dest_test_params o test_params_of
+
+fun map_report f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
+ make_test_params ((size, iterations), ((default_type, no_assms), ((expect, f report), quiet)));
+
+fun set_reporting report = Context.proof_map (Data.map (apsnd (map_report (K report))))
val add_generator = Data.map o apfst o AList.update (op =);
(* generating tests *)
fun mk_tester_select name ctxt =
- case AList.lookup (op =) ((fst o Data.get o ProofContext.theory_of) ctxt) name
+ case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name
of NONE => error ("No such quickcheck generator: " ^ name)
| SOME generator => generator ctxt;
-fun mk_testers ctxt report t =
- (map snd o fst o Data.get o ProofContext.theory_of) ctxt
- |> map_filter (fn generator => try (generator ctxt report) t);
+fun mk_testers ctxt t =
+ (map snd o fst o Data.get o Context.Proof) ctxt
+ |> map_filter (fn generator => try (generator ctxt) t);
-fun mk_testers_strict ctxt report t =
+fun mk_testers_strict ctxt t =
let
- val generators = ((map snd o fst o Data.get o ProofContext.theory_of) ctxt)
- val testers = map (fn generator => Exn.capture (generator ctxt report) t) generators;
+ val generators = ((map snd o fst o Data.get o Context.Proof) ctxt)
+ val testers = map (fn generator => Exn.capture (generator ctxt) t) generators;
in if forall (is_none o Exn.get_result) testers
then [(Exn.release o snd o split_last) testers]
else map_filter Exn.get_result testers
@@ -156,13 +165,13 @@
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, (description, time)) end
-fun gen_test_term ctxt quiet report generator_name size i t =
+fun gen_test_term ctxt quiet generator_name size i t =
let
val (names, t') = prep_test_term t;
val (testers, comp_time) = cpu_time "quickcheck compilation"
(fn () => (case generator_name
- of NONE => if quiet then mk_testers ctxt report t' else mk_testers_strict ctxt report t'
- | SOME name => [mk_tester_select name ctxt report t']));
+ of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
+ | SOME name => [mk_tester_select name ctxt t']));
fun iterate f 0 report = (NONE, report)
| iterate f j report =
let
@@ -190,11 +199,13 @@
(fn result => case result of NONE => NONE
| SOME ts => SOME (names ~~ ts)) (with_size 1 []))
in
- (result, ([exec_time, comp_time], if report then SOME reports else NONE))
+ (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
end;
fun test_term ctxt quiet generator_name size i t =
- fst (gen_test_term ctxt quiet false generator_name size i t)
+ ctxt
+ |> set_reporting false
+ |> (fn ctxt' => fst (gen_test_term ctxt' quiet generator_name size i t))
exception WELLSORTED of string
@@ -216,7 +227,7 @@
datatype wellsorted_error = Wellsorted_Error of string | Term of term
-fun test_goal quiet report generator_name size iterations default_Ts no_assms insts i state =
+fun test_goal quiet generator_name size iterations default_Ts no_assms insts i state =
let
val lthy = Proof.context_of state;
val thy = Proof.theory_of state;
@@ -249,7 +260,7 @@
case f t of
(SOME res, report) => (SOME res, rev (report :: reports))
| (NONE, report) => collect_results f (report :: reports) ts
- in collect_results (gen_test_term lthy quiet report generator_name size iterations) [] correct_inst_goals end;
+ in collect_results (gen_test_term lthy quiet generator_name size iterations) [] correct_inst_goals end;
(* pretty printing *)
@@ -296,9 +307,11 @@
let
val ctxt = Proof.context_of state;
val Test_Params {size, iterations, default_type, no_assms, ...} =
- (snd o Data.get o Proof.theory_of) state;
+ (snd o Data.get o Context.Proof) ctxt;
val res =
- try (test_goal true false NONE size iterations default_type no_assms [] 1) state;
+ state
+ |> Proof.map_context (set_reporting false)
+ |> try (test_goal true NONE size iterations default_type no_assms [] 1);
in
case res of
NONE => (false, state)
@@ -353,23 +366,24 @@
fun quickcheck_params_cmd args thy =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = ProofContext.init_global thy
val f = fold (parse_test_param ctxt) args;
in
thy
- |> (Data.map o apsnd o map_test_params) f
+ |> (Context.theory_map o Data.map o apsnd o map_test_params) f
end;
fun gen_quickcheck args i state =
let
- val thy = Proof.theory_of state;
val ctxt = Proof.context_of state;
- val default_params = (dest_test_params o snd o Data.get) thy;
+ val default_params = (dest_test_params o snd o Data.get o Context.Proof) ctxt;
val f = fold (parse_test_param_inst ctxt) args;
val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) =
f (default_params, (NONE, []));
in
- test_goal quiet report generator_name size iterations default_type no_assms insts i state
+ state
+ |> Proof.map_context (set_reporting report)
+ |> test_goal quiet generator_name size iterations default_type no_assms insts i
|> tap (fn (SOME x, _) => if expect = No_Counterexample then
error ("quickcheck expected to find no counterexample but found one") else ()
| (NONE, _) => if expect = Counterexample then