| author | wenzelm |
| Tue, 30 Jul 2013 15:09:25 +0200 | |
| changeset 52788 | da1fdbfebd39 |
| parent 52787 | c143ad7811fc |
| child 52789 | 44fd3add1348 |
--- a/NEWS Tue Jul 30 12:07:14 2013 +0200 +++ b/NEWS Tue Jul 30 15:09:25 2013 +0200 @@ -70,6 +70,12 @@ *** Pure *** +* Type theory is now immutable, without any special treatment of +drafts or linear updates (which could lead to "stale theory" errors in +the past). Discontinued obsolete operations like Theory.copy, +Theory.checkpoint, and the auxiliary type theory_ref. Minor +INCOMPATIBILITY. + * System option "proofs" has been discontinued. Instead the global state of Proofterm.proofs is persistently compiled into logic images as required, notably HOL-Proofs. Users no longer need to change
--- a/src/Doc/IsarImplementation/Integration.thy Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Doc/IsarImplementation/Integration.thy Tue Jul 30 15:09:25 2013 +0200 @@ -22,13 +22,7 @@ \medskip The toplevel maintains an implicit state, which is transformed by a sequence of transitions -- either interactively or - in batch-mode. In interactive mode, Isar state transitions are - encapsulated as safe transactions, such that both failure and undo - are handled conveniently without destroying the underlying draft - theory (cf.~\secref{sec:context-theory}). In batch mode, - transitions operate in a linear (destructive) fashion, such that - error conditions abort the present attempt to construct a theory or - proof altogether. + in batch-mode. The toplevel state is a disjoint sum of empty @{text toplevel}, or @{text theory}, or @{text proof}. On entering the main Isar loop we
--- a/src/Doc/IsarImplementation/Logic.thy Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Doc/IsarImplementation/Logic.thy Tue Jul 30 15:09:25 2013 +0200 @@ -718,8 +718,8 @@ \item Type @{ML_type thm} represents proven propositions. This is an abstract datatype that guarantees that its values have been constructed by basic principles of the @{ML_struct Thm} module. - Every @{ML_type thm} value contains a sliding back-reference to the - enclosing theory, cf.\ \secref{sec:context-theory}. + Every @{ML_type thm} value refers its background theory, + cf.\ \secref{sec:context-theory}. \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given theorem to a \emph{larger} theory, see also \secref{sec:context}.
--- a/src/Doc/IsarImplementation/Prelim.thy Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Doc/IsarImplementation/Prelim.thy Tue Jul 30 15:09:25 2013 +0200 @@ -80,24 +80,6 @@ ancestor theories. To this end, the system maintains a set of symbolic ``identification stamps'' within each theory. - In order to avoid the full-scale overhead of explicit sub-theory - identification of arbitrary intermediate stages, a theory is - switched into @{text "draft"} mode under certain circumstances. A - draft theory acts like a linear type, where updates invalidate - earlier versions. An invalidated draft is called \emph{stale}. - - The @{text "checkpoint"} operation produces a safe stepping stone - that will survive the next update without becoming stale: both the - old and the new theory remain valid and are related by the - sub-theory relation. Checkpointing essentially recovers purely - functional theory values, at the expense of some extra internal - bookkeeping. - - The @{text "copy"} operation produces an auxiliary version that has - the same data content, but is unrelated to the original: updates of - the copy do not affect the original, neither does the sub-theory - relation hold. - The @{text "merge"} operation produces the least upper bound of two theories, which actually degenerates into absorption of one theory into the other (according to the nominal sub-theory relation). @@ -110,10 +92,8 @@ \medskip The example in \figref{fig:ex-theory} below shows a theory graph derived from @{text "Pure"}, with theory @{text "Length"} importing @{text "Nat"} and @{text "List"}. The body of @{text - "Length"} consists of a sequence of updates, working mostly on - drafts internally, while transaction boundaries of Isar top-level - commands (\secref{sec:isar-toplevel}) are guaranteed to be safe - checkpoints. + "Length"} consists of a sequence of updates, resulting in locally a + linear sub-theory relation for each intermediate step. \begin{figure}[htb] \begin{center} @@ -125,56 +105,33 @@ @{text "Nat"} & & & & @{text "List"} \\ & $\searrow$ & & $\swarrow$ \\ & & @{text "Length"} \\ - & & \multicolumn{3}{l}{~~@{keyword "imports"}} \\ & & \multicolumn{3}{l}{~~@{keyword "begin"}} \\ & & $\vdots$~~ \\ - & & @{text "\<bullet>"}~~ \\ - & & $\vdots$~~ \\ - & & @{text "\<bullet>"}~~ \\ - & & $\vdots$~~ \\ & & \multicolumn{3}{l}{~~@{command "end"}} \\ \end{tabular} \caption{A theory definition depending on ancestors}\label{fig:ex-theory} \end{center} \end{figure} - \medskip There is a separate notion of \emph{theory reference} for - maintaining a live link to an evolving theory context: updates on - drafts are propagated automatically. Dynamic updating stops when - the next @{text "checkpoint"} is reached. - - Derived entities may store a theory reference in order to indicate - the formal context from which they are derived. This implicitly - assumes monotonic reasoning, because the referenced context may - become larger without further notice. -*} + \medskip Derived formal entities may retain a reference to the + background theory in order to indicate the formal context from which + they were produced. This provides an immutable certificate of the + background theory. *} text %mlref {* \begin{mldecls} @{index_ML_type theory} \\ @{index_ML Theory.eq_thy: "theory * theory -> bool"} \\ @{index_ML Theory.subthy: "theory * theory -> bool"} \\ - @{index_ML Theory.checkpoint: "theory -> theory"} \\ - @{index_ML Theory.copy: "theory -> theory"} \\ @{index_ML Theory.merge: "theory * theory -> theory"} \\ @{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\ @{index_ML Theory.parents_of: "theory -> theory list"} \\ @{index_ML Theory.ancestors_of: "theory -> theory list"} \\ \end{mldecls} - \begin{mldecls} - @{index_ML_type theory_ref} \\ - @{index_ML Theory.deref: "theory_ref -> theory"} \\ - @{index_ML Theory.check_thy: "theory -> theory_ref"} \\ - \end{mldecls} \begin{description} - \item Type @{ML_type theory} represents theory contexts. This is - essentially a linear type, with explicit runtime checking. - Primitive theory operations destroy the original version, which then - becomes ``stale''. This can be prevented by explicit checkpointing, - which the system does at least at the boundary of toplevel command - transactions \secref{sec:isar-toplevel}. + \item Type @{ML_type theory} represents theory contexts. \item @{ML "Theory.eq_thy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} check strict identity of two theories. @@ -185,18 +142,9 @@ (@{text "\<subseteq>"}) of the corresponding content (according to the semantics of the ML modules that implement the data). - \item @{ML "Theory.checkpoint"}~@{text "thy"} produces a safe - stepping stone in the linear development of @{text "thy"}. This - changes the old theory, but the next update will result in two - related, valid theories. - - \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text - "thy"} with the same data. The copy is not related to the original, - but the original is unchanged. - \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} absorbs one theory - into the other, without changing @{text "thy\<^sub>1"} or @{text "thy\<^sub>2"}. - This version of ad-hoc theory merge fails for unrelated theories! + into the other. This version of ad-hoc theory merge fails for + unrelated theories! \item @{ML "Theory.begin_theory"}~@{text "name parents"} constructs a new theory based on the given parents. This ML function is @@ -208,18 +156,6 @@ \item @{ML "Theory.ancestors_of"}~@{text "thy"} returns all ancestors of @{text thy} (not including @{text thy} itself). - \item Type @{ML_type theory_ref} represents a sliding reference to - an always valid theory; updates on the original are propagated - automatically. - - \item @{ML "Theory.deref"}~@{text "thy_ref"} turns a @{ML_type - "theory_ref"} into an @{ML_type "theory"} value. As the referenced - theory evolves monotonically over time, later invocations of @{ML - "Theory.deref"} may refer to a larger context. - - \item @{ML "Theory.check_thy"}~@{text "thy"} produces a @{ML_type - "theory_ref"} from a valid @{ML_type "theory"} value. - \end{description} *} @@ -254,13 +190,11 @@ subsection {* Proof context \label{sec:context-proof} *} -text {* A proof context is a container for pure data with a - back-reference to the theory from which it is derived. The @{text - "init"} operation creates a proof context from a given theory. - Modifications to draft theories are propagated to the proof context - as usual, but there is also an explicit @{text "transfer"} operation - to force resynchronization with more substantial updates to the - underlying theory. +text {* A proof context is a container for pure data that refers to + the theory from which it is derived. The @{text "init"} operation + creates a proof context from a given theory. There is an explicit + @{text "transfer"} operation to force resynchronization with updates + to the background theory -- this is rarely required in practice. Entities derived in a proof context need to record logical requirements explicitly, since there is no separate context @@ -293,15 +227,12 @@ \begin{description} \item Type @{ML_type Proof.context} represents proof contexts. - Elements of this type are essentially pure values, with a sliding - reference to the background theory. - \item @{ML Proof_Context.init_global}~@{text "thy"} produces a proof context - derived from @{text "thy"}, initializing all data. + \item @{ML Proof_Context.init_global}~@{text "thy"} produces a proof + context derived from @{text "thy"}, initializing all data. \item @{ML Proof_Context.theory_of}~@{text "ctxt"} selects the - background theory from @{text "ctxt"}, dereferencing its internal - @{ML_type theory_ref}. + background theory from @{text "ctxt"}. \item @{ML Proof_Context.transfer}~@{text "thy ctxt"} promotes the background theory of @{text "ctxt"} to the super theory @{text
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Jul 30 15:09:25 2013 +0200 @@ -995,7 +995,7 @@ Sign.add_type no_defs_lthy (type_binding_of spec, length (type_args_named_constrained_of spec), mixfix_of spec); - val fake_thy = Theory.copy #> fold add_fake_type specs; + val fake_thy = fold add_fake_type specs; val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy; fun mk_fake_T b =
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Tue Jul 30 15:09:25 2013 +0200 @@ -68,7 +68,6 @@ (* this theory is used just for parsing and error checking *) val tmp_thy = thy - |> Theory.copy |> fold (add_arity o thy_arity) dtnvs val dbinds : binding list =
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Jul 30 15:09:25 2013 +0200 @@ -408,7 +408,6 @@ (* this theory is used just for parsing *) val tmp_thy = thy |> - Theory.copy |> Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) => (tbind, length tvs, mx)) doms_raw)
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Tue Jul 30 15:09:25 2013 +0200 @@ -169,10 +169,10 @@ fun default_naming i = "v_" ^ string_of_int i datatype computer = Computer of - (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) + (theory * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) option Unsynchronized.ref -fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy +fun theory_of (Computer (Unsynchronized.ref (SOME (thy,_,_,_,_,_,_)))) = thy fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable) fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable @@ -304,7 +304,7 @@ val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable - in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end + in (thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end fun make_with_cache machine thy cache_patterns raw_thms = Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms))) @@ -388,7 +388,7 @@ datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int | Prem of AbstractMachine.term -datatype theorem = Theorem of theory_ref * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table +datatype theorem = Theorem of theory * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table * prem list * AbstractMachine.term * term list * sort list @@ -446,13 +446,12 @@ val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop) val _ = set_encoding computer encoding in - Theorem (Theory.check_thy (theory_of_thm th), stamp_of computer, vartab, varsubst, + Theorem (theory_of_thm th, stamp_of computer, vartab, varsubst, prems, concl, hyps, shyps) end -fun theory_of_theorem (Theorem (rthy,_,_,_,_,_,_,_)) = Theory.deref rthy -fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) = - Theorem (Theory.check_thy thy,p0,p1,p2,p3,p4,p5,p6) +fun theory_of_theorem (Theorem (thy,_,_,_,_,_,_,_)) = thy +fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) = Theorem (thy,p0,p1,p2,p3,p4,p5,p6) fun stamp_of_theorem (Theorem (_,s, _, _, _, _, _, _)) = s fun vartab_of_theorem (Theorem (_,_,vt,_,_,_,_,_)) = vt fun varsubst_of_theorem (Theorem (_,_,_,vs,_,_,_,_)) = vs
--- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Tue Jul 30 15:09:25 2013 +0200 @@ -233,7 +233,7 @@ datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list datatype pcomputer = - PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref * + PComputer of theory * Compute.computer * theorem list Unsynchronized.ref * pattern list Unsynchronized.ref (*fun collect_consts (Var x) = [] @@ -410,14 +410,13 @@ val (_, (pats, ths)) = add_monos thy monocs pats ths val computer = create_computer machine thy pats ths in - PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats) + PComputer (thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats) end fun make machine thy ths cs = make_with_cache machine thy [] ths cs -fun add_instances (PComputer (thyref, computer, rths, rpats)) cs = +fun add_instances (PComputer (thy, computer, rths, rpats)) cs = let - val thy = Theory.deref thyref val (changed, (pats, ths)) = add_monos thy cs (!rpats) (!rths) in if changed then
--- a/src/HOL/Nominal/nominal_datatype.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Tue Jul 30 15:09:25 2013 +0200 @@ -198,8 +198,7 @@ val new_type_names' = map (fn n => n ^ "_Rep") new_type_names; - val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy - ||> Theory.checkpoint; + val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy; val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names'); fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype.DtRec i); @@ -256,8 +255,7 @@ Primrec.add_primrec_overloaded (map (fn (s, sT) => (s, sT, false)) (List.take (perm_names' ~~ perm_names_types, length new_type_names))) - (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1 - ||> Theory.checkpoint; + (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1; (**** prove that permutation functions introduced by unfolding are ****) (**** equivalent to already existing permutation functions ****) @@ -429,7 +427,6 @@ (s, map (inter_sort thy sort o snd) tvs, [cp_class]) (fn _ => Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy) (full_new_type_names' ~~ tyvars) thy - |> Theory.checkpoint end; val (perm_thmss,thy3) = thy2 |> @@ -454,8 +451,7 @@ ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"), perm_append_thms), [Simplifier.simp_add]), ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"), - perm_eq_thms), [Simplifier.simp_add])] ||> - Theory.checkpoint; + perm_eq_thms), [Simplifier.simp_add])]; (**** Define representing sets ****) @@ -535,8 +531,7 @@ (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn)) (rep_set_names' ~~ recTs')) [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] - ||> Sign.restore_naming thy3 - ||> Theory.checkpoint; + ||> Sign.restore_naming thy3; (**** Prove that representing set is closed under permutation ****) @@ -598,8 +593,7 @@ (Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $ Free ("x", T))))), [])] thy) end)) - (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names)) - ||> Theory.checkpoint; + (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names)); val perm_defs = map snd typedefs; val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs; @@ -628,7 +622,6 @@ [Rep RS perm_closed RS Abs_inverse]) 1, asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy - |> Theory.checkpoint end) (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms); @@ -667,7 +660,7 @@ val thy7 = fold (fn x => fn thy => thy |> pt_instance x |> fold (cp_instance x) (atoms ~~ perm_closed_thmss)) - (atoms ~~ perm_closed_thmss) thy6 |> Theory.checkpoint; + (atoms ~~ perm_closed_thmss) thy6; (**** constructors ****) @@ -767,8 +760,7 @@ val def_name = (Long_Name.base_name cname) ^ "_def"; val ([def_thm], thy') = thy |> Sign.add_consts_i [(cname', constrT, mx)] |> - (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] ||> - Theory.checkpoint; + (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]; in (thy', defs @ [def_thm], eqns @ [eqn]) end; fun dt_constr_defs ((((((_, (_, _, constrs)), @@ -782,7 +774,7 @@ val (thy', defs', eqns') = fold (make_constr_def tname T T') (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, []) in - (Theory.checkpoint (Sign.parent_path thy'), defs', eqns @ [eqns'], dist_lemmas @ [dist]) + (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) end; val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = fold dt_constr_defs @@ -1112,8 +1104,7 @@ in fold (fn Type (s, Ts) => Axclass.prove_arity (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class]) (fn _ => Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy - end) (atoms ~~ finite_supp_thms) ||> - Theory.checkpoint; + end) (atoms ~~ finite_supp_thms); (**** strong induction theorem ****) @@ -1395,8 +1386,7 @@ Sign.add_path big_name |> Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>> Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>> - Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])] ||> - Theory.checkpoint; + Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])]; (**** recursion combinator ****) @@ -1504,8 +1494,7 @@ (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct") - ||> Sign.restore_naming thy10 - ||> Theory.checkpoint; + ||> Sign.restore_naming thy10; (** equivariance **) @@ -2009,8 +1998,7 @@ (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T) (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T') (set $ Free ("x", T) $ Free ("y", T')))))) - (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) - ||> Theory.checkpoint; + (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)); (* prove characteristic equations for primrec combinators *) @@ -2051,9 +2039,7 @@ ((Binding.name "rec_unique", map Drule.export_without_context rec_unique_thms), []), ((Binding.name "recs", rec_thms), [])] ||> Sign.parent_path ||> - map_nominal_datatypes (fold Symtab.update dt_infos) ||> - Theory.checkpoint; - + map_nominal_datatypes (fold Symtab.update dt_infos); in thy13 end;
--- a/src/HOL/TPTP/atp_problem_import.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Tue Jul 30 15:09:25 2013 +0200 @@ -57,7 +57,7 @@ ||> List.partition (has_role TPTP_Syntax.Role_Definition) in (map get_prop conjs, pairself (map get_prop) defs_and_nondefs, - thy |> Theory.checkpoint |> Proof_Context.init_global) + thy |> Proof_Context.init_global) end
--- a/src/HOL/Tools/Datatype/datatype.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Tue Jul 30 15:09:25 2013 +0200 @@ -181,8 +181,7 @@ coind = false, no_elim = true, no_ind = false, skip_mono = true} (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] - ||> Sign.restore_naming thy1 - ||> Theory.checkpoint; + ||> Sign.restore_naming thy1; (********************************* typedef ********************************) @@ -349,7 +348,7 @@ Logic.mk_equals (Const (iso_name, T --> Univ_elT), list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos); val (def_thms, thy') = - apsnd Theory.checkpoint ((Global_Theory.add_defs false o map Thm.no_attributes) defs thy); + (Global_Theory.add_defs false o map Thm.no_attributes) defs thy; (* prove characteristic equations *) @@ -361,7 +360,7 @@ in (thy', char_thms' @ char_thms) end; val (thy5, iso_char_thms) = - apfst Theory.checkpoint (fold_rev make_iso_defs (tl descr) (Sign.add_path big_name thy4, [])); + fold_rev make_iso_defs (tl descr) (Sign.add_path big_name thy4, []); (* prove isomorphism properties *) @@ -647,9 +646,7 @@ thy6 |> Global_Theory.note_thmss "" [((Binding.qualify true big_name (Binding.name "induct"), [case_names_induct]), - [([dt_induct], [])])] - ||> Theory.checkpoint; - + [([dt_induct], [])])]; in ((constr_inject', distinct_thms', dt_induct'), thy7) end; @@ -690,7 +687,6 @@ fun prep_specs parse raw_specs thy = let val ctxt = thy - |> Theory.copy |> Sign.add_types_global (map (fn ((b, args, mx), _) => (b, length args, mx)) raw_specs) |> Proof_Context.init_global |> fold (fn ((_, args, _), _) => fold (fn (a, _) =>
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Jul 30 15:09:25 2013 +0200 @@ -97,8 +97,7 @@ fold_map (fn ((tname, atts), thms) => Global_Theory.note_thmss "" [((Binding.qualify true tname (Binding.name name), atts), [(thms, [])])] - #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss) - ##> Theory.checkpoint; + #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss); fun store_thmss name tnames = store_thmss_atts name tnames (replicate (length tnames) []); @@ -106,8 +105,7 @@ fold_map (fn ((tname, atts), thm) => Global_Theory.note_thmss "" [((Binding.qualify true tname (Binding.name name), atts), [([thm], [])])] - #-> (fn [(_, [res])] => pair res)) (tnames ~~ attss ~~ thms) - ##> Theory.checkpoint; + #-> (fn [(_, [res])] => pair res)) (tnames ~~ attss ~~ thms); fun store_thms name tnames = store_thms_atts name tnames (replicate (length tnames) []);
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Jul 30 15:09:25 2013 +0200 @@ -109,8 +109,7 @@ fun prefix tyco = Binding.qualify true (Long_Name.base_name tyco) o Binding.qualify true "eq" o Binding.name; fun add_eq_thms tyco = - Theory.checkpoint - #> `(fn thy => mk_eq_eqns thy tyco) + `(fn thy => mk_eq_eqns thy tyco) #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK [((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Tue Jul 30 15:09:25 2013 +0200 @@ -149,8 +149,7 @@ (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] - ||> Sign.restore_naming thy0 - ||> Theory.checkpoint; + ||> Sign.restore_naming thy0; (* prove uniqueness and termination of primrec combinators *) @@ -238,8 +237,7 @@ (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T') (set $ Free ("x", T) $ Free ("y", T'))))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) - ||> Sign.parent_path - ||> Theory.checkpoint; + ||> Sign.parent_path; (* prove characteristic equations for primrec combinators *) @@ -262,7 +260,6 @@ |> Global_Theory.note_thmss "" [((Binding.name "recs", [Nitpick_Simps.add]), [(rec_thms, [])])] ||> Sign.parent_path - ||> Theory.checkpoint |-> (fn thms => pair (reccomb_names, maps #2 thms)) end; @@ -325,8 +322,7 @@ |> (Global_Theory.add_defs false o map Thm.no_attributes) [def]; in (defs @ [def_thm], thy') end) - (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1) - ||> Theory.checkpoint; + (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1); val case_thms = (map o map) (fn t => @@ -479,9 +475,8 @@ in -fun derive_datatype_props config dt_names descr induct inject distinct thy1 = +fun derive_datatype_props config dt_names descr induct inject distinct thy2 = let - val thy2 = thy1 |> Theory.checkpoint; val flat_descr = flat descr; val new_type_names = map Long_Name.base_name dt_names; val _ =
--- a/src/HOL/Tools/Function/size.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/Function/size.ML Tue Jul 30 15:09:25 2013 +0200 @@ -231,7 +231,6 @@ thy |> Sign.root_path |> Sign.add_path prefix - |> Theory.checkpoint |> prove_size_thms info new_type_names |> Sign.restore_naming thy end;
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Jul 30 15:09:25 2013 +0200 @@ -941,7 +941,7 @@ val T = Sign.the_const_type (Proof_Context.theory_of ctxt) name val t = Const (name, T) val thy' = - Theory.copy (Proof_Context.theory_of ctxt) + Proof_Context.theory_of ctxt |> Predicate_Compile.preprocess preprocess_options t val ctxt' = Proof_Context.init_global thy' val _ = tracing "Generating prolog program..." @@ -1020,7 +1020,7 @@ let val t' = fold_rev absfree (Term.add_frees t []) t val options = code_options_of (Proof_Context.theory_of ctxt) - val thy = Theory.copy (Proof_Context.theory_of ctxt) + val thy = Proof_Context.theory_of ctxt val ((((full_constname, constT), vs'), intro), thy1) = Predicate_Compile_Aux.define_quickcheck_predicate t' thy val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Jul 30 15:09:25 2013 +0200 @@ -99,7 +99,6 @@ | NONE => ([], thy) else Predicate_Compile_Fun.define_predicates (get_specs funnames) thy else ([], thy)) - (*||> Theory.checkpoint*) val _ = print_specs options thy1 fun_pred_specs val specs = (get_specs prednames) @ fun_pred_specs val (intross3, thy2) = process_specification options specs thy1
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Jul 30 15:09:25 2013 +0200 @@ -1118,12 +1118,12 @@ val ctxt' = Proof_Context.init_global thy' val rules as ((intro, elim), _) = create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T)) - in thy' + in + thy' |> set_function_name Pred name mode mode_cname |> add_predfun_data name mode (definition, rules) |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd - |> Theory.checkpoint end; in thy |> defined_function_of Pred name |> fold create_definition modes @@ -1366,8 +1366,7 @@ val _ = print_step options "Defining executable functions..." val thy'' = cond_timeit (Config.get ctxt Quickcheck.timing) "Defining executable functions..." - (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy' - |> Theory.checkpoint) + (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy') val ctxt'' = Proof_Context.init_global thy'' val _ = print_step options "Compiling equations..." val compiled_terms = @@ -1388,7 +1387,7 @@ fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [attrib])] thy)) - result_thms' thy'' |> Theory.checkpoint) + result_thms' thy'') in thy''' end @@ -1397,7 +1396,7 @@ let fun dest_steps (Steps s) = s val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps))) - val thy' = extend_intro_graph names thy |> Theory.checkpoint; + val thy' = extend_intro_graph names thy; fun strong_conn_of gr keys = Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr) val scc = strong_conn_of (PredData.get thy') names @@ -1414,7 +1413,7 @@ add_equations_of steps mode_analysis_options options preds thy end else thy) - scc thy'' |> Theory.checkpoint + scc thy'' in thy''' end val add_equations = gen_add_equations
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Jul 30 15:09:25 2013 +0200 @@ -224,7 +224,7 @@ fun compile_term compilation options ctxt t = let val t' = fold_rev absfree (Term.add_frees t []) t - val thy = Theory.copy (Proof_Context.theory_of ctxt) + val thy = Proof_Context.theory_of ctxt val ((((full_constname, constT), vs'), intro), thy1) = Predicate_Compile_Aux.define_quickcheck_predicate t' thy val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 30 15:09:25 2013 +0200 @@ -298,7 +298,6 @@ (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss); val thy1' = thy1 |> - Theory.copy |> Sign.add_types_global (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |> Extraction.add_typeof_eqns_i ty_eqs;
--- a/src/HOL/Tools/record.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/HOL/Tools/record.ML Tue Jul 30 15:09:25 2013 +0200 @@ -1555,8 +1555,7 @@ val ([ext_def], defs_thy) = timeit_msg ctxt "record extension constructor def:" (fn () => typ_thy |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd - |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])] - ||> Theory.checkpoint); + |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]); (* prepare propositions *) @@ -2009,8 +2008,7 @@ map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs ||>> (Global_Theory.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) - [make_spec, fields_spec, extend_spec, truncate_spec] - ||> Theory.checkpoint); + [make_spec, fields_spec, extend_spec, truncate_spec]); (* prepare propositions *) val _ = timing_msg ctxt "record preparing propositions";
--- a/src/Pure/Isar/class.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Isar/class.ML Tue Jul 30 15:09:25 2013 +0200 @@ -566,7 +566,6 @@ | NONE => NONE); in thy - |> Theory.checkpoint |> Proof_Context.init_global |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params)) |> fold (Variable.declare_typ o TFree) vs
--- a/src/Pure/Isar/class_declaration.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Isar/class_declaration.ML Tue Jul 30 15:09:25 2013 +0200 @@ -314,7 +314,6 @@ |> Expression.add_locale I b (Binding.qualify true "class" b) supexpr elems |> snd |> Local_Theory.exit_global |> 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) #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
--- a/src/Pure/Isar/code.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Isar/code.ML Tue Jul 30 15:09:25 2013 +0200 @@ -276,11 +276,11 @@ local type data = Any.T Datatab.table; -fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option); +fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory) option); structure Code_Data = Theory_Data ( - type T = spec * (data * theory_ref) option Synchronized.var; + type T = spec * (data * theory) option Synchronized.var; val empty = (make_spec (false, (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ()); val extend : T -> T = apsnd (K (empty_dataref ())); @@ -320,7 +320,9 @@ #> map_history_concluded (K true)) |> SOME; -val _ = Context.>> (Context.map_theory (Theory.at_begin continue_history #> Theory.at_end conclude_history)); +val _ = + Context.>> (Context.map_theory + (Theory.at_begin continue_history #> Theory.at_end conclude_history)); (* access to data dependent on abstract executable code *) @@ -328,17 +330,18 @@ fun change_yield_data (kind, mk, dest) theory f = let val dataref = (snd o Code_Data.get) theory; - val (datatab, thy_ref) = case Synchronized.value dataref - of SOME (datatab, thy_ref) => if Theory.eq_thy (theory, Theory.deref thy_ref) - then (datatab, thy_ref) - else (Datatab.empty, Theory.check_thy theory) - | NONE => (Datatab.empty, Theory.check_thy theory) + val (datatab, thy) = case Synchronized.value dataref + of SOME (datatab, thy) => + if Theory.eq_thy (theory, thy) + then (datatab, thy) + else (Datatab.empty, theory) + | NONE => (Datatab.empty, theory) val data = case Datatab.lookup datatab kind of SOME data => data | NONE => invoke_init kind; val result as (_, data') = f (dest data); val _ = Synchronized.change dataref - ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref)); + ((K o SOME) (Datatab.update (kind, mk data') datatab, thy)); in result end; end; (*local*) @@ -1039,7 +1042,7 @@ let val thm = Thm.close_derivation raw_thm; val c = const_eqn thy thm; - fun update_subsume thy verbose (thm, proper) eqns = + fun update_subsume verbose (thm, proper) eqns = let val args_of = snd o take_prefix is_Var o rev o snd o strip_comb o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; @@ -1058,13 +1061,12 @@ Display.string_of_thm_global thy thm') else (); true) else false; in (thm, proper) :: filter_out drop eqns end; - fun natural_order thy_ref eqns = - (eqns, Lazy.lazy (fn () => fold (update_subsume (Theory.deref thy_ref) false) eqns [])) - fun add_eqn' true (Default (eqns, _)) = - Default (natural_order (Theory.check_thy thy) ((thm, proper) :: eqns)) + fun natural_order eqns = + (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns [])) + fun add_eqn' true (Default (eqns, _)) = Default (natural_order ((thm, proper) :: eqns)) (*this restores the natural order and drops syntactic redundancies*) | add_eqn' true fun_spec = fun_spec - | add_eqn' false (Eqns eqns) = Eqns (update_subsume thy true (thm, proper) eqns) + | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns) | add_eqn' false _ = Eqns [(thm, proper)]; in change_fun_spec false c (add_eqn' default) thy end; @@ -1152,7 +1154,6 @@ (K ((map o apsnd o apsnd) register_for_constructors)); in thy - |> Theory.checkpoint |> `(fn thy => case_cong thy case_const entry) |-> (fn cong => map_exec_purge (register_case cong #> register_type)) end;
--- a/src/Pure/Isar/element.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Isar/element.ML Tue Jul 30 15:09:25 2013 +0200 @@ -50,7 +50,6 @@ val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism val satisfy_morphism: witness list -> morphism val eq_morphism: theory -> thm list -> morphism option - val transfer_morphism: theory -> morphism val init: context_i -> Context.generic -> Context.generic val activate_i: context_i -> Proof.context -> context_i * Proof.context val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context @@ -392,13 +391,11 @@ in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end; fun instT_morphism thy env = - let val thy_ref = Theory.check_thy thy in - Morphism.morphism - {binding = [], - typ = [instT_type env], - term = [instT_term env], - fact = [map (fn th => instT_thm (Theory.deref thy_ref) env th)]} - end; + Morphism.morphism + {binding = [], + typ = [instT_type env], + term = [instT_term env], + fact = [map (fn th => instT_thm thy env th)]}; (* instantiate types and terms *) @@ -437,13 +434,11 @@ end; fun inst_morphism thy (envT, env) = - let val thy_ref = Theory.check_thy thy in - Morphism.morphism - {binding = [], - typ = [instT_type envT], - term = [inst_term (envT, env)], - fact = [map (fn th => inst_thm (Theory.deref thy_ref) (envT, env) th)]} - end; + Morphism.morphism + {binding = [], + typ = [instT_type envT], + term = [inst_term (envT, env)], + fact = [map (fn th => inst_thm thy (envT, env) th)]}; (* satisfy hypotheses *) @@ -468,13 +463,6 @@ fact = [map (rewrite_rule thms)]}); -(* transfer to theory using closure *) - -fun transfer_morphism thy = - let val thy_ref = Theory.check_thy thy - in Morphism.thm_morphism (fn th => Thm.transfer (Theory.deref thy_ref) th) end; - - (** activate in context **)
--- a/src/Pure/Isar/local_theory.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Isar/local_theory.ML Tue Jul 30 15:09:25 2013 +0200 @@ -205,15 +205,12 @@ fun raw_theory f = #2 o raw_theory_result (f #> pair ()); -val checkpoint = raw_theory Theory.checkpoint; - fun background_theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |> Sign.map_naming (K (naming_of lthy)) |> f - ||> Sign.restore_naming thy - ||> Theory.checkpoint); + ||> Sign.restore_naming thy); fun background_theory f = #2 o background_theory_result (f #> pair ()); @@ -256,11 +253,11 @@ fun operation2 f x y = operation (fn ops => f ops x y); val pretty = operation #pretty; -val abbrev = apsnd checkpoint ooo operation2 #abbrev; -val define = apsnd checkpoint oo operation2 #define false; -val define_internal = apsnd checkpoint oo operation2 #define true; -val notes_kind = apsnd checkpoint ooo operation2 #notes; -val declaration = checkpoint ooo operation2 #declaration; +val abbrev = operation2 #abbrev; +val define = operation2 #define false; +val define_internal = operation2 #define true; +val notes_kind = operation2 #notes; +val declaration = operation2 #declaration; (* basic derived operations *) @@ -322,13 +319,12 @@ fun init naming operations target = target |> Data.map (fn [] => [make_lthy (naming, operations, I, false, target)] - | _ => error "Local theory already initialized") - |> checkpoint; + | _ => error "Local theory already initialized"); (* exit *) -val exit = Proof_Context.background_theory Theory.checkpoint o operation #exit; +val exit = operation #exit; val exit_global = Proof_Context.theory_of o exit; fun exit_result f (x, lthy) =
--- a/src/Pure/Isar/locale.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Isar/locale.ML Tue Jul 30 15:09:25 2013 +0200 @@ -431,6 +431,8 @@ (** Public activation functions **) +fun transfer_morphism thy = Morphism.thm_morphism (Thm.transfer thy); + fun activate_declarations dep = Context.proof_map (fn context => let val thy = Context.theory_of context; @@ -443,14 +445,14 @@ let val thy = Context.theory_of context; val activate = - activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export; + activate_notes Element.init (transfer_morphism o Context.theory_of) context export; in roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context) |-> Idents.put end; fun init name thy = - activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of) + activate_all name thy Element.init (transfer_morphism o Context.theory_of) (empty_idents, Context.Proof (Proof_Context.init_global thy)) |-> Idents.put |> Context.proof_of; @@ -628,7 +630,7 @@ fun cons_elem (elem as Notes _) = show_facts ? cons elem | cons_elem elem = cons elem; val elems = - activate_all name thy cons_elem (K (Element.transfer_morphism thy)) (empty_idents, []) + activate_all name thy cons_elem (K (transfer_morphism thy)) (empty_idents, []) |> snd |> rev; in Pretty.block
--- a/src/Pure/Isar/overloading.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Isar/overloading.ML Tue Jul 30 15:09:25 2013 +0200 @@ -194,7 +194,6 @@ (Term.dest_Const (prep_const ctxt const), (v, checked))); in thy - |> Theory.checkpoint |> Proof_Context.init_global |> Data.put overloading |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
--- a/src/Pure/Isar/toplevel.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Isar/toplevel.ML Tue Jul 30 15:09:25 2013 +0200 @@ -269,7 +269,6 @@ val (result, err) = cont_node |> Runtime.controlled_execution f - |> map_theory Theory.checkpoint |> state_error NONE handle exn => state_error (SOME exn) cont_node; in @@ -298,8 +297,7 @@ local fun apply_tr _ (Init f) (State (NONE, _)) = - State (SOME (Theory (Context.Theory - (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE) + State (SOME (Theory (Context.Theory (Runtime.controlled_execution f ()), NONE)), NONE) | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) = exit_transaction state | apply_tr int (Keep f) state = @@ -421,7 +419,6 @@ (fn Theory (Context.Theory thy, _) => let val thy' = thy |> Sign.new_group - |> Theory.checkpoint |> f int |> Sign.reset_group; in Theory (Context.Theory thy', NONE) end @@ -529,9 +526,9 @@ fun theory_to_proof f = begin_proof (fn _ => fn gthy => - (Context.Theory o Theory.checkpoint o Sign.reset_group o Proof_Context.theory_of, + (Context.Theory o Sign.reset_group o Proof_Context.theory_of, (case gthy of - Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) + Context.Theory thy => f (Sign.new_group thy) | _ => raise UNDEF))); end;
--- a/src/Pure/Proof/extraction.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Jul 30 15:09:25 2013 +0200 @@ -35,8 +35,7 @@ val typ = Simple_Syntax.read_typ; val add_syntax = - Theory.copy - #> Sign.root_path + Sign.root_path #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)] #> Sign.add_consts_i [(Binding.name "typeof", typ "'b => Type", NoSyn),
--- a/src/Pure/Proof/proof_syntax.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Tue Jul 30 15:09:25 2013 +0200 @@ -41,7 +41,6 @@ fun add_proof_syntax thy = thy - |> Theory.copy |> Sign.root_path |> Sign.set_defsort [] |> Sign.add_types_global [(Binding.name "proof", 0, NoSyn)]
--- a/src/Pure/ROOT.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/ROOT.ML Tue Jul 30 15:09:25 2013 +0200 @@ -315,7 +315,6 @@ toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm"; toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp"; toplevel_pp ["Context", "theory"] "Context.pretty_thy"; -toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; toplevel_pp ["Ast", "ast"] "Ast.pretty_ast"; toplevel_pp ["Path", "T"] "Path.pretty";
--- a/src/Pure/Thy/thy_load.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Thy/thy_load.ML Tue Jul 30 15:09:25 2013 +0200 @@ -210,8 +210,7 @@ fun begin_theory master_dir {name, imports, keywords} parents = Theory.begin_theory name parents |> put_deps master_dir imports - |> fold Thy_Header.declare_keyword keywords - |> Theory.checkpoint; + |> fold Thy_Header.declare_keyword keywords; fun excursion last_timing init elements = let
--- a/src/Pure/Tools/find_theorems.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/Tools/find_theorems.ML Tue Jul 30 15:09:25 2013 +0200 @@ -315,8 +315,7 @@ let val thy' = Proof_Context.theory_of ctxt - |> Context_Position.set_visible_global (Context_Position.is_visible ctxt) - |> Theory.checkpoint; + |> Context_Position.set_visible_global (Context_Position.is_visible ctxt); val ctxt' = Proof_Context.transfer thy' ctxt; val goal' = Thm.transfer thy' goal;
--- a/src/Pure/axclass.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/axclass.ML Tue Jul 30 15:09:25 2013 +0200 @@ -320,7 +320,7 @@ let val string_of_sort = Syntax.string_of_sort_global thy; val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; - val _ = Sign.primitive_classrel (c1, c2) (Theory.copy thy); + val _ = Sign.primitive_classrel (c1, c2) thy; val _ = (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of [] => ()
--- a/src/Pure/context.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/context.ML Tue Jul 30 15:09:25 2013 +0200 @@ -14,7 +14,6 @@ signature BASIC_CONTEXT = sig type theory - type theory_ref exception THEORY of string * theory list structure Proof: sig type context end structure Proof_Context: @@ -42,13 +41,10 @@ val str_of_thy: theory -> string val get_theory: theory -> string -> theory val this_theory: theory -> string -> theory - val deref: theory_ref -> theory - val check_thy: theory -> theory_ref val eq_thy: theory * theory -> bool val subthy: theory * theory -> bool val joinable: theory * theory -> bool val merge: theory * theory -> theory - val merge_refs: theory_ref * theory_ref -> theory_ref val finish_thy: theory -> theory val begin_thy: (theory -> pretty) -> string -> theory list -> theory (*proof context*) @@ -229,14 +225,6 @@ else get_theory thy name; -(* theory references *) (* FIXME dummy *) - -datatype theory_ref = Theory_Ref of theory; - -fun deref (Theory_Ref thy) = thy; -fun check_thy thy = Theory_Ref thy; - - (* build ids *) fun insert_id id ids = Inttab.update (id, ()) ids; @@ -285,8 +273,6 @@ else error (cat_lines ["Attempt to perform non-trivial merge of theories:", str_of_thy thy1, str_of_thy thy2]); -fun merge_refs (ref1, ref2) = check_thy (merge (deref ref1, deref ref2)); - (** build theories **) @@ -379,12 +365,12 @@ structure Proof = struct - datatype context = Context of Any.T Datatab.table * theory_ref; + datatype context = Context of Any.T Datatab.table * theory; end; -fun theory_of_proof (Proof.Context (_, thy_ref)) = deref thy_ref; +fun theory_of_proof (Proof.Context (_, thy)) = thy; fun data_of_proof (Proof.Context (data, _)) = data; -fun map_prf f (Proof.Context (data, thy_ref)) = Proof.Context (f data, thy_ref); +fun map_prf f (Proof.Context (data, thy)) = Proof.Context (f data, thy); (* proof data kinds *) @@ -406,19 +392,16 @@ in -fun raw_transfer thy' (Proof.Context (data, thy_ref)) = +fun raw_transfer thy' (Proof.Context (data, thy)) = let - val thy = deref thy_ref; val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory"; - val _ = check_thy thy; val data' = init_new_data data thy'; - val thy_ref' = check_thy thy'; - in Proof.Context (data', thy_ref') end; + in Proof.Context (data', thy') end; structure Proof_Context = struct val theory_of = theory_of_proof; - fun init_global thy = Proof.Context (init_data thy, check_thy thy); + fun init_global thy = Proof.Context (init_data thy, thy); fun get_global thy name = init_global (get_theory thy name); end;
--- a/src/Pure/global_theory.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/global_theory.ML Tue Jul 30 15:09:25 2013 +0200 @@ -75,7 +75,6 @@ "_" => "Pure.asm_rl" | name => name); val res = Facts.lookup context facts name; - val _ = Theory.check_thy thy; in (case res of NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)
--- a/src/Pure/theory.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/theory.ML Tue Jul 30 15:09:25 2013 +0200 @@ -12,13 +12,8 @@ val parents_of: theory -> theory list val ancestors_of: theory -> theory list val nodes_of: theory -> theory list - val check_thy: theory -> theory_ref - val deref: theory_ref -> theory val merge: theory * theory -> theory - val merge_refs: theory_ref * theory_ref -> theory_ref val merge_list: theory list -> theory - val checkpoint: theory -> theory - val copy: theory -> theory val requires: theory -> string -> string -> unit val get_markup: theory -> Markup.T val axiom_space: theory -> Name_Space.T @@ -55,18 +50,11 @@ val ancestors_of = Context.ancestors_of; fun nodes_of thy = thy :: ancestors_of thy; -val check_thy = Context.check_thy; -val deref = Context.deref; - val merge = Context.merge; -val merge_refs = Context.merge_refs; fun merge_list [] = raise THEORY ("Empty merge of theories", []) | merge_list (thy :: thys) = Library.foldl merge (thy, thys); -val checkpoint : theory -> theory = I; (* FIXME dummy *) -val copy : theory -> theory = I; (* FIXME dummy *) - fun requires thy name what = if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then () else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
--- a/src/Pure/thm.ML Tue Jul 30 12:07:14 2013 +0200 +++ b/src/Pure/thm.ML Tue Jul 30 15:09:25 2013 +0200 @@ -11,11 +11,7 @@ sig (*certified types*) type ctyp - val rep_ctyp: ctyp -> - {thy_ref: theory_ref, - T: typ, - maxidx: int, - sorts: sort Ord_List.T} + val rep_ctyp: ctyp -> {thy: theory, T: typ, maxidx: int, sorts: sort Ord_List.T} val theory_of_ctyp: ctyp -> theory val typ_of: ctyp -> typ val ctyp_of: theory -> typ -> ctyp @@ -23,14 +19,8 @@ (*certified terms*) type cterm exception CTERM of string * cterm list - val rep_cterm: cterm -> - {thy_ref: theory_ref, - t: term, - T: typ, - maxidx: int, - sorts: sort Ord_List.T} - val crep_cterm: cterm -> - {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T} + val rep_cterm: cterm -> {thy: theory, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T} + val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T} val theory_of_cterm: cterm -> theory val term_of: cterm -> term val cterm_of: theory -> term -> cterm @@ -40,7 +30,7 @@ type thm type conv = cterm -> thm val rep_thm: thm -> - {thy_ref: theory_ref, + {thy: theory, tags: Properties.T, maxidx: int, shyps: sort Ord_List.T, @@ -48,7 +38,7 @@ tpairs: (term * term) list, prop: term} val crep_thm: thm -> - {thy_ref: theory_ref, + {thy: theory, tags: Properties.T, maxidx: int, shyps: sort Ord_List.T, @@ -158,15 +148,11 @@ (** certified types **) -abstype ctyp = Ctyp of - {thy_ref: theory_ref, - T: typ, - maxidx: int, - sorts: sort Ord_List.T} +abstype ctyp = Ctyp of {thy: theory, T: typ, maxidx: int, sorts: sort Ord_List.T} with fun rep_ctyp (Ctyp args) = args; -fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref; +fun theory_of_ctyp (Ctyp {thy, ...}) = thy; fun typ_of (Ctyp {T, ...}) = T; fun ctyp_of thy raw_T = @@ -174,10 +160,10 @@ val T = Sign.certify_typ thy raw_T; val maxidx = Term.maxidx_of_typ T; val sorts = Sorts.insert_typ T []; - in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end; + in Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts} end; -fun dest_ctyp (Ctyp {thy_ref, T = Type (_, Ts), maxidx, sorts}) = - map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts +fun dest_ctyp (Ctyp {thy, T = Type (_, Ts), maxidx, sorts}) = + map (fn T => Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts}) Ts | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); @@ -185,74 +171,69 @@ (** certified terms **) (*certified terms with checked typ, maxidx, and sorts*) -abstype cterm = Cterm of - {thy_ref: theory_ref, - t: term, - T: typ, - maxidx: int, - sorts: sort Ord_List.T} +abstype cterm = Cterm of {thy: theory, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T} with exception CTERM of string * cterm list; fun rep_cterm (Cterm args) = args; -fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) = - {thy_ref = thy_ref, t = t, maxidx = maxidx, sorts = sorts, - T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}}; +fun crep_cterm (Cterm {thy, t, T, maxidx, sorts}) = + {thy = thy, t = t, maxidx = maxidx, sorts = sorts, + T = Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts}}; -fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref; +fun theory_of_cterm (Cterm {thy, ...}) = thy; fun term_of (Cterm {t, ...}) = t; -fun ctyp_of_term (Cterm {thy_ref, T, maxidx, sorts, ...}) = - Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}; +fun ctyp_of_term (Cterm {thy, T, maxidx, sorts, ...}) = + Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts}; fun cterm_of thy tm = let val (t, T, maxidx) = Sign.certify_term thy tm; val sorts = Sorts.insert_term t []; - in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; + in Cterm {thy = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; -fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) = - Theory.merge_refs (r1, r2); +fun merge_thys0 (Cterm {thy = thy1, ...}) (Cterm {thy = thy2, ...}) = + Theory.merge (thy1, thy2); (* destructors *) -fun dest_comb (Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) = +fun dest_comb (Cterm {t = c $ a, T, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in - (Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, - Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) + (Cterm {t = c, T = A --> T, thy = thy, maxidx = maxidx, sorts = sorts}, + Cterm {t = a, T = A, thy = thy, maxidx = maxidx, sorts = sorts}) end | dest_comb ct = raise CTERM ("dest_comb", [ct]); -fun dest_fun (Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) = +fun dest_fun (Cterm {t = c $ _, T, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0 - in Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end + in Cterm {t = c, T = A --> T, thy = thy, maxidx = maxidx, sorts = sorts} end | dest_fun ct = raise CTERM ("dest_fun", [ct]); -fun dest_arg (Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) = +fun dest_arg (Cterm {t = c $ a, T = _, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0 - in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end + in Cterm {t = a, T = A, thy = thy, maxidx = maxidx, sorts = sorts} end | dest_arg ct = raise CTERM ("dest_arg", [ct]); -fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy_ref, maxidx, sorts}) = +fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0; val B = Term.argument_type_of c 1; - in Cterm {t = c, T = A --> B --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end + in Cterm {t = c, T = A --> B --> T, thy = thy, maxidx = maxidx, sorts = sorts} end | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]); -fun dest_arg1 (Cterm {t = c $ a $ _, T = _, thy_ref, maxidx, sorts}) = +fun dest_arg1 (Cterm {t = c $ a $ _, T = _, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0 - in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end + in Cterm {t = a, T = A, thy = thy, maxidx = maxidx, sorts = sorts} end | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); -fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) = +fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy, maxidx, sorts}) = let val (y', t') = Term.dest_abs (the_default x a, T, t) in - (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, - Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) + (Cterm {t = Free (y', T), T = T, thy = thy, maxidx = maxidx, sorts = sorts}, + Cterm {t = t', T = U, thy = thy, maxidx = maxidx, sorts = sorts}) end | dest_abs _ ct = raise CTERM ("dest_abs", [ct]); @@ -263,7 +244,7 @@ (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...}) (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) = if T = dty then - Cterm {thy_ref = merge_thys0 cf cx, + Cterm {thy = merge_thys0 cf cx, t = f $ x, T = rty, maxidx = Int.max (maxidx1, maxidx2), @@ -275,7 +256,7 @@ (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...}) (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) = let val t = Term.lambda_name (x, t1) t2 in - Cterm {thy_ref = merge_thys0 ct1 ct2, + Cterm {thy = merge_thys0 ct1 ct2, t = t, T = T1 --> T2, maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} @@ -286,17 +267,17 @@ (* indexes *) -fun adjust_maxidx_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = +fun adjust_maxidx_cterm i (ct as Cterm {thy, t, T, maxidx, sorts}) = if maxidx = i then ct else if maxidx < i then - Cterm {maxidx = i, thy_ref = thy_ref, t = t, T = T, sorts = sorts} + Cterm {maxidx = i, thy = thy, t = t, T = T, sorts = sorts} else - Cterm {maxidx = Int.max (maxidx_of_term t, i), thy_ref = thy_ref, t = t, T = T, sorts = sorts}; + Cterm {maxidx = Int.max (maxidx_of_term t, i), thy = thy, t = t, T = T, sorts = sorts}; -fun incr_indexes_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = +fun incr_indexes_cterm i (ct as Cterm {thy, t, T, maxidx, sorts}) = if i < 0 then raise CTERM ("negative increment", [ct]) else if i = 0 then ct - else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t, + else Cterm {thy = thy, t = Logic.incr_indexes ([], i) t, T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; @@ -308,17 +289,16 @@ (ct1 as Cterm {t = t1, sorts = sorts1, ...}, ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = let - val thy = Theory.deref (merge_thys0 ct1 ct2); + val thy = merge_thys0 ct1 ct2; val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) = - (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts}, - Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}); + (Ctyp {T = TVar ((a, i), S), thy = thy, maxidx = i, sorts = sorts}, + Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts}); fun mk_ctinst ((x, i), (T, t)) = let val T = Envir.subst_type Tinsts T in - (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy, - maxidx = i, sorts = sorts}, - Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}) + (Cterm {t = Var ((x, i), T), T = T, thy = thy, maxidx = i, sorts = sorts}, + Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts}) end; in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; @@ -335,7 +315,7 @@ abstype thm = Thm of deriv * (*derivation*) - {thy_ref: theory_ref, (*dynamic reference to theory*) + {thy: theory, (*background theory*) tags: Properties.T, (*additional annotations/comments*) maxidx: int, (*maximum index of any Var or TVar*) shyps: sort Ord_List.T, (*sort hypotheses*) @@ -354,9 +334,9 @@ fun rep_thm (Thm (_, args)) = args; -fun crep_thm (Thm (_, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = - let fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps} in - {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps, +fun crep_thm (Thm (_, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) = + let fun cterm max t = Cterm {thy = thy, t = t, T = propT, maxidx = max, sorts = shyps} in + {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, hyps = map (cterm ~1) hyps, tpairs = map (pairself (cterm maxidx)) tpairs, prop = cterm maxidx prop} @@ -383,16 +363,16 @@ (* merge theories of cterms/thms -- trivial absorption only *) -fun merge_thys1 (Cterm {thy_ref = r1, ...}) (Thm (_, {thy_ref = r2, ...})) = - Theory.merge_refs (r1, r2); +fun merge_thys1 (Cterm {thy = thy1, ...}) (Thm (_, {thy = thy2, ...})) = + Theory.merge (thy1, thy2); -fun merge_thys2 (Thm (_, {thy_ref = r1, ...})) (Thm (_, {thy_ref = r2, ...})) = - Theory.merge_refs (r1, r2); +fun merge_thys2 (Thm (_, {thy = thy1, ...})) (Thm (_, {thy = thy2, ...})) = + Theory.merge (thy1, thy2); (* basic components *) -val theory_of_thm = Theory.deref o #thy_ref o rep_thm; +val theory_of_thm = #thy o rep_thm; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); val hyps_of = #hyps o rep_thm; @@ -410,26 +390,23 @@ | [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); (*the statement of any thm is a cterm*) -fun cprop_of (Thm (_, {thy_ref, maxidx, shyps, prop, ...})) = - Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; +fun cprop_of (Thm (_, {thy, maxidx, shyps, prop, ...})) = + Cterm {thy = thy, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; -fun cprem_of (th as Thm (_, {thy_ref, maxidx, shyps, prop, ...})) i = - Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, sorts = shyps, +fun cprem_of (th as Thm (_, {thy, maxidx, shyps, prop, ...})) i = + Cterm {thy = thy, maxidx = maxidx, T = propT, sorts = shyps, t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])}; (*explicit transfer to a super theory*) fun transfer thy' thm = let - val Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop}) = thm; - val thy = Theory.deref thy_ref; + val Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop}) = thm; val _ = Theory.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]); - val is_eq = Theory.eq_thy (thy, thy'); - val _ = Theory.check_thy thy; in - if is_eq then thm + if Theory.eq_thy (thy, thy') then thm else Thm (der, - {thy_ref = Theory.check_thy thy', + {thy = thy', tags = tags, maxidx = maxidx, shyps = shyps, @@ -450,7 +427,7 @@ raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, []) else Thm (der, - {thy_ref = merge_thys1 ct th, + {thy = merge_thys1 ct th, tags = tags, maxidx = maxidx, shyps = Sorts.union sorts shyps, @@ -461,11 +438,10 @@ fun weaken_sorts raw_sorts ct = let - val Cterm {thy_ref, t, T, maxidx, sorts} = ct; - val thy = Theory.deref thy_ref; + val Cterm {thy, t, T, maxidx, sorts} = ct; val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); val sorts' = Sorts.union sorts more_sorts; - in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; + in Cterm {thy = thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; (*dangling sort constraints of a thm*) fun extra_shyps (th as Thm (_, {shyps, ...})) = @@ -516,8 +492,8 @@ | join_promises promises = join_promises_of (Future.joins (map snd promises)) and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms)); -fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) = - Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body +fun fulfill_body (Thm (Deriv {promises, body}, {thy, ...})) = + Proofterm.fulfill_norm_proof thy (fulfill_promises promises) body and fulfill_promises promises = map fst promises ~~ map fulfill_body (Future.joins (map snd promises)); @@ -554,10 +530,9 @@ 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 Thm (Deriv {promises, ...}, {thy, 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 _ = Theory.eq_thy (thy, orig_thy) orelse err "bad theory"; val _ = prop aconv orig_prop orelse err "bad prop"; val _ = null tpairs orelse err "bad tpairs"; val _ = null hyps orelse err "bad hyps"; @@ -568,15 +543,14 @@ fun future future_thm ct = let - val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct; - val thy = Theory.deref thy_ref; + val Cterm {thy = thy, t = prop, T, maxidx, sorts} = ct; val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); val i = serial (); val future = future_thm |> Future.map (future_result i thy sorts prop); in Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop), - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -595,14 +569,12 @@ fun name_derivation name (thm as Thm (der, args)) = let val Deriv {promises, body} = der; - val {thy_ref, shyps, hyps, prop, tpairs, ...} = args; + val {thy, shyps, hyps, prop, tpairs, ...} = args; val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]); val ps = map (apsnd (Future.map fulfill_body)) promises; - val thy = Theory.deref thy_ref; val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body; val der' = make_deriv [] [] [pthm] proof; - val _ = Theory.check_thy thy; in Thm (der', args) end; @@ -619,7 +591,7 @@ val maxidx = maxidx_of_term prop; val shyps = Sorts.insert_term prop []; in - Thm (der, {thy_ref = Theory.check_thy thy, tags = [], + Thm (der, {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop}) end); in @@ -637,27 +609,23 @@ val get_tags = #tags o rep_thm; -fun map_tags f (Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = - Thm (der, {thy_ref = thy_ref, tags = f tags, maxidx = maxidx, +fun map_tags f (Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) = + Thm (der, {thy = thy, tags = f tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); (* technical adjustments *) -fun norm_proof (Thm (der, args as {thy_ref, ...})) = - let - val thy = Theory.deref thy_ref; - val der' = deriv_rule1 (Proofterm.rew_proof thy) der; - val _ = Theory.check_thy thy; - in Thm (der', args) end; +fun norm_proof (Thm (der, args as {thy, ...})) = + Thm (deriv_rule1 (Proofterm.rew_proof thy) der, args); -fun adjust_maxidx_thm i (th as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = +fun adjust_maxidx_thm i (th as Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) = if maxidx = i then th else if maxidx < i then - Thm (der, {maxidx = i, thy_ref = thy_ref, tags = tags, shyps = shyps, + Thm (der, {maxidx = i, thy = thy, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) else - Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy_ref = thy_ref, + Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy = thy, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); @@ -668,13 +636,13 @@ (*The assumption rule A |- A*) fun assume raw_ct = - let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in + let val Cterm {thy, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in if T <> propT then raise THM ("assume: prop", 0, []) else if maxidx <> ~1 then raise THM ("assume: variables", maxidx, []) else Thm (deriv_rule0 (Proofterm.Hyp prop), - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = ~1, shyps = sorts, @@ -697,7 +665,7 @@ raise THM ("implies_intr: assumptions must have type prop", 0, [th]) else Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der, - {thy_ref = merge_thys1 ct th, + {thy = merge_thys1 ct th, tags = [], maxidx = Int.max (maxidxA, maxidx), shyps = Sorts.union sorts shyps, @@ -722,7 +690,7 @@ Const ("==>", _) $ A $ B => if A aconv propA then Thm (deriv_rule2 (curry Proofterm.%%) der derA, - {thy_ref = merge_thys2 thAB thA, + {thy = merge_thys2 thAB thA, tags = [], maxidx = Int.max (maxA, maxidx), shyps = Sorts.union shypsA shyps, @@ -746,7 +714,7 @@ let fun result a = Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der, - {thy_ref = merge_thys1 ct th, + {thy = merge_thys1 ct th, tags = [], maxidx = maxidx, shyps = Sorts.union sorts shyps, @@ -758,10 +726,10 @@ raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in - case x of + (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a) - | _ => raise THM ("forall_intr: not a variable", 0, [th]) + | _ => raise THM ("forall_intr: not a variable", 0, [th])) end; (*Forall elimination @@ -778,7 +746,7 @@ raise THM ("forall_elim: type mismatch", 0, [th]) else Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der, - {thy_ref = merge_thys1 ct th, + {thy = merge_thys1 ct th, tags = [], maxidx = Int.max (maxidx, maxt), shyps = Sorts.union sorts shyps, @@ -793,9 +761,9 @@ (*Reflexivity t == t *) -fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) = +fun reflexive (Cterm {thy, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 Proofterm.reflexive, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -808,11 +776,11 @@ ------ u == t *) -fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = +fun symmetric (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) = (case prop of (eq as Const ("==", _)) $ t $ u => Thm (deriv_rule1 Proofterm.symmetric der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, @@ -839,7 +807,7 @@ if not (u aconv u') then err "middle term" else Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2, - {thy_ref = merge_thys2 th1 th2, + {thy = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, @@ -853,7 +821,7 @@ (%x. t)(u) == t[u/x] fully beta-reduces the term if full = true *) -fun beta_conversion full (Cterm {thy_ref, t, T = _, maxidx, sorts}) = +fun beta_conversion full (Cterm {thy, t, T = _, maxidx, sorts}) = let val t' = if full then Envir.beta_norm t else @@ -861,7 +829,7 @@ | _ => raise THM ("beta_conversion: not a redex", 0, [])); in Thm (deriv_rule0 Proofterm.reflexive, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -870,9 +838,9 @@ prop = Logic.mk_equals (t, t')}) end; -fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = +fun eta_conversion (Cterm {thy, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 Proofterm.reflexive, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -880,9 +848,9 @@ tpairs = [], prop = Logic.mk_equals (t, Envir.eta_contract t)}); -fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = +fun eta_long_conversion (Cterm {thy, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 Proofterm.reflexive, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -898,13 +866,13 @@ *) fun abstract_rule a (Cterm {t = x, T, sorts, ...}) - (th as Thm (der, {thy_ref, maxidx, hyps, shyps, tpairs, prop, ...})) = + (th as Thm (der, {thy, maxidx, hyps, shyps, tpairs, prop, ...})) = let val (t, u) = Logic.dest_equals prop handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); val result = Thm (deriv_rule1 (Proofterm.abstract_rule x a) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = Sorts.union sorts shyps, @@ -917,10 +885,10 @@ raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in - case x of + (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result) - | _ => raise THM ("abstract_rule: not a variable", 0, [th]) + | _ => raise THM ("abstract_rule: not a variable", 0, [th])) end; (*The combination rule @@ -942,19 +910,19 @@ else () | _ => raise THM ("combination: not function type", 0, [th1, th2])); in - case (prop1, prop2) of + (case (prop1, prop2) of (Const ("==", Type ("fun", [fT, _])) $ f $ g, Const ("==", Type ("fun", [tT, _])) $ t $ u) => (chktypes fT tT; Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2, - {thy_ref = merge_thys2 th1 th2, + {thy = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (f $ t, g $ u)})) - | _ => raise THM ("combination: premises", 0, [th1, th2]) + | _ => raise THM ("combination: premises", 0, [th1, th2])) end; (*Equality introduction @@ -970,11 +938,11 @@ prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); in - case (prop1, prop2) of + (case (prop1, prop2) of (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') => if A aconv A' andalso B aconv B' then Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2, - {thy_ref = merge_thys2 th1 th2, + {thy = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, @@ -982,7 +950,7 @@ tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (A, B)}) else err "not equal" - | _ => err "premises" + | _ => err "premises") end; (*The equal propositions rule @@ -998,11 +966,11 @@ tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); in - case prop1 of + (case prop1 of Const ("==", _) $ A $ B => if prop2 aconv A then Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2, - {thy_ref = merge_thys2 th1 th2, + {thy = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, @@ -1010,7 +978,7 @@ tpairs = union_tpairs tpairs1 tpairs2, prop = B}) else err "not equal" - | _ => err"major premise" + | _ => err"major premise") end; @@ -1021,25 +989,23 @@ Instantiates the theorem and deletes trivial tpairs. Resulting sequence may contain multiple elements if the tpairs are not all flex-flex.*) -fun flexflex_rule (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = - let val thy = Theory.deref thy_ref in - Unify.smash_unifiers thy tpairs (Envir.empty maxidx) - |> Seq.map (fn env => - if Envir.is_empty env then th - else - let - val tpairs' = tpairs |> map (pairself (Envir.norm_term env)) - (*remove trivial tpairs, of the form t==t*) - |> filter_out (op aconv); - val der' = deriv_rule1 (Proofterm.norm_proof' env) der; - val prop' = Envir.norm_term env prop; - val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); - val shyps = Envir.insert_sorts env shyps; - in - Thm (der', {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx, - shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) - end) - end; +fun flexflex_rule (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) = + Unify.smash_unifiers thy tpairs (Envir.empty maxidx) + |> Seq.map (fn env => + if Envir.is_empty env then th + else + let + val tpairs' = tpairs |> map (pairself (Envir.norm_term env)) + (*remove trivial tpairs, of the form t==t*) + |> filter_out (op aconv); + val der' = deriv_rule1 (Proofterm.norm_proof' env) der; + val prop' = Envir.norm_term env prop; + val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); + val shyps = Envir.insert_sorts env shyps; + in + Thm (der', {thy = thy, tags = [], maxidx = maxidx, + shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) + end); (*Generalization of fixed variables @@ -1051,7 +1017,7 @@ fun generalize ([], []) _ th = th | generalize (tfrees, frees) idx th = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...}) = th; + val Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...}) = th; val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); val bad_type = @@ -1072,7 +1038,7 @@ val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); in Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx', shyps = shyps, @@ -1093,33 +1059,33 @@ fun pretty_typing thy t T = Pretty.block [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T]; -fun add_inst (ct, cu) (thy_ref, sorts) = +fun add_inst (ct, cu) (thy, sorts) = let val Cterm {t = t, T = T, ...} = ct; val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; - val thy_ref' = Theory.merge_refs (thy_ref, merge_thys0 ct cu); + val thy' = Theory.merge (thy, merge_thys0 ct cu); val sorts' = Sorts.union sorts_u sorts; in (case t of Var v => - if T = U then ((v, (u, maxidx_u)), (thy_ref', sorts')) + if T = U then ((v, (u, maxidx_u)), (thy', sorts')) else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", - Pretty.fbrk, pretty_typing (Theory.deref thy_ref') t T, - Pretty.fbrk, pretty_typing (Theory.deref thy_ref') u U]), [T, U], [t, u]) + Pretty.fbrk, pretty_typing thy' t T, + Pretty.fbrk, pretty_typing thy' u U]), [T, U], [t, u]) | _ => raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: not a variable", - Pretty.fbrk, Syntax.pretty_term_global (Theory.deref thy_ref') t]), [], [t])) + Pretty.fbrk, Syntax.pretty_term_global thy' t]), [], [t])) end; -fun add_instT (cT, cU) (thy_ref, sorts) = +fun add_instT (cT, cU) (thy, sorts) = let - val Ctyp {T, thy_ref = thy_ref1, ...} = cT - and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; - val thy' = Theory.deref (Theory.merge_refs (thy_ref, Theory.merge_refs (thy_ref1, thy_ref2))); + val Ctyp {T, thy = thy1, ...} = cT + and Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; + val thy' = Theory.merge (thy, Theory.merge (thy1, thy2)); val sorts' = Sorts.union sorts_U sorts; in (case T of TVar (v as (_, S)) => - if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (Theory.check_thy thy', sorts')) + if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts')) else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) | _ => raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: not a type variable", @@ -1134,9 +1100,9 @@ fun instantiate ([], []) th = th | instantiate (instT, inst) th = let - val Thm (der, {thy_ref, hyps, shyps, tpairs, prop, ...}) = th; - val (inst', (instT', (thy_ref', shyps'))) = - (thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT; + val Thm (der, {thy, hyps, shyps, tpairs, prop, ...}) = th; + val (inst', (instT', (thy', shyps'))) = + (thy, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT; val subst = Term_Subst.instantiate_maxidx (instT', inst'); val (prop', maxidx1) = subst prop ~1; val (tpairs', maxidx') = @@ -1144,7 +1110,7 @@ in Thm (deriv_rule1 (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, - {thy_ref = thy_ref', + {thy = thy', tags = [], maxidx = maxidx', shyps = shyps', @@ -1157,14 +1123,14 @@ fun instantiate_cterm ([], []) ct = ct | instantiate_cterm (instT, inst) ct = let - val Cterm {thy_ref, t, T, sorts, ...} = ct; - val (inst', (instT', (thy_ref', sorts'))) = - (thy_ref, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT; + val Cterm {thy, t, T, sorts, ...} = ct; + val (inst', (instT', (thy', sorts'))) = + (thy, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT; val subst = Term_Subst.instantiate_maxidx (instT', inst'); val substT = Term_Subst.instantiateT_maxidx instT'; val (t', maxidx1) = subst t ~1; val (T', maxidx') = substT T maxidx1; - in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end + in Cterm {thy = thy', t = t', T = T', sorts = sorts', maxidx = maxidx'} end handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); end; @@ -1172,12 +1138,12 @@ (*The trivial implication A ==> A, justified by assume and forall rules. A can contain Vars, not so for assume!*) -fun trivial (Cterm {thy_ref, t =A, T, maxidx, sorts}) = +fun trivial (Cterm {thy, t = A, T, maxidx, sorts}) = if T <> propT then raise THM ("trivial: the term must have type prop", 0, []) else Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)), - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -1192,14 +1158,13 @@ *) fun of_class (cT, raw_c) = let - val Ctyp {thy_ref, T, ...} = cT; - val thy = Theory.deref thy_ref; + val Ctyp {thy, T, ...} = cT; val c = Sign.certify_class thy raw_c; val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c)); in if Sign.of_sort thy (T, [c]) then Thm (deriv_rule0 (Proofterm.OfClass (T, c)), - {thy_ref = Theory.check_thy thy, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -1211,9 +1176,8 @@ (*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})) = + | strip_shyps (thm as Thm (der, {thy, 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 []; @@ -1225,7 +1189,7 @@ in Thm (deriv_rule_unconditional (Proofterm.strip_shyps_proof algebra present witnessed extra') der, - {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx, + {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) end; @@ -1233,7 +1197,7 @@ fun unconstrainT (thm as Thm (der, args)) = let val Deriv {promises, body} = der; - val {thy_ref, shyps, hyps, tpairs, prop, ...} = args; + val {thy, shyps, hyps, tpairs, prop, ...} = args; fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); val _ = null hyps orelse err "illegal hyps"; @@ -1242,14 +1206,12 @@ val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); val ps = map (apsnd (Future.map fulfill_body)) promises; - val thy = Theory.deref thy_ref; val (pthm as (_, (_, prop', _)), proof) = Proofterm.unconstrain_thm_proof thy shyps prop ps body; val der' = make_deriv [] [] [pthm] proof; - val _ = Theory.check_thy thy; in Thm (der', - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx_of_term prop', shyps = [[]], (*potentially redundant*) @@ -1259,7 +1221,7 @@ end; (* Replace all TFrees not fixed or in the hyps by new TVars *) -fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = +fun varifyT_global' fixed (Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) = let val tfrees = fold Term.add_tfrees hyps fixed; val prop1 = attach_tpairs tpairs prop; @@ -1267,7 +1229,7 @@ val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = Int.max (0, maxidx), shyps = shyps, @@ -1279,14 +1241,14 @@ val varifyT_global = #2 o varifyT_global' []; (* Replace all TVars by TFrees that are often new *) -fun legacy_freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) = +fun legacy_freezeT (Thm (der, {thy, 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 (Proofterm.legacy_freezeT prop1) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx_of_term prop2, shyps = shyps, @@ -1319,7 +1281,7 @@ if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, []) else Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der, - {thy_ref = merge_thys1 goal orule, + {thy = merge_thys1 goal orule, tags = [], maxidx = maxidx + inc, shyps = Sorts.union shyps sorts, (*sic!*) @@ -1328,12 +1290,12 @@ prop = Logic.list_implies (map lift_all As, lift_all B)}) end; -fun incr_indexes i (thm as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = +fun incr_indexes i (thm as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) = if i < 0 then raise THM ("negative increment", 0, [thm]) else if i = 0 then thm else Thm (deriv_rule1 (Proofterm.incr_indexes i) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx + i, shyps = shyps, @@ -1344,8 +1306,7 @@ (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) fun assumption i state = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; - val thy = Theory.deref thy_ref; + val Thm (der, {thy, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); fun newth n (env, tpairs) = Thm (deriv_rule1 @@ -1363,7 +1324,7 @@ Logic.list_implies (Bs, C) else (*normalize the new rule fully*) Envir.norm_term env (Logic.list_implies (Bs, C)), - thy_ref = Theory.check_thy thy}); + thy = thy}); val (close, asms, concl) = Logic.assum_problems (~1, Bi); val concl' = close concl; @@ -1380,7 +1341,7 @@ Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*) fun eq_assumption i state = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; + val Thm (der, {thy, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val (_, asms, concl) = Logic.assum_problems (~1, Bi); in @@ -1388,7 +1349,7 @@ ~1 => raise THM ("eq_assumption", 0, [state]) | n => Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, @@ -1401,7 +1362,7 @@ (*For rotate_tac: fast rotation of assumptions of subgoal i*) fun rotate_rule k i state = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; + val Thm (der, {thy, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val params = Term.strip_all_vars Bi; val rest = Term.strip_all_body Bi; @@ -1417,7 +1378,7 @@ else raise THM ("rotate_rule", k, [state]); in Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, @@ -1432,7 +1393,7 @@ number of premises. Useful with etac and underlies defer_tac*) fun permute_prems j k rl = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...}) = rl; + val Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...}) = rl; val prems = Logic.strip_imp_prems prop and concl = Logic.strip_imp_concl prop; val moved_prems = List.drop (prems, j) @@ -1448,7 +1409,7 @@ else raise THM ("permute_prems: k", k, [rl]); in Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, @@ -1466,7 +1427,7 @@ preceding parameters may be renamed to make all params distinct.*) fun rename_params_rule (cs, i) state = let - val Thm (der, {thy_ref, tags, maxidx, shyps, hyps, ...}) = state; + val Thm (der, {thy, tags, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val iparams = map #1 (Logic.strip_params Bi); val short = length iparams - length cs; @@ -1483,7 +1444,7 @@ a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); state) | [] => Thm (der, - {thy_ref = thy_ref, + {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, @@ -1495,11 +1456,11 @@ (*** Preservation of bound variable names ***) -fun rename_boundvars pat obj (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = +fun rename_boundvars pat obj (thm as Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) = (case Term.rename_abs pat obj prop of NONE => thm | SOME prop' => Thm (der, - {thy_ref = thy_ref, + {thy = thy, tags = tags, maxidx = maxidx, hyps = hyps, @@ -1622,7 +1583,7 @@ tpairs=rtpairs, prop=rprop,...}) = orule (*How many hyps to skip over during normalization*) and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0) - val thy = Theory.deref (merge_thys2 state orule); + val thy = merge_thys2 state orule; (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **) fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) = let val normt = Envir.norm_term env; @@ -1654,7 +1615,7 @@ hyps = union_hyps rhyps shyps, tpairs = ntpairs, prop = Logic.list_implies normp, - thy_ref = Theory.check_thy thy}) + thy = thy}) in Seq.cons th thq end handle COMPOSE => thq; val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop) handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); @@ -1749,14 +1710,14 @@ (* oracle rule *) -fun invoke_oracle thy_ref1 name oracle arg = - let val Cterm {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = oracle arg in +fun invoke_oracle thy1 name oracle arg = + let val Cterm {thy = thy2, t = prop, T, maxidx, sorts} = oracle arg in if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else let val (ora, prf) = Proofterm.oracle_proof name prop in Thm (make_deriv [] [ora] [] prf, - {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), + {thy = Theory.merge (thy1, thy2), tags = [], maxidx = maxidx, shyps = sorts, @@ -1788,7 +1749,7 @@ let val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy); val thy' = Oracles.put tab' thy; - in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end; + in ((name, invoke_oracle thy' name oracle), thy') end; end;