removed dead code;
authorwenzelm
Fri Mar 07 11:34:41 2014 +0100 (2014-03-07)
changeset 5597251b342baecda
parent 55971 7644d63e8c3f
child 55973 471a71017cfc
removed dead code;
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
     1.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Fri Mar 07 10:22:27 2014 +0100
     1.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Mar 07 11:34:41 2014 +0100
     1.3 @@ -77,14 +77,6 @@
     1.4    | x => x);
     1.5  
     1.6  
     1.7 -fun index_tree (Const (@{const_name Tip}, _)) path tab = tab
     1.8 -  | index_tree (Const (@{const_name Node}, _) $ l $ x $ _ $ r) path tab =
     1.9 -      tab
    1.10 -      |> Termtab.update_new (x, path)
    1.11 -      |> index_tree l (path @ [Left])
    1.12 -      |> index_tree r (path @ [Right])
    1.13 -  | index_tree t _ _ = raise TERM ("index_tree: input not a tree", [t])
    1.14 -
    1.15  fun split_common_prefix xs [] = ([], xs, [])
    1.16    | split_common_prefix [] ys = ([], [], ys)
    1.17    | split_common_prefix (xs as (x :: xs')) (ys as (y :: ys')) =
    1.18 @@ -138,7 +130,6 @@
    1.19   *)
    1.20  fun naive_cterm_first_order_match (t, ct) env =
    1.21    let
    1.22 -    val thy = theory_of_cterm ct;
    1.23      fun mtch (env as (tyinsts, insts)) =
    1.24        fn (Var (ixn, T), ct) =>
    1.25            (case AList.lookup (op =) insts ixn of
     2.1 --- a/src/HOL/Statespace/state_fun.ML	Fri Mar 07 10:22:27 2014 +0100
     2.2 +++ b/src/HOL/Statespace/state_fun.ML	Fri Mar 07 11:34:41 2014 +0100
     2.3 @@ -174,7 +174,7 @@
     2.4    Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
     2.5      (fn ctxt => fn t =>
     2.6        (case t of
     2.7 -        ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =>
     2.8 +        Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _ =>
     2.9            let
    2.10              val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT;
    2.11                (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
    2.12 @@ -208,7 +208,7 @@
    2.13                  * updates again, the optimised term is constructed.
    2.14                  *)
    2.15              fun mk_updterm already
    2.16 -                (t as ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s)) =
    2.17 +                ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =
    2.18                    let
    2.19                      fun rest already = mk_updterm already;
    2.20                      val (dT :: cT :: nT :: vT :: sT :: _) = binder_types uT;
    2.21 @@ -238,7 +238,8 @@
    2.22                                Const (@{const_name StateFun.update},
    2.23                                  d'T --> c'T --> nT --> vT' --> sT --> sT);
    2.24                            in
    2.25 -                            (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars, comps', b)
    2.26 +                            (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars,
    2.27 +                              comps', b)
    2.28                            end)
    2.29                    end
    2.30                | mk_updterm _ t = init_seed t;
     3.1 --- a/src/HOL/Statespace/state_space.ML	Fri Mar 07 10:22:27 2014 +0100
     3.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Mar 07 11:34:41 2014 +0100
     3.3 @@ -78,16 +78,6 @@
     3.4  fun fold1' f [] x = x
     3.5    | fold1' f xs _ = fold1 f xs
     3.6  
     3.7 -fun sublist_idx eq xs ys =
     3.8 -  let
     3.9 -    fun sublist n xs ys =
    3.10 -         if is_prefix eq xs ys then SOME n
    3.11 -         else (case ys of [] => NONE
    3.12 -               | (y::ys') => sublist (n+1) xs ys')
    3.13 -  in sublist 0 xs ys end;
    3.14 -
    3.15 -fun is_sublist eq xs ys = is_some (sublist_idx eq xs ys);
    3.16 -
    3.17  fun sorted_subset eq [] ys = true
    3.18    | sorted_subset eq (x::xs) [] = false
    3.19    | sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys
    3.20 @@ -118,13 +108,6 @@
    3.21       {declinfo=declinfo,distinctthm=distinctthm,silent=silent};
    3.22  
    3.23  
    3.24 -fun delete_declinfo n ctxt =
    3.25 -  let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
    3.26 -  in NameSpaceData.put
    3.27 -       (make_namespace_data (Termtab.delete_safe n declinfo) distinctthm silent) ctxt
    3.28 -  end;
    3.29 -
    3.30 -
    3.31  fun update_declinfo (n,v) ctxt =
    3.32    let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
    3.33    in NameSpaceData.put
    3.34 @@ -252,7 +235,6 @@
    3.35    let
    3.36      val all_comps = parent_comps @ new_comps;
    3.37      val vars = (map (fn n => (Binding.name n, NONE, NoSyn)) all_comps);
    3.38 -    val full_name = Sign.full_bname thy name;
    3.39      val dist_thm_name = distinct_compsN;
    3.40  
    3.41      val dist_thm_full_name = dist_thm_name;
    3.42 @@ -296,7 +278,7 @@
    3.43      |> interprete_parent name dist_thm_full_name parent_expr
    3.44    end;
    3.45  
    3.46 -fun encode_dot x = if x= #"." then #"_" else x;
    3.47 +fun encode_dot x = if x = #"." then #"_" else x;
    3.48  
    3.49  fun encode_type (TFree (s, _)) = s
    3.50    | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
    3.51 @@ -309,23 +291,6 @@
    3.52  fun project_name T = projectN ^"_"^encode_type T;
    3.53  fun inject_name T = injectN ^"_"^encode_type T;
    3.54  
    3.55 -fun project_free T pT V = Free (project_name T, V --> pT);
    3.56 -fun inject_free T pT V = Free (inject_name T, pT --> V);
    3.57 -
    3.58 -fun get_name n = getN ^ "_" ^ n;
    3.59 -fun put_name n = putN ^ "_" ^ n;
    3.60 -fun get_const n T nT V = Free (get_name n, (nT --> V) --> T);
    3.61 -fun put_const n T nT V = Free (put_name n, T --> (nT --> V) --> (nT --> V));
    3.62 -
    3.63 -fun lookup_const T nT V =
    3.64 -  Const (@{const_name StateFun.lookup}, (V --> T) --> nT --> (nT --> V) --> T);
    3.65 -
    3.66 -fun update_const T nT V =
    3.67 -  Const (@{const_name StateFun.update},
    3.68 -    (V --> T) --> (T --> V) --> nT --> (T --> T) --> (nT --> V) --> (nT --> V));
    3.69 -
    3.70 -fun K_const T = Const (@{const_name K_statefun}, T --> T --> T);
    3.71 -
    3.72  
    3.73  fun add_declaration name decl thy =
    3.74    thy
    3.75 @@ -347,15 +312,12 @@
    3.76      val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
    3.77    in all_comps end;
    3.78  
    3.79 -fun take_upto i xs = List.take(xs,i) handle General.Subscript => xs;
    3.80 -
    3.81  fun statespace_definition state_type args name parents parent_comps components thy =
    3.82    let
    3.83      val full_name = Sign.full_bname thy name;
    3.84      val all_comps = parent_comps @ components;
    3.85  
    3.86      val components' = map (fn (n,T) => (n,(T,full_name))) components;
    3.87 -    val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps;
    3.88  
    3.89      fun parent_expr (prefix, (_, n, rs)) =
    3.90        (suffix namespaceN n, (prefix, Expression.Positional rs));
    3.91 @@ -452,11 +414,6 @@
    3.92  
    3.93  (* prepare arguments *)
    3.94  
    3.95 -fun read_raw_parent ctxt raw_T =
    3.96 -  (case Proof_Context.read_typ_abbrev ctxt raw_T of
    3.97 -    Type (name, Ts) => (Ts, name)
    3.98 -  | T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T));
    3.99 -
   3.100  fun read_typ ctxt raw_T env =
   3.101    let
   3.102      val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
   3.103 @@ -587,16 +544,15 @@
   3.104  (*** parse/print - translations ***)
   3.105  
   3.106  local
   3.107 +
   3.108  fun map_get_comp f ctxt (Free (name,_)) =
   3.109        (case (get_comp ctxt name) of
   3.110          SOME (T,_) => f T T dummyT
   3.111        | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*)))
   3.112    | map_get_comp _ _ _ = Syntax.free "arbitrary";
   3.113  
   3.114 -val get_comp_projection = map_get_comp project_free;
   3.115 -val get_comp_injection  = map_get_comp inject_free;
   3.116 +fun name_of (Free (n,_)) = n;
   3.117  
   3.118 -fun name_of (Free (n,_)) = n;
   3.119  in
   3.120  
   3.121  fun gen_lookup_tr ctxt s n =
   3.122 @@ -624,7 +580,7 @@
   3.123            then Syntax.const "_statespace_lookup" $ s $ n
   3.124            else raise Match
   3.125        | NONE => raise Match)
   3.126 -  | lookup_tr' _ ts = raise Match;
   3.127 +  | lookup_tr' _ _ = raise Match;
   3.128  
   3.129  fun gen_update_tr id ctxt n v s =
   3.130    let