--- a/NEWS Tue May 04 13:08:56 2010 -0700
+++ b/NEWS Tue May 04 13:11:15 2010 -0700
@@ -89,6 +89,9 @@
*** Pure ***
+* Predicates of locales introduces by classes carry a mandatory "class"
+prefix. INCOMPATIBILITY.
+
* 'code_reflect' allows to incorporate generated ML code into
runtime environment; replaces immature code_datatype antiquotation.
INCOMPATIBILITY.
@@ -137,6 +140,9 @@
*** HOL ***
+* Theory 'Finite_Set': various folding_* locales facilitate the application
+of the various fold combinators on finite sets.
+
* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
provides abstract red-black tree type which is backed by RBT_Impl
as implementation. INCOMPATIBILTY.
@@ -362,6 +368,12 @@
* Configuration options now admit dynamic default values, depending on
the context or even global references.
+* Most operations that refer to a global context are named
+accordingly, e.g. Simplifier.global_context or
+ProofContext.init_global. There are some situations where a global
+context actually works, but under normal circumstances one needs to
+pass the proper local context through the code!
+
*** System ***
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Tue May 04 13:08:56 2010 -0700
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Tue May 04 13:11:15 2010 -0700
@@ -243,7 +243,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type Proof.context} \\
- @{index_ML ProofContext.init: "theory -> Proof.context"} \\
+ @{index_ML ProofContext.init_global: "theory -> Proof.context"} \\
@{index_ML ProofContext.theory_of: "Proof.context -> theory"} \\
@{index_ML ProofContext.transfer: "theory -> Proof.context -> Proof.context"} \\
\end{mldecls}
@@ -254,7 +254,7 @@
of this type are essentially pure values, with a sliding reference
to the background theory.
- \item @{ML ProofContext.init}~@{text "thy"} produces a proof context
+ \item @{ML ProofContext.init_global}~@{text "thy"} produces a proof context
derived from @{text "thy"}, initializing all data.
\item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the
@@ -305,7 +305,7 @@
\item @{ML Context.proof_of}~@{text "context"} always produces a
proof context from the generic @{text "context"}, using @{ML
- "ProofContext.init"} as required (note that this re-initializes the
+ "ProofContext.init_global"} as required (note that this re-initializes the
context data with each invocation).
\end{description}
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 04 13:08:56 2010 -0700
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 04 13:11:15 2010 -0700
@@ -282,7 +282,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\
- \indexdef{}{ML}{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
+ \indexdef{}{ML}{ProofContext.init\_global}\verb|ProofContext.init_global: theory -> Proof.context| \\
\indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
\indexdef{}{ML}{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
\end{mldecls}
@@ -293,7 +293,7 @@
of this type are essentially pure values, with a sliding reference
to the background theory.
- \item \verb|ProofContext.init|~\isa{thy} produces a proof context
+ \item \verb|ProofContext.init_global|~\isa{thy} produces a proof context
derived from \isa{thy}, initializing all data.
\item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
@@ -355,7 +355,7 @@
theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
\item \verb|Context.proof_of|~\isa{context} always produces a
- proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
+ proof context from the generic \isa{context}, using \verb|ProofContext.init_global| as required (note that this re-initializes the
context data with each invocation).
\end{description}%
--- a/src/HOL/Bali/TypeSafe.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Bali/TypeSafe.thy Tue May 04 13:11:15 2010 -0700
@@ -9,8 +9,6 @@
section "error free"
-hide_const field
-
lemma error_free_halloc:
assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
error_free_s0: "error_free s0"
--- a/src/HOL/Big_Operators.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Big_Operators.thy Tue May 04 13:11:15 2010 -0700
@@ -33,7 +33,7 @@
text {* for ad-hoc proofs for @{const fold_image} *}
lemma (in comm_monoid_add) comm_monoid_mult:
- "comm_monoid_mult (op +) 0"
+ "class.comm_monoid_mult (op +) 0"
proof qed (auto intro: add_assoc add_commute)
notation times (infixl "*" 70)
@@ -1200,7 +1200,8 @@
context semilattice_inf
begin
-lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
+lemma ab_semigroup_idem_mult_inf:
+ "class.ab_semigroup_idem_mult inf"
proof qed (rule inf_assoc inf_commute inf_idem)+
lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
@@ -1270,7 +1271,7 @@
context semilattice_sup
begin
-lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
+lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
@@ -1490,15 +1491,15 @@
using assms by (rule Max.hom_commute)
lemma ab_semigroup_idem_mult_min:
- "ab_semigroup_idem_mult min"
+ "class.ab_semigroup_idem_mult min"
proof qed (auto simp add: min_def)
lemma ab_semigroup_idem_mult_max:
- "ab_semigroup_idem_mult max"
+ "class.ab_semigroup_idem_mult max"
proof qed (auto simp add: max_def)
lemma max_lattice:
- "semilattice_inf (op \<ge>) (op >) max"
+ "class.semilattice_inf (op \<ge>) (op >) max"
by (fact min_max.dual_semilattice)
lemma dual_max:
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Tue May 04 13:11:15 2010 -0700
@@ -94,7 +94,7 @@
fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
| after_qed _ = I
in
- ProofContext.init thy
+ ProofContext.init_global thy
|> fold Variable.auto_fixes ts
|> (fn ctxt1 => ctxt1
|> prepare
@@ -187,7 +187,7 @@
end
fun prove thy meth vc =
- ProofContext.init thy
+ ProofContext.init_global thy
|> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
|> Proof.apply meth
|> Seq.hd
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Tue May 04 13:11:15 2010 -0700
@@ -232,7 +232,7 @@
in apsnd sort_fst_str (fold split axs ([], [])) end
fun mark_axioms thy axs =
- Boogie_Axioms.get (ProofContext.init thy)
+ Boogie_Axioms.get (ProofContext.init_global thy)
|> Termtab.make o map (fn thm => (Thm.prop_of thm, Unused thm))
|> fold mark axs
|> split_list_kind thy o Termtab.dest
--- a/src/HOL/Complete_Lattice.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Complete_Lattice.thy Tue May 04 13:11:15 2010 -0700
@@ -33,8 +33,8 @@
begin
lemma dual_complete_lattice:
- "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
- by (auto intro!: complete_lattice.intro dual_bounded_lattice)
+ "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
(unfold_locales, (fact bot_least top_greatest
Sup_upper Sup_least Inf_lower Inf_greatest)+)
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 04 13:11:15 2010 -0700
@@ -265,7 +265,7 @@
lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq
le_less neq_iff linear less_not_permute
-lemma axiom[no_atp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
--- a/src/HOL/Divides.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Divides.thy Tue May 04 13:11:15 2010 -0700
@@ -379,6 +379,8 @@
class ring_div = semiring_div + comm_ring_1
begin
+subclass ring_1_no_zero_divisors ..
+
text {* Negation respects modular equivalence. *}
lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
--- a/src/HOL/Finite_Set.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Finite_Set.thy Tue May 04 13:11:15 2010 -0700
@@ -509,13 +509,8 @@
subsection {* Class @{text finite} *}
-setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
class finite =
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
-setup {* Sign.parent_path *}
-hide_const finite
-
-context finite
begin
lemma finite [simp]: "finite (A \<Colon> 'a set)"
@@ -1734,12 +1729,10 @@
qed
lemma insert [simp]:
- assumes "finite A" and "x \<notin> A"
- shows "F (insert x A) = (if A = {} then x else x * F A)"
-proof (cases "A = {}")
- case True then show ?thesis by simp
-next
- case False then obtain b where "b \<in> A" by blast
+ assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
+ shows "F (insert x A) = x * F A"
+proof -
+ from `A \<noteq> {}` obtain b where "b \<in> A" by blast
then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
with `finite A` have "finite B" by simp
interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
@@ -1833,8 +1826,6 @@
(simp_all add: assoc in_idem `finite A`)
qed
-declare insert [simp del]
-
lemma eq_fold_idem':
assumes "finite A"
shows "F (insert a A) = fold (op *) a A"
@@ -1844,13 +1835,13 @@
qed
lemma insert_idem [simp]:
- assumes "finite A"
- shows "F (insert x A) = (if A = {} then x else x * F A)"
+ assumes "finite A" and "A \<noteq> {}"
+ shows "F (insert x A) = x * F A"
proof (cases "x \<in> A")
- case False with `finite A` show ?thesis by (rule insert)
+ case False from `finite A` `x \<notin> A` `A \<noteq> {}` show ?thesis by (rule insert)
next
- case True then have "A \<noteq> {}" by auto
- with `finite A` show ?thesis by (simp add: in_idem insert_absorb True)
+ case True
+ from `finite A` `A \<noteq> {}` show ?thesis by (simp add: in_idem insert_absorb True)
qed
lemma union_idem:
--- a/src/HOL/HOL.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/HOL.thy Tue May 04 13:11:15 2010 -0700
@@ -1493,7 +1493,7 @@
Context.theory_map (Induct.map_simpset (fn ss => ss
setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
map (Simplifier.rewrite_rule (map Thm.symmetric
- @{thms induct_rulify_fallback induct_true_def induct_false_def})))
+ @{thms induct_rulify_fallback})))
addsimprocs
[Simplifier.simproc @{theory} "swap_induct_false"
["induct_false ==> PROP P ==> PROP Q"]
@@ -1886,7 +1886,6 @@
*}
hide_const (open) eq
-hide_const eq
text {* Cases *}
--- a/src/HOL/Hoare/Hoare_Logic.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Hoare/Hoare_Logic.thy Tue May 04 13:11:15 2010 -0700
@@ -27,18 +27,19 @@
types 'a sem = "'a => 'a => bool"
-consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
-primrec
-"iter 0 b S = (%s s'. s ~: b & (s=s'))"
-"iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))"
+inductive Sem :: "'a com \<Rightarrow> 'a sem"
+where
+ "Sem (Basic f) s (f s)"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
+| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "s \<notin> b \<Longrightarrow> Sem (While b x c) s s"
+| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
+ Sem (While b x c) s s'"
-consts Sem :: "'a com => 'a sem"
-primrec
-"Sem(Basic f) s s' = (s' = f s)"
-"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')"
-"Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s : b --> Sem c1 s s') &
- (s ~: b --> Sem c2 s s'))"
-"Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')"
+inductive_cases [elim!]:
+ "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
+ "Sem (IF b THEN c1 ELSE c2 FI) s s'"
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
"Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
@@ -209,19 +210,18 @@
\<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
by (auto simp:Valid_def)
-lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
- (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
+lemma While_aux:
+ assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+ shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
+ s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
+ using assms
+ by (induct "WHILE b INV {i} DO c OD" s s') auto
lemma WhileRule:
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
apply (clarsimp simp:Valid_def)
-apply(drule iter_aux)
- prefer 2 apply assumption
+apply(drule While_aux)
+ apply assumption
apply blast
apply blast
done
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue May 04 13:11:15 2010 -0700
@@ -25,22 +25,23 @@
types 'a sem = "'a option => 'a option => bool"
-consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
-primrec
-"iter 0 b S = (\<lambda>s s'. s \<notin> Some ` b \<and> s=s')"
-"iter (Suc n) b S =
- (\<lambda>s s'. s \<in> Some ` b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s'))"
+inductive Sem :: "'a com \<Rightarrow> 'a sem"
+where
+ "Sem (Basic f) None None"
+| "Sem (Basic f) (Some s) (Some (f s))"
+| "Sem Abort s None"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
+| "Sem (IF b THEN c1 ELSE c2 FI) None None"
+| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "Sem (While b x c) None None"
+| "s \<notin> b \<Longrightarrow> Sem (While b x c) (Some s) (Some s)"
+| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
+ Sem (While b x c) (Some s) s'"
-consts Sem :: "'a com => 'a sem"
-primrec
-"Sem(Basic f) s s' = (case s of None \<Rightarrow> s' = None | Some t \<Rightarrow> s' = Some(f t))"
-"Sem Abort s s' = (s' = None)"
-"Sem(c1;c2) s s' = (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
-"Sem(IF b THEN c1 ELSE c2 FI) s s' =
- (case s of None \<Rightarrow> s' = None
- | Some t \<Rightarrow> ((t \<in> b \<longrightarrow> Sem c1 s s') \<and> (t \<notin> b \<longrightarrow> Sem c2 s s')))"
-"Sem(While b x c) s s' =
- (if s = None then s' = None else \<exists>n. iter n b (Sem c) s s')"
+inductive_cases [elim!]:
+ "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
+ "Sem (IF b THEN c1 ELSE c2 FI) s s'"
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
"Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
@@ -212,23 +213,20 @@
\<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
by (fastsimp simp:Valid_def image_def)
-lemma iter_aux:
- "! s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
- (\<And>s s'. s \<in> Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> Some ` (I \<inter> -b))";
-apply(unfold image_def)
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
+lemma While_aux:
+ assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+ shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
+ s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
+ using assms
+ by (induct "WHILE b INV {i} DO c OD" s s') auto
lemma WhileRule:
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
apply(simp add:Valid_def)
apply(simp (no_asm) add:image_def)
apply clarify
-apply(drule iter_aux)
- prefer 2 apply assumption
+apply(drule While_aux)
+ apply assumption
apply blast
apply blast
done
--- a/src/HOL/Imperative_HOL/Heap.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Imperative_HOL/Heap.thy Tue May 04 13:11:15 2010 -0700
@@ -216,6 +216,9 @@
and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
unfolding noteq_refs_def noteq_arrs_def by auto
+lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
+ unfolding noteq_refs_def by auto
+
lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def)
--- a/src/HOL/Import/proof_kernel.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Import/proof_kernel.ML Tue May 04 13:11:15 2010 -0700
@@ -213,7 +213,7 @@
fun smart_string_of_cterm ct =
let
val thy = Thm.theory_of_cterm ct
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val {t,T,...} = rep_cterm ct
(* Hack to avoid parse errors with Trueprop *)
val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
@@ -2065,7 +2065,7 @@
let
val (HOLThm args) = norm_hthm (theory_of_thm th) hth
in
- apsnd strip_shyps args
+ apsnd Thm.strip_shyps args
end
fun to_isa_term tm = tm
--- a/src/HOL/Import/shuffler.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Import/shuffler.ML Tue May 04 13:11:15 2010 -0700
@@ -502,7 +502,7 @@
t |> disamb_bound thy
|> chain (Simplifier.full_rewrite ss)
|> chain eta_conversion
- |> strip_shyps
+ |> Thm.strip_shyps
val _ = message ("norm_term: " ^ (string_of_thm th))
in
th
--- a/src/HOL/IsaMakefile Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/IsaMakefile Tue May 04 13:11:15 2010 -0700
@@ -423,7 +423,7 @@
Library/Nat_Bijection.thy $(SRC)/Tools/float.ML \
$(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \
Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \
- Library/OptionalSugar.thy \
+ Library/OptionalSugar.thy Library/Convex.thy \
Library/Predicate_Compile_Quickcheck.thy Library/SML_Quickcheck.thy
@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
@@ -1095,7 +1095,10 @@
Multivariate_Analysis/Path_Connected.thy \
Multivariate_Analysis/Real_Integration.thy \
Multivariate_Analysis/Topology_Euclidean_Space.thy \
- Multivariate_Analysis/Vec1.thy
+ Multivariate_Analysis/Vec1.thy Library/Glbs.thy \
+ Library/Inner_Product.thy Library/Numeral_Type.thy \
+ Library/Convex.thy Library/FrechetDeriv.thy \
+ Library/Product_Vector.thy Library/Product_plus.thy
@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Multivariate_Analysis
@@ -1109,7 +1112,10 @@
Probability/Borel.thy Probability/Measure.thy \
Probability/Lebesgue.thy Probability/Product_Measure.thy \
Probability/Probability_Space.thy Probability/Information.thy \
- Probability/ex/Dining_Cryptographers.thy
+ Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy \
+ Library/Convex.thy Library/Product_Vector.thy \
+ Library/Product_plus.thy Library/Inner_Product.thy \
+ Library/Nat_Bijection.thy
@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Probability
--- a/src/HOL/Lattices.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Lattices.thy Tue May 04 13:11:15 2010 -0700
@@ -67,8 +67,8 @@
text {* Dual lattice *}
lemma dual_semilattice:
- "semilattice_inf (op \<ge>) (op >) sup"
-by (rule semilattice_inf.intro, rule dual_order)
+ "class.semilattice_inf (op \<ge>) (op >) sup"
+by (rule class.semilattice_inf.intro, rule dual_order)
(unfold_locales, simp_all add: sup_least)
end
@@ -235,8 +235,8 @@
begin
lemma dual_lattice:
- "lattice (op \<ge>) (op >) sup inf"
- by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
+ "class.lattice (op \<ge>) (op >) sup inf"
+ by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
(unfold_locales, auto)
lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
@@ -347,8 +347,8 @@
by(simp add: inf_sup_aci inf_sup_distrib1)
lemma dual_distrib_lattice:
- "distrib_lattice (op \<ge>) (op >) sup inf"
- by (rule distrib_lattice.intro, rule dual_lattice)
+ "class.distrib_lattice (op \<ge>) (op >) sup inf"
+ by (rule class.distrib_lattice.intro, rule dual_lattice)
(unfold_locales, fact inf_sup_distrib1)
lemmas sup_inf_distrib =
@@ -419,7 +419,7 @@
begin
lemma dual_bounded_lattice:
- "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
by unfold_locales (auto simp add: less_le_not_le)
end
@@ -431,8 +431,8 @@
begin
lemma dual_boolean_algebra:
- "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
- by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
+ "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
(unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
lemma compl_inf_bot:
--- a/src/HOL/Library/Convex.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Library/Convex.thy Tue May 04 13:11:15 2010 -0700
@@ -1,3 +1,10 @@
+(* Title: HOL/Library/Convex.thy
+ Author: Armin Heller, TU Muenchen
+ Author: Johannes Hoelzl, TU Muenchen
+*)
+
+header {* Convexity in real vector spaces *}
+
theory Convex
imports Product_Vector
begin
--- a/src/HOL/Library/Library.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Library/Library.thy Tue May 04 13:11:15 2010 -0700
@@ -12,6 +12,7 @@
Code_Integer
Continuity
ContNotDenum
+ Convex
Countable
Diagonalize
Dlist
--- a/src/HOL/Library/Multiset.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Library/Multiset.thy Tue May 04 13:11:15 2010 -0700
@@ -1239,7 +1239,7 @@
qed
have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
- show "order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
+ show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
qed (auto simp add: le_multiset_def irrefl dest: trans)
qed
--- a/src/HOL/Matrix/cplex/matrixlp.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Matrix/cplex/matrixlp.ML Tue May 04 13:11:15 2010 -0700
@@ -81,7 +81,7 @@
fun matrix_simplify th =
let
val simp_th = matrix_compute (cprop_of th)
- val th = strip_shyps (equal_elim simp_th th)
+ val th = Thm.strip_shyps (equal_elim simp_th th)
fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
in
removeTrue th
--- a/src/HOL/Mutabelle/Mutabelle.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Mutabelle/Mutabelle.thy Tue May 04 13:11:15 2010 -0700
@@ -61,16 +61,16 @@
(*
ML {*
-Quickcheck.test_term (ProofContext.init @{theory})
+Quickcheck.test_term (ProofContext.init_global @{theory})
false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps}))
*}
ML {*
fun is_executable thy th = can (Quickcheck.test_term
- (ProofContext.init thy) false (SOME "SML") 1 1) (prop_of th);
+ (ProofContext.init_global thy) false (SOME "SML") 1 1) (prop_of th);
fun is_executable_term thy t = can (Quickcheck.test_term
- (ProofContext.init thy) false (SOME "SML") 1 1) t;
+ (ProofContext.init_global thy) false (SOME "SML") 1 1) t;
fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
--- a/src/HOL/Mutabelle/mutabelle.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Mutabelle/mutabelle.ML Tue May 04 13:11:15 2010 -0700
@@ -499,14 +499,14 @@
fun is_executable thy insts th =
(Quickcheck.test_term
- (ProofContext.init thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
+ (ProofContext.init_global thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
priority "executable"; true) handle ERROR s =>
(priority ("not executable: " ^ s); false);
fun qc_recursive usedthy [] insts sz qciter acc = rev acc
| qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter
(priority ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
- (ProofContext.init usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
+ (ProofContext.init_global usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
handle ERROR msg => (priority msg; qc_recursive usedthy xs insts sz qciter acc);
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue May 04 13:11:15 2010 -0700
@@ -97,7 +97,7 @@
fun invoke_quickcheck quickcheck_generator thy t =
TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
(fn _ =>
- case Quickcheck.gen_test_term (ProofContext.init thy) true true (SOME quickcheck_generator)
+ case Quickcheck.gen_test_term (ProofContext.init_global thy) true true (SOME quickcheck_generator)
size iterations (preprocess thy [] t) of
(NONE, (time_report, report)) => (NoCex, (time_report, report))
| (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
@@ -133,7 +133,7 @@
fun invoke_nitpick thy t =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val state = Proof.init ctxt
in
let
@@ -251,7 +251,7 @@
end
fun is_executable_term thy t = can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) (Quickcheck.test_term
- (ProofContext.init thy) false (SOME "SML") 1 0)) (preprocess thy [] t)
+ (ProofContext.init_global thy) false (SOME "SML") 1 0)) (preprocess thy [] t)
fun is_executable_thm thy th = is_executable_term thy (prop_of th)
val freezeT =
--- a/src/HOL/Nominal/nominal_datatype.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue May 04 13:11:15 2010 -0700
@@ -151,7 +151,7 @@
val meta_spec = thm "meta_spec";
fun projections rule =
- Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
+ Project_Rule.projections (ProofContext.init_global (Thm.theory_of_thm rule)) rule
|> map (Drule.export_without_context #> Rule_Cases.save rule);
val supp_prod = thm "supp_prod";
@@ -1617,7 +1617,7 @@
val y = Free ("y", U);
val y' = Free ("y'", U)
in
- Drule.export_without_context (Goal.prove (ProofContext.init thy11) []
+ Drule.export_without_context (Goal.prove (ProofContext.init_global thy11) []
(map (augment_sort thy11 fs_cp_sort)
(finite_prems @
[HOLogic.mk_Trueprop (R $ x $ y),
@@ -1712,7 +1712,7 @@
(Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
val rec_unique_thms = split_conj_thm (Goal.prove
- (ProofContext.init thy11) (map fst rec_unique_frees)
+ (ProofContext.init_global thy11) (map fst rec_unique_frees)
(map (augment_sort thy11 fs_cp_sort)
(flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
(augment_sort thy11 fs_cp_sort
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Tue May 04 13:11:15 2010 -0700
@@ -124,7 +124,7 @@
(* Find the variable we instantiate *)
let
val thy = theory_of_thm thm;
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val ss = global_simpset_of thy;
val abs_fresh = PureThy.get_thms thy "abs_fresh";
val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
--- a/src/HOL/Orderings.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Orderings.thy Tue May 04 13:11:15 2010 -0700
@@ -106,7 +106,7 @@
text {* Dual order *}
lemma dual_preorder:
- "preorder (op \<ge>) (op >)"
+ "class.preorder (op \<ge>) (op >)"
proof qed (auto simp add: less_le_not_le intro: order_trans)
end
@@ -186,7 +186,7 @@
text {* Dual order *}
lemma dual_order:
- "order (op \<ge>) (op >)"
+ "class.order (op \<ge>) (op >)"
by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
end
@@ -257,8 +257,8 @@
text {* Dual order *}
lemma dual_linorder:
- "linorder (op \<ge>) (op >)"
-by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
+ "class.linorder (op \<ge>) (op >)"
+by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
text {* min/max *}
--- a/src/HOL/Probability/Caratheodory.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Probability/Caratheodory.thy Tue May 04 13:11:15 2010 -0700
@@ -1,7 +1,7 @@
header {*Caratheodory Extension Theorem*}
theory Caratheodory
- imports Sigma_Algebra SupInf SeriesPlus
+ imports Sigma_Algebra SeriesPlus
begin
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
--- a/src/HOL/Probability/Information.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Probability/Information.thy Tue May 04 13:11:15 2010 -0700
@@ -1,5 +1,5 @@
theory Information
-imports Probability_Space Product_Measure "../Multivariate_Analysis/Convex"
+imports Probability_Space Product_Measure Convex
begin
section "Convex theory"
--- a/src/HOL/Probability/Product_Measure.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Probability/Product_Measure.thy Tue May 04 13:11:15 2010 -0700
@@ -1,5 +1,5 @@
theory Product_Measure
-imports "~~/src/HOL/Probability/Lebesgue"
+imports Lebesgue
begin
definition
--- a/src/HOL/Quotient_Examples/FSet.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Quotient_Examples/FSet.thy Tue May 04 13:11:15 2010 -0700
@@ -359,6 +359,10 @@
then show "concat a \<approx> concat b" by simp
qed
+lemma [quot_respect]:
+ "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+ by auto
+
text {* Distributive lattice with bot *}
lemma sub_list_not_eq:
@@ -551,6 +555,11 @@
is
"concat"
+quotient_definition
+ "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+ "filter"
+
text {* Compositional Respectfullness and Preservation *}
lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
@@ -782,7 +791,7 @@
by (induct l) (simp_all add: not_memb_nil)
lemma set_cong:
- shows "(set x = set y) = (x \<approx> y)"
+ shows "(x \<approx> y) = (set x = set y)"
by auto
lemma inj_map_eq_iff:
@@ -868,6 +877,38 @@
then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
qed
+text {* Set *}
+
+lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
+ by (metis rev_append set_append set_cong set_rev sub_list_append sub_list_append_left sub_list_def sub_list_not_eq subset_Un_eq)
+
+lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
+ by (auto simp add: sub_list_set)
+
+lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
+ by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
+
+lemma memb_set: "memb x xs = (x \<in> set xs)"
+ by (simp only: memb_def)
+
+lemma filter_set: "set (filter P xs) = P \<inter> (set xs)"
+ by (induct xs, simp)
+ (metis Int_insert_right_if0 Int_insert_right_if1 List.set.simps(2) filter.simps(2) mem_def)
+
+lemma delete_raw_set: "set (delete_raw xs x) = set xs - {x}"
+ by (induct xs) auto
+
+lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys"
+ by (induct xs) (simp_all add: memb_def)
+
+text {* Raw theorems of ffilter *}
+
+lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
+unfolding sub_list_def memb_def by auto
+
+lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)"
+unfolding memb_def by auto
+
text {* Lifted theorems *}
lemma not_fin_fnil: "x |\<notin>| {||}"
@@ -919,7 +960,7 @@
by (lifting none_memb_nil)
lemma fset_cong:
- "(fset_to_set S = fset_to_set T) = (S = T)"
+ "(S = T) = (fset_to_set S = fset_to_set T)"
by (lifting set_cong)
text {* fcard *}
@@ -1029,7 +1070,7 @@
lemma fmap_set_image:
"fset_to_set (fmap f S) = f ` (fset_to_set S)"
- by (induct S) (simp_all)
+ by (induct S) simp_all
lemma inj_fmap_eq_iff:
"inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
@@ -1042,6 +1083,40 @@
"x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
by (lifting memb_append)
+text {* to_set *}
+
+lemma fin_set: "(x |\<in>| xs) = (x \<in> fset_to_set xs)"
+ by (lifting memb_set)
+
+lemma fnotin_set: "(x |\<notin>| xs) = (x \<notin> fset_to_set xs)"
+ by (simp add: fin_set)
+
+lemma fcard_set: "fcard xs = card (fset_to_set xs)"
+ by (lifting fcard_raw_set)
+
+lemma fsubseteq_set: "(xs |\<subseteq>| ys) = (fset_to_set xs \<subseteq> fset_to_set ys)"
+ by (lifting sub_list_set)
+
+lemma fsubset_set: "(xs |\<subset>| ys) = (fset_to_set xs \<subset> fset_to_set ys)"
+ unfolding less_fset by (lifting sub_list_neq_set)
+
+lemma ffilter_set: "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
+ by (lifting filter_set)
+
+lemma fdelete_set: "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
+ by (lifting delete_raw_set)
+
+lemma inter_set: "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
+ by (lifting inter_raw_set)
+
+lemma union_set: "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
+ by (lifting set_append)
+
+lemmas fset_to_set_trans =
+ fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
+ inter_set union_set ffilter_set fset_to_set_simps
+ fset_cong fdelete_set fmap_set_image
+
text {* ffold *}
lemma ffold_nil: "ffold f z {||} = z"
@@ -1142,6 +1217,75 @@
lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
by (lifting concat_append)
+text {* ffilter *}
+
+lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+by (lifting sub_list_filter)
+
+lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+by (lifting list_eq_filter)
+
+lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
+
+section {* lemmas transferred from Finite_Set theory *}
+
+text {* finiteness for finite sets holds *}
+lemma finite_fset: "finite (fset_to_set S)"
+ by (induct S) auto
+
+lemma fset_choice: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+ unfolding fset_to_set_trans
+ by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
+
+lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+ unfolding fset_to_set_trans
+ by (rule subset_empty)
+
+lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+ unfolding fset_to_set_trans
+ by (rule not_psubset_empty)
+
+lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+ unfolding fset_to_set_trans
+ by (rule card_mono[OF finite_fset])
+
+lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+ unfolding fset_to_set_trans
+ by (rule card_seteq[OF finite_fset])
+
+lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+ unfolding fset_to_set_trans
+ by (rule psubset_card_mono[OF finite_fset])
+
+lemma fcard_funion_finter: "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+ unfolding fset_to_set_trans
+ by (rule card_Un_Int[OF finite_fset finite_fset])
+
+lemma fcard_funion_disjoint: "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+ unfolding fset_to_set_trans
+ by (rule card_Un_disjoint[OF finite_fset finite_fset])
+
+lemma fcard_delete1_less: "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
+ unfolding fset_to_set_trans
+ by (rule card_Diff1_less[OF finite_fset])
+
+lemma fcard_delete2_less: "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
+ unfolding fset_to_set_trans
+ by (rule card_Diff2_less[OF finite_fset])
+
+lemma fcard_delete1_le: "fcard (fdelete xs x) <= fcard xs"
+ unfolding fset_to_set_trans
+ by (rule card_Diff1_le[OF finite_fset])
+
+lemma fcard_psubset: "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+ unfolding fset_to_set_trans
+ by (rule card_psubset[OF finite_fset])
+
+lemma fcard_fmap_le: "fcard (fmap f xs) \<le> fcard xs"
+ unfolding fset_to_set_trans
+ by (rule card_image_le[OF finite_fset])
+
ML {*
fun dest_fsetT (Type (@{type_name fset}, [T])) = T
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
--- a/src/HOL/SEQ.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/SEQ.thy Tue May 04 13:11:15 2010 -0700
@@ -464,10 +464,12 @@
lemma convergent_setsum:
fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
- assumes "finite A" and "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
+ assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
-using assms
-by (induct A set: finite, simp_all add: convergent_const convergent_add)
+proof (cases "finite A")
+ case True from this and assms show ?thesis
+ by (induct A set: finite) (simp_all add: convergent_const convergent_add)
+qed (simp add: convergent_const)
lemma (in bounded_linear) convergent:
assumes "convergent (\<lambda>n. X n)"
--- a/src/HOL/Statespace/state_space.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Statespace/state_space.ML Tue May 04 13:11:15 2010 -0700
@@ -440,7 +440,7 @@
fun string_of_typ T =
setmp_CRITICAL show_sorts true
- (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
+ (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
val fixestate = (case state_type of
NONE => []
| SOME s =>
@@ -502,7 +502,7 @@
*)
val _ = writeln ("Defining statespace " ^ quote name ^ " ...");
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
fun add_parent (Ts,pname,rs) env =
let
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue May 04 13:11:15 2010 -0700
@@ -100,7 +100,7 @@
val def' = Syntax.check_term lthy def;
val ((_, (_, thm)), lthy') = Specification.definition
(NONE, (Attrib.empty_binding, def')) lthy;
- val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+ val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
in (thm', lthy') end;
fun tac thms = Class.intro_classes_tac []
--- a/src/HOL/Tools/Datatype/datatype_data.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Tue May 04 13:11:15 2010 -0700
@@ -165,7 +165,7 @@
fun read_typ thy str sorts =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
|> fold (Variable.declare_typ o TFree) sorts;
val T = Syntax.read_typ ctxt str;
in (T, Term.add_tfreesT T sorts) end;
@@ -316,7 +316,7 @@
val (splits, thy9) = Datatype_Abs_Proofs.prove_split_thms
config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
- val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
+ val inducts = Project_Rule.projections (ProofContext.init_global thy2) induct;
val dt_infos = map_index
(make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
(hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
@@ -435,7 +435,7 @@
end;
in
thy
- |> ProofContext.init
+ |> ProofContext.init_global
|> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
end;
--- a/src/HOL/Tools/Function/relation.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Function/relation.ML Tue May 04 13:11:15 2010 -0700
@@ -14,19 +14,20 @@
structure Function_Relation : FUNCTION_RELATION =
struct
-fun inst_thm ctxt rel st =
+fun inst_state_tac ctxt rel st =
let
val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
- val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
- in
- Drule.cterm_instantiate [(Rvar, rel')] st'
+ in case Term.add_vars (prop_of st') [] of
+ [v] =>
+ PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
+ | _ => Seq.empty
end
fun relation_tac ctxt rel i =
TRY (Function_Common.apply_termination_rule ctxt i)
- THEN PRIMITIVE (inst_thm ctxt rel)
+ THEN inst_state_tac ctxt rel
val setup =
Method.setup @{binding relation}
--- a/src/HOL/Tools/Function/size.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Function/size.ML Tue May 04 13:11:15 2010 -0700
@@ -133,7 +133,7 @@
val (thm, lthy') = lthy
|> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
|-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
- val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
+ val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy');
val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
in (thm', lthy') end;
@@ -152,7 +152,7 @@
||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
||> Local_Theory.exit_global;
- val ctxt = ProofContext.init thy';
+ val ctxt = ProofContext.init_global thy';
val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue May 04 13:11:15 2010 -0700
@@ -286,7 +286,7 @@
end
fun default_params thy =
- extract_params (ProofContext.init thy) false (default_raw_params thy)
+ extract_params (ProofContext.init_global thy) false (default_raw_params thy)
o map (apsnd single)
val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue May 04 13:11:15 2010 -0700
@@ -778,7 +778,7 @@
let
val (_, args) = strip_comb atom
in rewrite_args args end
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
val intro_t = prop_of intro'
val concl = Logic.strip_imp_concl intro_t
@@ -860,7 +860,8 @@
fun peephole_optimisation thy intro =
let
- val process = MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init thy))
+ val process =
+ MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy))
fun process_False intro_t =
if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
fun process_True intro_t =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue May 04 13:11:15 2010 -0700
@@ -580,7 +580,7 @@
fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
| replace_eqs t = t
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
val prems = Thm.prems_of elimrule
val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
@@ -608,7 +608,7 @@
val no_compilation = ([], ([], []))
fun fetch_pred_data thy name =
- case try (Inductive.the_inductive (ProofContext.init thy)) name of
+ case try (Inductive.the_inductive (ProofContext.init_global thy)) name of
SOME (info as (_, result)) =>
let
fun is_intro_of intro =
@@ -621,7 +621,7 @@
val pre_elim = nth (#elims result) index
val pred = nth (#preds result) index
val nparams = length (Inductive.params_of (#raw_induct result))
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val elim_t = mk_casesrule ctxt pred intros
val elim =
prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
@@ -636,7 +636,7 @@
in PredData.map (Graph.map_node name (map_pred_data add)) end
fun is_inductive_predicate thy name =
- is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
+ is_some (try (Inductive.the_inductive (ProofContext.init_global thy)) name)
fun depending_preds_of thy (key, value) =
let
@@ -688,7 +688,7 @@
val pred = Const (constname, T)
val pre_elim =
(Drule.export_without_context o Skip_Proof.make_thm thy)
- (mk_casesrule (ProofContext.init thy) pred pre_intros)
+ (mk_casesrule (ProofContext.init_global thy) pred pre_intros)
in register_predicate (constname, pre_intros, pre_elim) thy end
fun defined_function_of compilation pred =
@@ -1160,7 +1160,7 @@
fun is_possible_output thy vs t =
forall
(fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
- (non_invertible_subterms (ProofContext.init thy) t)
+ (non_invertible_subterms (ProofContext.init_global thy) t)
andalso
(forall (is_eqT o snd)
(inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
@@ -1367,7 +1367,7 @@
val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
in (modes, modes) end
val (in_ts, out_ts) = split_mode mode ts
- val in_vs = maps (vars_of_destructable_term (ProofContext.init thy)) in_ts
+ val in_vs = maps (vars_of_destructable_term (ProofContext.init_global thy)) in_ts
val out_vs = terms_vs out_ts
fun known_vs_after p vs = (case p of
Prem t => union (op =) vs (term_vs t)
@@ -1939,7 +1939,7 @@
fun compile_pred options compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val compilation_modifiers = if pol then compilation_modifiers else
negative_comp_modifiers_of compilation_modifiers
val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
@@ -2072,11 +2072,11 @@
val simprules = [defthm, @{thm eval_pred},
@{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
- val introthm = Goal.prove (ProofContext.init thy)
+ val introthm = Goal.prove (ProofContext.init_global thy)
(argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
- val elimthm = Goal.prove (ProofContext.init thy)
+ val elimthm = Goal.prove (ProofContext.init_global thy)
(argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
val opt_neg_introthm =
if is_all_input mode then
@@ -2090,7 +2090,7 @@
Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps
(@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
THEN rtac @{thm Predicate.singleI} 1
- in SOME (Goal.prove (ProofContext.init thy) (argnames @ hoarg_names') []
+ in SOME (Goal.prove (ProofContext.init_global thy) (argnames @ hoarg_names') []
neg_introtrm (fn _ => tac))
end
else NONE
@@ -2604,7 +2604,7 @@
fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
in
Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
@@ -2667,7 +2667,7 @@
val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
val (preds, intrs) = unify_consts thy preds intrs
val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs]
- (ProofContext.init thy)
+ (ProofContext.init_global thy)
val preds = map dest_Const preds
val all_vs = terms_vs intrs
val all_modes =
@@ -2744,7 +2744,7 @@
val nparams = nparams_of thy predname
val elim' =
(Drule.export_without_context o Skip_Proof.make_thm thy)
- (mk_casesrule (ProofContext.init thy) nparams intros)
+ (mk_casesrule (ProofContext.init_global thy) nparams intros)
in
if not (Thm.equiv_thm (elim, elim')) then
error "Introduction and elimination rules do not match!"
@@ -2757,7 +2757,7 @@
fun add_code_equations thy preds result_thmss =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
fun add_code_equation (predname, T) (pred, result_thms) =
let
val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
@@ -3047,7 +3047,7 @@
fun after_qed thms goal_ctxt =
let
val global_thms = ProofContext.export goal_ctxt
- (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
+ (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms)
in
goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #>
((case compilation options of
@@ -3164,7 +3164,7 @@
| DSeq => dseq_comp_modifiers
| Pos_Random_DSeq => pos_random_dseq_comp_modifiers
| New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
- val t_pred = compile_expr comp_modifiers (ProofContext.init thy)
+ val t_pred = compile_expr comp_modifiers (ProofContext.init_global thy)
(body, deriv) additional_arguments;
val T_pred = dest_predT compfuns (fastype_of t_pred)
val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue May 04 13:11:15 2010 -0700
@@ -129,7 +129,7 @@
fun split_all_pairs thy th =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val ((_, [th']), ctxt') = Variable.import true [th] ctxt
val t = prop_of th'
val frees = Term.add_frees t []
@@ -153,7 +153,7 @@
fun inline_equations thy th =
let
- val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init thy)
+ val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init_global thy)
val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th
(*val _ = print_step options
("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
@@ -188,7 +188,7 @@
tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
" with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
else ()
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
fun filtering th =
if is_equationlike th andalso
defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue May 04 13:11:15 2010 -0700
@@ -195,7 +195,7 @@
SOME raw_split_thm =>
let
val (f, args) = strip_comb t
- val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
+ val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue May 04 13:11:15 2010 -0700
@@ -64,7 +64,7 @@
fun instantiated_case_rewrites thy Tcon =
let
val rew_ths = case_rewrites thy Tcon
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
fun instantiate th =
let
val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
@@ -128,9 +128,10 @@
| SOME raw_split_thm =>
let
val (f, args) = strip_comb atom
- val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
+ val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
(* TODO: contextify things - this line is to unvarify the split_thm *)
- (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
+ (*val ((_, [isplit_thm]), _) =
+ Variable.import true [split_thm] (ProofContext.init_global thy)*)
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
val Tcons = datatype_names_of_case_name thy (fst (dest_Const f))
@@ -188,7 +189,7 @@
fun flatten_intros constname intros thy =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val ((_, intros), ctxt') = Variable.import true intros ctxt
val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
(flatten constname) (map prop_of intros) ([], thy)
@@ -206,7 +207,7 @@
fun introrulify thy ths =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val ((_, ths'), ctxt') = Variable.import true ths ctxt
fun introrulify' th =
let
@@ -277,7 +278,7 @@
SOME specss => (specss, thy)
| NONE =>*)
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val intros =
if forall is_pred_equation specs then
map (map_term thy (maps_premises (split_conjs thy))) (introrulify thy (map rewrite specs))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue May 04 13:11:15 2010 -0700
@@ -200,7 +200,7 @@
(map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
val tac = fn _ => Skip_Proof.cheat_tac thy1
- val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac
+ val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
val (thy3, preproc_time) = cpu_time "predicate preprocessing"
(fn () => Predicate_Compile.preprocess options const thy2)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Tue May 04 13:11:15 2010 -0700
@@ -65,7 +65,7 @@
fun specialise_intros black_list (pred, intros) pats thy =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue May 04 13:11:15 2010 -0700
@@ -48,7 +48,7 @@
fun atomize_thm thm =
let
- val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
+ val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
val thm'' = Object_Logic.atomize (cprop_of thm')
in
@{thm equal_elim_rule1} OF [thm'', thm']
--- a/src/HOL/Tools/TFL/post.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/TFL/post.ML Tue May 04 13:11:15 2010 -0700
@@ -140,8 +140,8 @@
fun simplify_defn strict thy cs ss congs wfs id pats def0 =
let
- val ctxt = ProofContext.init thy
- val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
+ val ctxt = ProofContext.init_global thy
+ val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
val {rules,rows,TCs,full_pats_TCs} =
Prim.post_definition congs (thy, (def,pats))
val {lhs=f,rhs} = S.dest_eq (concl def)
--- a/src/HOL/Tools/TFL/rules.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/TFL/rules.ML Tue May 04 13:11:15 2010 -0700
@@ -134,9 +134,8 @@
in fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
end;
-(* freezeT expensive! *)
fun UNDISCH thm =
- let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
+ let val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm)))
in Thm.implies_elim (thm RS mp) (ASSUME tm) end
handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
| THM _ => raise RULES_ERR "UNDISCH" "";
@@ -252,7 +251,7 @@
| place _ _ = raise RULES_ERR "organize" "not a permutation.2"
in place
end;
-(* freezeT expensive! *)
+
fun DISJ_CASESL disjth thl =
let val c = cconcl disjth
fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
@@ -265,7 +264,7 @@
| DL th (th1::rst) =
let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
- in DL (Thm.freezeT disjth) (organize eq tml thl)
+ in DL disjth (organize eq tml thl)
end;
@@ -814,7 +813,7 @@
let
val thy = Thm.theory_of_cterm ptm;
val t = Thm.term_of ptm;
- val ctxt = ProofContext.init thy |> Variable.auto_fixes t;
+ val ctxt = ProofContext.init_global thy |> Variable.auto_fixes t;
in
if strict then Goal.prove ctxt [] [] t (K tac)
else Goal.prove ctxt [] [] t (K tac)
--- a/src/HOL/Tools/TFL/tfl.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/TFL/tfl.ML Tue May 04 13:11:15 2010 -0700
@@ -361,7 +361,7 @@
(*For Isabelle, the lhs of a definition must be a constant.*)
fun const_def sign (c, Ty, rhs) =
- singleton (Syntax.check_terms (ProofContext.init sign))
+ singleton (Syntax.check_terms (ProofContext.init_global sign))
(Const("==",dummyT) $ Const(c,Ty) $ rhs);
(*Make all TVars available for instantiation by adding a ? to the front*)
@@ -541,7 +541,7 @@
thy
|> PureThy.add_defs false
[Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
- val def = Thm.freezeT def0;
+ val def = Thm.unvarify_global def0;
val dummy =
if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
else ()
--- a/src/HOL/Tools/choice_specification.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/choice_specification.ML Tue May 04 13:11:15 2010 -0700
@@ -78,10 +78,9 @@
| NONE => mk_definitional cos arg
end
-fun add_specification axiomatic cos arg =
- arg |> apsnd Thm.freezeT
- |> proc_exprop axiomatic cos
- |> apsnd Drule.export_without_context
+fun add_specification axiomatic cos =
+ proc_exprop axiomatic cos
+ #> apsnd Drule.export_without_context
(* Collect all intances of constants in term *)
@@ -217,15 +216,16 @@
then writeln "specification"
else ()
in
- arg |> apsnd Thm.freezeT
+ arg |> apsnd Thm.unvarify_global
|> process_all (zip3 alt_names rew_imps frees)
end
- fun after_qed [[thm]] = ProofContext.theory (fn thy =>
- #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
+ fun after_qed [[thm]] = (ProofContext.theory (fn thy =>
+ #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm)))));
in
thy
- |> ProofContext.init
+ |> ProofContext.init_global
+ |> Variable.declare_term ex_prop
|> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
end;
--- a/src/HOL/Tools/cnf_funcs.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/cnf_funcs.ML Tue May 04 13:11:15 2010 -0700
@@ -436,8 +436,8 @@
val var = new_free ()
val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *)
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
- val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
- val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
@@ -447,8 +447,8 @@
val var = new_free ()
val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *)
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
- val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
- val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
in
iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *)
end
@@ -467,8 +467,8 @@
val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *)
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *)
- val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
- val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
in
iff_trans OF [thm1, thm5]
end
--- a/src/HOL/Tools/inductive.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/inductive.ML Tue May 04 13:11:15 2010 -0700
@@ -323,11 +323,11 @@
(* prove monotonicity *)
-fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos ctxt =
+fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
(message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
" Proving monotonicity ...";
(if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
- (map (fst o dest_Free) params) []
+ [] []
(HOLogic.mk_Trueprop
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
(fn _ => EVERY [rtac @{thm monoI} 1,
@@ -340,7 +340,7 @@
(* prove introduction rules *)
-fun prove_intrs quiet_mode coind mono fp_def k params intr_ts rec_preds_defs ctxt =
+fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' =
let
val _ = clean_message quiet_mode " Proving the introduction rules ...";
@@ -354,27 +354,27 @@
val rules = [refl, TrueI, notFalseI, exI, conjI];
- val intrs = map_index (fn (i, intr) => rulify
- (Skip_Proof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
+ val intrs = map_index (fn (i, intr) =>
+ Skip_Proof.prove ctxt [] [] intr (fn _ => EVERY
[rewrite_goals_tac rec_preds_defs,
rtac (unfold RS iffD2) 1,
EVERY1 (select_disj (length intr_ts) (i + 1)),
(*Not ares_tac, since refl must be tried before any equality assumptions;
backtracking may occur if the premises have extra variables!*)
- DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]))) intr_ts
+ DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
+ |> rulify
+ |> singleton (ProofContext.export ctxt ctxt')) intr_ts
in (intrs, unfold) end;
(* prove elimination rules *)
-fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt =
+fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' =
let
val _ = clean_message quiet_mode " Proving the elimination rules ...";
- val ([pname], ctxt') = ctxt |>
- Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
- Variable.variant_fixes ["P"];
+ val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt;
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
fun dest_intr r =
@@ -410,7 +410,7 @@
EVERY (map (fn prem =>
DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
|> rulify
- |> singleton (ProofContext.export ctxt'' ctxt),
+ |> singleton (ProofContext.export ctxt'' ctxt'''),
map #2 c_intrs, length Ts)
end
@@ -488,16 +488,14 @@
(* prove induction rule *)
fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
- fp_def rec_preds_defs ctxt =
+ fp_def rec_preds_defs ctxt ctxt''' =
let
val _ = clean_message quiet_mode " Proving the induction rule ...";
val thy = ProofContext.theory_of ctxt;
(* predicates for induction rule *)
- val (pnames, ctxt') = ctxt |>
- Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
- Variable.variant_fixes (mk_names "P" (length cs));
+ val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt;
val preds = map2 (curry Free) pnames
(map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs);
@@ -592,7 +590,7 @@
rewrite_goals_tac simp_thms',
atac 1])])
- in singleton (ProofContext.export ctxt'' ctxt) (induct RS lemma) end;
+ in singleton (ProofContext.export ctxt'' ctxt''') (induct RS lemma) end;
@@ -689,11 +687,13 @@
||> Local_Theory.restore_naming lthy';
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
- val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos lthy'';
- val ((_, [mono']), lthy''') =
- Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
+ val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
+ val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
+ val (_, lthy'''') =
+ Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
+ ProofContext.export lthy''' lthy'' [mono]) lthy'';
- in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
+ in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
list_comb (rec_const, params), preds, argTs, bs, xs)
end;
@@ -774,31 +774,30 @@
val ((intr_names, intr_atts), intr_ts) =
apfst split_list (split_list (map (check_rule lthy cs params) intros));
- val (lthy1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
+ val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
monos params cnames_syn lthy;
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
- params intr_ts rec_preds_defs lthy1;
+ intr_ts rec_preds_defs lthy2 lthy1;
val elims =
if no_elim then []
else
prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
- unfold rec_preds_defs lthy1;
+ unfold rec_preds_defs lthy2 lthy1;
val raw_induct = zero_var_indexes
(if no_ind then Drule.asm_rl
else if coind then
- singleton (ProofContext.export
- (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
+ singleton (ProofContext.export lthy2 lthy1)
(rotate_prems ~1 (Object_Logic.rulify
(fold_rule rec_preds_defs
(rewrite_rule simp_thms'''
(mono RS (fp_def RS @{thm def_coinduct}))))))
else
prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
- rec_preds_defs lthy1);
+ rec_preds_defs lthy2 lthy1);
- val (intrs', elims', induct, inducts, lthy2) = declare_rules rec_name coind no_ind
+ val (intrs', elims', induct, inducts, lthy3) = declare_rules rec_name coind no_ind
cnames preds intrs intr_names intr_atts elims raw_induct lthy1;
val result =
@@ -809,11 +808,11 @@
induct = induct,
inducts = inducts};
- val lthy3 = lthy2
+ val lthy4 = lthy3
|> Local_Theory.declaration false (fn phi =>
let val result' = morph_result phi result;
in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
- in (result, lthy3) end;
+ in (result, lthy4) end;
(* external interfaces *)
--- a/src/HOL/Tools/inductive_codegen.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/inductive_codegen.ML Tue May 04 13:11:15 2010 -0700
@@ -66,7 +66,7 @@
val nparms = (case optnparms of
SOME k => k
| NONE => (case rules of
- [] => (case try (Inductive.the_inductive (ProofContext.init thy)) s of
+ [] => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
SOME (_, {raw_induct, ...}) =>
length (Inductive.params_of raw_induct)
| NONE => 0)
@@ -84,7 +84,7 @@
fun get_clauses thy s =
let val {intros, graph, ...} = CodegenData.get thy
in case Symtab.lookup intros s of
- NONE => (case try (Inductive.the_inductive (ProofContext.init thy)) s of
+ NONE => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
NONE => NONE
| SOME ({names, ...}, {intrs, raw_induct, ...}) =>
SOME (names, Codegen.thyname_of_const thy s,
--- a/src/HOL/Tools/inductive_realizer.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/inductive_realizer.ML Tue May 04 13:11:15 2010 -0700
@@ -137,7 +137,7 @@
fun fun_of_prem thy rsets vs params rule ivs intr =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val args = map (Free o apfst fst o dest_Var) ivs;
val args' = map (Free o apfst fst)
(subtract (op =) params (Term.add_vars (prop_of intr) []));
@@ -484,7 +484,7 @@
fun add_ind_realizers name rsets thy =
let
val (_, {intrs, induct, raw_induct, elims, ...}) =
- Inductive.the_inductive (ProofContext.init thy) name;
+ Inductive.the_inductive (ProofContext.init_global thy) name;
val vss = sort (int_ord o pairself length)
(subsets (map fst (relevant_vars (concl_of (hd intrs)))))
in
--- a/src/HOL/Tools/old_primrec.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/old_primrec.ML Tue May 04 13:11:15 2010 -0700
@@ -214,7 +214,7 @@
fs @ map Bound (0 ::(length ls downto 1))))
val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def";
val def_prop =
- singleton (Syntax.check_terms (ProofContext.init thy))
+ singleton (Syntax.check_terms (ProofContext.init_global thy))
(Logic.mk_equals (Const (fname, dummyT), rhs));
in (def_name, def_prop) end;
--- a/src/HOL/Tools/recdef.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/recdef.ML Tue May 04 13:11:15 2010 -0700
@@ -160,7 +160,7 @@
fun prepare_hints thy opt_src =
let
- val ctxt0 = ProofContext.init thy;
+ val ctxt0 = ProofContext.init_global thy;
val ctxt =
(case opt_src of
NONE => ctxt0
@@ -172,7 +172,7 @@
fun prepare_hints_i thy () =
let
- val ctxt0 = ProofContext.init thy;
+ val ctxt0 = ProofContext.init_global thy;
val {simps, congs, wfs} = get_global_hints thy;
in (claset_of ctxt0, simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
@@ -234,7 +234,7 @@
val _ = requires_recdef thy;
val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
- val congs = eval_thms (ProofContext.init thy) raw_congs;
+ val congs = eval_thms (ProofContext.init_global thy) raw_congs;
val (thy2, induct_rules) = tfl_fn thy congs name eqs;
val ([induct_rules'], thy3) =
thy2
--- a/src/HOL/Tools/record.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/record.ML Tue May 04 13:11:15 2010 -0700
@@ -1038,7 +1038,7 @@
let val thm =
if ! quick_and_dirty then Skip_Proof.make_thm thy prop
else if Goal.future_enabled () then
- Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
+ Goal.future_result (ProofContext.init_global thy) (Future.fork_pri ~1 prf) prop
else prf ()
in Drule.export_without_context thm end;
@@ -1048,7 +1048,7 @@
if ! quick_and_dirty then Skip_Proof.prove
else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
else Goal.prove_future;
- val prf = prv (ProofContext.init thy) [] asms prop tac;
+ val prf = prv (ProofContext.init_global thy) [] asms prop tac;
in if stndrd then Drule.export_without_context prf else prf end;
val prove_future_global = prove_common false;
@@ -1090,7 +1090,7 @@
else mk_comp_id acc;
val prop = lhs === rhs;
val othm =
- Goal.prove (ProofContext.init thy) [] [] prop
+ Goal.prove (ProofContext.init_global thy) [] [] prop
(fn _ =>
simp_tac defset 1 THEN
REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
@@ -1114,7 +1114,7 @@
else mk_comp (u' $ f') (u $ f);
val prop = lhs === rhs;
val othm =
- Goal.prove (ProofContext.init thy) [] [] prop
+ Goal.prove (ProofContext.init_global thy) [] [] prop
(fn _ =>
simp_tac defset 1 THEN
REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
@@ -1155,7 +1155,7 @@
val (_, args) = strip_comb lhs;
val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
in
- Goal.prove (ProofContext.init thy) [] [] prop'
+ Goal.prove (ProofContext.init_global thy) [] [] prop'
(fn _ =>
simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
@@ -1247,7 +1247,7 @@
val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)];
val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
in
- Goal.prove (ProofContext.init thy) [] [] prop
+ Goal.prove (ProofContext.init_global thy) [] [] prop
(fn _ =>
simp_tac simpset 1 THEN
REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
@@ -2388,7 +2388,7 @@
if quiet_mode then ()
else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T)
handle TYPE (msg, _, _) => error msg;
@@ -2438,7 +2438,7 @@
fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
val (parent, ctxt2) = read_parent raw_parent ctxt1;
--- a/src/HOL/Tools/typecopy.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/typecopy.ML Tue May 04 13:11:15 2010 -0700
@@ -52,7 +52,7 @@
fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
let
val ty = Sign.certify_typ thy raw_ty;
- val ctxt = ProofContext.init thy |> Variable.declare_typ ty;
+ val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
val vs = map (ProofContext.check_tfree ctxt) raw_vs;
val tac = Tactic.rtac UNIV_witness 1;
fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
--- a/src/HOL/Tools/typedef.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Tools/typedef.ML Tue May 04 13:11:15 2010 -0700
@@ -182,7 +182,8 @@
val thy = ProofContext.theory_of set_lthy;
val cert = Thm.cterm_of thy;
val (defs, A) =
- Local_Defs.export_cterm set_lthy (ProofContext.init thy) (cert set') ||> Thm.term_of;
+ Local_Defs.export_cterm set_lthy (ProofContext.init_global thy) (cert set')
+ ||> Thm.term_of;
val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
--- a/src/HOL/Wellfounded.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Wellfounded.thy Tue May 04 13:11:15 2010 -0700
@@ -68,7 +68,7 @@
assumes lin: "OFCLASS('a::ord, linorder_class)"
shows "OFCLASS('a::ord, wellorder_class)"
using lin by (rule wellorder_class.intro)
- (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
+ (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
lemma (in wellorder) wf:
"wf {(x, y). x < y}"
--- a/src/HOL/Word/WordArith.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/Word/WordArith.thy Tue May 04 13:11:15 2010 -0700
@@ -17,7 +17,7 @@
by (auto simp del: word_uint.Rep_inject
simp: word_uint.Rep_inject [symmetric])
-lemma signed_linorder: "linorder word_sle word_sless"
+lemma signed_linorder: "class.linorder word_sle word_sless"
proof
qed (unfold word_sle_def word_sless_def, auto)
--- a/src/HOL/ex/Landau.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOL/ex/Landau.thy Tue May 04 13:11:15 2010 -0700
@@ -187,7 +187,7 @@
proof -
interpret preorder_equiv less_eq_fun less_fun proof
qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
- show "preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
+ show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
show "preorder_equiv.equiv less_eq_fun = equiv_fun"
by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
qed
--- a/src/HOLCF/CompactBasis.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOLCF/CompactBasis.thy Tue May 04 13:11:15 2010 -0700
@@ -237,12 +237,12 @@
where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
lemma fold_pd_PDUnit:
- assumes "ab_semigroup_idem_mult f"
+ assumes "class.ab_semigroup_idem_mult f"
shows "fold_pd g f (PDUnit x) = g x"
unfolding fold_pd_def Rep_PDUnit by simp
lemma fold_pd_PDPlus:
- assumes "ab_semigroup_idem_mult f"
+ assumes "class.ab_semigroup_idem_mult f"
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
proof -
interpret ab_semigroup_idem_mult f by fact
--- a/src/HOLCF/ConvexPD.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy Tue May 04 13:11:15 2010 -0700
@@ -412,7 +412,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
lemma ACI_convex_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
apply unfold_locales
apply (simp add: convex_plus_assoc)
apply (simp add: convex_plus_commute)
--- a/src/HOLCF/LowerPD.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOLCF/LowerPD.thy Tue May 04 13:11:15 2010 -0700
@@ -393,7 +393,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
lemma ACI_lower_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
apply unfold_locales
apply (simp add: lower_plus_assoc)
apply (simp add: lower_plus_commute)
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue May 04 13:11:15 2010 -0700
@@ -189,7 +189,7 @@
(K (beta_tac 1));
val tuple_unfold_thm =
(@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
- |> Local_Defs.unfold (ProofContext.init thy) @{thms split_conv};
+ |> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv};
fun mk_unfold_thms [] thm = []
| mk_unfold_thms (n::[]) thm = [(n, thm)]
@@ -380,7 +380,7 @@
fun read_typ thy str sorts =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
|> fold (Variable.declare_typ o TFree) sorts;
val T = Syntax.read_typ ctxt str;
in (T, Term.add_tfreesT T sorts) end;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue May 04 13:11:15 2010 -0700
@@ -71,7 +71,7 @@
end;
fun legacy_infer_term thy t =
- let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
+ let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init_global thy)
in singleton (Syntax.check_terms ctxt) (intern_term thy t) end;
fun pg'' thy defs t tacs =
@@ -347,7 +347,7 @@
(* ----- theorems concerning finiteness and induction ----------------------- *)
- val global_ctxt = ProofContext.init thy;
+ val global_ctxt = ProofContext.init_global thy;
val _ = trace " Proving ind...";
val ind =
@@ -422,7 +422,7 @@
bot :: map (fn (c,_) => Long_Name.base_name c) cons;
in adms @ flat (map2 one_eq bottoms eqs) end;
-val inducts = Project_Rule.projections (ProofContext.init thy) ind;
+val inducts = Project_Rule.projections (ProofContext.init_global thy) ind;
fun ind_rule (dname, rule) =
((Binding.empty, [rule]),
[Rule_Cases.case_names case_ns, Induct.induct_type dname]);
@@ -470,7 +470,7 @@
local
fun legacy_infer_term thy t =
- singleton (Syntax.check_terms (ProofContext.init thy)) (intern_term thy t);
+ singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
fun infer_props thy = map (apsnd (legacy_infer_prop thy));
fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
--- a/src/HOLCF/Tools/pcpodef.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOLCF/Tools/pcpodef.ML Tue May 04 13:11:15 2010 -0700
@@ -170,7 +170,7 @@
(*rhs*)
val tmp_ctxt =
- ProofContext.init thy
+ ProofContext.init_global thy
|> fold (Variable.declare_typ o TFree) raw_args;
val set = prep_term tmp_ctxt raw_set;
val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
@@ -207,7 +207,7 @@
val ((_, (_, below_ldef)), lthy4) = lthy3
|> Specification.definition (NONE,
((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
- val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
+ val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4);
val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
val thy5 = lthy4
|> Class.prove_instantiation_instance
@@ -322,7 +322,7 @@
fun gen_cpodef_proof prep_term prep_constraint
((def, name), (b, raw_args, mx), set, opt_morphs) thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val args = map (apsnd (prep_constraint ctxt)) raw_args;
val (goal1, goal2, make_result) =
prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
@@ -333,7 +333,7 @@
fun gen_pcpodef_proof prep_term prep_constraint
((def, name), (b, raw_args, mx), set, opt_morphs) thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val args = map (apsnd (prep_constraint ctxt)) raw_args;
val (goal1, goal2, make_result) =
prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
--- a/src/HOLCF/Tools/repdef.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/HOLCF/Tools/repdef.ML Tue May 04 13:11:15 2010 -0700
@@ -65,7 +65,7 @@
(*rhs*)
val tmp_ctxt =
- ProofContext.init thy
+ ProofContext.init_global thy
|> fold (Variable.declare_typ o TFree) raw_args;
val defl = prep_term tmp_ctxt raw_defl;
val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
@@ -119,7 +119,7 @@
Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
val ((_, (_, approx_ldef)), lthy) =
Specification.definition (NONE, (approx_bind, approx_eqn)) lthy;
- val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+ val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef;
@@ -161,7 +161,7 @@
fun repdef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args;
in snd (gen_add_repdef Syntax.read_term def name (b, args, mx) A morphs thy) end;
--- a/src/HOLCF/UpperPD.thy Tue May 04 13:08:56 2010 -0700
+++ b/src/HOLCF/UpperPD.thy Tue May 04 13:11:15 2010 -0700
@@ -388,7 +388,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
lemma ACI_upper_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
apply unfold_locales
apply (simp add: upper_plus_assoc)
apply (simp add: upper_plus_commute)
--- a/src/Provers/classical.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Provers/classical.ML Tue May 04 13:11:15 2010 -0700
@@ -210,7 +210,7 @@
fun dup_elim th =
let
val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
- val ctxt = ProofContext.init (Thm.theory_of_thm rl);
+ val ctxt = ProofContext.init_global (Thm.theory_of_thm rl);
in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
@@ -856,7 +856,7 @@
fun global_claset_of thy =
let val (cs, ctxt_cs) = GlobalClaset.get thy
- in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
+ in context_cs (ProofContext.init_global thy) cs (ctxt_cs) end;
(* context dependent components *)
--- a/src/Provers/quantifier1.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Provers/quantifier1.ML Tue May 04 13:11:15 2010 -0700
@@ -113,7 +113,7 @@
in exqu [] end;
fun prove_conv tac thy tu =
- Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
+ Goal.prove (ProofContext.init_global thy) [] [] (Logic.mk_equals tu)
(K (rtac iff_reflection 1 THEN tac));
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)
--- a/src/Pure/Isar/class.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/class.ML Tue May 04 13:11:15 2010 -0700
@@ -32,7 +32,7 @@
fun calculate thy class sups base_sort param_map assm_axiom =
let
- val empty_ctxt = ProofContext.init thy;
+ val empty_ctxt = ProofContext.init_global thy;
(* instantiation of canonical interpretation *)
val aT = TFree (Name.aT, base_sort);
@@ -143,7 +143,7 @@
#> add_typ_check ~10 "singleton_fixate" singleton_fixate;
val raw_supexpr = (map (fn sup => (sup, (("", false),
Expression.Positional []))) sups, []);
- val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
+ val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy
|> prep_decl raw_supexpr init_class_body raw_elems;
fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
| fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
@@ -194,7 +194,7 @@
val sup_sort = inter_sort base_sort sups;
(* process elements as class specification *)
- val class_ctxt = begin sups base_sort (ProofContext.init thy);
+ val class_ctxt = begin sups base_sort (ProofContext.init_global thy);
val ((_, _, syntax_elems), _) = class_ctxt
|> Expression.cert_declaration supexpr I inferred_elems;
fun check_vars e vs = if null vs
@@ -276,16 +276,16 @@
#> pair (param_map, params, assm_axiom)))
end;
-fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
let
- val class = Sign.full_name thy bname;
+ val class = Sign.full_name thy b;
val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
prep_class_spec thy raw_supclasses raw_elems;
in
thy
- |> Expression.add_locale bname Binding.empty supexpr elems
+ |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
|> snd |> Local_Theory.exit_global
- |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
+ |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
||> Theory.checkpoint
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
@@ -340,7 +340,7 @@
val subclass = gen_subclass (K I) user_proof;
fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
-val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init) user_proof;
+val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
end; (*local*)
--- a/src/Pure/Isar/class_target.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/class_target.ML Tue May 04 13:11:15 2010 -0700
@@ -157,7 +157,7 @@
fun print_classes thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val algebra = Sign.classes_of thy;
val arities =
Symtab.empty
@@ -372,7 +372,7 @@
ProofContext.theory ((fold o fold) AxClass.add_classrel results);
in
thy
- |> ProofContext.init
+ |> ProofContext.init_global
|> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
end;
@@ -421,7 +421,7 @@
fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
(raw_tyco, raw_sorts, raw_sort)) raw_tycos;
val tycos = map #1 all_arities;
@@ -514,7 +514,7 @@
in
thy
|> Theory.checkpoint
- |> ProofContext.init
+ |> ProofContext.init_global
|> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
|> fold (Variable.declare_typ o TFree) vs
|> fold (Variable.declare_names o Free o snd) params
@@ -554,7 +554,7 @@
fun prove_instantiation_exit_result f tac x lthy =
let
val morph = ProofContext.export_morphism lthy
- (ProofContext.init (ProofContext.theory_of lthy));
+ (ProofContext.init_global (ProofContext.theory_of lthy));
val y = f morph x;
in
lthy
@@ -597,7 +597,7 @@
((fold o fold) AxClass.add_arity results);
in
thy
- |> ProofContext.init
+ |> ProofContext.init_global
|> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
end;
--- a/src/Pure/Isar/code.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/code.ML Tue May 04 13:11:15 2010 -0700
@@ -337,7 +337,7 @@
fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
fun read_signature thy = cert_signature thy o Type.strip_sorts
- o Syntax.parse_typ (ProofContext.init thy);
+ o Syntax.parse_typ (ProofContext.init_global thy);
fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
@@ -554,7 +554,7 @@
fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
-fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init thy);
+fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy);
fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
apfst (meta_rewrite thy);
@@ -778,7 +778,7 @@
val _ = if c = const_abs_eqn thy abs_thm then ()
else error ("Wrong head of abstract code equation,\nexpected constant "
^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
- in Abstract (Thm.freezeT abs_thm, tyco) end;
+ in Abstract (Thm.legacy_freezeT abs_thm, tyco) end;
fun constrain_cert thy sorts (Equations (cert_thm, propers)) =
let
@@ -941,7 +941,7 @@
fun print_codesetup thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val exec = the_exec thy;
fun pretty_equations const thms =
(Pretty.block o Pretty.fbreaks) (
--- a/src/Pure/Isar/constdefs.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/constdefs.ML Tue May 04 13:11:15 2010 -0700
@@ -26,7 +26,7 @@
fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
- val thy_ctxt = ProofContext.init thy;
+ val thy_ctxt = ProofContext.init_global thy;
val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
val ((d, mx), var_ctxt) =
(case raw_decl of
@@ -62,7 +62,7 @@
fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
--- a/src/Pure/Isar/expression.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/expression.ML Tue May 04 13:11:15 2010 -0700
@@ -642,7 +642,7 @@
|> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
|> PureThy.add_defs false
[((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
- val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
+ val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
val cert = Thm.cterm_of defs_thy;
@@ -729,7 +729,7 @@
error ("Duplicate definition of locale " ^ quote name);
val ((fixed, deps, body_elems), (parms, ctxt')) =
- prep_decl raw_import I raw_body (ProofContext.init thy);
+ prep_decl raw_import I raw_body (ProofContext.init_global thy);
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
val predicate_binding =
@@ -795,7 +795,7 @@
fun gen_interpretation prep_expr parse_prop prep_attr
expression equations theory =
let
- val ((propss, deps, export), expr_ctxt) = ProofContext.init theory
+ val ((propss, deps, export), expr_ctxt) = ProofContext.init_global theory
|> prep_expr expression;
val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
@@ -809,7 +809,8 @@
val eqn_attrss = map2 (fn attrs => fn eqn =>
((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
fun meta_rewrite thy =
- map (Local_Defs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def) o maps snd;
+ map (Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) #> Drule.abs_def) o
+ maps snd;
in
thy
|> PureThy.note_thmss Thm.lemmaK eqn_attrss
--- a/src/Pure/Isar/local_theory.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/local_theory.ML Tue May 04 13:11:15 2010 -0700
@@ -181,7 +181,8 @@
Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
fun target_morphism lthy = standard_morphism lthy (target_of lthy);
-fun global_morphism lthy = standard_morphism lthy (ProofContext.init (ProofContext.theory_of lthy));
+fun global_morphism lthy =
+ standard_morphism lthy (ProofContext.init_global (ProofContext.theory_of lthy));
(* primitive operations *)
@@ -270,7 +271,7 @@
fun exit_result_global f (x, lthy) =
let
val thy = exit_global lthy;
- val thy_ctxt = ProofContext.init thy;
+ val thy_ctxt = ProofContext.init_global thy;
val phi = standard_morphism lthy thy_ctxt;
in (f phi x, thy) end;
--- a/src/Pure/Isar/locale.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/locale.ML Tue May 04 13:11:15 2010 -0700
@@ -99,7 +99,7 @@
(* syntax declarations *)
notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
(* theorem declarations *)
- dependencies: ((string * morphism) * serial) list
+ dependencies: ((string * (morphism * morphism)) * serial) list
(* locale dependencies (sublocale relation) *)
};
@@ -143,7 +143,8 @@
(binding,
mk_locale ((parameters, spec, intros, axioms),
((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
- map (fn d => (d, serial ())) dependencies))) #> snd);
+ map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies))) #> snd);
+ (* FIXME *)
fun change_locale name =
Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
@@ -223,7 +224,7 @@
then (deps, marked)
else
let
- val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
+ val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
val marked' = (name, instance) :: marked;
val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
in
@@ -308,7 +309,7 @@
fun init name thy =
activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
- ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
+ ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
fun print_locale thy show_facts raw_name =
let
@@ -408,11 +409,10 @@
(* Diagnostic *)
-fun print_registrations thy raw_name =
+fun pretty_reg thy (name, morph) =
let
- val name = intern thy raw_name;
val name' = extern thy name;
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
@@ -422,23 +422,22 @@
else prt_term t;
fun prt_inst ts =
Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
- fun prt_reg (name, morph) =
- let
- val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
- val ts = instance_of thy name morph;
- in
- case qs of
- [] => prt_inst ts
- | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
- Pretty.brk 1, prt_inst ts]
- end;
+
+ val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
+ val ts = instance_of thy name morph;
in
- (case these_registrations thy name of
- [] => Pretty.str ("no interpretations")
- | regs => Pretty.big_list "interpretations:" (map prt_reg (rev regs)))
- |> Pretty.writeln
+ case qs of
+ [] => prt_inst ts
+ | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
+ Pretty.brk 1, prt_inst ts]
end;
+fun print_registrations thy raw_name =
+ (case these_registrations thy (intern thy raw_name) of
+ [] => Pretty.str ("no interpretations")
+ | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
+ |> Pretty.writeln;
+
(* Add and extend registrations *)
@@ -489,7 +488,7 @@
fun add_dependency loc (dep, morph) export thy =
thy
- |> (change_locale loc o apsnd) (cons ((dep, morph $> export), serial ()))
+ |> (change_locale loc o apsnd) (cons ((dep, (morph, export)), serial ()))
|> (fn thy => fold_rev (add_reg_activate_facts export)
(all_registrations thy) thy);
--- a/src/Pure/Isar/object_logic.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/object_logic.ML Tue May 04 13:11:15 2010 -0700
@@ -186,7 +186,7 @@
fun atomize_prems ct =
if Logic.has_meta_prems (Thm.term_of ct) then
Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
- (ProofContext.init (Thm.theory_of_cterm ct)) ct
+ (ProofContext.init_global (Thm.theory_of_cterm ct)) ct
else Conv.all_conv ct;
val atomize_prems_tac = CONVERSION atomize_prems;
--- a/src/Pure/Isar/overloading.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/overloading.ML Tue May 04 13:11:15 2010 -0700
@@ -156,7 +156,7 @@
in
thy
|> Theory.checkpoint
- |> ProofContext.init
+ |> ProofContext.init_global
|> OverloadingData.put overloading
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
|> add_improvable_syntax
--- a/src/Pure/Isar/proof_context.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/proof_context.ML Tue May 04 13:11:15 2010 -0700
@@ -9,7 +9,7 @@
signature PROOF_CONTEXT =
sig
val theory_of: Proof.context -> theory
- val init: theory -> Proof.context
+ val init_global: theory -> Proof.context
type mode
val mode_default: mode
val mode_stmt: mode
--- a/src/Pure/Isar/proof_display.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/proof_display.ML Tue May 04 13:11:15 2010 -0700
@@ -48,7 +48,7 @@
fun pretty_theorems_diff verbose prev_thys thy =
let
- val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
+ val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy);
val facts = PureThy.facts_of thy;
val thmss =
Facts.dest_static (map PureThy.facts_of prev_thys) facts
--- a/src/Pure/Isar/skip_proof.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/skip_proof.ML Tue May 04 13:11:15 2010 -0700
@@ -39,6 +39,6 @@
else tac args st);
fun prove_global thy xs asms prop tac =
- Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
+ Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
end;
--- a/src/Pure/Isar/specification.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/specification.ML Tue May 04 13:11:15 2010 -0700
@@ -169,7 +169,7 @@
fun gen_axioms do_print prep raw_vars raw_specs thy =
let
- val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
+ val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init_global thy);
val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
(*consts*)
--- a/src/Pure/Isar/theory_target.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Isar/theory_target.ML Tue May 04 13:11:15 2010 -0700
@@ -114,7 +114,7 @@
fun import_export_proof ctxt (name, raw_th) =
let
val thy = ProofContext.theory_of ctxt;
- val thy_ctxt = ProofContext.init thy;
+ val thy_ctxt = ProofContext.init_global thy;
val certT = Thm.ctyp_of thy;
val cert = Thm.cterm_of thy;
@@ -213,7 +213,7 @@
fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
let
- val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
+ val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
val target_ctxt = Local_Theory.target_of lthy;
val (mx1, mx2, mx3) = fork_mixfix ta mx;
@@ -286,7 +286,7 @@
fun define ta ((b, mx), ((name, atts), rhs)) lthy =
let
val thy = ProofContext.theory_of lthy;
- val thy_ctxt = ProofContext.init thy;
+ val thy_ctxt = ProofContext.init_global thy;
val name' = Thm.def_binding_optional b name;
@@ -342,7 +342,7 @@
fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
else if not (null overloading) then Overloading.init overloading
- else if not is_locale then ProofContext.init
+ else if not is_locale then ProofContext.init_global
else if not is_class then Locale.init target
else Class_Target.init target;
@@ -364,7 +364,7 @@
fun gen_overloading prep_const raw_ops thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val ops = raw_ops |> map (fn (name, const, checked) =>
(name, Term.dest_Const (prep_const ctxt const), checked));
in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
--- a/src/Pure/Proof/extraction.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Proof/extraction.ML Tue May 04 13:11:15 2010 -0700
@@ -136,8 +136,7 @@
| strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
| strip_abs _ _ = error "strip_abs: not an abstraction";
-fun prf_subst_TVars tye =
- map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
+val prf_subst_TVars = map_proof_types o typ_subst_TVars;
fun relevant_vars types prop = List.foldr (fn
(Var ((a, _), T), vs) => (case strip_type T of
--- a/src/Pure/Proof/proof_syntax.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Proof/proof_syntax.ML Tue May 04 13:11:15 2010 -0700
@@ -206,7 +206,7 @@
|> add_proof_syntax
|> add_proof_atom_consts
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
- |> ProofContext.init
+ |> ProofContext.init_global
|> ProofContext.allow_dummies
|> ProofContext.set_mode ProofContext.mode_schematic;
in
--- a/src/Pure/Proof/reconstruct.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Proof/reconstruct.ML Tue May 04 13:11:15 2010 -0700
@@ -376,8 +376,7 @@
val varify = map_type_tfree (fn p as (a, S) =>
if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
in
- (maxidx', prfs', map_proof_terms (subst_TVars tye o
- map_types varify) (typ_subst_TVars tye o varify) prf)
+ (maxidx', prfs', map_proof_types (typ_subst_TVars tye o varify) prf)
end
| expand maxidx prfs prf = (maxidx, prfs, prf);
--- a/src/Pure/Syntax/syntax.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/Syntax/syntax.ML Tue May 04 13:11:15 2010 -0700
@@ -850,10 +850,10 @@
val read_term = singleton o read_terms;
val read_prop = singleton o read_props;
-val read_sort_global = read_sort o ProofContext.init;
-val read_typ_global = read_typ o ProofContext.init;
-val read_term_global = read_term o ProofContext.init;
-val read_prop_global = read_prop o ProofContext.init;
+val read_sort_global = read_sort o ProofContext.init_global;
+val read_typ_global = read_typ o ProofContext.init_global;
+val read_term_global = read_term o ProofContext.init_global;
+val read_prop_global = read_prop o ProofContext.init_global;
(* pretty = uncheck + unparse *)
@@ -876,7 +876,7 @@
structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
val is_pretty_global = PrettyGlobal.get;
val set_pretty_global = PrettyGlobal.put;
-val init_pretty_global = set_pretty_global true o ProofContext.init;
+val init_pretty_global = set_pretty_global true o ProofContext.init_global;
val pretty_term_global = pretty_term o init_pretty_global;
val pretty_typ_global = pretty_typ o init_pretty_global;
--- a/src/Pure/axclass.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/axclass.ML Tue May 04 13:11:15 2010 -0700
@@ -198,7 +198,7 @@
(case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
SOME thm => Thm.transfer thy thm
| NONE => error ("Unproven class relation " ^
- Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
+ Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));
fun put_trancl_classrel ((c1, c2), th) thy =
let
@@ -245,7 +245,7 @@
(case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
SOME (thm, _) => Thm.transfer thy thm
| NONE => error ("Unproven type arity " ^
- Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
+ Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));
fun thynames_of_arity thy (c, a) =
Symtab.lookup_list (proven_arities_of thy) a
@@ -357,7 +357,7 @@
in (c1, c2) end;
fun read_classrel thy raw_rel =
- cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
+ cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init_global thy)) raw_rel)
handle TYPE (msg, _, _) => error msg;
@@ -461,7 +461,7 @@
fun prove_classrel raw_rel tac thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val (c1, c2) = cert_classrel thy raw_rel;
val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
@@ -475,7 +475,7 @@
fun prove_arity raw_arity tac thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val arity = ProofContext.cert_arity ctxt raw_arity;
val names = map (prefix arity_prefix) (Logic.name_arities arity);
val props = Logic.mk_arities arity;
@@ -509,7 +509,7 @@
fun define_class (bclass, raw_super) raw_params raw_specs thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val pp = Syntax.pp ctxt;
@@ -623,7 +623,7 @@
(map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
fun ax_arity prep =
- axiomatize (prep o ProofContext.init) Logic.mk_arities
+ axiomatize (prep o ProofContext.init_global) Logic.mk_arities
(map (prefix arity_prefix) o Logic.name_arities) add_arity;
fun class_const c =
@@ -643,7 +643,7 @@
in
val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel;
+val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init_global) read_classrel;
val axiomatize_classrel = ax_classrel cert_classrel;
val axiomatize_classrel_cmd = ax_classrel read_classrel;
val axiomatize_arity = ax_arity ProofContext.cert_arity;
--- a/src/Pure/codegen.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/codegen.ML Tue May 04 13:11:15 2010 -0700
@@ -822,7 +822,7 @@
val generate_code_i = gen_generate_code Sign.cert_term;
val generate_code =
- gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init);
+ gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init_global);
(**** Reflection ****)
@@ -908,7 +908,7 @@
fun eval_term thy t =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val e =
let
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
--- a/src/Pure/context.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/context.ML Tue May 04 13:11:15 2010 -0700
@@ -20,7 +20,7 @@
structure ProofContext:
sig
val theory_of: Proof.context -> theory
- val init: theory -> Proof.context
+ val init_global: theory -> Proof.context
end
end;
@@ -481,7 +481,7 @@
structure ProofContext =
struct
val theory_of = theory_of_proof;
- fun init thy = Proof.Context (init_data thy, check_thy thy);
+ fun init_global thy = Proof.Context (init_data thy, check_thy thy);
end;
structure Proof_Data =
@@ -529,7 +529,7 @@
fun proof_map f = the_proof o f o Proof;
val theory_of = cases I ProofContext.theory_of;
-val proof_of = cases ProofContext.init I;
+val proof_of = cases ProofContext.init_global I;
--- a/src/Pure/drule.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/drule.ML Tue May 04 13:11:15 2010 -0700
@@ -307,7 +307,7 @@
Similar code in type/freeze_thaw*)
fun legacy_freeze_thaw_robust th =
- let val fth = Thm.freezeT th
+ let val fth = Thm.legacy_freezeT th
val thy = Thm.theory_of_thm fth
val {prop, tpairs, ...} = rep_thm fth
in
@@ -329,7 +329,7 @@
(*Basic version of the function above. No option to rename Vars apart in thaw.
The Frees created from Vars have nice names.*)
fun legacy_freeze_thaw th =
- let val fth = Thm.freezeT th
+ let val fth = Thm.legacy_freezeT th
val thy = Thm.theory_of_thm fth
val {prop, tpairs, ...} = rep_thm fth
in
--- a/src/Pure/goal.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/goal.ML Tue May 04 13:11:15 2010 -0700
@@ -137,7 +137,8 @@
Thm.adjust_maxidx_thm ~1 #>
Drule.implies_intr_list assms #>
Drule.forall_intr_list fixes #>
- Thm.generalize (map #1 tfrees, []) 0);
+ Thm.generalize (map #1 tfrees, []) 0 #>
+ Thm.strip_shyps);
val local_result =
Thm.future global_result global_prop
|> Thm.instantiate (instT, [])
@@ -211,7 +212,7 @@
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
fun prove_global thy xs asms prop tac =
- Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
+ Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
--- a/src/Pure/meta_simplifier.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/meta_simplifier.ML Tue May 04 13:11:15 2010 -0700
@@ -299,7 +299,7 @@
in
fun print_term_global ss warn a thy t =
- print_term ss warn (K a) t (ProofContext.init thy);
+ print_term ss warn (K a) t (ProofContext.init_global thy);
fun if_enabled (Simpset ({context, ...}, _)) flag f =
(case context of
@@ -355,7 +355,7 @@
fun context ctxt =
map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
-val global_context = context o ProofContext.init;
+val global_context = context o ProofContext.init_global;
fun activate_context thy ss =
let
--- a/src/Pure/old_goals.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/old_goals.ML Tue May 04 13:11:15 2010 -0700
@@ -219,7 +219,7 @@
fun simple_read_term thy T s =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
|> ProofContext.allow_dummies
|> ProofContext.set_mode ProofContext.mode_schematic;
val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
--- a/src/Pure/proofterm.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/proofterm.ML Tue May 04 13:11:15 2010 -0700
@@ -58,8 +58,10 @@
val strip_combt: proof -> proof * term option list
val strip_combP: proof -> proof * proof list
val strip_thm: proof_body -> proof_body
- val map_proof_terms_option: (term -> term option) -> (typ -> typ option) -> proof -> proof
+ val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
+ val map_proof_types_same: typ Same.operation -> proof Same.operation
val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
+ val map_proof_types: (typ -> typ) -> proof -> proof
val fold_proof_terms: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
val maxidx_proof: proof -> int -> int
val size_of_proof: proof -> int
@@ -80,7 +82,7 @@
val implies_intr_proof: term -> proof -> proof
val forall_intr_proof: term -> string -> proof -> proof
val varify_proof: term -> (string * sort) list -> proof -> proof
- val freezeT: term -> proof -> proof
+ val legacy_freezeT: term -> proof -> proof
val rotate_proof: term list -> term -> int -> proof -> proof
val permute_prems_prf: term list -> int -> int -> proof -> proof
val generalize: string list * string list -> int -> proof -> proof
@@ -106,6 +108,8 @@
val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof
val equal_intr: term -> term -> proof -> proof -> proof
val equal_elim: term -> term -> proof -> proof -> proof
+ val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
+ sort list -> proof -> proof
val axm_proof: string -> term -> proof
val oracle_proof: string -> term -> oracle * proof
val promise_proof: theory -> serial -> term -> proof
@@ -273,10 +277,8 @@
val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
-fun map_proof_terms_option f g =
+fun map_proof_same term typ ofclass =
let
- val term = Same.function f;
- val typ = Same.function g;
val typs = Same.map typ;
fun proof (Abst (s, T, prf)) =
@@ -292,22 +294,23 @@
(proof prf1 %% Same.commit proof prf2
handle Same.SAME => prf1 %% proof prf2)
| proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
- | proof (OfClass (T, c)) = OfClass (typ T, c)
+ | proof (OfClass T_c) = ofclass T_c
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
| proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
| proof (PThm (i, ((a, prop, SOME Ts), body))) =
PThm (i, ((a, prop, SOME (typs Ts)), body))
| proof _ = raise Same.SAME;
- in Same.commit proof end;
+ in proof end;
+
+fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c));
+fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
fun same eq f x =
let val x' = f x
in if eq (x, x') then raise Same.SAME else x' end;
-fun map_proof_terms f g =
- map_proof_terms_option
- (fn t => SOME (same (op =) f t) handle Same.SAME => NONE)
- (fn T => SOME (same (op =) g T) handle Same.SAME => NONE);
+fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g));
+fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f));
fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
| fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
@@ -652,7 +655,7 @@
in
-fun freezeT t prf =
+fun legacy_freezeT t prf =
let
val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
@@ -696,17 +699,17 @@
(***** generalization *****)
fun generalize (tfrees, frees) idx =
- map_proof_terms_option
- (Term_Subst.generalize_option (tfrees, frees) idx)
- (Term_Subst.generalizeT_option tfrees idx);
+ Same.commit (map_proof_terms_same
+ (Term_Subst.generalize_same (tfrees, frees) idx)
+ (Term_Subst.generalizeT_same tfrees idx));
(***** instantiation *****)
fun instantiate (instT, inst) =
- map_proof_terms_option
- (Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst))
- (Term_Subst.instantiateT_option instT);
+ Same.commit (map_proof_terms_same
+ (Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst))
+ (Term_Subst.instantiateT_same instT));
(***** lifting *****)
@@ -757,9 +760,8 @@
end;
fun incr_indexes i =
- map_proof_terms_option
- (Same.capture (Logic.incr_indexes_same ([], i)))
- (Same.capture (Logic.incr_tvar_same i));
+ Same.commit (map_proof_terms_same
+ (Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i));
(***** proof by assumption *****)
@@ -884,6 +886,22 @@
equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
+(**** sort hypotheses ****)
+
+fun strip_shyps_proof algebra present witnessed extra_sorts prf =
+ let
+ fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
+ val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts;
+ val replacements = present @ extra @ witnessed;
+ fun replace T =
+ if exists (fn (T', _) => T' = T) present then raise Same.SAME
+ else
+ (case get_first (get (Type.sort_of_atyp T)) replacements of
+ SOME T' => T'
+ | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term");
+ in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
+
+
(***** axioms and theorems *****)
val proofs = Unsynchronized.ref 2;
--- a/src/Pure/sign.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/sign.ML Tue May 04 13:11:15 2010 -0700
@@ -361,7 +361,7 @@
fun gen_syntax change_gram parse_typ mode args thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
@@ -398,7 +398,7 @@
fun gen_add_consts parse_typ raw_args thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global 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
@@ -497,7 +497,7 @@
fun gen_trrules f args thy = thy |> map_syn (fn syn =>
let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
- in f (ProofContext.init thy) (is_logtype thy) syn rules syn end);
+ in f (ProofContext.init_global thy) (is_logtype thy) syn rules syn end);
val add_trrules = gen_trrules Syntax.update_trrules;
val del_trrules = gen_trrules Syntax.remove_trrules;
--- a/src/Pure/simplifier.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/simplifier.ML Tue May 04 13:11:15 2010 -0700
@@ -127,7 +127,7 @@
fun map_simpset f = Context.theory_map (map_ss f);
fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
fun global_simpset_of thy =
- MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
+ MetaSimplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy));
fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
--- a/src/Pure/term_subst.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/term_subst.ML Tue May 04 13:11:15 2010 -0700
@@ -13,6 +13,8 @@
val map_atyps_option: (typ -> typ option) -> term -> term option
val map_types_option: (typ -> typ option) -> term -> term option
val map_aterms_option: (term -> term option) -> term -> term option
+ val generalizeT_same: string list -> int -> typ Same.operation
+ val generalize_same: string list * string list -> int -> term Same.operation
val generalize: string list * string list -> int -> term -> term
val generalizeT: string list -> int -> typ -> typ
val generalize_option: string list * string list -> int -> term -> term option
@@ -21,12 +23,12 @@
val instantiate_maxidx:
((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
term -> int -> term * int
+ val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
term -> term
- val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
- val instantiate_option: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
- term -> term option
- val instantiateT_option: ((indexname * sort) * typ) list -> typ -> typ option
+ val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
+ val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
+ term Same.operation
val zero_var_indexes: term -> term
val zero_var_indexes_inst: term list ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list
@@ -70,8 +72,6 @@
(* generalization of fixed variables *)
-local
-
fun generalizeT_same [] _ _ = raise Same.SAME
| generalizeT_same tfrees idx ty =
let
@@ -99,16 +99,12 @@
| gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u);
in gen tm end;
-in
-
-fun generalize names i tm = generalize_same names i tm handle Same.SAME => tm;
-fun generalizeT names i ty = generalizeT_same names i ty handle Same.SAME => ty;
+fun generalize names i tm = Same.commit (generalize_same names i) tm;
+fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty;
fun generalize_option names i tm = SOME (generalize_same names i tm) handle Same.SAME => NONE;
fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle Same.SAME => NONE;
-end;
-
(* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
@@ -118,7 +114,7 @@
fun no_indexes1 inst = map no_index inst;
fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
-fun instantiateT_same maxidx instT ty =
+fun instT_same maxidx instT ty =
let
fun maxify i = if i > ! maxidx then maxidx := i else ();
@@ -134,11 +130,11 @@
| subst_typs [] = raise Same.SAME;
in subst_typ ty end;
-fun instantiate_same maxidx (instT, inst) tm =
+fun inst_same maxidx (instT, inst) tm =
let
fun maxify i = if i > ! maxidx then maxidx := i else ();
- val substT = instantiateT_same maxidx instT;
+ val substT = instT_same maxidx instT;
fun subst (Const (c, T)) = Const (c, substT T)
| subst (Free (x, T)) = Free (x, substT T)
| subst (Var ((x, i), T)) =
@@ -158,31 +154,23 @@
fun instantiateT_maxidx instT ty i =
let val maxidx = Unsynchronized.ref i
- in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
+ in (Same.commit (instT_same maxidx instT) ty, ! maxidx) end;
fun instantiate_maxidx insts tm i =
let val maxidx = Unsynchronized.ref i
- in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
+ in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
fun instantiateT [] ty = ty
- | instantiateT instT ty =
- (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
- handle Same.SAME => ty);
+ | instantiateT instT ty = Same.commit (instT_same (Unsynchronized.ref ~1) (no_indexes1 instT)) ty;
fun instantiate ([], []) tm = tm
- | instantiate insts tm =
- (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
- handle Same.SAME => tm);
+ | instantiate insts tm = Same.commit (inst_same (Unsynchronized.ref ~1) (no_indexes2 insts)) tm;
-fun instantiateT_option [] _ = NONE
- | instantiateT_option instT ty =
- (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
- handle Same.SAME => NONE);
+fun instantiateT_same [] _ = raise Same.SAME
+ | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty;
-fun instantiate_option ([], []) _ = NONE
- | instantiate_option insts tm =
- (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
- handle Same.SAME => NONE);
+fun instantiate_same ([], []) _ = raise Same.SAME
+ | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm;
end;
--- a/src/Pure/theory.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/theory.ML Tue May 04 13:11:15 2010 -0700
@@ -238,7 +238,7 @@
fun check_def thy unchecked overloaded (b, tm) defs =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val name = Sign.full_name thy b;
val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
handle TERM (msg, _) => error msg;
--- a/src/Pure/thm.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/thm.ML Tue May 04 13:11:15 2010 -0700
@@ -69,7 +69,6 @@
val weaken: cterm -> thm -> thm
val weaken_sorts: sort list -> cterm -> cterm
val extra_shyps: thm -> sort list
- val strip_shyps: thm -> thm
(*meta rules*)
val assume: cterm -> thm
@@ -138,9 +137,10 @@
val varifyT_global: thm -> thm
val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val of_class: ctyp * class -> thm
+ val strip_shyps: thm -> thm
val unconstrainT: ctyp -> thm -> thm
val unconstrain_allTs: thm -> thm
- val freezeT: thm -> thm
+ val legacy_freezeT: thm -> thm
val assumption: int -> thm -> thm Seq.seq
val eq_assumption: int -> thm -> thm
val rotate_rule: int -> int -> thm -> thm
@@ -476,26 +476,6 @@
val sorts' = Sorts.union sorts more_sorts;
in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
-
-
-(** sort contexts of theorems **)
-
-(*remove extra sorts that are witnessed by type signature information*)
-fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
- | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
- let
- val thy = Theory.deref thy_ref;
- val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
- val extra = fold (Sorts.remove_sort o #2) present shyps;
- val witnessed = Sign.witness_sorts thy present extra;
- val extra' = fold (Sorts.remove_sort o #2) witnessed extra
- |> Sorts.minimal_sorts (Sign.classes_of thy);
- val shyps' = fold (Sorts.insert_sort o #2) present extra';
- in
- Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
- shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
- end;
-
(*dangling sort constraints of a thm*)
fun extra_shyps (th as Thm (_, {shyps, ...})) =
Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
@@ -532,6 +512,9 @@
fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
+fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
+ make_deriv promises oracles thms (f proof);
+
(* fulfilled proofs *)
@@ -565,14 +548,13 @@
(* future rule *)
-fun future_result i orig_thy orig_shyps orig_prop raw_thm =
+fun future_result i orig_thy orig_shyps orig_prop thm =
let
+ fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
+ val Thm (Deriv {promises, ...}, {thy_ref, shyps, hyps, tpairs, prop, ...}) = thm;
+
+ val _ = Theory.eq_thy (Theory.deref thy_ref, orig_thy) orelse err "bad theory";
val _ = Theory.check_thy orig_thy;
- val thm = strip_shyps (transfer orig_thy raw_thm);
- val _ = Theory.check_thy orig_thy;
- fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
-
- val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
val _ = prop aconv orig_prop orelse err "bad prop";
val _ = null tpairs orelse err "bad tpairs";
val _ = null hyps orelse err "bad hyps";
@@ -1220,6 +1202,25 @@
else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
end;
+(*Remove extra sorts that are witnessed by type signature information*)
+fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
+ | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
+ let
+ val thy = Theory.deref thy_ref;
+ val algebra = Sign.classes_of thy;
+
+ val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
+ val extra = fold (Sorts.remove_sort o #2) present shyps;
+ val witnessed = Sign.witness_sorts thy present extra;
+ val extra' = fold (Sorts.remove_sort o #2) witnessed extra
+ |> Sorts.minimal_sorts algebra;
+ val shyps' = fold (Sorts.insert_sort o #2) present extra';
+ in
+ Thm (deriv_rule_unconditional (Pt.strip_shyps_proof algebra present witnessed extra') der,
+ {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
+ shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
+ end;
+
(*Internalize sort constraints of type variable*)
fun unconstrainT
(Ctyp {thy_ref = thy_ref1, T, ...})
@@ -1266,14 +1267,14 @@
val varifyT_global = #2 o varifyT_global' [];
-(* Replace all TVars by new TFrees *)
-fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
+(* Replace all TVars by TFrees that are often new *)
+fun legacy_freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
let
val prop1 = attach_tpairs tpairs prop;
val prop2 = Type.legacy_freeze prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
in
- Thm (deriv_rule1 (Pt.freezeT prop1) der,
+ Thm (deriv_rule1 (Pt.legacy_freezeT prop1) der,
{thy_ref = thy_ref,
tags = [],
maxidx = maxidx_of_term prop2,
--- a/src/Pure/type.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/type.ML Tue May 04 13:11:15 2010 -0700
@@ -53,6 +53,7 @@
val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
(*special treatment of type vars*)
+ val sort_of_atyp: typ -> sort
val strip_sorts: typ -> typ
val no_tvars: typ -> typ
val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
@@ -271,6 +272,13 @@
(** special treatment of type vars **)
+(* sort_of_atyp *)
+
+fun sort_of_atyp (TFree (_, S)) = S
+ | sort_of_atyp (TVar (_, S)) = S
+ | sort_of_atyp T = raise TYPE ("sort_of_atyp", [T], []);
+
+
(* strip_sorts *)
fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts)
--- a/src/Pure/variable.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Pure/variable.ML Tue May 04 13:11:15 2010 -0700
@@ -235,7 +235,7 @@
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
val declare_thm = Thm.fold_terms declare_internal;
-fun global_thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
+fun global_thm_context th = declare_thm th (ProofContext.init_global (Thm.theory_of_thm th));
(* renaming term/type frees *)
@@ -376,9 +376,9 @@
val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
val tfrees = mk_tfrees [];
val idx = Proofterm.maxidx_proof prf ~1 + 1;
- val gen_term = Term_Subst.generalize_option (tfrees, frees) idx;
- val gen_typ = Term_Subst.generalizeT_option tfrees idx;
- in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
+ val gen_term = Term_Subst.generalize_same (tfrees, frees) idx;
+ val gen_typ = Term_Subst.generalizeT_same tfrees idx;
+ in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end;
fun gen_export (mk_tfrees, frees) ths =
--- a/src/Tools/Code/code_eval.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Tools/Code/code_eval.ML Tue May 04 13:11:15 2010 -0700
@@ -47,7 +47,7 @@
fun eval some_target reff postproc thy t args =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
fun evaluator naming program ((_, (_, ty)), t) deps =
let
val _ = if Code_Thingol.contains_dictvar t then
--- a/src/Tools/Code/code_preproc.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Tools/Code/code_preproc.ML Tue May 04 13:11:15 2010 -0700
@@ -87,7 +87,7 @@
fun add_unfold_post raw_thm thy =
let
- val thm = Local_Defs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
+ val thm = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) raw_thm;
val thm_sym = Thm.symmetric thm;
in
thy |> map_pre_post (fn (pre, post) =>
@@ -157,7 +157,7 @@
fun print_codeproc thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val pre = (#pre o the_thmproc) thy;
val post = (#post o the_thmproc) thy;
val functrans = (map fst o #functrans o the_thmproc) thy;
--- a/src/Tools/WWW_Find/find_theorems.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Tools/WWW_Find/find_theorems.ML Tue May 04 13:11:15 2010 -0700
@@ -210,7 +210,7 @@
fun do_find () =
let
- val ctxt = ProofContext.init (theory thy_name);
+ val ctxt = ProofContext.init_global (theory thy_name);
val query = get_query ();
val (othmslen, thms) = apsnd rev
(Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
--- a/src/Tools/nbe.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Tools/nbe.ML Tue May 04 13:11:15 2010 -0700
@@ -105,14 +105,14 @@
|> Drule.cterm_rule Thm.varifyT_global
|> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) =>
(((v, 0), sort), TFree (v, sort'))) vs, []))
- |> Drule.cterm_rule Thm.freezeT
+ |> Drule.cterm_rule Thm.legacy_freezeT
|> conv
|> Thm.varifyT_global
|> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
|> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
(((v, 0), []), TVar ((v, 0), sort))) vs, [])
|> strip_of_class
- |> Thm.freezeT
+ |> Thm.legacy_freezeT
end;
fun lift_triv_classes_rew thy rew t =
@@ -521,7 +521,7 @@
fun compile_eval thy program vs_t deps =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val (gr, (_, idx_tab)) =
Nbe_Functions.change thy (ensure_stmts ctxt program);
in
--- a/src/Tools/quickcheck.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/Tools/quickcheck.ML Tue May 04 13:11:15 2010 -0700
@@ -295,7 +295,7 @@
fun quickcheck_params_cmd args thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val f = fold (parse_test_param ctxt) args;
in
thy
--- a/src/ZF/Tools/datatype_package.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/ZF/Tools/datatype_package.ML Tue May 04 13:11:15 2010 -0700
@@ -401,7 +401,7 @@
fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
fun read_is strs =
map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
|> Syntax.check_terms ctxt;
--- a/src/ZF/Tools/ind_cases.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/ZF/Tools/ind_cases.ML Tue May 04 13:11:15 2010 -0700
@@ -46,7 +46,7 @@
fun inductive_cases args thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val facts = args |> map (fn ((name, srcs), props) =>
((name, map (Attrib.attribute thy) srcs),
map (Thm.no_attributes o single o smart_cases ctxt) props));
--- a/src/ZF/Tools/induct_tacs.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/ZF/Tools/induct_tacs.ML Tue May 04 13:11:15 2010 -0700
@@ -163,7 +163,7 @@
fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
--- a/src/ZF/Tools/inductive_package.ML Tue May 04 13:08:56 2010 -0700
+++ b/src/ZF/Tools/inductive_package.ML Tue May 04 13:11:15 2010 -0700
@@ -62,7 +62,7 @@
raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
let
val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
val (intr_names, intr_tms) = split_list (map fst intr_specs);
@@ -174,7 +174,7 @@
|> Sign.add_path big_rec_base_name
|> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
- val ctxt1 = ProofContext.init thy1;
+ val ctxt1 = ProofContext.init_global thy1;
(*fetch fp definitions from the theory*)
@@ -261,7 +261,7 @@
THEN (PRIMITIVE (fold_rule part_rec_defs));
(*Elimination*)
- val elim = rule_by_tactic (ProofContext.init thy1) basic_elim_tac
+ val elim = rule_by_tactic (ProofContext.init_global thy1) basic_elim_tac
(unfold RS Ind_Syntax.equals_CollectD)
(*Applies freeness of the given constructors, which *must* be unfolded by
@@ -554,7 +554,7 @@
fun add_inductive (srec_tms, sdom_sum) intr_srcs
(raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
#> Syntax.check_terms ctxt;