# HG changeset patch
# User wenzelm
# Date 1414588476 -3600
# Node ID aa43c6f05bcaea46cfab4d6f89597d8d05b04cb4
# Parent  ee85e7b82d008db39d0934fa0c87a4496779fad9
modernized setup;
tuned whitespace;

diff -r ee85e7b82d00 -r aa43c6f05bca src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Wed Oct 29 14:05:36 2014 +0100
+++ b/src/HOL/Fun_Def.thy	Wed Oct 29 14:14:36 2014 +0100
@@ -135,8 +135,6 @@
   (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
 *} "termination prover for lexicographic orderings"
 
-setup Lexicographic_Order.setup
-
 
 subsection {* Congruence rules *}
 
@@ -308,8 +306,6 @@
 ML_file "Tools/Function/scnp_reconstruct.ML"
 ML_file "Tools/Function/fun_cases.ML"
 
-setup ScnpReconstruct.setup
-
 ML_val -- "setup inactive"
 {*
   Context.theory_map (Function_Common.set_termination_prover
diff -r ee85e7b82d00 -r aa43c6f05bca src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Wed Oct 29 14:05:36 2014 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Wed Oct 29 14:14:36 2014 +0100
@@ -9,7 +9,6 @@
 sig
   val lex_order_tac : bool -> Proof.context -> tactic -> tactic
   val lexicographic_order_tac : bool -> Proof.context -> tactic
-  val setup: theory -> theory
 end
 
 structure Lexicographic_Order : LEXICOGRAPHIC_ORDER =
@@ -214,7 +213,9 @@
   lex_order_tac quiet ctxt
     (auto_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems termination_simp})))
 
-val setup =
-  Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
+val _ =
+  Theory.setup
+    (Context.theory_map
+      (Function_Common.set_termination_prover (lexicographic_order_tac false)))
 
 end;
diff -r ee85e7b82d00 -r aa43c6f05bca src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Oct 29 14:05:36 2014 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Oct 29 14:14:36 2014 +0100
@@ -7,13 +7,10 @@
 
 signature SCNP_RECONSTRUCT =
 sig
-
   val sizechange_tac : Proof.context -> tactic -> tactic
 
   val decomp_scnp_tac : ScnpSolve.label list -> Proof.context -> tactic
 
-  val setup : theory -> theory
-
   datatype multiset_setup =
     Multiset of
     {
@@ -30,9 +27,7 @@
      reduction_pair : thm
     }
 
-
   val multiset_setup : multiset_setup -> theory -> theory
-
 end
 
 structure ScnpReconstruct : SCNP_RECONSTRUCT =
@@ -45,6 +40,7 @@
 val natT = HOLogic.natT
 val nat_pairT = HOLogic.mk_prodT (natT, natT)
 
+
 (* Theory dependencies *)
 
 datatype multiset_setup =
@@ -74,26 +70,24 @@
 val multiset_setup = Multiset_Setup.put o SOME
 
 fun undef _ = error "undef"
+
 fun get_multiset_setup thy = Multiset_Setup.get thy
   |> the_default (Multiset
-{ msetT = undef, mk_mset=undef,
-  mset_regroup_conv=undef, mset_member_tac = undef,
-  mset_nonempty_tac = undef, mset_pwleq_tac = undef,
-  set_of_simps = [],reduction_pair = refl,
-  smsI'=refl, wmsI2''=refl, wmsI1=refl })
+    { msetT = undef, mk_mset=undef,
+      mset_regroup_conv=undef, mset_member_tac = undef,
+      mset_nonempty_tac = undef, mset_pwleq_tac = undef,
+      set_of_simps = [],reduction_pair = refl,
+      smsI'=refl, wmsI2''=refl, wmsI1=refl })
 
 fun order_rpair _ MAX = @{thm max_rpair_set}
   | order_rpair msrp MS  = msrp
   | order_rpair _ MIN = @{thm min_rpair_set}
 
-fun ord_intros_max true =
-    (@{thm smax_emptyI}, @{thm smax_insertI})
-  | ord_intros_max false =
-    (@{thm wmax_emptyI}, @{thm wmax_insertI})
-fun ord_intros_min true =
-    (@{thm smin_emptyI}, @{thm smin_insertI})
-  | ord_intros_min false =
-    (@{thm wmin_emptyI}, @{thm wmin_insertI})
+fun ord_intros_max true = (@{thm smax_emptyI}, @{thm smax_insertI})
+  | ord_intros_max false = (@{thm wmax_emptyI}, @{thm wmax_insertI})
+
+fun ord_intros_min true = (@{thm smin_emptyI}, @{thm smin_insertI})
+  | ord_intros_min false = (@{thm wmin_emptyI}, @{thm wmin_insertI})
 
 fun gen_probl D cs =
   let
@@ -131,6 +125,7 @@
   THEN etac @{thm ssubst} 1
   THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.case}
 
+
 (* Sets *)
 
 val setT = HOLogic.mk_setT
@@ -154,20 +149,20 @@
     val Multiset
           { msetT, mk_mset,
             mset_regroup_conv, mset_pwleq_tac, set_of_simps,
-            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...} 
+            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...}
         = get_multiset_setup thy
 
     fun measure_fn p = nth (Termination.get_measures D p)
 
     fun get_desc_thm cidx m1 m2 bStrict =
-      case Termination.get_descent D (nth cs cidx) m1 m2
-       of SOME (Termination.Less thm) =>
+      (case Termination.get_descent D (nth cs cidx) m1 m2 of
+        SOME (Termination.Less thm) =>
           if bStrict then thm
           else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
-        | SOME (Termination.LessEq (thm, _))  =>
+      | SOME (Termination.LessEq (thm, _))  =>
           if not bStrict then thm
           else raise Fail "get_desc_thm"
-        | _ => raise Fail "get_desc_thm"
+      | _ => raise Fail "get_desc_thm")
 
     val (label, lev, sl, covering) = certificate
 
@@ -184,7 +179,8 @@
                              (not tag_flag)
               |> Conv.fconv_rule (Thm.beta_conversion true)
 
-            val rule = if strict
+            val rule =
+              if strict
               then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
               else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
           in
@@ -193,72 +189,72 @@
           end
 
         fun steps_tac MAX strict lq lp =
-          let
-            val (empty, step) = ord_intros_max strict
-          in
-            if length lq = 0
-            then rtac empty 1 THEN set_finite_tac 1
-                 THEN (if strict then set_nonempty_tac 1 else all_tac)
-            else
               let
-                val (j, b) :: rest = lq
-                val (i, a) = the (covering g strict j)
-                fun choose xs = set_member_tac (Library.find_index (curry op = (i, a)) xs) 1
-                val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
+                val (empty, step) = ord_intros_max strict
               in
-                rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
+                if length lq = 0
+                then rtac empty 1 THEN set_finite_tac 1
+                     THEN (if strict then set_nonempty_tac 1 else all_tac)
+                else
+                  let
+                    val (j, b) :: rest = lq
+                    val (i, a) = the (covering g strict j)
+                    fun choose xs = set_member_tac (Library.find_index (curry op = (i, a)) xs) 1
+                    val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
+                  in
+                    rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
+                  end
               end
-          end
           | steps_tac MIN strict lq lp =
-          let
-            val (empty, step) = ord_intros_min strict
-          in
-            if length lp = 0
-            then rtac empty 1
-                 THEN (if strict then set_nonempty_tac 1 else all_tac)
-            else
               let
-                val (i, a) :: rest = lp
-                val (j, b) = the (covering g strict i)
-                fun choose xs = set_member_tac (Library.find_index (curry op = (j, b)) xs) 1
-                val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
+                val (empty, step) = ord_intros_min strict
               in
-                rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
+                if length lp = 0
+                then rtac empty 1
+                     THEN (if strict then set_nonempty_tac 1 else all_tac)
+                else
+                  let
+                    val (i, a) :: rest = lp
+                    val (j, b) = the (covering g strict i)
+                    fun choose xs = set_member_tac (Library.find_index (curry op = (j, b)) xs) 1
+                    val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
+                  in
+                    rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
+                  end
               end
-          end
           | steps_tac MS strict lq lp =
-          let
-            fun get_str_cover (j, b) =
-              if is_some (covering g true j) then SOME (j, b) else NONE
-            fun get_wk_cover (j, b) = the (covering g false j)
+              let
+                fun get_str_cover (j, b) =
+                  if is_some (covering g true j) then SOME (j, b) else NONE
+                fun get_wk_cover (j, b) = the (covering g false j)
 
-            val qs = subtract (op =) (map_filter get_str_cover lq) lq
-            val ps = map get_wk_cover qs
+                val qs = subtract (op =) (map_filter get_str_cover lq) lq
+                val ps = map get_wk_cover qs
 
-            fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
-            val iqs = indices lq qs
-            val ips = indices lp ps
+                fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
+                val iqs = indices lq qs
+                val ips = indices lp ps
 
-            local open Conv in
-            fun t_conv a C =
-              params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
-            val goal_rewrite =
-                t_conv arg1_conv (mset_regroup_conv iqs)
-                then_conv t_conv arg_conv (mset_regroup_conv ips)
-            end
-          in
-            CONVERSION goal_rewrite 1
-            THEN (if strict then rtac smsI' 1
-                  else if qs = lq then rtac wmsI2'' 1
-                  else rtac wmsI1 1)
-            THEN mset_pwleq_tac 1
-            THEN EVERY (map2 (less_proof false) qs ps)
-            THEN (if strict orelse qs <> lq
-                  then Local_Defs.unfold_tac ctxt set_of_simps
-                       THEN steps_tac MAX true
-                       (subtract (op =) qs lq) (subtract (op =) ps lp)
-                  else all_tac)
-          end
+                local open Conv in
+                fun t_conv a C =
+                  params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
+                val goal_rewrite =
+                    t_conv arg1_conv (mset_regroup_conv iqs)
+                    then_conv t_conv arg_conv (mset_regroup_conv ips)
+                end
+              in
+                CONVERSION goal_rewrite 1
+                THEN (if strict then rtac smsI' 1
+                      else if qs = lq then rtac wmsI2'' 1
+                      else rtac wmsI1 1)
+                THEN mset_pwleq_tac 1
+                THEN EVERY (map2 (less_proof false) qs ps)
+                THEN (if strict orelse qs <> lq
+                      then Local_Defs.unfold_tac ctxt set_of_simps
+                           THEN steps_tac MAX true
+                           (subtract (op =) qs lq) (subtract (op =) ps lp)
+                      else all_tac)
+              end
       in
         rem_inv_img ctxt
         THEN steps_tac label strict (nth lev q) (nth lev p)
@@ -270,8 +266,8 @@
       HOLogic.pair_const natT natT $
         (measure_fn p i $ Bound 0) $ HOLogic.mk_number natT tag
 
-    fun pt_lev (p, lm) = Abs ("x", Termination.get_types D p,
-                           mk_set nat_pairT (map (tag_pair p) lm))
+    fun pt_lev (p, lm) =
+      Abs ("x", Termination.get_types D p, mk_set nat_pairT (map (tag_pair p) lm))
 
     val level_mapping =
       map_index pt_lev lev
@@ -295,36 +291,32 @@
 fun single_scnp_tac use_tags orders ctxt D = Termination.CALLS (fn (cs, i) =>
   let
     val ms_configured = is_some (Multiset_Setup.get (Proof_Context.theory_of ctxt))
-    val orders' = if ms_configured then orders
-                  else filter_out (curry op = MS) orders
+    val orders' =
+      if ms_configured then orders
+      else filter_out (curry op = MS) orders
     val gp = gen_probl D cs
     val certificate = generate_certificate use_tags orders' gp
   in
-    case certificate
-     of NONE => no_tac
-      | SOME cert =>
-          SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
-          THEN TRY (rtac @{thm wf_empty} i)
+    (case certificate of
+      NONE => no_tac
+    | SOME cert =>
+        SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
+        THEN TRY (rtac @{thm wf_empty} i))
   end)
 
-local open Termination in
-
 fun gen_decomp_scnp_tac orders autom_tac ctxt =
-TERMINATION ctxt autom_tac (fn D => 
-  let
-    val decompose = decompose_tac D
-    val scnp_full = single_scnp_tac true orders ctxt D
-  in
-    REPEAT_ALL_NEW (scnp_full ORELSE' decompose)
-  end)
-end
+  Termination.TERMINATION ctxt autom_tac (fn D =>
+    let
+      val decompose = Termination.decompose_tac D
+      val scnp_full = single_scnp_tac true orders ctxt D
+    in
+      REPEAT_ALL_NEW (scnp_full ORELSE' decompose)
+    end)
 
 fun gen_sizechange_tac orders autom_tac ctxt =
   TRY (Function_Common.apply_termination_rule ctxt 1)
   THEN TRY (Termination.wf_union_tac ctxt)
-  THEN
-   (rtac @{thm wf_empty} 1
-    ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
+  THEN (rtac @{thm wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
 
 fun sizechange_tac ctxt autom_tac =
   gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
@@ -347,9 +339,11 @@
      (Args.$$$ "ms" >> K MS))
   || Scan.succeed [MAX, MS, MIN]
 
-val setup = Method.setup @{binding size_change}
-  (Scan.lift orders --| Method.sections clasimp_modifiers >>
-    (fn orders => SIMPLE_METHOD o decomp_scnp_tac orders))
-  "termination prover with graph decomposition and the NP subset of size change termination"
+val _ =
+  Theory.setup
+    (Method.setup @{binding size_change}
+      (Scan.lift orders --| Method.sections clasimp_modifiers >>
+        (fn orders => SIMPLE_METHOD o decomp_scnp_tac orders))
+      "termination prover with graph decomposition and the NP subset of size change termination")
 
 end