--- a/Admin/isatest/isatest-makedist Mon Feb 22 09:15:12 2010 +0100
+++ b/Admin/isatest/isatest-makedist Mon Feb 22 09:17:49 2010 +0100
@@ -94,12 +94,6 @@
$SSH macbroy22 "$MAKEALL $HOME/settings/at-poly"
# give test some time to copy settings and start
sleep 15
-$SSH macbroy20 "$MAKEALL $HOME/settings/at-poly-5.1-para-e"
-sleep 15
-#$SSH macbroy24 "$MAKEALL -l HOL proofterms $HOME/settings/at-sml-dev-p"
-#sleep 15
-$SSH macbroy21 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
-sleep 15
$SSH macbroy23 "$MAKEALL -l HOL HOL-ex $HOME/settings/at-sml-dev-e"
sleep 15
$SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
--- a/Admin/isatest/settings/at64-poly Mon Feb 22 09:15:12 2010 +0100
+++ b/Admin/isatest/settings/at64-poly Mon Feb 22 09:17:49 2010 +0100
@@ -1,12 +1,12 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2"
- ML_SYSTEM="polyml-5.2"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86_64-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 500"
+ ML_OPTIONS="-H 1000"
-ISABELLE_HOME_USER=~/isabelle-at64-poly-e
+ISABELLE_HOME_USER=~/isabelle-at64-poly
# Where to look for isabelle tools (multiple dirs separated by ':').
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
@@ -24,5 +24,4 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-unset KODKODI
-
+init_component /home/isabelle/contrib_devel/kodkodi
--- a/NEWS Mon Feb 22 09:15:12 2010 +0100
+++ b/NEWS Mon Feb 22 09:17:49 2010 +0100
@@ -4,6 +4,41 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Authentic syntax for *all* term constants: provides simple and
+robust correspondence between formal entities and concrete syntax.
+Substantial INCOMPATIBILITY concerning low-level syntax translations
+(translation rules and translation functions in ML). Some hints on
+upgrading:
+
+ - Many existing uses of 'syntax' and 'translations' can be replaced
+ by more modern 'notation' and 'abbreviation', which are
+ independent of this issue.
+
+ - 'translations' require markup within the AST; the term syntax
+ provides the following special forms:
+
+ CONST c -- produces syntax version of constant c from context
+ XCONST c -- literally c, checked as constant from context
+ c -- literally c, if declared by 'syntax'
+
+ Plain identifiers are treated as AST variables -- occasionally the
+ system indicates accidental variables via the error "rhs contains
+ extra variables".
+
+ - 'parse_translation' etc. in ML may use the following
+ antiquotations:
+
+ @{const_syntax c} -- ML version of "CONST c" above
+ @{syntax_const c} -- literally c (checked wrt. 'syntax' declarations)
+
+Note that old non-authentic syntax was based on unqualified base
+names, so all of the above would coincide. Recall that 'print_syntax'
+and ML_command "set Syntax.trace_ast" help to diagnose syntax
+problems.
+
+
*** Pure ***
* Code generator: details of internal data cache have no impact on
--- a/doc-src/more_antiquote.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/doc-src/more_antiquote.ML Mon Feb 22 09:17:49 2010 +0100
@@ -91,9 +91,9 @@
val (_, eqngr) = Code_Preproc.obtain thy [const] [];
fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
val thms = Code_Preproc.cert eqngr const
- |> Code.equations_thms_cert thy
+ |> Code.equations_of_cert thy
|> snd
- |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE)
+ |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
|> map (holize o no_vars ctxt o AxClass.overload thy);
in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
--- a/src/Cube/Cube.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Cube/Cube.thy Mon Feb 22 09:17:49 2010 +0100
@@ -18,43 +18,43 @@
context' typing'
consts
- Abs :: "[term, term => term] => term"
- Prod :: "[term, term => term] => term"
- Trueprop :: "[context, typing] => prop"
- MT_context :: "context"
- Context :: "[typing, context] => context"
- star :: "term" ("*")
- box :: "term" ("[]")
- app :: "[term, term] => term" (infixl "^" 20)
- Has_type :: "[term, term] => typing"
+ Abs :: "[term, term => term] => term"
+ Prod :: "[term, term => term] => term"
+ Trueprop :: "[context, typing] => prop"
+ MT_context :: "context"
+ Context :: "[typing, context] => context"
+ star :: "term" ("*")
+ box :: "term" ("[]")
+ app :: "[term, term] => term" (infixl "^" 20)
+ Has_type :: "[term, term] => typing"
syntax
- Trueprop :: "[context', typing'] => prop" ("(_/ |- _)")
- Trueprop1 :: "typing' => prop" ("(_)")
- "" :: "id => context'" ("_")
- "" :: "var => context'" ("_")
- MT_context :: "context'" ("")
- Context :: "[typing', context'] => context'" ("_ _")
- Has_type :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5)
- Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
- Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
- arrow :: "[term, term] => term" (infixr "->" 10)
+ "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ |- _)")
+ "_Trueprop1" :: "typing' => prop" ("(_)")
+ "" :: "id => context'" ("_")
+ "" :: "var => context'" ("_")
+ "\<^const>Cube.MT_context" :: "context'" ("")
+ "\<^const>Cube.Context" :: "[typing', context'] => context'" ("_ _")
+ "\<^const>Cube.Has_type" :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5)
+ "_Lam" :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
+ "_Pi" :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
+ "_arrow" :: "[term, term] => term" (infixr "->" 10)
translations
("prop") "x:X" == ("prop") "|- x:X"
- "Lam x:A. B" == "CONST Abs(A, %x. B)"
- "Pi x:A. B" => "CONST Prod(A, %x. B)"
- "A -> B" => "CONST Prod(A, %_. B)"
+ "Lam x:A. B" == "CONST Abs(A, %x. B)"
+ "Pi x:A. B" => "CONST Prod(A, %x. B)"
+ "A -> B" => "CONST Prod(A, %_. B)"
syntax (xsymbols)
- Trueprop :: "[context', typing'] => prop" ("(_/ \<turnstile> _)")
- box :: "term" ("\<box>")
- Lam :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
- Pi :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
- arrow :: "[term, term] => term" (infixr "\<rightarrow>" 10)
+ "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ \<turnstile> _)")
+ "\<^const>Cube.box" :: "term" ("\<box>")
+ "_Lam" :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
+ "_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
+ "_arrow" :: "[term, term] => term" (infixr "\<rightarrow>" 10)
print_translation {*
- [(@{const_syntax Prod}, dependent_tr' (@{syntax_const Pi}, @{syntax_const arrow}))]
+ [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
*}
axioms
--- a/src/FOL/simpdata.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/FOL/simpdata.ML Mon Feb 22 09:17:49 2010 +0100
@@ -128,7 +128,7 @@
(*No simprules, but basic infastructure for simplification*)
val FOL_basic_ss =
- Simplifier.theory_context @{theory} empty_ss
+ Simplifier.global_context @{theory} empty_ss
setsubgoaler asm_simp_tac
setSSolver (mk_solver "FOL safe" safe_solver)
setSolver (mk_solver "FOL unsafe" unsafe_solver)
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Mon Feb 22 09:17:49 2010 +0100
@@ -72,26 +72,25 @@
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
-fun linr_tac ctxt q i =
- (ObjectLogic.atomize_prems_tac i)
- THEN (REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}] i))
- THEN (fn st =>
+fun linr_tac ctxt q =
+ ObjectLogic.atomize_prems_tac
+ THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
+ THEN' SUBGOAL (fn (g, i) =>
let
- val g = List.nth (prems_of st, i - 1)
val thy = ProofContext.theory_of ctxt
(* Transform the term*)
val (t,np,nh) = prepare_for_linr thy q g
(* Some simpsets for dealing with mod div abs and nat*)
- val simpset0 = Simplifier.theory_context thy HOL_basic_ss addsimps comp_arith
+ val simpset0 = Simplifier.context ctxt HOL_basic_ss addsimps comp_arith
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
[simp_tac simpset0 1,
- TRY (simp_tac (Simplifier.theory_context thy ferrack_ss) 1)]
+ TRY (simp_tac (Simplifier.context ctxt ferrack_ss) 1)]
(trivial ct))
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
- val (th, tac) = case (prop_of pre_thm) of
+ val (th, tac) = case prop_of pre_thm of
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
let val pth = linr_oracle (cterm_of thy (Pattern.eta_long [] t1))
in
@@ -101,9 +100,7 @@
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
end
| _ => (pre_thm, assm_tac i)
- in (rtac (((mp_step nh) o (spec_step np)) th) i
- THEN tac) st
- end handle Subscript => no_tac st);
+ in rtac ((mp_step nh o spec_step np) th) i THEN tac end);
val setup =
Method.setup @{binding rferrack}
--- a/src/HOL/Import/hol4rews.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Import/hol4rews.ML Mon Feb 22 09:17:49 2010 +0100
@@ -613,13 +613,13 @@
end
local
- fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x
- | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
- | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
+ fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
+ | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
+ | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
| handle_meta [x] = Appl[Constant "Trueprop",x]
| handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
in
-val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
+val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]
end
local
--- a/src/HOL/Import/proof_kernel.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML Mon Feb 22 09:17:49 2010 +0100
@@ -1248,7 +1248,7 @@
fun rewrite_hol4_term t thy =
let
val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
- val hol4ss = Simplifier.theory_context thy empty_ss
+ val hol4ss = Simplifier.global_context thy empty_ss
setmksimps single addsimps hol4rews1
in
Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
--- a/src/HOL/Import/shuffler.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Import/shuffler.ML Mon Feb 22 09:17:49 2010 +0100
@@ -488,7 +488,7 @@
fun norm_term thy t =
let
val norms = ShuffleData.get thy
- val ss = Simplifier.theory_context thy empty_ss
+ val ss = Simplifier.global_context thy empty_ss
setmksimps single
addsimps (map (Thm.transfer thy) norms)
addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
--- a/src/HOL/Induct/ROOT.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Induct/ROOT.ML Mon Feb 22 09:17:49 2010 +0100
@@ -1,5 +1,5 @@
setmp_noncritical quick_and_dirty true
use_thys ["Common_Patterns"];
-use_thys ["QuoDataType", "QuoNestedDataType", "Term",
+use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList",
"ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/SList.thy Mon Feb 22 09:17:49 2010 +0100
@@ -0,0 +1,434 @@
+(* Title: HOL/Induct/SList.thy
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+
+This theory is strictly of historical interest. It illustrates how
+recursive datatypes can be constructed in higher-order logic from
+first principles. Isabelle's datatype package automates a
+construction of this sort.
+
+Enriched theory of lists; mutual indirect recursive data-types.
+
+Definition of type 'a list (strict lists) by a least fixed point
+
+We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
+and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
+
+so that list can serve as a "functor" for defining other recursive types.
+
+This enables the conservative construction of mutual recursive data-types
+such as
+
+datatype 'a m = Node 'a * ('a m) list
+*)
+
+header {* Extended List Theory (old) *}
+
+theory SList
+imports Sexp
+begin
+
+(*Hilbert_Choice is needed for the function "inv"*)
+
+(* *********************************************************************** *)
+(* *)
+(* Building up data type *)
+(* *)
+(* *********************************************************************** *)
+
+
+(* Defining the Concrete Constructors *)
+definition
+ NIL :: "'a item" where
+ "NIL = In0(Numb(0))"
+
+definition
+ CONS :: "['a item, 'a item] => 'a item" where
+ "CONS M N = In1(Scons M N)"
+
+inductive_set
+ list :: "'a item set => 'a item set"
+ for A :: "'a item set"
+ where
+ NIL_I: "NIL: list A"
+ | CONS_I: "[| a: A; M: list A |] ==> CONS a M : list A"
+
+
+typedef (List)
+ 'a list = "list(range Leaf) :: 'a item set"
+ by (blast intro: list.NIL_I)
+
+abbreviation "Case == Datatype.Case"
+abbreviation "Split == Datatype.Split"
+
+definition
+ List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b" where
+ "List_case c d = Case(%x. c)(Split(d))"
+
+definition
+ List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b" where
+ "List_rec M c d = wfrec (pred_sexp^+)
+ (%g. List_case c (%x y. d x y (g y))) M"
+
+
+(* *********************************************************************** *)
+(* *)
+(* Abstracting data type *)
+(* *)
+(* *********************************************************************** *)
+
+(*Declaring the abstract list constructors*)
+
+no_translations
+ "[x, xs]" == "x#[xs]"
+ "[x]" == "x#[]"
+no_notation
+ Nil ("[]") and
+ Cons (infixr "#" 65)
+
+definition
+ Nil :: "'a list" ("[]") where
+ "Nil = Abs_List(NIL)"
+
+definition
+ "Cons" :: "['a, 'a list] => 'a list" (infixr "#" 65) where
+ "x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))"
+
+definition
+ (* list Recursion -- the trancl is Essential; see list.ML *)
+ list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b" where
+ "list_rec l c d =
+ List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
+
+definition
+ list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b" where
+ "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
+
+(* list Enumeration *)
+translations
+ "[x, xs]" == "x#[xs]"
+ "[x]" == "x#[]"
+
+ "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)"
+
+
+(* *********************************************************************** *)
+(* *)
+(* Generalized Map Functionals *)
+(* *)
+(* *********************************************************************** *)
+
+
+(* Generalized Map Functionals *)
+
+definition
+ Rep_map :: "('b => 'a item) => ('b list => 'a item)" where
+ "Rep_map f xs = list_rec xs NIL(%x l r. CONS(f x) r)"
+
+definition
+ Abs_map :: "('a item => 'b) => 'a item => 'b list" where
+ "Abs_map g M = List_rec M Nil (%N L r. g(N)#r)"
+
+
+definition
+ map :: "('a=>'b) => ('a list => 'b list)" where
+ "map f xs = list_rec xs [] (%x l r. f(x)#r)"
+
+consts take :: "['a list,nat] => 'a list"
+primrec
+ take_0: "take xs 0 = []"
+ take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
+
+lemma ListI: "x : list (range Leaf) ==> x : List"
+by (simp add: List_def)
+
+lemma ListD: "x : List ==> x : list (range Leaf)"
+by (simp add: List_def)
+
+lemma list_unfold: "list(A) = usum {Numb(0)} (uprod A (list(A)))"
+ by (fast intro!: list.intros [unfolded NIL_def CONS_def]
+ elim: list.cases [unfolded NIL_def CONS_def])
+
+(*This justifies using list in other recursive type definitions*)
+lemma list_mono: "A<=B ==> list(A) <= list(B)"
+apply (rule subsetI)
+apply (erule list.induct)
+apply (auto intro!: list.intros)
+done
+
+(*Type checking -- list creates well-founded sets*)
+lemma list_sexp: "list(sexp) <= sexp"
+apply (rule subsetI)
+apply (erule list.induct)
+apply (unfold NIL_def CONS_def)
+apply (auto intro: sexp.intros sexp_In0I sexp_In1I)
+done
+
+(* A <= sexp ==> list(A) <= sexp *)
+lemmas list_subset_sexp = subset_trans [OF list_mono list_sexp]
+
+
+(*Induction for the type 'a list *)
+lemma list_induct:
+ "[| P(Nil);
+ !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)"
+apply (unfold Nil_def Cons_def)
+apply (rule Rep_List_inverse [THEN subst])
+(*types force good instantiation*)
+apply (rule Rep_List [unfolded List_def, THEN list.induct], simp)
+apply (erule Abs_List_inverse [unfolded List_def, THEN subst], blast)
+done
+
+
+(*** Isomorphisms ***)
+
+lemma inj_on_Abs_list: "inj_on Abs_List (list(range Leaf))"
+apply (rule inj_on_inverseI)
+apply (erule Abs_List_inverse [unfolded List_def])
+done
+
+(** Distinctness of constructors **)
+
+lemma CONS_not_NIL [iff]: "CONS M N ~= NIL"
+by (simp add: NIL_def CONS_def)
+
+lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
+lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE, standard]
+lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]
+
+lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
+apply (unfold Nil_def Cons_def)
+apply (rule CONS_not_NIL [THEN inj_on_Abs_list [THEN inj_on_contraD]])
+apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
+done
+
+lemmas Nil_not_Cons [iff] = Cons_not_Nil [THEN not_sym, standard]
+lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE, standard]
+lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]
+
+(** Injectiveness of CONS and Cons **)
+
+lemma CONS_CONS_eq [iff]: "(CONS K M)=(CONS L N) = (K=L & M=N)"
+by (simp add: CONS_def)
+
+(*For reasoning about abstract list constructors*)
+declare Rep_List [THEN ListD, intro] ListI [intro]
+declare list.intros [intro,simp]
+declare Leaf_inject [dest!]
+
+lemma Cons_Cons_eq [iff]: "(x#xs=y#ys) = (x=y & xs=ys)"
+apply (simp add: Cons_def)
+apply (subst Abs_List_inject)
+apply (auto simp add: Rep_List_inject)
+done
+
+lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]
+
+lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
+ by (induct L == "CONS M N" set: list) auto
+
+lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
+apply (simp add: CONS_def In1_def)
+apply (fast dest!: Scons_D)
+done
+
+
+(*Reasoning about constructors and their freeness*)
+
+
+lemma not_CONS_self: "N: list(A) ==> !M. N ~= CONS M N"
+apply (erule list.induct) apply simp_all done
+
+lemma not_Cons_self2: "\<forall>x. l ~= x#l"
+by (induct l rule: list_induct) simp_all
+
+
+lemma neq_Nil_conv2: "(xs ~= []) = (\<exists>y ys. xs = y#ys)"
+by (induct xs rule: list_induct) auto
+
+(** Conversion rules for List_case: case analysis operator **)
+
+lemma List_case_NIL [simp]: "List_case c h NIL = c"
+by (simp add: List_case_def NIL_def)
+
+lemma List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
+by (simp add: List_case_def CONS_def)
+
+
+(*** List_rec -- by wf recursion on pred_sexp ***)
+
+(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
+ hold if pred_sexp^+ were changed to pred_sexp. *)
+
+lemma List_rec_unfold_lemma:
+ "(%M. List_rec M c d) ==
+ wfrec (pred_sexp^+) (%g. List_case c (%x y. d x y (g y)))"
+by (simp add: List_rec_def)
+
+lemmas List_rec_unfold =
+ def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl],
+ standard]
+
+
+(** pred_sexp lemmas **)
+
+lemma pred_sexp_CONS_I1:
+ "[| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+"
+by (simp add: CONS_def In1_def)
+
+lemma pred_sexp_CONS_I2:
+ "[| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+"
+by (simp add: CONS_def In1_def)
+
+lemma pred_sexp_CONS_D:
+ "(CONS M1 M2, N) : pred_sexp^+ ==>
+ (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"
+apply (frule pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD])
+apply (blast dest!: sexp_CONS_D intro: pred_sexp_CONS_I1 pred_sexp_CONS_I2
+ trans_trancl [THEN transD])
+done
+
+
+(** Conversion rules for List_rec **)
+
+lemma List_rec_NIL [simp]: "List_rec NIL c h = c"
+apply (rule List_rec_unfold [THEN trans])
+apply (simp add: List_case_NIL)
+done
+
+lemma List_rec_CONS [simp]:
+ "[| M: sexp; N: sexp |]
+ ==> List_rec (CONS M N) c h = h M N (List_rec N c h)"
+apply (rule List_rec_unfold [THEN trans])
+apply (simp add: pred_sexp_CONS_I2)
+done
+
+
+(*** list_rec -- by List_rec ***)
+
+lemmas Rep_List_in_sexp =
+ subsetD [OF range_Leaf_subset_sexp [THEN list_subset_sexp]
+ Rep_List [THEN ListD]]
+
+
+lemma list_rec_Nil [simp]: "list_rec Nil c h = c"
+by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Nil_def)
+
+
+lemma list_rec_Cons [simp]: "list_rec (a#l) c h = h a l (list_rec l c h)"
+by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Cons_def
+ Rep_List_inverse Rep_List [THEN ListD] inj_Leaf Rep_List_in_sexp)
+
+
+(*Type checking. Useful?*)
+lemma List_rec_type:
+ "[| M: list(A);
+ A<=sexp;
+ c: C(NIL);
+ !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h x y r: C(CONS x y)
+ |] ==> List_rec M c h : C(M :: 'a item)"
+apply (erule list.induct, simp)
+apply (insert list_subset_sexp)
+apply (subst List_rec_CONS, blast+)
+done
+
+
+
+(** Generalized map functionals **)
+
+lemma Rep_map_Nil [simp]: "Rep_map f Nil = NIL"
+by (simp add: Rep_map_def)
+
+lemma Rep_map_Cons [simp]:
+ "Rep_map f(x#xs) = CONS(f x)(Rep_map f xs)"
+by (simp add: Rep_map_def)
+
+lemma Rep_map_type: "(!!x. f(x): A) ==> Rep_map f xs: list(A)"
+apply (simp add: Rep_map_def)
+apply (rule list_induct, auto)
+done
+
+lemma Abs_map_NIL [simp]: "Abs_map g NIL = Nil"
+by (simp add: Abs_map_def)
+
+lemma Abs_map_CONS [simp]:
+ "[| M: sexp; N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
+by (simp add: Abs_map_def)
+
+(*Eases the use of primitive recursion.*)
+lemma def_list_rec_NilCons:
+ "[| !!xs. f(xs) = list_rec xs c h |]
+ ==> f [] = c & f(x#xs) = h x xs (f xs)"
+by simp
+
+lemma Abs_map_inverse:
+ "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |]
+ ==> Rep_map f (Abs_map g M) = M"
+apply (erule list.induct, simp_all)
+apply (insert list_subset_sexp)
+apply (subst Abs_map_CONS, blast)
+apply blast
+apply simp
+done
+
+(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
+
+(** list_case **)
+
+(* setting up rewrite sets *)
+
+text{*Better to have a single theorem with a conjunctive conclusion.*}
+declare def_list_rec_NilCons [OF list_case_def, simp]
+
+(** list_case **)
+
+lemma expand_list_case:
+ "P(list_case a f xs) = ((xs=[] --> P a ) & (!y ys. xs=y#ys --> P(f y ys)))"
+by (induct xs rule: list_induct) simp_all
+
+
+(**** Function definitions ****)
+
+declare def_list_rec_NilCons [OF map_def, simp]
+
+(** The functional "map" and the generalized functionals **)
+
+lemma Abs_Rep_map:
+ "(!!x. f(x): sexp) ==>
+ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"
+apply (induct xs rule: list_induct)
+apply (simp_all add: Rep_map_type list_sexp [THEN subsetD])
+done
+
+
+(** Additional mapping lemmas **)
+
+lemma map_ident [simp]: "map(%x. x)(xs) = xs"
+by (induct xs rule: list_induct) simp_all
+
+lemma map_compose: "map(f o g)(xs) = map f (map g xs)"
+apply (simp add: o_def)
+apply (induct xs rule: list_induct)
+apply simp_all
+done
+
+
+(** take **)
+
+lemma take_Suc1 [simp]: "take [] (Suc x) = []"
+by simp
+
+lemma take_Suc2 [simp]: "take(a#xs)(Suc x) = a#take xs x"
+by simp
+
+lemma take_Nil [simp]: "take [] n = []"
+by (induct n) simp_all
+
+lemma take_take_eq [simp]: "\<forall>n. take (take xs n) n = take xs n"
+apply (induct xs rule: list_induct)
+apply simp_all
+apply (rule allI)
+apply (induct_tac n)
+apply auto
+done
+
+end
--- a/src/HOL/IsaMakefile Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/IsaMakefile Mon Feb 22 09:17:49 2010 +0100
@@ -455,8 +455,8 @@
$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \
Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy \
Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \
- Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/Term.thy \
- Induct/Tree.thy Induct/document/root.tex
+ Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy \
+ Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
--- a/src/HOL/Library/LaTeXsugar.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Mon Feb 22 09:17:49 2010 +0100
@@ -64,10 +64,10 @@
consts DUMMY :: 'a ("\<^raw:\_>")
(* THEOREMS *)
+notation (Rule output)
+ "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
syntax (Rule output)
- "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
-
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
@@ -76,21 +76,20 @@
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
-syntax (Axiom output)
- "Trueprop" :: "bool \<Rightarrow> prop"
- ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+notation (Axiom output)
+ "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+notation (IfThen output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThen output)
- "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+notation (IfThenNoBox output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThenNoBox output)
- "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
--- a/src/HOL/Library/OptionalSugar.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Library/OptionalSugar.thy Mon Feb 22 09:17:49 2010 +0100
@@ -37,15 +37,15 @@
(* Let *)
translations
- "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
- "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
+ "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
+ "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)"
"_tuple_args x (_tuple_args y z)" ==
"_tuple_args x (_tuple_arg (_tuple y z))"
- "_bind (Some p) e" <= "_bind p (CONST the e)"
- "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
- "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
+ "_bind (CONST Some p) e" <= "_bind p (CONST the e)"
+ "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
+ "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
(* type constraints with spacing *)
setup {*
--- a/src/HOL/Library/Quotient_Sum.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Mon Feb 22 09:17:49 2010 +0100
@@ -24,7 +24,7 @@
declare [[map "+" = (sum_map, sum_rel)]]
-text {* should probably be in Sum_Type.thy *}
+text {* should probably be in @{theory Sum_Type} *}
lemma split_sum_all:
shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
apply(auto)
--- a/src/HOL/List.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/List.thy Mon Feb 22 09:17:49 2010 +0100
@@ -358,11 +358,11 @@
parse_translation (advanced) {*
let
- val NilC = Syntax.const @{const_name Nil};
- val ConsC = Syntax.const @{const_name Cons};
- val mapC = Syntax.const @{const_name map};
- val concatC = Syntax.const @{const_name concat};
- val IfC = Syntax.const @{const_name If};
+ val NilC = Syntax.const @{const_syntax Nil};
+ val ConsC = Syntax.const @{const_syntax Cons};
+ val mapC = Syntax.const @{const_syntax map};
+ val concatC = Syntax.const @{const_syntax concat};
+ val IfC = Syntax.const @{const_syntax If};
fun singl x = ConsC $ x $ NilC;
@@ -371,12 +371,14 @@
val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
val e = if opti then singl e else e;
val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
- val case2 = Syntax.const @{syntax_const "_case1"} $ Syntax.const Term.dummy_patternN $ NilC;
+ val case2 =
+ Syntax.const @{syntax_const "_case1"} $
+ Syntax.const @{const_syntax dummy_pattern} $ NilC;
val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
in lambda x ft end;
- fun abs_tr ctxt (p as Free(s,T)) e opti =
+ fun abs_tr ctxt (p as Free (s, T)) e opti =
let
val thy = ProofContext.theory_of ctxt;
val s' = Sign.intern_const thy s;
@@ -1677,12 +1679,23 @@
lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
by(simp add: hd_conv_nth)
+lemma set_take_subset_set_take:
+ "m <= n \<Longrightarrow> set(take m xs) <= set(take n xs)"
+by(induct xs arbitrary: m n)(auto simp:take_Cons split:nat.split)
+
lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
+lemma set_drop_subset_set_drop:
+ "m >= n \<Longrightarrow> set(drop m xs) <= set(drop n xs)"
+apply(induct xs arbitrary: m n)
+apply(auto simp:drop_Cons split:nat.split)
+apply (metis set_drop_subset subset_iff)
+done
+
lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
using set_take_subset by fast
--- a/src/HOL/MicroJava/DFA/Semilat.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Mon Feb 22 09:17:49 2010 +0100
@@ -22,16 +22,17 @@
"lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
"plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
(*<*)
-syntax
- "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
- "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
- "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
+notation
+ "lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and
+ "lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and
+ "plussub" ("(_ /+'__ _)" [65, 1000, 66] 65)
(*>*)
-syntax (xsymbols)
- "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50)
- "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50)
- "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
+notation (xsymbols)
+ "lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
+ "lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
+ "plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
(*<*)
+syntax
(* allow \<sub> instead of \<bsub>..\<esub> *)
"_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
"_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Feb 22 09:17:49 2010 +0100
@@ -1,4 +1,4 @@
-(* Title: Library/Euclidean_Space
+(* Title: Library/Multivariate_Analysis/Euclidean_Space.thy
Author: Amine Chaieb, University of Cambridge
*)
@@ -66,8 +66,8 @@
instantiation cart :: (plus,finite) plus
begin
-definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))"
-instance ..
+ definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))"
+ instance ..
end
instantiation cart :: (times,finite) times
@@ -76,39 +76,42 @@
instance ..
end
-instantiation cart :: (minus,finite) minus begin
+instantiation cart :: (minus,finite) minus
+begin
definition vector_minus_def : "op - \<equiv> (\<lambda> x y. (\<chi> i. (x$i) - (y$i)))"
-instance ..
+ instance ..
end
-instantiation cart :: (uminus,finite) uminus begin
+instantiation cart :: (uminus,finite) uminus
+begin
definition vector_uminus_def : "uminus \<equiv> (\<lambda> x. (\<chi> i. - (x$i)))"
-instance ..
+ instance ..
end
-instantiation cart :: (zero,finite) zero begin
+instantiation cart :: (zero,finite) zero
+begin
definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)"
-instance ..
+ instance ..
end
-instantiation cart :: (one,finite) one begin
+instantiation cart :: (one,finite) one
+begin
definition vector_one_def : "1 \<equiv> (\<chi> i. 1)"
-instance ..
+ instance ..
end
instantiation cart :: (ord,finite) ord
- begin
-definition vector_le_def:
- "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
-definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"
-
-instance by (intro_classes)
+begin
+ definition vector_le_def:
+ "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
+ definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"
+ instance by (intro_classes)
end
instantiation cart :: (scaleR, finite) scaleR
begin
-definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
-instance ..
+ definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
+ instance ..
end
text{* Also the scalar-vector multiplication. *}
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Feb 22 09:17:49 2010 +0100
@@ -1,11 +1,11 @@
-(* Title: HOL/Library/Finite_Cartesian_Product
- Author: Amine Chaieb, University of Cambridge
+(* Title: HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
+ Author: Amine Chaieb, University of Cambridge
*)
header {* Definition of finite Cartesian product types. *}
theory Finite_Cartesian_Product
-imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
+imports Main
begin
subsection {* Finite Cartesian products, with indexing and lambdas. *}
@@ -14,9 +14,9 @@
('a, 'b) cart = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
morphisms Cart_nth Cart_lambda ..
-notation Cart_nth (infixl "$" 90)
-
-notation (xsymbols) Cart_lambda (binder "\<chi>" 10)
+notation
+ Cart_nth (infixl "$" 90) and
+ Cart_lambda (binder "\<chi>" 10)
(*
Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
@@ -39,10 +39,7 @@
*}
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
- apply auto
- apply (rule ext)
- apply auto
- done
+ by (auto intro: ext)
lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)
@@ -75,7 +72,10 @@
unfolding sndcart_def by simp
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"
-by (auto, case_tac x, auto)
+ apply auto
+ apply (case_tac x)
+ apply auto
+ done
lemma fstcart_pastecart[simp]: "fstcart (pastecart x y) = x"
by (simp add: Cart_eq)
@@ -90,9 +90,9 @@
using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis
lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))"
- by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
+ by (metis pastecart_fst_snd)
-lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"
- by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
+lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"
+ by (metis pastecart_fst_snd)
end
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Feb 22 09:17:49 2010 +0100
@@ -1547,7 +1547,7 @@
(augment_sort thy1 pt_cp_sort
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
(fn _ => rtac rec_induct 1 THEN REPEAT
- (simp_tac (Simplifier.theory_context thy11 HOL_basic_ss
+ (simp_tac (Simplifier.global_context thy11 HOL_basic_ss
addsimps flat perm_simps'
addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
(resolve_tac rec_intrs THEN_ALL_NEW
@@ -1951,7 +1951,7 @@
(HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
(fn _ => EVERY
[cut_facts_tac [th'] 1,
- full_simp_tac (Simplifier.theory_context thy11 HOL_ss
+ full_simp_tac (Simplifier.global_context thy11 HOL_ss
addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
addsimprocs [NominalPermeq.perm_simproc_app]) 1,
full_simp_tac (HOL_ss addsimps (calc_atm @
--- a/src/HOL/Nominal/nominal_inductive.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Feb 22 09:17:49 2010 +0100
@@ -274,7 +274,7 @@
val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
val pt2_atoms = map (fn aT => PureThy.get_thm thy
("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
- val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
+ val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
addsimprocs [mk_perm_bool_simproc ["Fun.id"],
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
@@ -455,7 +455,7 @@
concl))
in map mk_prem prems end) cases_prems;
- val cases_eqvt_ss = Simplifier.theory_context thy HOL_ss
+ val cases_eqvt_ss = Simplifier.global_context thy HOL_ss
addsimps eqvt_thms @ swap_simps @ perm_pi_simp
addsimprocs [NominalPermeq.perm_simproc_app,
NominalPermeq.perm_simproc_fun];
@@ -611,7 +611,7 @@
atoms)
end;
val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
- val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps
+ val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
(NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
[mk_perm_bool_simproc names,
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
--- a/src/HOL/Nominal/nominal_inductive2.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Feb 22 09:17:49 2010 +0100
@@ -292,7 +292,7 @@
val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
val pt2_atoms = map (fn a => PureThy.get_thm thy
("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
- val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
+ val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
addsimprocs [mk_perm_bool_simproc ["Fun.id"],
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
--- a/src/HOL/Nominal/nominal_permeq.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Mon Feb 22 09:17:49 2010 +0100
@@ -143,7 +143,7 @@
fun perm_simp_gen stac dyn_thms eqvt_thms ss i =
("general simplification of permutations", fn st =>
let
- val ss' = Simplifier.theory_context (theory_of_thm st) ss
+ val ss' = Simplifier.global_context (theory_of_thm st) ss
addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
delcongs weak_congs
addcongs strong_congs
@@ -221,7 +221,7 @@
("analysing permutation compositions on the lhs",
fn st => EVERY
[rtac trans i,
- asm_full_simp_tac (Simplifier.theory_context (theory_of_thm st) empty_ss
+ asm_full_simp_tac (Simplifier.global_context (theory_of_thm st) empty_ss
addsimprocs [perm_compose_simproc]) i,
asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st);
--- a/src/HOL/Prolog/prolog.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Prolog/prolog.ML Mon Feb 22 09:17:49 2010 +0100
@@ -59,7 +59,7 @@
in map zero_var_indexes (at thm) end;
val atomize_ss =
- Simplifier.theory_context @{theory} empty_ss
+ Simplifier.global_context @{theory} empty_ss
setmksimps (mksimps mksimps_pairs)
addsimps [
all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
--- a/src/HOL/Quotient.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Quotient.thy Mon Feb 22 09:17:49 2010 +0100
@@ -270,7 +270,7 @@
In the following theorem R1 can be instantiated with anything,
but we know some of the types of the Rep and Abs functions;
so by solving Quotient assumptions we can get a unique R1 that
- will be provable; which is why we need to use apply_rsp and
+ will be provable; which is why we need to use @{text apply_rsp} and
not the primed version *}
lemma apply_rsp:
@@ -465,7 +465,7 @@
using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
by metis
-section {* Bex1_rel quantifier *}
+section {* @{text Bex1_rel} quantifier *}
definition
Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
--- a/src/HOL/Tools/Datatype/datatype_case.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Mon Feb 22 09:17:49 2010 +0100
@@ -310,6 +310,8 @@
fun case_tr err tab_of ctxt [t, u] =
let
val thy = ProofContext.theory_of ctxt;
+ val intern_const_syntax = Consts.intern_syntax (Sign.consts_of thy);
+
(* replace occurrences of dummy_pattern by distinct variables *)
(* internalize constant names *)
fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
@@ -319,9 +321,7 @@
let val x = Name.variant used "x"
in (Free (x, T), x :: used) end
| prep_pat (Const (s, T)) used =
- (case try (unprefix Syntax.constN) s of
- SOME c => (Const (c, T), used)
- | NONE => (Const (Sign.intern_const thy s, T), used))
+ (Const (intern_const_syntax s, T), used)
| prep_pat (v as Free (s, T)) used =
let val s' = Sign.intern_const thy s
in
@@ -422,8 +422,7 @@
| _ => NONE;
val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
-val dest_case' = gen_dest_case
- (try (dest_Const #> fst #> unprefix Syntax.constN)) (K dummyT);
+val dest_case' = gen_dest_case (try (dest_Const #> fst #> Syntax.unmark_const)) (K dummyT);
(* destruct nested patterns *)
@@ -455,14 +454,13 @@
fun case_tr' tab_of cname ctxt ts =
let
val thy = ProofContext.theory_of ctxt;
- val consts = ProofContext.consts_of ctxt;
fun mk_clause (pat, rhs) =
let val xs = Term.add_frees pat []
in
Syntax.const @{syntax_const "_case1"} $
map_aterms
(fn Free p => Syntax.mark_boundT p
- | Const (s, _) => Const (Consts.extern_early consts s, dummyT)
+ | Const (s, _) => Syntax.const (Syntax.mark_const s)
| t => t) pat $
map_aterms
(fn x as Free (s, T) =>
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Feb 22 09:17:49 2010 +0100
@@ -223,7 +223,7 @@
fun add_case_tr' case_names thy =
Sign.add_advanced_trfuns ([], [],
map (fn case_name =>
- let val case_name' = Sign.const_syntax_name thy case_name
+ let val case_name' = Syntax.mark_const case_name
in (case_name', Datatype_Case.case_tr' info_of_case case_name')
end) case_names, []) thy;
--- a/src/HOL/Tools/Quotient/quotient_info.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Mon Feb 22 09:17:49 2010 +0100
@@ -59,7 +59,7 @@
(type T = maps_info Symtab.table
val empty = Symtab.empty
val extend = I
- val merge = Symtab.merge (K true))
+ fun merge data = Symtab.merge (K true) data)
fun maps_defined thy s =
Symtab.defined (MapsData.get thy) s
@@ -123,7 +123,7 @@
(type T = quotdata_info Symtab.table
val empty = Symtab.empty
val extend = I
- val merge = Symtab.merge (K true))
+ fun merge data = Symtab.merge (K true) data)
fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
{qtyp = Morphism.typ phi qtyp,
@@ -193,7 +193,7 @@
fun qconsts_lookup thy t =
let
val (name, qty) = dest_Const t
- fun matches x =
+ fun matches (x: qconsts_info) =
let
val (name', qty') = dest_Const (#qconst x);
in
--- a/src/HOL/Tools/TFL/rules.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Mon Feb 22 09:17:49 2010 +0100
@@ -663,7 +663,7 @@
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
let val globals = func::G
- val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss
+ val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
val dummy = term_ref := []
--- a/src/HOL/Tools/TFL/tfl.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Mon Feb 22 09:17:49 2010 +0100
@@ -440,7 +440,7 @@
(*case_ss causes minimal simplification: bodies of case expressions are
not simplified. Otherwise large examples (Red-Black trees) are too
slow.*)
- val case_ss = Simplifier.theory_context theory
+ val case_ss = Simplifier.global_context theory
(HOL_basic_ss addcongs
(map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
val corollaries' = map (Simplifier.simplify case_ss) corollaries
--- a/src/HOL/Tools/lin_arith.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Mon Feb 22 09:17:49 2010 +0100
@@ -6,7 +6,7 @@
signature LIN_ARITH =
sig
- val pre_tac: Proof.context -> int -> tactic
+ val pre_tac: simpset -> int -> tactic
val simple_tac: Proof.context -> int -> tactic
val tac: Proof.context -> int -> tactic
val simproc: simpset -> term -> thm option
@@ -705,13 +705,12 @@
setmksimps (mksimps mksimps_pairs)
addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj,
not_all, not_ex, not_not]
- fun prem_nnf_tac i st =
- full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset)
- i st
+ fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset)
in
-fun split_once_tac ctxt split_thms =
+fun split_once_tac ss split_thms =
let
+ val ctxt = Simplifier.the_context ss
val thy = ProofContext.theory_of ctxt
val cond_split_tac = SUBGOAL (fn (subgoal, i) =>
let
@@ -734,7 +733,7 @@
REPEAT_DETERM o etac rev_mp,
cond_split_tac,
rtac ccontr,
- prem_nnf_tac,
+ prem_nnf_tac ss,
TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
]
end;
@@ -746,15 +745,16 @@
(* subgoals and finally attempt to solve them by finding an immediate *)
(* contradiction (i.e., a term and its negation) in their premises. *)
-fun pre_tac ctxt i =
+fun pre_tac ss i =
let
+ val ctxt = Simplifier.the_context ss;
val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
fun is_relevant t = is_some (decomp ctxt t)
in
DETERM (
TRY (filter_prems_tac is_relevant i)
THEN (
- (TRY o REPEAT_ALL_NEW (split_once_tac ctxt split_thms))
+ (TRY o REPEAT_ALL_NEW (split_once_tac ss split_thms))
THEN_ALL_NEW
(CONVERSION Drule.beta_eta_conversion
THEN'
@@ -859,7 +859,7 @@
addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
@{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
fun prem_nnf_tac i st =
- full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
+ full_simp_tac (Simplifier.global_context (Thm.theory_of_thm st) nnf_simpset) i st;
in
fun refute_tac test prep_tac ref_tac =
let val refute_prems_tac =
--- a/src/HOL/Tools/record.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/record.ML Mon Feb 22 09:17:49 2010 +0100
@@ -145,16 +145,15 @@
rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
val isomT = fastype_of body;
- val isom_bind = Binding.name (name ^ isoN);
- val isom_name = Sign.full_name typ_thy isom_bind;
+ val isom_binding = Binding.name (name ^ isoN);
+ val isom_name = Sign.full_name typ_thy isom_binding;
val isom = Const (isom_name, isomT);
- val isom_spec = (Thm.def_name (name ^ isoN), Logic.mk_equals (isom, body));
val ([isom_def], cdef_thy) =
typ_thy
- |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
+ |> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd
|> PureThy.add_defs false
- [Thm.no_attributes (apfst (Binding.conceal o Binding.name) isom_spec)];
+ [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
@@ -162,7 +161,7 @@
val thm_thy =
cdef_thy
|> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
- |> Sign.parent_path
+ |> Sign.restore_naming thy
|> Code.add_default_eqn isom_def;
in
((isom, cons $ isom), thm_thy)
@@ -280,11 +279,9 @@
(* constructor *)
-fun mk_extC (name, T) Ts = (suffix extN name, Ts ---> T);
-
fun mk_ext (name, T) ts =
let val Ts = map fastype_of ts
- in list_comb (Const (mk_extC (name, T) Ts), ts) end;
+ in list_comb (Const (suffix extN name, Ts ---> T), ts) end;
(* selector *)
@@ -518,7 +515,7 @@
val is_selector = Symtab.defined o #selectors o get_sel_upd;
val get_updates = Symtab.lookup o #updates o get_sel_upd;
-fun get_ss_with_context getss thy = Simplifier.theory_context thy (getss (get_sel_upd thy));
+fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));
val get_simpset = get_ss_with_context #simpset;
val get_sel_upd_defs = get_ss_with_context #defset;
@@ -802,10 +799,7 @@
let
val (args, rest) = split_args (map fst (but_last fields)) fargs;
val more' = mk_ext rest;
- in
- (* FIXME authentic syntax *)
- list_comb (Syntax.const (suffix extN ext), args @ [more'])
- end
+ in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end
| NONE => err ("no fields defined for " ^ ext))
| NONE => err (name ^ " is no proper field"))
| mk_ext [] = more;
@@ -848,96 +842,6 @@
val print_record_type_abbr = Unsynchronized.ref true;
val print_record_type_as_fields = Unsynchronized.ref true;
-local
-
-fun field_updates_tr' (tm as Const (c, _) $ k $ u) =
- let
- val t =
- (case k of
- Abs (_, _, Abs (_, _, t) $ Bound 0) =>
- if null (loose_bnos t) then t else raise Match
- | Abs (_, _, t) =>
- if null (loose_bnos t) then t else raise Match
- | _ => raise Match);
- in
- (case try (unsuffix updateN) c of
- SOME name =>
- (* FIXME check wrt. record data (??) *)
- (* FIXME early extern (!??) *)
- apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
- (field_updates_tr' u)
- | NONE => ([], tm))
- end
- | field_updates_tr' tm = ([], tm);
-
-fun record_update_tr' tm =
- (case field_updates_tr' tm of
- ([], _) => raise Match
- | (ts, u) =>
- Syntax.const @{syntax_const "_record_update"} $ u $
- foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
-
-in
-
-fun field_update_tr' name =
- let
- (* FIXME authentic syntax *)
- val update_name = suffix updateN name;
- fun tr' [t, u] = record_update_tr' (Syntax.const update_name $ t $ u)
- | tr' _ = raise Match;
- in (update_name, tr') end;
-
-end;
-
-
-local
-
-(* FIXME early extern (!??) *)
-(* FIXME Syntax.free (??) *)
-fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
-
-fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
-
-fun record_tr' ctxt t =
- let
- val thy = ProofContext.theory_of ctxt;
-
- fun strip_fields t =
- (case strip_comb t of
- (Const (ext, _), args as (_ :: _)) =>
- (case try (unsuffix extN) (Sign.intern_const thy ext) of (* FIXME authentic syntax *)
- SOME ext' =>
- (case get_extfields thy ext' of
- SOME fields =>
- (let
- val f :: fs = but_last (map fst fields);
- val fields' = Sign.extern_const thy f :: map Long_Name.base_name fs;
- val (args', more) = split_last args;
- in (fields' ~~ args') @ strip_fields more end
- handle Library.UnequalLengths => [("", t)])
- | NONE => [("", t)])
- | NONE => [("", t)])
- | _ => [("", t)]);
-
- val (fields, (_, more)) = split_last (strip_fields t);
- val _ = null fields andalso raise Match;
- val u = foldr1 fields_tr' (map field_tr' fields);
- in
- case more of
- Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
- | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
- end;
-
-in
-
-fun record_ext_tr' name =
- let
- val ext_name = suffix extN name;
- fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
- in (ext_name, tr') end;
-
-end;
-
local
@@ -1059,6 +963,97 @@
end;
+local
+
+(* FIXME Syntax.free (??) *)
+fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
+fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
+
+fun record_tr' ctxt t =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val extern = Consts.extern (ProofContext.consts_of ctxt);
+
+ fun strip_fields t =
+ (case strip_comb t of
+ (Const (ext, _), args as (_ :: _)) =>
+ (case try (Syntax.unmark_const o unsuffix extN) ext of
+ SOME ext' =>
+ (case get_extfields thy ext' of
+ SOME fields =>
+ (let
+ val f :: fs = but_last (map fst fields);
+ val fields' = extern f :: map Long_Name.base_name fs;
+ val (args', more) = split_last args;
+ in (fields' ~~ args') @ strip_fields more end
+ handle Library.UnequalLengths => [("", t)])
+ | NONE => [("", t)])
+ | NONE => [("", t)])
+ | _ => [("", t)]);
+
+ val (fields, (_, more)) = split_last (strip_fields t);
+ val _ = null fields andalso raise Match;
+ val u = foldr1 fields_tr' (map field_tr' fields);
+ in
+ case more of
+ Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
+ | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
+ end;
+
+in
+
+fun record_ext_tr' name =
+ let
+ val ext_name = Syntax.mark_const (name ^ extN);
+ fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
+ in (ext_name, tr') end;
+
+end;
+
+
+local
+
+fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
+ let
+ val extern = Consts.extern (ProofContext.consts_of ctxt);
+ val t =
+ (case k of
+ Abs (_, _, Abs (_, _, t) $ Bound 0) =>
+ if null (loose_bnos t) then t else raise Match
+ | Abs (_, _, t) =>
+ if null (loose_bnos t) then t else raise Match
+ | _ => raise Match);
+ in
+ (case Option.map extern (try Syntax.unmark_const c) of
+ SOME update_name =>
+ (case try (unsuffix updateN) update_name of
+ SOME name =>
+ apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
+ (field_updates_tr' ctxt u)
+ | NONE => ([], tm))
+ | NONE => ([], tm))
+ end
+ | field_updates_tr' _ tm = ([], tm);
+
+fun record_update_tr' ctxt tm =
+ (case field_updates_tr' ctxt tm of
+ ([], _) => raise Match
+ | (ts, u) =>
+ Syntax.const @{syntax_const "_record_update"} $ u $
+ foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
+
+in
+
+fun field_update_tr' name =
+ let
+ val update_name = Syntax.mark_const (name ^ updateN);
+ fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
+ | tr' _ _ = raise Match;
+ in (update_name, tr') end;
+
+end;
+
+
(** record simprocs **)
@@ -1573,11 +1568,9 @@
(s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
| _ => false);
- fun is_all t =
- (case t of
- Const (quantifier, _) $ _ =>
- if quantifier = @{const_name all} orelse quantifier = @{const_name All} then ~1 else 0
- | _ => 0);
+ fun is_all (Const (@{const_name all}, _) $ _) = ~1
+ | is_all (Const (@{const_name All}, _) $ _) = ~1
+ | is_all _ = 0;
in
if has_rec goal then
Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i
@@ -1662,27 +1655,30 @@
fun extension_definition name fields alphas zeta moreT more vars thy =
let
- val base = Long_Name.base_name;
+ val base_name = Long_Name.base_name name;
+
val fieldTs = map snd fields;
+ val fields_moreTs = fieldTs @ [moreT];
+
val alphas_zeta = alphas @ [zeta];
val alphas_zetaTs = map (fn a => TFree (a, HOLogic.typeS)) alphas_zeta;
- val extT_name = suffix ext_typeN name
- val extT = Type (extT_name, alphas_zetaTs);
- val fields_moreTs = fieldTs @ [moreT];
-
-
- (*before doing anything else, create the tree of new types
- that will back the record extension*)
+
+ val ext_binding = Binding.name (suffix extN base_name);
+ val ext_name = suffix extN name;
+ val extT = Type (suffix ext_typeN name, alphas_zetaTs);
+ val ext_type = fields_moreTs ---> extT;
+
+
+ (* the tree of new types that will back the record extension *)
val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
fun mk_iso_tuple (left, right) (thy, i) =
let
val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
- val nm = suffix suff (Long_Name.base_name name);
- val ((_, cons), thy') =
- Iso_Tuple_Support.add_iso_tuple_type
- (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
+ val ((_, cons), thy') = thy
+ |> Iso_Tuple_Support.add_iso_tuple_type
+ (suffix suff base_name, alphas_zeta) (fastype_of left, fastype_of right);
in
(cons $ left $ right, (thy', i + 1))
end;
@@ -1720,19 +1716,15 @@
(* prepare declarations and definitions *)
- (*fields constructor*)
- val ext_decl = mk_extC (name, extT) fields_moreTs;
- val ext_spec = list_comb (Const ext_decl, vars @ [more]) :== ext_body;
-
- fun mk_ext args = list_comb (Const ext_decl, args);
-
-
(* 1st stage part 2: define the ext constant *)
+ fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
+ val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
+
fun mk_defs () =
typ_thy
- |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)]
- |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name ext_spec)]
+ |> Sign.declare_const ((ext_binding, ext_type), NoSyn) |> snd
+ |> PureThy.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
||> Theory.checkpoint
val ([ext_def], defs_thy) =
timeit_msg "record extension constructor def:" mk_defs;
@@ -1856,7 +1848,7 @@
fun obj_to_meta_all thm =
let
fun E thm = (* FIXME proper name *)
- (case (SOME (spec OF [thm]) handle THM _ => NONE) of
+ (case SOME (spec OF [thm]) handle THM _ => NONE of
SOME thm' => E thm'
| NONE => thm);
val th1 = E thm;
@@ -1876,16 +1868,12 @@
(* record_definition *)
-fun record_definition (args, b) parent (parents: parent_info list) raw_fields thy =
+fun record_definition (args, binding) parent (parents: parent_info list) raw_fields thy =
let
- val external_names = Name_Space.external_names (Sign.naming_of thy);
-
val alphas = map fst args;
- val base_name = Binding.name_of b; (* FIXME include qualifier etc. (!?) *)
- val name = Sign.full_name thy b;
- val full = Sign.full_name_path thy base_name;
- val base = Long_Name.base_name;
+ val name = Sign.full_name thy binding;
+ val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *)
val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
val field_syntax = map #3 raw_fields;
@@ -1895,13 +1883,13 @@
val parent_names = map fst parent_fields;
val parent_types = map snd parent_fields;
val parent_fields_len = length parent_fields;
- val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
+ val parent_variants =
+ Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
val parent_vars = ListPair.map Free (parent_variants, parent_types);
val parent_len = length parents;
val fields = map (apfst full) bfields;
val names = map fst fields;
- val extN = full b;
val types = map snd fields;
val alphas_fields = fold Term.add_tfree_namesT types [];
val alphas_ext = inter (op =) alphas_fields alphas;
@@ -1931,18 +1919,20 @@
val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
- (* 1st stage: extension_thy *)
-
- val ((extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), extension_thy) =
+ (* 1st stage: ext_thy *)
+
+ val extension_name = full binding;
+
+ val ((extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
thy
- |> Sign.add_path base_name
- |> extension_definition extN fields alphas_ext zeta moreT more vars;
+ |> Sign.qualified_path false binding
+ |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
val _ = timing_msg "record preparing definitions";
val Type extension_scheme = extT;
val extension_name = unsuffix ext_typeN (fst extension_scheme);
val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
- val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
+ val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extension_name];
val extension_id = implode extension_names;
fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
@@ -1978,13 +1968,9 @@
val w = Free (wN, rec_schemeT 0)
- (* prepare print translation functions *)
- (* FIXME authentic syntax *)
-
- val field_update_tr's =
- map field_update_tr' (distinct (op =) (maps external_names (full_moreN :: names)));
-
- val record_ext_tr's = map record_ext_tr' (external_names extN);
+ (* print translations *)
+
+ val external_names = Name_Space.external_names (Sign.naming_of ext_thy);
val record_ext_type_abbr_tr's =
let
@@ -1995,9 +1981,13 @@
val record_ext_type_tr's =
let
(*avoid conflict with record_type_abbr_tr's*)
- val trnames = if parent_len > 0 then external_names extN else [];
+ val trnames = if parent_len > 0 then external_names extension_name else [];
in map record_ext_type_tr' trnames end;
+ val advanced_print_translation =
+ map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
+ record_ext_type_tr's @ record_ext_type_abbr_tr's;
+
(* prepare declarations *)
@@ -2013,8 +2003,8 @@
(*record (scheme) type abbreviation*)
val recordT_specs =
- [(Binding.suffix_name schemeN b, alphas @ [zeta], rec_schemeT0, NoSyn),
- (b, alphas, recT0, NoSyn)];
+ [(Binding.suffix_name schemeN binding, alphas @ [zeta], rec_schemeT0, NoSyn),
+ (binding, alphas, recT0, NoSyn)];
val ext_defs = ext_def :: map #ext_def parents;
@@ -2035,8 +2025,8 @@
fun to_Var (Free (c, T)) = Var ((c, 1), T);
in mk_rec (map to_Var all_vars_more) 0 end;
- val cterm_rec = cterm_of extension_thy r_rec0;
- val cterm_vrs = cterm_of extension_thy r_rec0_Vars;
+ val cterm_rec = cterm_of ext_thy r_rec0;
+ val cterm_vrs = cterm_of ext_thy r_rec0_Vars;
val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
val init_thm = named_cterm_instantiate insts updacc_eq_triv;
val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
@@ -2057,10 +2047,10 @@
(*selectors*)
fun mk_sel_spec ((c, T), thm) =
let
- val acc $ arg =
- (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Envir.beta_eta_contract o concl_of) thm;
+ val (acc $ arg, _) =
+ HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
val _ =
- if (arg aconv r_rec0) then ()
+ if arg aconv r_rec0 then ()
else raise TERM ("mk_sel_spec: different arg", [arg]);
in
Const (mk_selC rec_schemeT0 (c, T)) :== acc
@@ -2070,8 +2060,8 @@
(*updates*)
fun mk_upd_spec ((c, T), thm) =
let
- val upd $ _ $ arg =
- fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (concl_of thm))));
+ val (upd $ _ $ arg, _) =
+ HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
val _ =
if arg aconv r_rec0 then ()
else raise TERM ("mk_sel_spec: different arg", [arg]);
@@ -2096,17 +2086,15 @@
(* 2st stage: defs_thy *)
fun mk_defs () =
- extension_thy
- |> Sign.add_trfuns ([], [], field_update_tr's, [])
- |> Sign.add_advanced_trfuns
- ([], [], record_ext_tr's @ record_ext_type_tr's @ record_ext_type_abbr_tr's, [])
- |> Sign.parent_path
+ ext_thy
+ |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
+ |> Sign.restore_naming thy
|> Sign.add_tyabbrs_i recordT_specs
- |> Sign.add_path base_name
- |> Sign.add_consts_i
- (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx)) sel_decls (field_syntax @ [NoSyn]))
- |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, NoSyn)))
- (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
+ |> Sign.qualified_path false binding
+ |> fold (fn ((x, T), mx) => snd o Sign.declare_const ((Binding.name x, T), mx))
+ (sel_decls ~~ (field_syntax @ [NoSyn]))
+ |> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn))
+ (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
|> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
sel_specs
||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
@@ -2137,9 +2125,9 @@
(*updates*)
fun mk_upd_prop (i, (c, T)) =
let
- val x' = Free (Name.variant all_variants (base c ^ "'"), T --> T);
+ val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
val n = parent_fields_len + i;
- val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more
+ val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
@@ -2401,7 +2389,7 @@
|> add_record_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
|> add_extfields extension_name (fields @ [(full_moreN, moreT)])
|> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
- |> Sign.parent_path;
+ |> Sign.restore_naming thy;
in final_thy end;
@@ -2411,12 +2399,12 @@
(*We do all preparations and error checks here, deferring the real
work to record_definition.*)
fun gen_add_record prep_typ prep_raw_parent quiet_mode
- (params, b) raw_parent raw_fields thy =
+ (params, binding) raw_parent raw_fields thy =
let
val _ = Theory.requires thy "Record" "record definitions";
val _ =
if quiet_mode then ()
- else writeln ("Defining record " ^ quote (Binding.name_of b) ^ " ...");
+ else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
val ctxt = ProofContext.init thy;
@@ -2456,7 +2444,7 @@
(* errors *)
- val name = Sign.full_name thy b;
+ val name = Sign.full_name thy binding;
val err_dup_record =
if is_none (get_record thy name) then []
else ["Duplicate definition of record " ^ quote name];
@@ -2493,9 +2481,9 @@
val _ = if null errs then () else error (cat_lines errs);
in
- thy |> record_definition (args, b) parent parents bfields
+ thy |> record_definition (args, binding) parent parents bfields
end
- handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of b));
+ handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
val add_record = gen_add_record cert_typ (K I);
val add_record_cmd = gen_add_record read_typ read_raw_parent;
--- a/src/HOL/Tools/simpdata.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/simpdata.ML Mon Feb 22 09:17:49 2010 +0100
@@ -164,7 +164,7 @@
("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
val HOL_basic_ss =
- Simplifier.theory_context @{theory} empty_ss
+ Simplifier.global_context @{theory} empty_ss
setsubgoaler asm_simp_tac
setSSolver safe_solver
setSolver unsafe_solver
--- a/src/HOL/Tools/string_syntax.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML Mon Feb 22 09:17:49 2010 +0100
@@ -15,15 +15,14 @@
(* nibble *)
-val nib_prefix = "String.nibble.";
-
val mk_nib =
- Syntax.Constant o unprefix nib_prefix o
+ Syntax.Constant o Syntax.mark_const o
fst o Term.dest_Const o HOLogic.mk_nibble;
-fun dest_nib (Syntax.Constant c) =
- HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT))
- handle TERM _ => raise Match;
+fun dest_nib (Syntax.Constant s) =
+ (case try Syntax.unmark_const s of
+ NONE => raise Match
+ | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
(* char *)
--- a/src/HOL/Tools/typedef.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/Tools/typedef.ML Mon Feb 22 09:17:49 2010 +0100
@@ -119,8 +119,7 @@
if def then
theory
|> Sign.add_consts_i [(name, setT', NoSyn)] (* FIXME authentic syntax *)
- |> PureThy.add_defs false
- [((Binding.map_name Thm.def_name name, Logic.mk_equals (setC, set)), [])]
+ |> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])]
|-> (fn [th] => pair (SOME th))
else (NONE, theory);
fun contract_def NONE th = th
--- a/src/HOL/ex/Arith_Examples.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/ex/Arith_Examples.thy Mon Feb 22 09:17:49 2010 +0100
@@ -123,12 +123,12 @@
(* FIXME: need to replace 1 by its numeral representation *)
apply (subst numeral_1_eq_1 [symmetric])
(* FIXME: arith does not know about iszero *)
- apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
+ apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
oops
lemma "(i::int) mod 42 <= 41"
(* FIXME: arith does not know about iszero *)
- apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
+ apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
oops
lemma "-(i::int) * 1 = 0 ==> i = 0"
--- a/src/HOL/ex/Binary.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOL/ex/Binary.thy Mon Feb 22 09:17:49 2010 +0100
@@ -191,7 +191,7 @@
parse_translation {*
let
val syntax_consts =
- map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
+ map_aterms (fn Const (c, T) => Const (Syntax.mark_const c, T) | a => a);
fun binary_tr [Const (num, _)] =
let
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Mon Feb 22 09:17:49 2010 +0100
@@ -8,7 +8,7 @@
imports HOLCF
begin
-domain 'a seq = nil | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65)
+domain 'a seq = nil ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65)
consts
sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Feb 22 09:17:49 2010 +0100
@@ -40,7 +40,7 @@
"_partlist" :: "args => 'a Seq" ("[(_)?]")
translations
"[x, xs!]" == "x>>[xs!]"
- "[x!]" == "x>>CONST nil"
+ "[x!]" == "x>>nil"
"[x, xs?]" == "x>>[xs?]"
"[x?]" == "x>>CONST UU"
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Mon Feb 22 09:17:49 2010 +0100
@@ -7,6 +7,7 @@
signature DOMAIN_SYNTAX =
sig
val calc_syntax:
+ theory ->
bool ->
typ ->
(string * typ list) *
@@ -28,7 +29,7 @@
open Domain_Library;
infixr 5 -->; infixr 6 ->>;
-fun calc_syntax (* FIXME authentic syntax *)
+fun calc_syntax thy
(definitional : bool)
(dtypeprod : typ)
((dname : string, typevars : typ list),
@@ -60,7 +61,7 @@
val escape = let
fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
else c::esc cs
- | esc [] = []
+ | esc [] = []
in implode o esc o Symbol.explode end;
fun dis_name_ con =
@@ -113,41 +114,45 @@
(* ----- case translation --------------------------------------------------- *)
+ fun syntax b = Syntax.mark_const (Sign.full_bname thy b);
+
local open Syntax in
local
- fun c_ast con mx = Constant (Binding.name_of con); (* FIXME proper const syntax *)
- fun expvar n = Variable ("e"^(string_of_int n));
- fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
- (string_of_int m));
+ fun c_ast authentic con = Constant ((authentic ? syntax) (Binding.name_of con));
+ fun expvar n = Variable ("e" ^ string_of_int n);
+ fun argvar n m _ = Variable ("a" ^ string_of_int n ^ "_" ^ string_of_int m);
fun argvars n args = mapn (argvar n) 1 args;
- fun app s (l,r) = mk_appl (Constant s) [l,r];
+ fun app s (l, r) = mk_appl (Constant s) [l, r];
val cabs = app "_cabs";
- val capp = app "Rep_CFun";
- fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
- fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
+ val capp = app @{const_syntax Rep_CFun};
+ fun con1 authentic n (con,args,mx) =
+ Library.foldl capp (c_ast authentic con, argvars n args);
+ fun case1 authentic n (con,args,mx) =
+ app "_case1" (con1 authentic n (con,args,mx), expvar n);
fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
- fun when1 n m = if n = m then arg1 n else K (Constant "UU");
+ fun when1 n m = if n = m then arg1 n else K (Constant @{const_syntax UU});
fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
fun app_pat x = mk_appl (Constant "_pat") [x];
fun args_list [] = Constant "_noargs"
- | args_list xs = foldr1 (app "_args") xs;
+ | args_list xs = foldr1 (app "_args") xs;
in
- val case_trans =
- ParsePrintRule
- (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
- capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
-
- fun one_abscon_trans n (con,mx,args) =
+ fun case_trans authentic =
ParsePrintRule
- (cabs (con1 n (con,mx,args), expvar n),
- Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'));
- val abscon_trans = mapn one_abscon_trans 1 cons';
+ (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn (case1 authentic) 1 cons')),
+ capp (Library.foldl capp
+ (Constant (syntax (dnam ^ "_when")), mapn arg1 1 cons'), Variable "x"));
- fun one_case_trans (con,args,mx) =
+ fun one_abscon_trans authentic n (con,mx,args) =
+ ParsePrintRule
+ (cabs (con1 authentic n (con,mx,args), expvar n),
+ Library.foldl capp (Constant (syntax (dnam ^ "_when")), mapn (when1 n) 1 cons'));
+ fun abscon_trans authentic = mapn (one_abscon_trans authentic) 1 cons';
+
+ fun one_case_trans authentic (con,args,mx) =
let
- val cname = c_ast con mx;
- val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
+ val cname = c_ast authentic con;
+ val pname = Constant (syntax (strip_esc (Binding.name_of con) ^ "_pat"));
val ns = 1 upto length args;
val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
@@ -160,7 +165,7 @@
PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
app "_match" (mk_appl pname ps, args_list vs))]
end;
- val Case_trans = maps one_case_trans cons';
+ val Case_trans = maps (one_case_trans false) cons' @ maps (one_case_trans true) cons';
end;
end;
val optional_consts =
@@ -169,7 +174,7 @@
in (optional_consts @ [const_when] @
consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
[const_take, const_finite],
- (case_trans::(abscon_trans @ Case_trans)))
+ (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans)))
end; (* let *)
(* ----- putting all the syntax stuff together ------------------------------ *)
@@ -192,9 +197,9 @@
val const_bisim =
(Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list =
- map (calc_syntax definitional funprod) eqs';
+ map (calc_syntax thy'' definitional funprod) eqs';
in thy''
- |> ContConsts.add_consts_i
+ |> Cont_Consts.add_consts
(maps fst ctt @
(if length eqs'>1 andalso not definitional
then [const_copy] else []) @
--- a/src/HOLCF/Tools/cont_consts.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML Mon Feb 22 09:17:49 2010 +0100
@@ -7,37 +7,28 @@
signature CONT_CONSTS =
sig
- val add_consts: (binding * string * mixfix) list -> theory -> theory
- val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
+ val add_consts: (binding * typ * mixfix) list -> theory -> theory
+ val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory
end;
-structure ContConsts: CONT_CONSTS =
+structure Cont_Consts: CONT_CONSTS =
struct
(* misc utils *)
-fun first (x,_,_) = x;
-fun second (_,x,_) = x;
-fun third (_,_,x) = x;
-fun upd_first f (x,y,z) = (f x, y, z);
-fun upd_second f (x,y,z) = ( x, f y, z);
-fun upd_third f (x,y,z) = ( x, y, f z);
-
-fun change_arrow 0 T = T
-| change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
-| change_arrow _ _ = sys_error "cont_consts: change_arrow";
+fun change_arrow 0 T = T
+ | change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T])
+ | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []);
fun trans_rules name2 name1 n mx =
let
- fun argnames _ 0 = []
- | argnames c n = chr c::argnames (c+1) (n-1);
- val vnames = argnames (ord "A") n;
+ val vnames = Name.invents Name.context "a" n;
val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
in
[Syntax.ParsePrintRule
(Syntax.mk_appl (Constant name2) (map Variable vnames),
- fold (fn arg => fn t => Syntax.mk_appl (Constant "Rep_CFun") [t, Variable arg])
+ fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_CFun}) [t, Variable a])
vnames (Constant name1))] @
(case mx of
Infix _ => [extra_parse_rule]
@@ -53,42 +44,51 @@
declaration with the original name, type ...=>..., and the original mixfix
is generated and connected to the other declaration via some translation.
*)
-fun transform (c, T, mx) =
- let
- val c1 = Binding.name_of c;
- val c2 = "_cont_" ^ c1;
- val n = Syntax.mixfix_args mx
- in ((c, T, NoSyn),
- (Binding.name c2, change_arrow n T, mx),
- trans_rules c2 c1 n mx) end;
+fun transform thy (c, T, mx) =
+ let
+ fun syntax b = Syntax.mark_const (Sign.full_bname thy b);
+ val c1 = Binding.name_of c;
+ val c2 = c1 ^ "_cont_syntax";
+ val n = Syntax.mixfix_args mx;
+ in
+ ((c, T, NoSyn),
+ (Binding.name c2, change_arrow n T, mx),
+ trans_rules (syntax c2) (syntax c1) n mx)
+ end;
-fun cfun_arity (Type(n,[_,T])) = if n = @{type_name "->"} then 1+cfun_arity T else 0
-| cfun_arity _ = 0;
+fun cfun_arity (Type (n, [_, T])) = if n = @{type_name "->"} then 1 + cfun_arity T else 0
+ | cfun_arity _ = 0;
-fun is_contconst (_,_,NoSyn ) = false
-| is_contconst (_,_,Binder _) = false
-| is_contconst (c,T,mx ) =
- cfun_arity T >= Syntax.mixfix_args mx
- handle ERROR msg => cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c));
+fun is_contconst (_, _, NoSyn) = false
+ | is_contconst (_, _, Binder _) = false (* FIXME ? *)
+ | is_contconst (c, T, mx) =
+ let
+ val n = Syntax.mixfix_args mx handle ERROR msg =>
+ cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c));
+ in cfun_arity T >= n end;
-(* add_consts(_i) *)
+(* add_consts *)
+
+local
fun gen_add_consts prep_typ raw_decls thy =
let
- val decls = map (upd_second (prep_typ thy)) raw_decls;
+ val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls;
val (contconst_decls, normal_decls) = List.partition is_contconst decls;
- val transformed_decls = map transform contconst_decls;
+ val transformed_decls = map (transform thy) contconst_decls;
in
thy
- |> Sign.add_consts_i
- (normal_decls @ map first transformed_decls @ map second transformed_decls)
- (* FIXME authentic syntax *)
- |> Sign.add_trrules_i (maps third transformed_decls)
+ |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
+ |> Sign.add_trrules_i (maps #3 transformed_decls)
end;
-val add_consts = gen_add_consts Syntax.read_typ_global;
-val add_consts_i = gen_add_consts Sign.certify_typ;
+in
+
+val add_consts = gen_add_consts Sign.certify_typ;
+val add_consts_cmd = gen_add_consts Syntax.read_typ_global;
+
+end;
(* outer syntax *)
@@ -97,7 +97,7 @@
val _ =
OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
- (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts));
+ (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts_cmd));
end;
--- a/src/Provers/Arith/fast_lin_arith.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Feb 22 09:17:49 2010 +0100
@@ -56,7 +56,7 @@
val pre_decomp: Proof.context -> typ list * term list -> (typ list * term list) list
(*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
- val pre_tac: Proof.context -> int -> tactic
+ val pre_tac: simpset -> int -> tactic
(*the limit on the number of ~= allowed; because each ~= is split
into two cases, this can lead to an explosion*)
@@ -792,7 +792,7 @@
(* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
(* user-defined preprocessing of the subgoal *)
- DETERM (LA_Data.pre_tac ctxt i) THEN
+ DETERM (LA_Data.pre_tac ss i) THEN
PRIMITIVE (trace_thm ctxt "State after pre_tac:") THEN
(* prove every resulting subgoal, using its justification *)
EVERY (map just1 justs)
--- a/src/Provers/hypsubst.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Provers/hypsubst.ML Mon Feb 22 09:17:49 2010 +0100
@@ -156,7 +156,7 @@
let fun tac i st = SUBGOAL (fn (Bi, _) =>
let
val (k, _) = eq_var bnd true Bi
- val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss
+ val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
setmksimps (mk_eqs bnd)
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
etac thin_rl i, rotate_tac (~k) i]
--- a/src/Pure/Concurrent/task_queue.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Mon Feb 22 09:17:49 2010 +0100
@@ -34,12 +34,14 @@
val finish: task -> queue -> bool * queue
end;
-structure Task_Queue:> TASK_QUEUE =
+structure Task_Queue: TASK_QUEUE =
struct
(* tasks *)
-datatype task = Task of int option * serial;
+abstype task = Task of int option * serial
+with
+
val dummy_task = Task (NONE, ~1);
fun new_task pri = Task (pri, serial ());
@@ -47,15 +49,20 @@
fun str_of_task (Task (_, i)) = string_of_int i;
fun task_ord (Task t1, Task t2) = prod_ord (rev_order o option_ord int_ord) int_ord (t1, t2);
+val eq_task = is_equal o task_ord;
+
+end;
+
structure Task_Graph = Graph(type key = task val ord = task_ord);
(* nested groups *)
-datatype group = Group of
+abstype group = Group of
{parent: group option,
id: serial,
- status: exn list Synchronized.var};
+ status: exn list Synchronized.var}
+with
fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
@@ -90,6 +97,8 @@
fun str_of_group group =
(is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
+end;
+
(* jobs *)
@@ -246,7 +255,7 @@
let
val group = get_group jobs task;
val groups' = groups
- |> fold (fn gid => Inttab.remove_list (op =) (gid, task)) (group_ancestry group);
+ |> fold (fn gid => Inttab.remove_list eq_task (gid, task)) (group_ancestry group);
val jobs' = Task_Graph.del_node task jobs;
val maximal = null (Task_Graph.imm_succs jobs task);
in (maximal, make_queue groups' jobs') end;
--- a/src/Pure/Isar/expression.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/Isar/expression.ML Mon Feb 22 09:17:49 2010 +0100
@@ -604,7 +604,7 @@
(* achieve plain syntax for locale predicates (without "PROP") *)
-fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
+fun aprop_tr' n c = (Syntax.mark_const c, fn ctxt => fn args =>
if length args = n then
Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *)
Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
@@ -641,8 +641,7 @@
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
|> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
|> PureThy.add_defs false
- [((Binding.conceal (Binding.map_name Thm.def_name binding),
- Logic.mk_equals (head, body)), [])];
+ [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
val cert = Thm.cterm_of defs_thy;
--- a/src/Pure/Isar/proof_context.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Feb 22 09:17:49 2010 +0100
@@ -28,7 +28,6 @@
val full_name: Proof.context -> binding -> string
val syn_of: Proof.context -> Syntax.syntax
val consts_of: Proof.context -> Consts.T
- val const_syntax_name: Proof.context -> string -> string
val the_const_constraint: Proof.context -> string -> typ
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
@@ -235,7 +234,6 @@
val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
val consts_of = #1 o #consts o rep_context;
-val const_syntax_name = Consts.syntax_name o consts_of;
val the_const_constraint = Consts.the_constraint o consts_of;
val facts_of = #facts o rep_context;
@@ -707,10 +705,10 @@
val consts = consts_of ctxt;
in
t
- |> Sign.extern_term (Consts.extern_early consts) thy
+ |> Sign.extern_term thy
|> Local_Syntax.extern_term syntax
- |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (Local_Syntax.syn_of syntax)
- (not (PureThy.old_appl_syntax thy))
+ |> Syntax.standard_unparse_term (Consts.extern consts) ctxt
+ (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
end;
in
@@ -990,7 +988,7 @@
fun const_ast_tr intern ctxt [Syntax.Variable c] =
let
val Const (c', _) = read_const_proper ctxt c;
- val d = if intern then const_syntax_name ctxt c' else c;
+ val d = if intern then Syntax.mark_const c' else c;
in Syntax.Constant d end
| const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
@@ -1018,7 +1016,9 @@
fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
| const_syntax ctxt (Const (c, _), mx) =
- Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
+ (case try (Consts.type_scheme (consts_of ctxt)) c of
+ SOME T => SOME (false, (Syntax.mark_const c, T, mx))
+ | NONE => NONE)
| const_syntax _ _ = NONE;
in
--- a/src/Pure/ML/ml_antiquote.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Mon Feb 22 09:17:49 2010 +0100
@@ -114,7 +114,7 @@
fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
#1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
- |> syn ? ProofContext.const_syntax_name ctxt
+ |> syn ? Syntax.mark_const
|> ML_Syntax.print_string);
val _ = inline "const_name" (const false);
--- a/src/Pure/Proof/proof_syntax.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Mon Feb 22 09:17:49 2010 +0100
@@ -67,8 +67,8 @@
("", paramT --> paramsT, Delimfix "_")]
|> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
- (Syntax.constN ^ "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
- (Syntax.constN ^ "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
+ (Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
+ (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
|> Sign.add_modesyntax_i ("latex", false)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
|> Sign.add_trrules_i (map Syntax.ParsePrintRule
@@ -78,10 +78,10 @@
[Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
(Syntax.mk_appl (Constant "_Lam")
[Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
- Syntax.mk_appl (Constant (Syntax.constN ^ "AbsP")) [Variable "A",
+ Syntax.mk_appl (Constant (Syntax.mark_const "AbsP")) [Variable "A",
(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
(Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
- Syntax.mk_appl (Constant (Syntax.constN ^ "Abst"))
+ Syntax.mk_appl (Constant (Syntax.mark_const "Abst"))
[(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
--- a/src/Pure/Syntax/lexicon.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/Syntax/lexicon.ML Mon Feb 22 09:17:49 2010 +0100
@@ -31,7 +31,11 @@
val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
val read_float: string -> {mant: int, exp: int}
val fixedN: string
+ val mark_fixed: string -> string
+ val unmark_fixed: string -> string
val constN: string
+ val mark_const: string -> string
+ val unmark_const: string -> string
end;
signature LEXICON =
@@ -331,8 +335,13 @@
(* specific identifiers *)
+val fixedN = "\\<^fixed>";
+val mark_fixed = prefix fixedN;
+val unmark_fixed = unprefix fixedN;
+
val constN = "\\<^const>";
-val fixedN = "\\<^fixed>";
+val mark_const = prefix constN;
+val unmark_const = unprefix constN;
(* read numbers *)
--- a/src/Pure/Syntax/printer.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/Syntax/printer.ML Mon Feb 22 09:17:49 2010 +0100
@@ -321,10 +321,10 @@
else pr, args))
and atomT a =
- (case try (unprefix Lexicon.constN) a of
+ (case try Lexicon.unmark_const a of
SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c))
| NONE =>
- (case try (unprefix Lexicon.fixedN) a of
+ (case try Lexicon.unmark_fixed a of
SOME x => the (token_trans "_free" x)
| NONE => Pretty.str a))
@@ -340,8 +340,8 @@
let
val nargs = length args;
val markup = Pretty.mark
- (Markup.const (unprefix Lexicon.constN a) handle Fail _ =>
- (Markup.fixed (unprefix Lexicon.fixedN a)))
+ (Markup.const (Lexicon.unmark_const a) handle Fail _ =>
+ (Markup.fixed (Lexicon.unmark_fixed a)))
handle Fail _ => I;
(*find matching table entry, or print as prefix / postfix*)
--- a/src/Pure/Syntax/syn_trans.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Mon Feb 22 09:17:49 2010 +0100
@@ -129,13 +129,15 @@
(* type propositions *)
-fun mk_type ty = Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty);
+fun mk_type ty =
+ Lexicon.const "_constrain" $
+ Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "itself" $ ty);
fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty
| ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
fun sort_constraint_tr (*"_sort_constraint"*) [ty] =
- Lexicon.const "Pure.sort_constraint" $ mk_type ty
+ Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
| sort_constraint_tr (*"_sort_constraint"*) ts = raise TERM ("sort_constraint_tr", ts);
@@ -152,7 +154,7 @@
(case Ast.unfold_ast_p "_asms" asms of
(asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
| _ => raise Ast.AST ("bigimpl_ast_tr", asts))
- in Ast.fold_ast_p "==>" (prems, concl) end
+ in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
| bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
@@ -350,7 +352,7 @@
(* type propositions *)
-fun type_prop_tr' _ (*"_type_prop"*) T [Const ("Pure.sort_constraint", _)] =
+fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] =
Lexicon.const "_sort_constraint" $ TypeExt.term_of_typ true T
| type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t
@@ -366,7 +368,7 @@
fun is_prop Ts t =
fastype_of1 (Ts, t) = propT handle TERM _ => false;
- fun is_term (Const ("Pure.term", _) $ _) = true
+ fun is_term (Const ("\\<^const>Pure.term", _) $ _) = true
| is_term _ = false;
fun tr' _ (t as Const _) = t
@@ -379,7 +381,7 @@
| tr' Ts (t as Bound _) =
if is_prop Ts t then aprop t else t
| tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
- | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
+ | tr' Ts (t as t1 $ (t2 as Const ("\\<^const>TYPE", Type ("itself", [T])))) =
if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
else tr' Ts t1 $ tr' Ts t2
| tr' Ts (t as t1 $ t2) =
@@ -393,7 +395,7 @@
fun impl_ast_tr' (*"==>"*) asts =
if TypeExt.no_brackets () then raise Match
else
- (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of
+ (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
(prems as _ :: _ :: _, concl) =>
let
val (asms, asm) = split_last prems;
@@ -514,11 +516,13 @@
[("_abs", abs_ast_tr'),
("_idts", idtyp_ast_tr' "_idts"),
("_pttrns", idtyp_ast_tr' "_pttrns"),
- ("==>", impl_ast_tr'),
+ ("\\<^const>==>", impl_ast_tr'),
("_index", index_ast_tr')]);
val pure_trfunsT =
- [("_type_prop", type_prop_tr'), ("TYPE", type_tr'), ("_type_constraint_", type_constraint_tr')];
+ [("_type_prop", type_prop_tr'),
+ ("\\<^const>TYPE", type_tr'),
+ ("_type_constraint_", type_constraint_tr')];
fun struct_trfuns structs =
([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
--- a/src/Pure/Syntax/syntax.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Feb 22 09:17:49 2010 +0100
@@ -302,7 +302,7 @@
lexicon =
if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
gram = if changed then Parser.extend_gram gram xprods else gram,
- consts = Library.merge (op =) (consts1, filter_out Long_Name.is_qualified consts2),
+ consts = Library.merge (op =) (consts1, filter_out (can Lexicon.unmark_const) consts2),
prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
parse_ast_trtab =
update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
--- a/src/Pure/Syntax/type_ext.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML Mon Feb 22 09:17:49 2010 +0100
@@ -123,7 +123,9 @@
| decode (t $ u) = decode t $ decode u
| decode (Const (a, T)) =
let val c =
- (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => snd (map_const a))
+ (case try Lexicon.unmark_const a of
+ SOME c => c
+ | NONE => snd (map_const a))
in Const (c, map_type T) end
| decode (Free (a, T)) =
(case (map_free a, map_const a) of
--- a/src/Pure/axclass.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/axclass.ML Mon Feb 22 09:17:49 2010 +0100
@@ -474,7 +474,7 @@
val ([def], def_thy) =
thy
|> Sign.primitive_class (bclass, super)
- |> PureThy.add_defs false [((Binding.map_name Thm.def_name bconst, class_eq), [])];
+ |> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])];
val (raw_intro, (raw_classrel, raw_axioms)) =
split_defined (length conjs) def ||> chop (length super);
--- a/src/Pure/codegen.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/codegen.ML Mon Feb 22 09:17:49 2010 +0100
@@ -299,7 +299,7 @@
val del_unfold = map_unfold o MetaSimplifier.del_simp;
fun unfold_preprocessor thy =
- let val ss = Simplifier.theory_context thy (UnfoldData.get thy)
+ let val ss = Simplifier.global_context thy (UnfoldData.get thy)
in map (Thm.transfer thy #> Simplifier.full_simplify ss) end;
--- a/src/Pure/consts.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/consts.ML Mon Feb 22 09:17:49 2010 +0100
@@ -21,15 +21,13 @@
val space_of: T -> Name_Space.T
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
+ val intern_syntax: T -> xstring -> string
val extern: T -> string -> xstring
- val extern_early: T -> string -> xstring
- val syntax: T -> string * mixfix -> string * typ * mixfix
- val syntax_name: T -> string -> string
val read_const: T -> string -> term
val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
- val declare: bool -> Name_Space.naming -> binding * typ -> T -> T
+ val declare: Name_Space.naming -> binding * typ -> T -> T
val constrain: string * typ option -> T -> T
val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string ->
binding * term -> T -> (term * term) * T
@@ -46,7 +44,7 @@
(* datatype T *)
-type decl = {T: typ, typargs: int list list, authentic: bool};
+type decl = {T: typ, typargs: int list list};
type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
datatype T = Consts of
@@ -128,18 +126,10 @@
val intern = Name_Space.intern o space_of;
val extern = Name_Space.extern o space_of;
-fun extern_early consts c =
- (case try (the_const consts) c of
- SOME ({authentic = true, ...}, _) => Syntax.constN ^ c
- | _ => extern consts c);
-
-fun syntax consts (c, mx) =
- let
- val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg;
- val c' = if authentic then Syntax.constN ^ c else Long_Name.base_name c;
- in (c', T, mx) end;
-
-fun syntax_name consts c = #1 (syntax consts (c, NoSyn));
+fun intern_syntax consts name =
+ (case try Syntax.unmark_const name of
+ SOME c => c
+ | NONE => intern consts name);
(* read_const *)
@@ -231,10 +221,10 @@
(* declarations *)
-fun declare authentic naming (b, declT) =
+fun declare naming (b, declT) =
map_consts (fn (decls, constraints, rev_abbrevs) =>
let
- val decl = {T = declT, typargs = typargs_of declT, authentic = authentic};
+ val decl = {T = declT, typargs = typargs_of declT};
val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
in (decls', constraints, rev_abbrevs) end);
@@ -285,7 +275,7 @@
in
consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
let
- val decl = {T = T, typargs = typargs_of T, authentic = true};
+ val decl = {T = T, typargs = typargs_of T};
val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
val (_, decls') = decls
|> Name_Space.define true naming (b, (decl, SOME abbr));
--- a/src/Pure/drule.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/drule.ML Mon Feb 22 09:17:49 2010 +0100
@@ -77,7 +77,6 @@
val flexflex_unique: thm -> thm
val export_without_context: thm -> thm
val export_without_context_open: thm -> thm
- val get_def: theory -> xstring -> thm
val store_thm: binding -> thm -> thm
val store_standard_thm: binding -> thm -> thm
val store_thm_open: binding -> thm -> thm
@@ -451,8 +450,6 @@
val read_prop = certify o Simple_Syntax.read_prop;
-fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
-
fun store_thm name th =
Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
--- a/src/Pure/meta_simplifier.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/meta_simplifier.ML Mon Feb 22 09:17:49 2010 +0100
@@ -111,7 +111,7 @@
val inherit_context: simpset -> simpset -> simpset
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
- val theory_context: theory -> simpset -> simpset
+ val global_context: theory -> simpset -> simpset
val debug_bounds: bool Unsynchronized.ref
val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
val set_solvers: solver list -> simpset -> simpset
@@ -341,7 +341,7 @@
fun context ctxt =
map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
-val theory_context = context o ProofContext.init;
+val global_context = context o ProofContext.init;
fun activate_context thy ss =
let
@@ -1025,7 +1025,8 @@
val b' = #1 (Term.dest_Free (Thm.term_of v));
val _ =
if b <> b' then
- warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
+ warning ("Simplifier: renamed bound variable " ^
+ quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
else ();
val ss' = add_bound ((b', T), a) ss;
val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
@@ -1240,7 +1241,7 @@
fun rewrite _ [] ct = Thm.reflexive ct
| rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
- (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
+ (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
fun simplify full thms = Conv.fconv_rule (rewrite full thms);
val rewrite_rule = simplify true;
@@ -1254,7 +1255,7 @@
(*Rewrite the subgoals of a proof state (represented by a theorem)*)
fun rewrite_goals_rule thms th =
Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
- (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
+ (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
(*Rewrite the subgoal of a proof state (represented by a theorem)*)
fun rewrite_goal_rule mode prover ss i thm =
@@ -1278,7 +1279,7 @@
fun rewrite_goal_tac rews =
let val ss = empty_ss addsimps rews in
fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
- (theory_context (Thm.theory_of_thm st) ss) i st
+ (global_context (Thm.theory_of_thm st) ss) i st
end;
(*Prunes all redundant parameters from the proof state by rewriting.
@@ -1316,7 +1317,7 @@
fun gen_norm_hhf ss th =
(if Drule.is_norm_hhf (Thm.prop_of th) then th
else Conv.fconv_rule
- (rewrite_cterm (true, false, false) (K (K NONE)) (theory_context (Thm.theory_of_thm th) ss)) th)
+ (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th)
|> Thm.adjust_maxidx_thm ~1
|> Drule.gen_all;
--- a/src/Pure/more_thm.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/more_thm.ML Mon Feb 22 09:17:49 2010 +0100
@@ -77,6 +77,7 @@
val untag: string -> attribute
val def_name: string -> string
val def_name_optional: string -> string -> string
+ val def_binding: Binding.binding -> Binding.binding
val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
val has_name_hint: thm -> bool
val get_name_hint: thm -> string
@@ -384,8 +385,10 @@
fun def_name_optional c "" = def_name c
| def_name_optional _ name = name;
+val def_binding = Binding.map_name def_name;
+
fun def_binding_optional b name =
- if Binding.is_empty name then Binding.map_name def_name b else name;
+ if Binding.is_empty name then def_binding b else name;
(* unofficial theorem names *)
--- a/src/Pure/old_goals.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/old_goals.ML Mon Feb 22 09:17:49 2010 +0100
@@ -16,6 +16,7 @@
val simple_read_term: theory -> typ -> string -> term
val read_term: theory -> string -> term
val read_prop: theory -> string -> term
+ val get_def: theory -> xstring -> thm
type proof
val premises: unit -> thm list
val reset_goals: unit -> unit
@@ -220,6 +221,8 @@
fun read_prop thy = simple_read_term thy propT;
+fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
+
(*** Goal package ***)
--- a/src/Pure/pure_thy.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/pure_thy.ML Mon Feb 22 09:17:49 2010 +0100
@@ -225,6 +225,7 @@
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
+val const = Syntax.mark_const;
val typeT = Syntax.typeT;
val spropT = Syntax.spropT;
@@ -310,11 +311,11 @@
("_indexvar", typ "index", Delimfix "'\\<index>"),
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
("_update_name", typ "idt", NoSyn),
- ("==>", typ "prop => prop => prop", Delimfix "op ==>"),
- (Term.dummy_patternN, typ "aprop", Delimfix "'_"),
+ (const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
+ (const Term.dummy_patternN, typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
- ("Pure.term", typ "logic => prop", Delimfix "TERM _"),
- ("Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
+ (const "Pure.term", typ "logic => prop", Delimfix "TERM _"),
+ (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
#> Sign.add_syntax_i applC_syntax
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
[("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
@@ -326,14 +327,14 @@
("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_type_constraint_", typ "'a", NoSyn),
("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
- ("==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
- ("all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
- ("==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
+ (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
+ (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
+ (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Delimfix "\\<dots>")]
#> Sign.add_modesyntax_i ("", false)
- [("prop", typ "prop => prop", Mixfix ("_", [0], 0))]
+ [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
#> Sign.add_modesyntax_i ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts_i
--- a/src/Pure/sign.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/sign.ML Mon Feb 22 09:17:49 2010 +0100
@@ -41,7 +41,6 @@
val declared_tyname: theory -> string -> bool
val declared_const: theory -> string -> bool
val const_monomorphic: theory -> string -> bool
- val const_syntax_name: theory -> string -> string
val const_typargs: theory -> string * typ -> typ list
val const_instance: theory -> string * typ list -> typ
val mk_const: theory -> string * typ list -> term
@@ -59,7 +58,7 @@
val intern_typ: theory -> typ -> typ
val extern_typ: theory -> typ -> typ
val intern_term: theory -> term -> term
- val extern_term: (string -> xstring) -> theory -> term -> term
+ val extern_term: theory -> term -> term
val intern_tycons: theory -> typ -> typ
val arity_number: theory -> string -> int
val arity_sorts: theory -> string -> sort -> sort list
@@ -226,7 +225,6 @@
val the_const_type = Consts.the_type o consts_of;
val const_type = try o the_const_type;
val const_monomorphic = Consts.is_monomorphic o consts_of;
-val const_syntax_name = Consts.syntax_name o consts_of;
val const_typargs = Consts.typargs o consts_of;
val const_instance = Consts.instance o consts_of;
@@ -299,7 +297,7 @@
val intern_typ = typ_mapping intern_class intern_type;
val extern_typ = typ_mapping extern_class extern_type;
val intern_term = term_mapping intern_class intern_type intern_const;
-fun extern_term h = term_mapping extern_class extern_type (K h);
+val extern_term = term_mapping extern_class extern_type (K Syntax.mark_const);
val intern_tycons = typ_mapping (K I) intern_type;
end;
@@ -486,7 +484,10 @@
fun notation add mode args thy =
let
val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
- fun const_syntax (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
+ fun const_syntax (Const (c, _), mx) =
+ (case try (Consts.type_scheme (consts_of thy)) c of
+ SOME T => SOME (Syntax.mark_const c, T, mx)
+ | NONE => NONE)
| const_syntax _ = NONE;
in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
@@ -495,35 +496,34 @@
local
-fun gen_add_consts parse_typ authentic raw_args thy =
+fun gen_add_consts parse_typ raw_args thy =
let
val ctxt = ProofContext.init thy;
val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
fun prep (b, raw_T, mx) =
let
val c = full_name thy b;
- val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b;
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
val T' = Logic.varifyT T;
- in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
+ in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end;
val args = map prep raw_args;
in
thy
- |> map_consts (fold (Consts.declare authentic (naming_of thy) o #1) args)
+ |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
|> add_syntax_i (map #2 args)
|> pair (map #3 args)
end;
in
-fun add_consts args = snd o gen_add_consts Syntax.parse_typ false args;
-fun add_consts_i args = snd o gen_add_consts (K I) false args;
+fun add_consts args = snd o gen_add_consts Syntax.parse_typ args;
+fun add_consts_i args = snd o gen_add_consts (K I) args;
fun declare_const ((b, T), mx) thy =
let
val pos = Binding.pos_of b;
- val ([const as Const (c, _)], thy') = gen_add_consts (K I) true [(b, T, mx)] thy;
+ val ([const as Const (c, _)], thy') = gen_add_consts (K I) [(b, T, mx)] thy;
val _ = Position.report (Markup.const_decl c) pos;
in (const, thy') end;
--- a/src/Pure/simplifier.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Pure/simplifier.ML Mon Feb 22 09:17:49 2010 +0100
@@ -36,7 +36,7 @@
val inherit_context: simpset -> simpset -> simpset
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
- val theory_context: theory -> simpset -> simpset
+ val global_context: theory -> simpset -> simpset
val simproc_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
val simproc: theory -> string -> string list
--- a/src/Sequents/ILL_predlog.thy Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Sequents/ILL_predlog.thy Mon Feb 22 09:17:49 2010 +0100
@@ -11,7 +11,7 @@
disj :: "[plf,plf] => plf" (infixr "|" 35)
impl :: "[plf,plf] => plf" (infixr ">" 35)
eq :: "[plf,plf] => plf" (infixr "=" 35)
- ff :: "plf"
+ ff :: "plf" ("ff")
PL :: "plf => o" ("[* / _ / *]" [] 100)
@@ -22,8 +22,8 @@
"[* A & B *]" == "[*A*] && [*B*]"
"[* A | B *]" == "![*A*] ++ ![*B*]"
- "[* - A *]" == "[*A > CONST ff*]"
- "[* XCONST ff *]" == "0"
+ "[* - A *]" == "[*A > ff*]"
+ "[* ff *]" == "0"
"[* A = B *]" => "[* (A > B) & (B > A) *]"
"[* A > B *]" == "![*A*] -o [*B*]"
--- a/src/Sequents/simpdata.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Sequents/simpdata.ML Mon Feb 22 09:17:49 2010 +0100
@@ -68,7 +68,7 @@
(*No simprules, but basic infrastructure for simplification*)
val LK_basic_ss =
- Simplifier.theory_context @{theory} empty_ss
+ Simplifier.global_context @{theory} empty_ss
setsubgoaler asm_simp_tac
setSSolver (mk_solver "safe" safe_solver)
setSolver (mk_solver "unsafe" unsafe_solver)
--- a/src/Tools/Code/code_preproc.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML Mon Feb 22 09:17:49 2010 +0100
@@ -129,7 +129,7 @@
fun preprocess thy =
let
- val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
+ val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
in
preprocess_functrans thy
#> (map o apfst) (rewrite_eqn pre)
@@ -137,7 +137,7 @@
fun preprocess_conv thy ct =
let
- val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
+ val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
in
ct
|> Simplifier.rewrite pre
@@ -146,7 +146,7 @@
fun postprocess_conv thy ct =
let
- val post = (Simplifier.theory_context thy o #post o the_thmproc) thy;
+ val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
in
ct
|> AxClass.overload_conv thy
--- a/src/ZF/Tools/datatype_package.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML Mon Feb 22 09:17:49 2010 +0100
@@ -298,7 +298,7 @@
(*** Prove the recursor theorems ***)
- val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of
+ val recursor_eqns = case try (OldGoals.get_def thy1) recursor_base_name of
NONE => (writeln " [ No recursion operator ]";
[])
| SOME recursor_def =>
--- a/src/ZF/Tools/inductive_package.ML Mon Feb 22 09:15:12 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML Mon Feb 22 09:17:49 2010 +0100
@@ -179,7 +179,7 @@
(*fetch fp definitions from the theory*)
val big_rec_def::part_rec_defs =
- map (Drule.get_def thy1)
+ map (OldGoals.get_def thy1)
(case rec_names of [_] => rec_names
| _ => big_rec_base_name::rec_names);
@@ -327,7 +327,7 @@
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
If the premises get simplified, then the proofs could fail.*)
- val min_ss = Simplifier.theory_context thy empty_ss
+ val min_ss = Simplifier.global_context thy empty_ss
setmksimps (map mk_eq o ZF_atomize o gen_all)
setSolver (mk_solver "minimal"
(fn prems => resolve_tac (triv_rls@prems)