--- a/NEWS Thu Jun 10 12:08:33 2010 +0200
+++ b/NEWS Thu Jun 10 12:28:27 2010 +0200
@@ -4,6 +4,26 @@
New in this Isabelle version
----------------------------
+*** HOL ***
+
+* Some previously unqualified names have been qualified:
+
+ types
+ nat ~> Nat.nat
+ * ~> Product_Type,*
+ + ~> Sum_Type.+
+
+ constants
+ Ball ~> Set.Ball
+ Bex ~> Set.Bex
+ Suc ~> Nat.Suc
+ Pair ~> Product_Type.Pair
+ fst ~> Product_Type.fst
+ snd ~> Product_Type.snd
+ split ~> Product_Type.split
+ curry ~> Product_Type.curry
+
+INCOMPATIBILITY.
New in Isabelle2009-2 (June 2010)
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Jun 10 12:28:27 2010 +0200
@@ -3440,7 +3440,7 @@
fun dest_float (@{const "Float"} $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
fun dest_ivl (Const (@{const_name "Some"}, _) $
- (Const (@{const_name "Pair"}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
+ (Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
| dest_ivl (Const (@{const_name "None"}, _)) = NONE
| dest_ivl t = raise TERM ("dest_result", [t])
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Jun 10 12:28:27 2010 +0200
@@ -2964,7 +2964,7 @@
fun rz rT = Const(@{const_name Groups.zero},rT);
fun dest_nat t = case t of
- Const ("Suc",_)$t' => 1 + dest_nat t'
+ Const (@{const_name Suc}, _) $ t' => 1 + dest_nat t'
| _ => (snd o HOLogic.dest_number) t;
fun num_of_term m t =
--- a/src/HOL/Hoare/hoare_tac.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Thu Jun 10 12:28:27 2010 +0200
@@ -41,9 +41,9 @@
else let val (n, T) = dest_Free x ;
val z = mk_bodyC xs;
val T2 = case z of Free(_, T) => T
- | Const ("Pair", Type ("fun", [_, Type
+ | Const (@{const_name Pair}, Type ("fun", [_, Type
("fun", [_, T])])) $ _ $ _ => T;
- in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
+ in Const (@{const_name Pair}, [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
(** maps a subgoal of the form:
VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jun 10 12:28:27 2010 +0200
@@ -123,7 +123,7 @@
import_theory pair;
type_maps
- prod > "*";
+ prod > "Product_Type.*";
const_maps
"," > Pair
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jun 10 12:28:27 2010 +0200
@@ -38,9 +38,9 @@
bool > bool
fun > fun
N_1 > Product_Type.unit
- prod > "*"
- num > nat
- sum > "+"
+ prod > "Product_Type.*"
+ num > Nat.nat
+ sum > "Sum_Type.+"
(* option > Datatype.option*);
const_renames
--- a/src/HOL/Import/HOL/num.imp Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Import/HOL/num.imp Thu Jun 10 12:28:27 2010 +0200
@@ -3,10 +3,10 @@
import_segment "hol4"
type_maps
- "num" > "nat"
+ "num" > "Nat.nat"
const_maps
- "SUC" > "Suc"
+ "SUC" > "Nat.Suc"
"0" > "0" :: "nat"
thm_maps
--- a/src/HOL/Import/HOL/pair.imp Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Import/HOL/pair.imp Thu Jun 10 12:28:27 2010 +0200
@@ -7,17 +7,17 @@
"LEX" > "LEX_def"
type_maps
- "prod" > "*"
+ "prod" > "Product_Type.*"
const_maps
- "pair_case" > "split"
- "UNCURRY" > "split"
- "SND" > "snd"
+ "pair_case" > "Product_Type.split"
+ "UNCURRY" > "Product_Type.split"
+ "FST" > "Product_Type.fst"
+ "SND" > "Product_Type.snd"
"RPROD" > "HOL4Base.pair.RPROD"
"LEX" > "HOL4Base.pair.LEX"
- "FST" > "fst"
- "CURRY" > "curry"
- "," > "Pair"
+ "CURRY" > "Product_Type.curry"
+ "," > "Product_Type.Pair"
"##" > "prod_fun"
thm_maps
--- a/src/HOL/Import/HOLLight/hollight.imp Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Thu Jun 10 12:28:27 2010 +0200
@@ -6,9 +6,9 @@
"sum" > "+"
"recspace" > "HOLLight.hollight.recspace"
"real" > "HOLLight.hollight.real"
- "prod" > "*"
+ "prod" > "Product_Type.*"
"option" > "HOLLight.hollight.option"
- "num" > "nat"
+ "num" > "Nat.nat"
"nadd" > "HOLLight.hollight.nadd"
"list" > "HOLLight.hollight.list"
"int" > "HOLLight.hollight.int"
@@ -128,10 +128,10 @@
"TL" > "HOLLight.hollight.TL"
"T" > "True"
"SURJ" > "HOLLight.hollight.SURJ"
- "SUC" > "Suc"
+ "SUC" > "Nat.Suc"
"SUBSET" > "HOLLight.hollight.SUBSET"
"SOME" > "HOLLight.hollight.SOME"
- "SND" > "snd"
+ "SND" > "Product_Type.snd"
"SING" > "HOLLight.hollight.SING"
"SETSPEC" > "HOLLight.hollight.SETSPEC"
"REVERSE" > "HOLLight.hollight.REVERSE"
@@ -188,7 +188,7 @@
"GSPEC" > "HOLLight.hollight.GSPEC"
"GEQ" > "HOLLight.hollight.GEQ"
"GABS" > "HOLLight.hollight.GABS"
- "FST" > "fst"
+ "FST" > "Product_Type.fst"
"FNIL" > "HOLLight.hollight.FNIL"
"FINREC" > "HOLLight.hollight.FINREC"
"FINITE" > "HOLLight.hollight.FINITE"
@@ -239,7 +239,7 @@
"<" > "HOLLight.hollight.<"
"/\\" > "op &"
"-" > "Groups.minus" :: "nat => nat => nat"
- "," > "Pair"
+ "," > "Product_Type.Pair"
"+" > "Groups.plus" :: "nat => nat => nat"
"*" > "Groups.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
--- a/src/HOL/Inductive.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Inductive.thy Thu Jun 10 12:28:27 2010 +0200
@@ -9,7 +9,6 @@
uses
("Tools/inductive.ML")
"Tools/dseq.ML"
- ("Tools/inductive_codegen.ML")
"Tools/Datatype/datatype_aux.ML"
"Tools/Datatype/datatype_prop.ML"
"Tools/Datatype/datatype_case.ML"
@@ -286,9 +285,6 @@
use "Tools/old_primrec.ML"
use "Tools/primrec.ML"
-use "Tools/inductive_codegen.ML"
-setup InductiveCodegen.setup
-
text{* Lambda-abstractions with pattern matching: *}
syntax
--- a/src/HOL/Library/Binomial.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Library/Binomial.thy Thu Jun 10 12:28:27 2010 +0200
@@ -235,7 +235,7 @@
have eq: "insert 0 {1 .. n} = {0..n}" by auto
have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
(\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
- apply (rule setprod_reindex_cong[where f = "Suc"])
+ apply (rule setprod_reindex_cong [where f = Suc])
using n0 by (auto simp add: expand_fun_eq field_simps)
have ?thesis apply (simp add: pochhammer_def)
unfolding setprod_insert[OF th0, unfolded eq]
--- a/src/HOL/Library/Countable.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Library/Countable.thy Thu Jun 10 12:28:27 2010 +0200
@@ -70,7 +70,7 @@
text {* Sums *}
-instance "+":: (countable, countable) countable
+instance "+" :: (countable, countable) countable
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
| Inr b \<Rightarrow> to_nat (True, to_nat b))"])
(simp split: sum.split_asm)
--- a/src/HOL/Library/Diagonalize.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Library/Diagonalize.thy Thu Jun 10 12:28:27 2010 +0200
@@ -81,7 +81,7 @@
done
-subsection {* Diagonalization: an injective embedding of two @{typ "nat"}s to one @{typ "nat"} *}
+subsection {* Diagonalization: an injective embedding of two @{typ nat}s to one @{typ nat} *}
definition diagonalize :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"diagonalize m n = sum (m + n) + m"
--- a/src/HOL/Library/Efficient_Nat.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Jun 10 12:28:27 2010 +0200
@@ -11,7 +11,7 @@
text {*
When generating code for functions on natural numbers, the
canonical representation using @{term "0::nat"} and
- @{term "Suc"} is unsuitable for computations involving large
+ @{term Suc} is unsuitable for computations involving large
numbers. The efficiency of the generated code can be improved
drastically by implementing natural numbers by target-language
integers. To do this, just include this theory.
@@ -362,7 +362,7 @@
Since natural numbers are implemented
using integers in ML, the coercion function @{const "of_nat"} of type
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
- For the @{const "nat"} function for converting an integer to a natural
+ For the @{const nat} function for converting an integer to a natural
number, we give a specific implementation using an ML function that
returns its input value, provided that it is non-negative, and otherwise
returns @{text "0"}.
--- a/src/HOL/Library/Formal_Power_Series.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Thu Jun 10 12:28:27 2010 +0200
@@ -2031,7 +2031,7 @@
done
also have "\<dots> = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
unfolding fps_deriv_nth
- apply (rule setsum_reindex_cong[where f="Suc"])
+ apply (rule setsum_reindex_cong [where f = Suc])
by (auto simp add: mult_assoc)
finally have th0: "(fps_deriv (a oo b))$n = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" .
--- a/src/HOL/Library/SML_Quickcheck.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy Thu Jun 10 12:28:27 2010 +0200
@@ -6,7 +6,7 @@
begin
setup {*
- InductiveCodegen.quickcheck_setup #>
+ Inductive_Codegen.quickcheck_setup #>
Quickcheck.add_generator ("SML", Codegen.test_term)
*}
--- a/src/HOL/Modelcheck/mucke_oracle.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu Jun 10 12:28:27 2010 +0200
@@ -832,7 +832,7 @@
(* OUTPUT - relevant *)
(* transforms constructor term to a mucke-suitable output *)
-fun term_OUTPUT sg (Const("Pair",_) $ a $ b) =
+fun term_OUTPUT sg (Const(@{const_name Pair},_) $ a $ b) =
(term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
term_OUTPUT sg (a $ b) = (term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
term_OUTPUT sg (Const(s,t)) = post_last_dot s |
--- a/src/HOL/Nat.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Nat.thy Thu Jun 10 12:28:27 2010 +0200
@@ -39,16 +39,11 @@
Zero_RepI: "Nat Zero_Rep"
| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
-global
-
-typedef (open Nat)
- nat = Nat
+typedef (open Nat) nat = Nat
by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
definition Suc :: "nat => nat" where
- Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
-
-local
+ "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
instantiation nat :: zero
begin
@@ -1457,8 +1452,7 @@
end
lemma mono_iff_le_Suc: "mono f = (\<forall>n. f n \<le> f (Suc n))"
-unfolding mono_def
-by (auto intro:lift_Suc_mono_le[of f])
+ unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
lemma mono_nat_linear_lb:
"(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"
--- a/src/HOL/Nominal/Examples/Support.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Nominal/Examples/Support.thy Thu Jun 10 12:28:27 2010 +0200
@@ -31,7 +31,7 @@
text {* An atom is either even or odd. *}
lemma even_or_odd:
- fixes n::"nat"
+ fixes n :: nat
shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)"
by (induct n) (presburger)+
--- a/src/HOL/Nominal/nominal_atoms.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Jun 10 12:28:27 2010 +0200
@@ -543,7 +543,7 @@
|> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
|> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
|> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
- |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+ |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
|> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
(pt_proof pt_thm_nprod)
|> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
@@ -604,7 +604,7 @@
in
thy
|> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
- |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
+ |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
|> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
(fs_proof fs_thm_nprod)
|> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
@@ -686,7 +686,7 @@
in
thy'
|> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
- |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
+ |> AxClass.prove_arity (@{type_name "*"}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
|> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
|> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jun 10 12:28:27 2010 +0200
@@ -121,7 +121,7 @@
val dj_cp = thm "dj_cp";
-fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]),
+fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [T, _])]),
Type ("fun", [_, U])])) = (T, U);
fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
--- a/src/HOL/Nominal/nominal_permeq.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Jun 10 12:28:27 2010 +0200
@@ -103,7 +103,7 @@
case redex of
(* case pi o (f x) == (pi o f) (pi o x) *)
(Const("Nominal.perm",
- Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
+ Type("fun",[Type("List.list",[Type(@{type_name "*"},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
(if (applicable_app f) then
let
val name = Long_Name.base_name n
@@ -190,8 +190,8 @@
fun perm_compose_simproc' sg ss redex =
(case redex of
(Const ("Nominal.perm", Type ("fun", [Type ("List.list",
- [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm",
- Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $
+ [Type (@{type_name "*"}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm",
+ Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [U as Type (uname,_),_])]),_])) $
pi2 $ t)) =>
let
val tname' = Long_Name.base_name tname
--- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Jun 10 12:28:27 2010 +0200
@@ -103,7 +103,7 @@
let fun get_pi_aux s =
(case s of
(Const (@{const_name "perm"} ,typrm) $
- (Var (pi,typi as Type(@{type_name "list"}, [Type ("*", [Type (tyatm,[]),_])]))) $
+ (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name "*"}, [Type (tyatm,[]),_])]))) $
(Var (n,ty))) =>
let
(* FIXME: this should be an operation the library *)
--- a/src/HOL/Product_Type.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Product_Type.thy Thu Jun 10 12:28:27 2010 +0200
@@ -9,6 +9,7 @@
imports Typedef Inductive Fun
uses
("Tools/split_rule.ML")
+ ("Tools/inductive_codegen.ML")
("Tools/inductive_set.ML")
begin
@@ -128,13 +129,10 @@
definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
"Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
-global
-
-typedef (Prod)
- ('a, 'b) "*" (infixr "*" 20)
- = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
+typedef (prod) ('a, 'b) "*" (infixr "*" 20)
+ = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
proof
- fix a b show "Pair_Rep a b \<in> ?Prod"
+ fix a b show "Pair_Rep a b \<in> ?prod"
by rule+
qed
@@ -143,35 +141,27 @@
type_notation (HTML output)
"*" ("(_ \<times>/ _)" [21, 20] 20)
-consts
- Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
-
-local
-
-defs
- Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)"
+definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
+ "Pair a b = Abs_prod (Pair_Rep a b)"
rep_datatype (prod) Pair proof -
fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
assume "\<And>a b. P (Pair a b)"
- then show "P p" by (cases p) (auto simp add: Prod_def Pair_def Pair_Rep_def)
+ then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
next
fix a c :: 'a and b d :: 'b
have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
by (auto simp add: Pair_Rep_def expand_fun_eq)
- moreover have "Pair_Rep a b \<in> Prod" and "Pair_Rep c d \<in> Prod"
- by (auto simp add: Prod_def)
+ moreover have "Pair_Rep a b \<in> prod" and "Pair_Rep c d \<in> prod"
+ by (auto simp add: prod_def)
ultimately show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
- by (simp add: Pair_def Abs_Prod_inject)
+ by (simp add: Pair_def Abs_prod_inject)
qed
subsubsection {* Tuple syntax *}
-global consts
- split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
-
-local defs
+definition split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
split_prod_case: "split == prod_case"
text {*
@@ -393,13 +383,11 @@
lemma surj_pair [simp]: "EX x y. p = (x, y)"
by (cases p) simp
-global consts
- fst :: "'a \<times> 'b \<Rightarrow> 'a"
- snd :: "'a \<times> 'b \<Rightarrow> 'b"
+definition fst :: "'a \<times> 'b \<Rightarrow> 'a" where
+ "fst p = (case p of (a, b) \<Rightarrow> a)"
-local defs
- fst_def: "fst p == case p of (a, b) \<Rightarrow> a"
- snd_def: "snd p == case p of (a, b) \<Rightarrow> b"
+definition snd :: "'a \<times> 'b \<Rightarrow> 'b" where
+ "snd p = (case p of (a, b) \<Rightarrow> b)"
lemma fst_conv [simp, code]: "fst (a, b) = a"
unfolding fst_def by simp
@@ -788,11 +776,8 @@
subsubsection {* Derived operations *}
-global consts
- curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
-
-local defs
- curry_def: "curry == (%c x y. c (Pair x y))"
+definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
+ "curry = (\<lambda>c x y. c (x, y))"
lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
by (simp add: curry_def)
@@ -1192,6 +1177,9 @@
subsection {* Inductively defined sets *}
+use "Tools/inductive_codegen.ML"
+setup Inductive_Codegen.setup
+
use "Tools/inductive_set.ML"
setup Inductive_Set.setup
--- a/src/HOL/Set.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Set.thy Thu Jun 10 12:28:27 2010 +0200
@@ -151,17 +151,11 @@
supset_eq ("op \<supseteq>") and
supset_eq ("(_/ \<supseteq> _)" [50, 51] 50)
-global
-
-consts
- Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers"
- Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers"
+definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)" -- "bounded universal quantifiers"
-local
-
-defs
- Ball_def: "Ball A P == ALL x. x:A --> P(x)"
- Bex_def: "Bex A P == EX x. x:A & P(x)"
+definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)" -- "bounded existential quantifiers"
syntax
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
--- a/src/HOL/SetInterval.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/SetInterval.thy Thu Jun 10 12:28:27 2010 +0200
@@ -770,7 +770,7 @@
qed
lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
-apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"])
+apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x - Suc 0"])
apply simp
apply fastsimp
apply auto
--- a/src/HOL/Sum_Type.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Sum_Type.thy Thu Jun 10 12:28:27 2010 +0200
@@ -17,21 +17,17 @@
definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
"Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
-global
-
-typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
+typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
by auto
-local
-
-lemma Inl_RepI: "Inl_Rep a \<in> Sum"
- by (auto simp add: Sum_def)
+lemma Inl_RepI: "Inl_Rep a \<in> sum"
+ by (auto simp add: sum_def)
-lemma Inr_RepI: "Inr_Rep b \<in> Sum"
- by (auto simp add: Sum_def)
+lemma Inr_RepI: "Inr_Rep b \<in> sum"
+ by (auto simp add: sum_def)
-lemma inj_on_Abs_Sum: "A \<subseteq> Sum \<Longrightarrow> inj_on Abs_Sum A"
- by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto
+lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A"
+ by (rule inj_on_inverseI, rule Abs_sum_inverse) auto
lemma Inl_Rep_inject: "inj_on Inl_Rep A"
proof (rule inj_onI)
@@ -49,28 +45,28 @@
by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq)
definition Inl :: "'a \<Rightarrow> 'a + 'b" where
- "Inl = Abs_Sum \<circ> Inl_Rep"
+ "Inl = Abs_sum \<circ> Inl_Rep"
definition Inr :: "'b \<Rightarrow> 'a + 'b" where
- "Inr = Abs_Sum \<circ> Inr_Rep"
+ "Inr = Abs_sum \<circ> Inr_Rep"
lemma inj_Inl [simp]: "inj_on Inl A"
-by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI)
+by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
using inj_Inl by (rule injD)
lemma inj_Inr [simp]: "inj_on Inr A"
-by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_Sum Inr_RepI)
+by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
using inj_Inr by (rule injD)
lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
proof -
- from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> Sum" by auto
- with inj_on_Abs_Sum have "inj_on Abs_Sum {Inl_Rep a, Inr_Rep b}" .
- with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_Sum (Inl_Rep a) \<noteq> Abs_Sum (Inr_Rep b)" by auto
+ from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
+ with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
+ with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" by auto
then show ?thesis by (simp add: Inl_def Inr_def)
qed
@@ -81,10 +77,10 @@
assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
shows P
-proof (rule Abs_Sum_cases [of s])
+proof (rule Abs_sum_cases [of s])
fix f
- assume "s = Abs_Sum f" and "f \<in> Sum"
- with assms show P by (auto simp add: Sum_def Inl_def Inr_def)
+ assume "s = Abs_sum f" and "f \<in> sum"
+ with assms show P by (auto simp add: sum_def Inl_def Inr_def)
qed
rep_datatype (sum) Inl Inr
--- a/src/HOL/Tools/Function/function_lib.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Thu Jun 10 12:28:27 2010 +0200
@@ -24,7 +24,7 @@
case vars of
(Free v) => lambda (Free v) t
| (Var v) => lambda (Var v) t
- | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
+ | (Const (@{const_name Pair}, Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
| _ => raise Match
--- a/src/HOL/Tools/Function/measure_functions.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML Thu Jun 10 12:28:27 2010 +0200
@@ -39,17 +39,17 @@
fun constant_0 T = Abs ("x", T, HOLogic.zero)
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
-fun mk_funorder_funs (Type ("+", [fT, sT])) =
+fun mk_funorder_funs (Type (@{type_name "+"}, [fT, sT])) =
map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
@ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
| mk_funorder_funs T = [ constant_1 T ]
-fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
+fun mk_ext_base_funs ctxt (Type (@{type_name "+"}, [fT, sT])) =
map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
(mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
| mk_ext_base_funs ctxt T = find_measures ctxt T
-fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
+fun mk_all_measure_funs ctxt (T as Type (@{type_name "+"}, _)) =
mk_ext_base_funs ctxt T @ mk_funorder_funs T
| mk_all_measure_funs ctxt T = find_measures ctxt T
--- a/src/HOL/Tools/Function/sum_tree.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML Thu Jun 10 12:28:27 2010 +0200
@@ -17,7 +17,7 @@
{left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
(* Sum types *)
-fun mk_sumT LT RT = Type ("+", [LT, RT])
+fun mk_sumT LT RT = Type (@{type_name "+"}, [LT, RT])
fun mk_sumcase TL TR T l r =
Const (@{const_name sum.sum_case},
(TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
@@ -27,18 +27,18 @@
fun mk_inj ST n i =
access_top_down
{ init = (ST, I : term -> term),
- left = (fn (T as Type ("+", [LT, RT]), inj) =>
+ left = (fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
(LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
- right =(fn (T as Type ("+", [LT, RT]), inj) =>
+ right =(fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
(RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
|> snd
fun mk_proj ST n i =
access_top_down
{ init = (ST, I : term -> term),
- left = (fn (T as Type ("+", [LT, RT]), proj) =>
+ left = (fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
(LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
- right =(fn (T as Type ("+", [LT, RT]), proj) =>
+ right =(fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
(RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
|> snd
--- a/src/HOL/Tools/Function/termination.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Thu Jun 10 12:28:27 2010 +0200
@@ -106,7 +106,7 @@
end
(* compute list of types for nodes *)
-fun node_types sk T = dest_tree (fn Type ("+", [LT, RT]) => (LT, RT)) sk T |> map snd
+fun node_types sk T = dest_tree (fn Type (@{type_name "+"}, [LT, RT]) => (LT, RT)) sk T |> map snd
(* find index and raw term *)
fun dest_inj (SLeaf i) trm = (i, trm)
@@ -148,7 +148,7 @@
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _)
+ val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
= Term.strip_qnt_body "Ex" c
in cons r o cons l end
in
@@ -185,7 +185,7 @@
val vs = Term.strip_qnt_vars "Ex" c
(* FIXME: throw error "dest_call" for malformed terms *)
- val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+ val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
= Term.strip_qnt_body "Ex" c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 10 12:28:27 2010 +0200
@@ -265,12 +265,12 @@
fun replace_ho_args mode hoargs ts =
let
fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs')
- | replace (Pair (m1, m2), Const ("Pair", T) $ t1 $ t2) hoargs =
+ | replace (Pair (m1, m2), Const (@{const_name Pair}, T) $ t1 $ t2) hoargs =
let
val (t1', hoargs') = replace (m1, t1) hoargs
val (t2', hoargs'') = replace (m2, t2) hoargs'
in
- (Const ("Pair", T) $ t1' $ t2', hoargs'')
+ (Const (@{const_name Pair}, T) $ t1' $ t2', hoargs'')
end
| replace (_, t) hoargs = (t, hoargs)
in
@@ -290,7 +290,7 @@
fun split_map_mode f mode ts =
let
fun split_arg_mode' (m as Fun _) t = f m t
- | split_arg_mode' (Pair (m1, m2)) (Const ("Pair", _) $ t1 $ t2) =
+ | split_arg_mode' (Pair (m1, m2)) (Const (@{const_name Pair}, _) $ t1 $ t2) =
let
val (i1, o1) = split_arg_mode' m1 t1
val (i2, o2) = split_arg_mode' m2 t2
@@ -334,7 +334,7 @@
end
| fold_map_aterms_prodT comb f T s = f T s
-fun map_filter_prod f (Const ("Pair", _) $ t1 $ t2) =
+fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) =
comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
| map_filter_prod f t = f t
@@ -561,8 +561,8 @@
(* combinators to apply a function to all basic parts of nested products *)
-fun map_products f (Const ("Pair", T) $ t1 $ t2) =
- Const ("Pair", T) $ map_products f t1 $ map_products f t2
+fun map_products f (Const (@{const_name Pair}, T) $ t1 $ t2) =
+ Const (@{const_name Pair}, T) $ map_products f t1 $ map_products f t2
| map_products f t = f t
(* split theorems of case expressions *)
@@ -756,7 +756,7 @@
(case HOLogic.strip_tupleT (fastype_of arg) of
(Ts as _ :: _ :: _) =>
let
- fun rewrite_arg' (Const (@{const_name "Pair"}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
+ fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
(args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
| rewrite_arg' (t, Type (@{type_name "*"}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 10 12:28:27 2010 +0200
@@ -117,7 +117,7 @@
end;
fun dest_randomT (Type ("fun", [@{typ Random.seed},
- Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
+ Type (@{type_name "*"}, [Type (@{type_name "*"}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
| dest_randomT T = raise TYPE ("dest_randomT", [T], [])
fun mk_tracing s t =
@@ -467,7 +467,7 @@
(* generation of case rules from user-given introduction rules *)
-fun mk_args2 (Type ("*", [T1, T2])) st =
+fun mk_args2 (Type (@{type_name "*"}, [T1, T2])) st =
let
val (t1, st') = mk_args2 T1 st
val (t2, st'') = mk_args2 T2 st'
@@ -1099,7 +1099,7 @@
fun all_input_of T =
let
val (Ts, U) = strip_type T
- fun input_of (Type ("*", [T1, T2])) = Pair (input_of T1, input_of T2)
+ fun input_of (Type (@{type_name "*"}, [T1, T2])) = Pair (input_of T1, input_of T2)
| input_of _ = Input
in
if U = HOLogic.boolT then
@@ -1190,7 +1190,7 @@
fun missing_vars vs t = subtract (op =) vs (term_vs t)
-fun output_terms (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) =
+fun output_terms (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =
output_terms (t1, d1) @ output_terms (t2, d2)
| output_terms (t1 $ t2, Mode_App (d1, d2)) =
output_terms (t1, d1) @ output_terms (t2, d2)
@@ -1206,7 +1206,7 @@
SOME ms => SOME (map (fn m => (Context m , [])) ms)
| NONE => NONE)
-fun derivations_of (ctxt : Proof.context) modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
+fun derivations_of (ctxt : Proof.context) modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) (Pair (m1, m2)) =
map_product
(fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
(derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2)
@@ -1236,7 +1236,7 @@
else if eq_mode (m, Output) then
(if is_possible_output ctxt vs t then [(Term Output, [])] else [])
else []
-and all_derivations_of ctxt modes vs (Const ("Pair", _) $ t1 $ t2) =
+and all_derivations_of ctxt modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) =
let
val derivs1 = all_derivations_of ctxt modes vs t1
val derivs2 = all_derivations_of ctxt modes vs t2
@@ -1665,7 +1665,7 @@
(case (t, deriv) of
(t1 $ t2, Mode_App (deriv1, deriv2)) =>
string_of_tderiv ctxt (t1, deriv1) ^ " $ " ^ string_of_tderiv ctxt (t2, deriv2)
- | (Const ("Pair", _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
+ | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
"(" ^ string_of_tderiv ctxt (t1, deriv1) ^ ", " ^ string_of_tderiv ctxt (t2, deriv2) ^ ")"
| (t, Term Input) => Syntax.string_of_term ctxt t ^ "[Input]"
| (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
@@ -1692,7 +1692,7 @@
val bs = map (pair "x") (binder_types (fastype_of t))
val bounds = map Bound (rev (0 upto (length bs) - 1))
in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end
- | (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
+ | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
(case (expr_of (t1, d1), expr_of (t2, d2)) of
(NONE, NONE) => NONE
| (NONE, SOME t) => SOME t
@@ -2010,7 +2010,7 @@
(ks @ [SOME k]))) arities));
fun split_lambda (x as Free _) t = lambda x t
- | split_lambda (Const ("Pair", _) $ t1 $ t2) t =
+ | split_lambda (Const (@{const_name Pair}, _) $ t1 $ t2) t =
HOLogic.mk_split (split_lambda t1 (split_lambda t2 t))
| split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
| split_lambda t _ = raise (TERM ("split_lambda", [t]))
@@ -2019,7 +2019,7 @@
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
-fun mk_args is_eval (m as Pair (m1, m2), T as Type ("*", [T1, T2])) names =
+fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name "*"}, [T1, T2])) names =
if eq_mode (m, Input) orelse eq_mode (m, Output) then
let
val x = Name.variant names "x"
@@ -3112,7 +3112,7 @@
in
if defined_functions compilation ctxt name then
let
- fun extract_mode (Const ("Pair", _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
+ fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
| extract_mode (Free (x, _)) = if member (op =) output_names x then Output else Input
| extract_mode _ = Input
val user_mode = fold_rev (curry Fun) (map extract_mode all_args) Bool
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Jun 10 12:28:27 2010 +0200
@@ -37,7 +37,7 @@
@{term "max :: int => _"}, @{term "max :: nat => _"},
@{term "min :: int => _"}, @{term "min :: nat => _"},
@{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
- @{term "Not"}, @{term "Suc"},
+ @{term "Not"}, @{term Suc},
@{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
@{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
@{term "nat"}, @{term "int"},
@@ -726,7 +726,7 @@
fun isnum t = case t of
Const(@{const_name Groups.zero},_) => true
| Const(@{const_name Groups.one},_) => true
- | @{term "Suc"}$s => isnum s
+ | @{term Suc}$s => isnum s
| @{term "nat"}$s => isnum s
| @{term "int"}$s => isnum s
| Const(@{const_name Groups.uminus},_)$s => isnum s
--- a/src/HOL/Tools/TFL/dcterm.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Thu Jun 10 12:28:27 2010 +0200
@@ -129,7 +129,7 @@
val dest_neg = dest_monop "not"
-val dest_pair = dest_binop "Pair";
+val dest_pair = dest_binop @{const_name Pair};
val dest_eq = dest_binop "op ="
val dest_imp = dest_binop "op -->"
val dest_conj = dest_binop "op &"
--- a/src/HOL/Tools/TFL/rules.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Thu Jun 10 12:28:27 2010 +0200
@@ -591,11 +591,11 @@
local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
fun mk_fst tm =
- let val ty as Type("*", [fty,sty]) = type_of tm
- in Const ("fst", ty --> fty) $ tm end
+ let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
+ in Const ("Product_Type.fst", ty --> fty) $ tm end
fun mk_snd tm =
- let val ty as Type("*", [fty,sty]) = type_of tm
- in Const ("snd", ty --> sty) $ tm end
+ let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
+ in Const ("Product_Type.snd", ty --> sty) $ tm end
in
fun XFILL tych x vstruct =
let fun traverse p xocc L =
--- a/src/HOL/Tools/TFL/usyntax.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jun 10 12:28:27 2010 +0200
@@ -197,7 +197,7 @@
local
fun mk_uncurry (xt, yt, zt) =
Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
-fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
+fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
in
@@ -268,11 +268,11 @@
fun mk_pair{fst,snd} =
let val ty1 = type_of fst
val ty2 = type_of snd
- val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2)
+ val c = Const(@{const_name Pair},ty1 --> ty2 --> prod_ty ty1 ty2)
in list_comb(c,[fst,snd])
end;
-fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
+fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
@@ -372,7 +372,7 @@
(* Miscellaneous *)
fun mk_vstruct ty V =
- let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
+ let fun follow_prod_type (Type(@{type_name "*"},[ty1,ty2])) vs =
let val (ltm,vs1) = follow_prod_type ty1 vs
val (rtm,vs2) = follow_prod_type ty2 vs1
in (mk_pair{fst=ltm, snd=rtm}, vs2) end
@@ -393,7 +393,7 @@
fun dest_relation tm =
if (type_of tm = HOLogic.boolT)
- then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
+ then let val (Const("op :",_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
in (R,y,x)
end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
else raise USYN_ERR "dest_relation" "not a boolean term";
--- a/src/HOL/Tools/float_arith.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/float_arith.ML Thu Jun 10 12:28:27 2010 +0200
@@ -206,7 +206,7 @@
fun mk_float (a, b) = @{term "float"} $
HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
-fun dest_float (Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) =
+fun dest_float (Const ("Float.float", _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
pairself (snd o HOLogic.dest_number) (a, b)
| dest_float t = ((snd o HOLogic.dest_number) t, 0);
--- a/src/HOL/Tools/groebner.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Thu Jun 10 12:28:27 2010 +0200
@@ -698,7 +698,7 @@
val holify_polynomial =
let fun holify_varpow (v,n) =
- if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n) (* FIXME *)
+ if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp nat} n) (* FIXME *)
fun holify_monomial vars (c,m) =
let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
in end_itlist ring_mk_mul (mk_const c :: xps)
--- a/src/HOL/Tools/hologic.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Thu Jun 10 12:28:27 2010 +0200
@@ -289,42 +289,42 @@
(* prod *)
-fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
+fun mk_prodT (T1, T2) = Type ("Product_Type.*", [T1, T2]);
-fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
+fun dest_prodT (Type ("Product_Type.*", [T1, T2])) = (T1, T2)
| dest_prodT T = raise TYPE ("dest_prodT", [T], []);
-fun pair_const T1 T2 = Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2));
+fun pair_const T1 T2 = Const ("Product_Type.Pair", [T1, T2] ---> mk_prodT (T1, T2));
fun mk_prod (t1, t2) =
let val T1 = fastype_of t1 and T2 = fastype_of t2 in
pair_const T1 T2 $ t1 $ t2
end;
-fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
+fun dest_prod (Const ("Product_Type.Pair", _) $ t1 $ t2) = (t1, t2)
| dest_prod t = raise TERM ("dest_prod", [t]);
fun mk_fst p =
let val pT = fastype_of p in
- Const ("fst", pT --> fst (dest_prodT pT)) $ p
+ Const ("Product_Type.fst", pT --> fst (dest_prodT pT)) $ p
end;
fun mk_snd p =
let val pT = fastype_of p in
- Const ("snd", pT --> snd (dest_prodT pT)) $ p
+ Const ("Product_Type.snd", pT --> snd (dest_prodT pT)) $ p
end;
fun split_const (A, B, C) =
- Const ("split", (A --> B --> C) --> mk_prodT (A, B) --> C);
+ Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C);
fun mk_split t =
(case Term.fastype_of t of
T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
- Const ("split", T --> mk_prodT (A, B) --> C) $ t
+ Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t
| _ => raise TERM ("mk_split: bad body type", [t]));
(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
-fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
+fun flatten_tupleT (Type ("Product_Type.*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
| flatten_tupleT T = [T];
@@ -334,14 +334,14 @@
| mk_tupleT Ts = foldr1 mk_prodT Ts;
fun strip_tupleT (Type ("Product_Type.unit", [])) = []
- | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
+ | strip_tupleT (Type ("Product_Type.*", [T1, T2])) = T1 :: strip_tupleT T2
| strip_tupleT T = [T];
fun mk_tuple [] = unit
| mk_tuple ts = foldr1 mk_prod ts;
fun strip_tuple (Const ("Product_Type.Unity", _)) = []
- | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
+ | strip_tuple (Const ("Product_Type.Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
| strip_tuple t = [t];
@@ -367,14 +367,14 @@
fun strip_ptupleT ps =
let
fun factors p T = if member (op =) ps p then (case T of
- Type ("*", [T1, T2]) =>
+ Type ("Product_Type.*", [T1, T2]) =>
factors (1::p) T1 @ factors (2::p) T2
| _ => ptuple_err "strip_ptupleT") else [T]
in factors [] end;
val flat_tupleT_paths =
let
- fun factors p (Type ("*", [T1, T2])) =
+ fun factors p (Type ("Product_Type.*", [T1, T2])) =
p :: factors (1::p) T1 @ factors (2::p) T2
| factors p _ = []
in factors [] end;
@@ -383,7 +383,7 @@
let
fun mk p T ts =
if member (op =) ps p then (case T of
- Type ("*", [T1, T2]) =>
+ Type ("Product_Type.*", [T1, T2]) =>
let
val (t, ts') = mk (1::p) T1 ts;
val (u, ts'') = mk (2::p) T2 ts'
@@ -395,14 +395,14 @@
fun strip_ptuple ps =
let
fun dest p t = if member (op =) ps p then (case t of
- Const ("Pair", _) $ t $ u =>
+ Const ("Product_Type.Pair", _) $ t $ u =>
dest (1::p) t @ dest (2::p) u
| _ => ptuple_err "strip_ptuple") else [t]
in dest [] end;
val flat_tuple_paths =
let
- fun factors p (Const ("Pair", _) $ t $ u) =
+ fun factors p (Const ("Product_Type.Pair", _) $ t $ u) =
p :: factors (1::p) t @ factors (2::p) u
| factors p _ = []
in factors [] end;
@@ -414,7 +414,7 @@
let
fun ap ((p, T) :: pTs) =
if member (op =) ps p then (case T of
- Type ("*", [T1, T2]) =>
+ Type ("Product_Type.*", [T1, T2]) =>
split_const (T1, T2, map snd pTs ---> T3) $
ap ((1::p, T1) :: (2::p, T2) :: pTs)
| _ => ptuple_err "mk_psplits")
@@ -427,7 +427,7 @@
val strip_psplits =
let
fun strip [] qs Ts t = (t, rev Ts, qs)
- | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
+ | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) =
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
| strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
| strip (p :: ps) qs Ts t = strip ps qs
@@ -438,16 +438,16 @@
(* nat *)
-val natT = Type ("nat", []);
+val natT = Type ("Nat.nat", []);
val zero = Const ("Groups.zero_class.zero", natT);
fun is_zero (Const ("Groups.zero_class.zero", _)) = true
| is_zero _ = false;
-fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
+fun mk_Suc t = Const ("Nat.Suc", natT --> natT) $ t;
-fun dest_Suc (Const ("Suc", _) $ t) = t
+fun dest_Suc (Const ("Nat.Suc", _) $ t) = t
| dest_Suc t = raise TERM ("dest_Suc", [t]);
val Suc_zero = mk_Suc zero;
@@ -459,7 +459,7 @@
in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
fun dest_nat (Const ("Groups.zero_class.zero", _)) = 0
- | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
+ | dest_nat (Const ("Nat.Suc", _) $ t) = dest_nat t + 1
| dest_nat t = raise TERM ("dest_nat", [t]);
val class_size = "Nat.size";
--- a/src/HOL/Tools/inductive_codegen.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Jun 10 12:28:27 2010 +0200
@@ -14,7 +14,7 @@
val quickcheck_setup : theory -> theory
end;
-structure InductiveCodegen : INDUCTIVE_CODEGEN =
+structure Inductive_Codegen : INDUCTIVE_CODEGEN =
struct
open Codegen;
@@ -41,7 +41,7 @@
);
-fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
+fun warn thm = warning ("Inductive_Codegen: Not a proper clause:\n" ^
Display.string_of_thm_without_context thm);
fun add_node x g = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
@@ -324,7 +324,7 @@
| distinct_v t nvs = (t, nvs);
fun is_exhaustive (Var _) = true
- | is_exhaustive (Const ("Pair", _) $ t $ u) =
+ | is_exhaustive (Const (@{const_name Pair}, _) $ t $ u) =
is_exhaustive t andalso is_exhaustive u
| is_exhaustive _ = false;
@@ -569,7 +569,7 @@
and mk_ind_def thy defs gr dep names module modecs intrs nparms =
add_edge_acyclic (hd names, dep) gr handle
Graph.CYCLES (xs :: _) =>
- error ("InductiveCodegen: illegal cyclic dependencies:\n" ^ commas xs)
+ error ("Inductive_Codegen: illegal cyclic dependencies:\n" ^ commas xs)
| Graph.UNDEF _ =>
let
val _ $ u = Logic.strip_imp_concl (hd intrs);
@@ -825,7 +825,7 @@
val s = "structure TestTerm =\nstruct\n\n" ^
cat_lines (map snd code) ^
"\nopen Generated;\n\n" ^ string_of
- (Pretty.block [str "val () = InductiveCodegen.test_fn :=",
+ (Pretty.block [str "val () = Inductive_Codegen.test_fn :=",
Pretty.brk 1, str "(fn p =>", Pretty.brk 1,
str "case Seq.pull (testf p) of", Pretty.brk 1,
str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
--- a/src/HOL/Tools/inductive_set.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Thu Jun 10 12:28:27 2010 +0200
@@ -401,7 +401,7 @@
else thm
in map preproc end;
-fun code_ind_att optmod = to_pred_att [] #> InductiveCodegen.add optmod NONE;
+fun code_ind_att optmod = to_pred_att [] #> Inductive_Codegen.add optmod NONE;
(**** definition of inductive sets ****)
--- a/src/HOL/Tools/lin_arith.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Jun 10 12:28:27 2010 +0200
@@ -461,7 +461,7 @@
(* ?P ((?n::nat) mod (number_of ?k)) =
((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
(ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
- | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+ | (Const ("Divides.div_class.mod", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name Groups.zero}, split_type)
@@ -493,7 +493,7 @@
(* ?P ((?n::nat) div (number_of ?k)) =
((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
(ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
- | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+ | (Const ("Divides.div_class.div", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name Groups.zero}, split_type)
--- a/src/HOL/Tools/meson.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Jun 10 12:28:27 2010 +0200
@@ -395,7 +395,7 @@
since this code expects to be called on a clause form.*)
val is_conn = member (op =)
["Trueprop", "op &", "op |", "op -->", "Not",
- "All", "Ex", "Ball", "Bex"];
+ "All", "Ex", @{const_name Ball}, @{const_name Bex}];
(*True if the term contains a function--not a logical connective--where the type
of any argument contains bool.*)
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Thu Jun 10 12:28:27 2010 +0200
@@ -97,7 +97,7 @@
(*Split up a sum into the list of its constituent terms, on the way removing any
Sucs and counting them.*)
-fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
+fun dest_Suc_sum (Const (@{const_name Suc}, _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
| dest_Suc_sum (t, (k,ts)) =
let val (t1,t2) = dest_plus t
in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end
--- a/src/HOL/Tools/refute.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Tools/refute.ML Thu Jun 10 12:28:27 2010 +0200
@@ -657,14 +657,14 @@
(* other optimizations *)
| Const (@{const_name Finite_Set.card}, _) => t
| Const (@{const_name Finite_Set.finite}, _) => t
- | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
- | Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
+ | Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, Type ("bool", [])])])) => t
+ | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) => t
+ | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) => t
+ | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) => t
| Const (@{const_name List.append}, _) => t
(* UNSOUND
| Const (@{const_name lfp}, _) => t
@@ -834,17 +834,17 @@
| Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
| Const (@{const_name Finite_Set.finite}, T) =>
collect_type_axioms T axs
- | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
+ | Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name Groups.plus}, T as Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ | Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
collect_type_axioms T axs
- | Const (@{const_name Groups.minus}, T as Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ | Const (@{const_name Groups.minus}, T as Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
collect_type_axioms T axs
- | Const (@{const_name Groups.times}, T as Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
collect_type_axioms T axs
| Const (@{const_name List.append}, T) => collect_type_axioms T axs
(* UNSOUND
@@ -2654,7 +2654,7 @@
case t of
Const (@{const_name Finite_Set.card},
Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
- Type ("nat", [])])) =>
+ @{typ nat}])) =>
let
(* interpretation -> int *)
fun number_of_elements (Node xs) =
@@ -2670,7 +2670,7 @@
| number_of_elements (Leaf _) =
raise REFUTE ("Finite_Set_card_interpreter",
"interpretation for set type is a leaf")
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* takes an interpretation for a set and returns an interpretation *)
(* for a 'nat' denoting the set's cardinality *)
(* interpretation -> interpretation *)
@@ -2730,10 +2730,10 @@
fun Nat_less_interpreter thy model args t =
case t of
- Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
+ Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
let
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* the 'n'-th nat is not less than the first 'n' nats, while it *)
(* is less than the remaining 'size_of_nat - n' nats *)
(* int -> interpretation *)
@@ -2753,10 +2753,10 @@
fun Nat_plus_interpreter thy model args t =
case t of
- Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
let
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* int -> int -> interpretation *)
fun plus m n =
let
@@ -2784,10 +2784,10 @@
fun Nat_minus_interpreter thy model args t =
case t of
- Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
let
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* int -> int -> interpretation *)
fun minus m n =
let
@@ -2812,10 +2812,10 @@
fun Nat_times_interpreter thy model args t =
case t of
- Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
let
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* nat -> nat -> interpretation *)
fun mult m n =
let
@@ -3050,7 +3050,7 @@
fun Product_Type_fst_interpreter thy model args t =
case t of
- Const (@{const_name fst}, Type ("fun", [Type ("*", [T, U]), _])) =>
+ Const (@{const_name fst}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
let
val constants_T = make_constants thy model T
val size_U = size_of_type thy model U
@@ -3069,7 +3069,7 @@
fun Product_Type_snd_interpreter thy model args t =
case t of
- Const (@{const_name snd}, Type ("fun", [Type ("*", [T, U]), _])) =>
+ Const (@{const_name snd}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
let
val size_T = size_of_type thy model T
val constants_U = make_constants thy model U
@@ -3279,8 +3279,8 @@
add_interpreter "lfp" lfp_interpreter #>
add_interpreter "gfp" gfp_interpreter #>
*)
- add_interpreter "fst" Product_Type_fst_interpreter #>
- add_interpreter "snd" Product_Type_snd_interpreter #>
+ add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #>
+ add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #>
add_printer "stlc" stlc_printer #>
add_printer "IDT" IDT_printer;
--- a/src/HOL/Transitive_Closure.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Jun 10 12:28:27 2010 +0200
@@ -858,7 +858,7 @@
val rtrancl_trans = @{thm rtrancl_trans};
fun decomp (@{const Trueprop} $ t) =
- let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
+ let fun dec (Const ("op :", _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
| decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
| decr r = (r,"r");
--- a/src/HOL/ex/Codegenerator_Candidates.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Thu Jun 10 12:28:27 2010 +0200
@@ -26,6 +26,8 @@
While_Combinator
begin
+declare lexn.simps [code del]
+
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
empty: "sublist [] xs"
| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
--- a/src/HOL/ex/Dedekind_Real.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Thu Jun 10 12:28:27 2010 +0200
@@ -2006,7 +2006,7 @@
qed
text {*
- There must be other proofs, e.g. @{text "Suc"} of the largest
+ There must be other proofs, e.g. @{text Suc} of the largest
integer in the cut representing @{text "x"}.
*}
--- a/src/HOL/ex/Refute_Examples.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Thu Jun 10 12:28:27 2010 +0200
@@ -774,7 +774,7 @@
oops
lemma "P Suc"
- refute -- {* @{term "Suc"} is a partial function (regardless of the size
+ refute -- {* @{term Suc} is a partial function (regardless of the size
of the model), hence @{term "P Suc"} is undefined, hence no
model will be found *}
oops
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jun 10 12:28:27 2010 +0200
@@ -34,9 +34,9 @@
exception malformed;
-fun fst_type (Type("*",[a,_])) = a |
+fun fst_type (Type(@{type_name "*"},[a,_])) = a |
fst_type _ = raise malformed;
-fun snd_type (Type("*",[_,a])) = a |
+fun snd_type (Type(@{type_name "*"},[_,a])) = a |
snd_type _ = raise malformed;
fun element_type (Type("set",[a])) = a |
@@ -121,10 +121,10 @@
fun delete_ul_string s = implode(delete_ul (explode s));
-fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
+fun type_list_of sign (Type(@{type_name "*"},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
type_list_of sign a = [(Syntax.string_of_typ_global sign a)];
-fun structured_tuple l (Type("*",s::t::_)) =
+fun structured_tuple l (Type(@{type_name "*"},s::t::_)) =
let
val (r,str) = structured_tuple l s;
in
--- a/src/HOLCF/IOA/meta_theory/automaton.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML Thu Jun 10 12:28:27 2010 +0200
@@ -298,7 +298,7 @@
(string_of_typ thy t));
fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
-comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
+comp_st_type_of thy (a::r) = Type(@{type_name "*"},[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
comp_st_type_of _ _ = error "empty automaton list";
(* checking consistency of action types (for composition) *)
@@ -387,11 +387,11 @@
thy
|> Sign.add_consts_i
[(Binding.name automaton_name,
-Type("*",
-[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
- Type("*",[Type("set",[st_typ]),
- Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
- Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
+Type(@{type_name "*"},
+[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
+ Type(@{type_name "*"},[Type("set",[st_typ]),
+ Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
+ Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
|> add_defs
[(automaton_name ^ "_def",
@@ -442,11 +442,11 @@
thy
|> Sign.add_consts_i
[(Binding.name automaton_name,
-Type("*",
-[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
- Type("*",[Type("set",[st_typ]),
- Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
- Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
+Type(@{type_name "*"},
+[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
+ Type(@{type_name "*"},[Type("set",[st_typ]),
+ Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
+ Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
|> add_defs
[(automaton_name ^ "_def",
--- a/src/HOLCF/Tools/Domain/domain_library.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu Jun 10 12:28:27 2010 +0200
@@ -215,7 +215,7 @@
| prj _ _ _ [] _ = raise Fail "Domain_Library.prj: empty list"
| prj f1 _ x (_::y::ys) 0 = f1 x y
| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
-fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
+fun proj x = prj (fn S => K (%%: @{const_name fst} $ S)) (fn S => K (%%: @{const_name snd} $ S)) x;
fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
val UU = %%: @{const_name UU};
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Jun 10 12:28:27 2010 +0200
@@ -179,7 +179,7 @@
then copy_of_dtyp map_tab
mk_take (dtyp_of arg) ` (%# arg)
else (%# arg);
- val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
+ val lhs = (dc_take dname $ (%%: @{const_name Suc} $ %:"n")) ` (con_app con args);
val rhs = con_app2 con one_rhs args;
val goal = mk_trp (lhs === rhs);
val rules =
--- a/src/Pure/Isar/class_target.ML Thu Jun 10 12:08:33 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Thu Jun 10 12:28:27 2010 +0200
@@ -465,8 +465,8 @@
explode #> scan_valids #> implode
end;
-fun type_name "*" = "prod"
- | type_name "+" = "sum"
+fun type_name "Product_Type.*" = "prod"
+ | type_name "Sum_Type.+" = "sum"
| type_name s = sanitize_name (Long_Name.base_name s);
fun resort_terms pp algebra consts constraints ts =