merged
authorLars Hupel <lars.hupel@mytum.de>
Tue, 11 Jul 2017 12:24:27 +0200
changeset 66266 130dea8500cb
parent 66262 a51e72d79670 (current diff)
parent 66265 d6053815df06 (diff)
child 66267 04b626416eae
merged
--- 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 \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close>
 
 theory State_Monad
-imports Main Monad_Syntax
+imports Main
 begin
 
 subsection \<open>Motivation\<close>
--- 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
 
--- 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 \<open>Higman's lemma\<close>
 
 theory Higman
-imports Old_Datatype
+imports Main
 begin
 
 text \<open>
--- 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 \<open>Extracting the program\<close>
 
 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]
--- 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 \<open>The pigeonhole principle\<close>
 
 theory Pigeonhole
-imports Util "~~/src/HOL/Library/Code_Target_Numeral"
+imports Util Old_Datatype "~~/src/HOL/Library/Code_Target_Numeral"
 begin
 
 text \<open>
--- 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 \<open>Quotient and remainder\<close>
 
 theory QuotRem
-imports Util
+imports Old_Datatype Util
 begin
 
 text \<open>Derivation of quotient and remainder using program extraction.\<close>
--- 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 \<open>Auxiliary lemmas used in program extraction examples\<close>
 
 theory Util
-imports "~~/src/HOL/Library/Old_Datatype"
+imports Main
 begin
 
 text \<open>Decidability of equality on natural numbers.\<close>
--- 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;
--- 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;
 
--- 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)