# HG changeset patch # User Lars Hupel # Date 1499768667 -7200 # Node ID 130dea8500cb709aca5d4a1680820ce0db535052 # Parent a51e72d79670d88339f5d7a9dde89241dd3fa3c9# Parent d6053815df065958f4b913cd354299d5eb83f0d1 merged diff -r a51e72d79670 -r 130dea8500cb src/HOL/Library/State_Monad.thy --- a/src/HOL/Library/State_Monad.thy Tue Jul 11 09:31:36 2017 +0200 +++ b/src/HOL/Library/State_Monad.thy Tue Jul 11 12:24:27 2017 +0200 @@ -5,7 +5,7 @@ section \Combinator syntax for generic, open state monads (single-threaded monads)\ theory State_Monad -imports Main Monad_Syntax +imports Main begin subsection \Motivation\ diff -r a51e72d79670 -r 130dea8500cb src/HOL/Proofs/Extraction/Euclid.thy --- a/src/HOL/Proofs/Extraction/Euclid.thy Tue Jul 11 09:31:36 2017 +0200 +++ b/src/HOL/Proofs/Extraction/Euclid.thy Tue Jul 11 12:24:27 2017 +0200 @@ -10,6 +10,7 @@ imports "~~/src/HOL/Computational_Algebra/Primes" Util + Old_Datatype "~~/src/HOL/Library/Code_Target_Numeral" begin diff -r a51e72d79670 -r 130dea8500cb src/HOL/Proofs/Extraction/Higman.thy --- a/src/HOL/Proofs/Extraction/Higman.thy Tue Jul 11 09:31:36 2017 +0200 +++ b/src/HOL/Proofs/Extraction/Higman.thy Tue Jul 11 12:24:27 2017 +0200 @@ -6,7 +6,7 @@ section \Higman's lemma\ theory Higman -imports Old_Datatype +imports Main begin text \ diff -r a51e72d79670 -r 130dea8500cb src/HOL/Proofs/Extraction/Higman_Extraction.thy --- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy Tue Jul 11 09:31:36 2017 +0200 +++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Tue Jul 11 12:24:27 2017 +0200 @@ -6,7 +6,7 @@ subsection \Extracting the program\ theory Higman_Extraction -imports Higman "~~/src/HOL/Library/State_Monad" Random +imports Higman Old_Datatype "~~/src/HOL/Library/State_Monad" begin declare R.induct [ind_realizer] diff -r a51e72d79670 -r 130dea8500cb src/HOL/Proofs/Extraction/Pigeonhole.thy --- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Tue Jul 11 09:31:36 2017 +0200 +++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Tue Jul 11 12:24:27 2017 +0200 @@ -5,7 +5,7 @@ section \The pigeonhole principle\ theory Pigeonhole -imports Util "~~/src/HOL/Library/Code_Target_Numeral" +imports Util Old_Datatype "~~/src/HOL/Library/Code_Target_Numeral" begin text \ diff -r a51e72d79670 -r 130dea8500cb src/HOL/Proofs/Extraction/QuotRem.thy --- a/src/HOL/Proofs/Extraction/QuotRem.thy Tue Jul 11 09:31:36 2017 +0200 +++ b/src/HOL/Proofs/Extraction/QuotRem.thy Tue Jul 11 12:24:27 2017 +0200 @@ -5,7 +5,7 @@ section \Quotient and remainder\ theory QuotRem -imports Util +imports Old_Datatype Util begin text \Derivation of quotient and remainder using program extraction.\ diff -r a51e72d79670 -r 130dea8500cb src/HOL/Proofs/Extraction/Util.thy --- a/src/HOL/Proofs/Extraction/Util.thy Tue Jul 11 09:31:36 2017 +0200 +++ b/src/HOL/Proofs/Extraction/Util.thy Tue Jul 11 12:24:27 2017 +0200 @@ -5,7 +5,7 @@ section \Auxiliary lemmas used in program extraction examples\ theory Util -imports "~~/src/HOL/Library/Old_Datatype" +imports Main begin text \Decidability of equality on natural numbers.\ diff -r a51e72d79670 -r 130dea8500cb src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Jul 11 09:31:36 2017 +0200 +++ b/src/Pure/Isar/code.ML Tue Jul 11 12:24:27 2017 +0200 @@ -555,8 +555,8 @@ in -fun generic_assert_eqn strictness thy check_patterns thm_proper = - handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy thm_proper; +fun generic_assert_eqn strictness thy check_patterns eqn = + handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy eqn; fun generic_assert_abs_eqn strictness thy check_patterns thm = handle_strictness I (raw_assert_abs_eqn thy check_patterns) strictness thy thm; diff -r a51e72d79670 -r 130dea8500cb src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Tue Jul 11 09:31:36 2017 +0200 +++ b/src/Pure/Isar/local_theory.ML Tue Jul 11 12:24:27 2017 +0200 @@ -19,7 +19,7 @@ val assert: local_theory -> local_theory val reset: local_theory -> local_theory val level: Proof.context -> int - val assert_bottom: bool -> local_theory -> local_theory + val assert_bottom: local_theory -> local_theory val mark_brittle: local_theory -> local_theory val assert_nonbrittle: local_theory -> local_theory val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory @@ -118,8 +118,28 @@ fun init _ = []; ); +(* nested structure *) + +val level = length o Data.get; (*1: main target at bottom, >= 2: nested context*) + fun assert lthy = - if null (Data.get lthy) then error "Missing local theory context" else lthy; + if level lthy = 0 then error "Missing local theory context" else lthy; + +fun assert_bottom lthy = + let + val _ = assert lthy; + in + if level lthy > 1 then error "Not at bottom of local theory nesting" + else lthy + end; + +fun assert_not_bottom lthy = + let + val _ = assert lthy; + in + if level lthy = 1 then error "Already at bottom of local theory nesting" + else lthy + end; val bottom_of = List.last o Data.get o assert; val top_of = hd o Data.get o assert; @@ -131,21 +151,6 @@ fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy); - -(* nested structure *) - -val level = length o Data.get; (*1: main target at bottom, >= 2: nested context*) - -fun assert_bottom b lthy = - let - val _ = assert lthy; - val b' = level lthy <= 1; - in - if b andalso not b' then error "Not at bottom of local theory nesting" - else if not b andalso b' then error "Already at bottom of local theory nesting" - else lthy - end; - fun map_contexts f lthy = let val n = level lthy in lthy |> (Data.map o map_index) @@ -272,9 +277,9 @@ val notes_kind = operation2 #notes; val declaration = operation2 #declaration; fun theory_registration dep_morph mixin export = - assert_bottom true #> operation (fn ops => #theory_registration ops dep_morph mixin export); + assert_bottom #> operation (fn ops => #theory_registration ops dep_morph mixin export); fun locale_dependency dep_morph mixin export = - assert_bottom true #> operation (fn ops => #locale_dependency ops dep_morph mixin export); + assert_bottom #> operation (fn ops => #locale_dependency ops dep_morph mixin export); (* theorems *) @@ -382,7 +387,7 @@ fun close_target lthy = let - val _ = assert_bottom false lthy; + val _ = assert_not_bottom lthy; val ({after_close, ...} :: rest) = Data.get lthy; in lthy |> Data.put rest |> reset |> after_close end; diff -r a51e72d79670 -r 130dea8500cb src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Tue Jul 11 09:31:36 2017 +0200 +++ b/src/Pure/Isar/named_target.ML Tue Jul 11 12:24:27 2017 +0200 @@ -163,7 +163,7 @@ fun begin ("-", _) thy = theory_init thy | begin target thy = init NONE (Locale.check thy target) thy; -val exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; +val exit = Local_Theory.assert_bottom #> Local_Theory.exit_global; fun switch NONE (Context.Theory thy) = (Context.Theory o exit, theory_init thy)