# HG changeset patch # User haftmann # Date 1276165707 -7200 # Node ID 92a75e6d938b649bad14b44e7cee96fa3df02476 # Parent 842fff4c35ef2515da18be8c28b9c27eba163495# Parent 6ff1fce8e156d1591e1e685df31a4c91063e83a2 merged diff -r 842fff4c35ef -r 92a75e6d938b NEWS --- 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) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Decision_Procs/Approximation.thy --- 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]) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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 = diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Hoare/hoare_tac.ML --- 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]**) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Import/HOL/num.imp --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Import/HOL/pair.imp --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Import/HOLLight/hollight.imp --- 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.$" diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Inductive.thy --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Library/Binomial.thy --- 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: "(\n\{1\nat..n}. a + of_nat n) = (\n\{0\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] diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Library/Countable.thy --- 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 "(\x. case x of Inl a \ to_nat (False, to_nat a) | Inr b \ to_nat (True, to_nat b))"]) (simp split: sum.split_asm) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Library/Diagonalize.thy --- 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 \ nat \ nat" where "diagonalize m n = sum (m + n) + m" diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Library/Efficient_Nat.thy --- 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 \ 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"}. diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Library/Formal_Power_Series.thy --- 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 "\ = setsum (\i. of_nat (i + 1) * a$(i+1) * (setsum (\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 (\i. of_nat (i + 1) * a$(i+1) * (setsum (\j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" . diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Library/SML_Quickcheck.thy --- 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) *} diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Modelcheck/mucke_oracle.ML --- 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 | diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Nat.thy --- 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 \ 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 = (\n. f n \ 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 f m < f n) \ f(m)+k \ f(m+k)" diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Nominal/Examples/Support.thy --- 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 "\i. (n = 2*i) \ (n=2*i+1)" by (induct n) (presburger)+ diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Nominal/nominal_atoms.ML --- 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) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Nominal/nominal_datatype.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Nominal/nominal_permeq.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Nominal/nominal_thmdecls.ML --- 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 *) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Product_Type.thy --- 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 \ 'b \ 'a \ 'b \ bool" where "Pair_Rep a b = (\x y. x = a \ y = b)" -global - -typedef (Prod) - ('a, 'b) "*" (infixr "*" 20) - = "{f. \a b. f = Pair_Rep (a\'a) (b\'b)}" +typedef (prod) ('a, 'b) "*" (infixr "*" 20) + = "{f. \a b. f = Pair_Rep (a\'a) (b\'b)}" proof - fix a b show "Pair_Rep a b \ ?Prod" + fix a b show "Pair_Rep a b \ ?prod" by rule+ qed @@ -143,35 +141,27 @@ type_notation (HTML output) "*" ("(_ \/ _)" [21, 20] 20) -consts - Pair :: "'a \ 'b \ 'a \ 'b" - -local - -defs - Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)" +definition Pair :: "'a \ 'b \ 'a \ 'b" where + "Pair a b = Abs_prod (Pair_Rep a b)" rep_datatype (prod) Pair proof - fix P :: "'a \ 'b \ bool" and p assume "\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 \ a = c \ b = d" by (auto simp add: Pair_Rep_def expand_fun_eq) - moreover have "Pair_Rep a b \ Prod" and "Pair_Rep c d \ Prod" - by (auto simp add: Prod_def) + moreover have "Pair_Rep a b \ prod" and "Pair_Rep c d \ prod" + by (auto simp add: prod_def) ultimately show "Pair a b = Pair c d \ a = c \ 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 \ 'b \ 'c) \ 'a \ 'b \ 'c" - -local defs +definition split :: "('a \ 'b \ 'c) \ 'a \ 'b \ '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 \ 'b \ 'a" - snd :: "'a \ 'b \ 'b" +definition fst :: "'a \ 'b \ 'a" where + "fst p = (case p of (a, b) \ a)" -local defs - fst_def: "fst p == case p of (a, b) \ a" - snd_def: "snd p == case p of (a, b) \ b" +definition snd :: "'a \ 'b \ 'b" where + "snd p = (case p of (a, b) \ 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 \ 'b \ 'c) \ 'a \ 'b \ 'c" - -local defs - curry_def: "curry == (%c x y. c (Pair x y))" +definition curry :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c" where + "curry = (\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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Set.thy --- 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 \") and supset_eq ("(_/ \ _)" [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 \ ('a \ bool) \ bool" where + "Ball A P \ (\x. x \ A \ 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 \ ('a \ bool) \ bool" where + "Bex A P \ (\x. x \ A \ P x)" -- "bounded existential quantifiers" syntax "_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/SetInterval.thy --- 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 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}" -apply (rule card_bij_eq [of "Suc" _ _ "\x. x - Suc 0"]) +apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"]) apply simp apply fastsimp apply auto diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Sum_Type.thy --- 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 \ 'a \ 'b \ bool \ bool" where "Inr_Rep b x y p \ y = b \ \ p" -global - -typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\a. f = Inl_Rep (a::'a)) \ (\b. f = Inr_Rep (b::'b))}" +typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\a. f = Inl_Rep (a::'a)) \ (\b. f = Inr_Rep (b::'b))}" by auto -local - -lemma Inl_RepI: "Inl_Rep a \ Sum" - by (auto simp add: Sum_def) +lemma Inl_RepI: "Inl_Rep a \ sum" + by (auto simp add: sum_def) -lemma Inr_RepI: "Inr_Rep b \ Sum" - by (auto simp add: Sum_def) +lemma Inr_RepI: "Inr_Rep b \ sum" + by (auto simp add: sum_def) -lemma inj_on_Abs_Sum: "A \ Sum \ inj_on Abs_Sum A" - by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto +lemma inj_on_Abs_sum: "A \ sum \ 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 \ 'a + 'b" where - "Inl = Abs_Sum \ Inl_Rep" + "Inl = Abs_sum \ Inl_Rep" definition Inr :: "'b \ 'a + 'b" where - "Inr = Abs_Sum \ Inr_Rep" + "Inr = Abs_sum \ 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 \ 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 \ x = y" using inj_Inr by (rule injD) lemma Inl_not_Inr: "Inl a \ Inr b" proof - - from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \ 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) \ Abs_Sum (Inr_Rep b)" by auto + from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \ 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) \ Abs_sum (Inr_Rep b)" by auto then show ?thesis by (simp add: Inl_def Inr_def) qed @@ -81,10 +77,10 @@ assumes "\x::'a. s = Inl x \ P" and "\y::'b. s = Inr y \ 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 \ Sum" - with assms show P by (auto simp add: Sum_def Inl_def Inr_def) + assume "s = Abs_sum f" and "f \ sum" + with assms show P by (auto simp add: sum_def Inl_def Inr_def) qed rep_datatype (sum) Inl Inr diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/Function/function_lib.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/Function/measure_functions.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/Function/sum_tree.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/Function/termination.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/TFL/dcterm.ML --- 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 &" diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/TFL/rules.ML --- 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 = diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/TFL/usyntax.ML --- 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"; diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/float_arith.ML --- 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); diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/groebner.ML --- 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) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/hologic.ML --- 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"; diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/inductive_codegen.ML --- 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 "_"], diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/inductive_set.ML --- 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 ****) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/lin_arith.ML --- 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) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/meson.ML --- 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.*) diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/nat_numeral_simprocs.ML --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Tools/refute.ML --- 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; diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/Transitive_Closure.thy --- 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"); diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/ex/Codegenerator_Candidates.thy --- 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 \ 'a list \ bool" where empty: "sublist [] xs" | drop: "sublist ys xs \ sublist ys (x # xs)" diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/ex/Dedekind_Real.thy --- 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"}. *} diff -r 842fff4c35ef -r 92a75e6d938b src/HOL/ex/Refute_Examples.thy --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOLCF/IOA/Modelcheck/MuIOA.thy --- 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 diff -r 842fff4c35ef -r 92a75e6d938b src/HOLCF/IOA/meta_theory/automaton.ML --- 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", diff -r 842fff4c35ef -r 92a75e6d938b src/HOLCF/Tools/Domain/domain_library.ML --- 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}; diff -r 842fff4c35ef -r 92a75e6d938b src/HOLCF/Tools/Domain/domain_theorems.ML --- 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 = diff -r 842fff4c35ef -r 92a75e6d938b src/Pure/Isar/class_target.ML --- 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 =