src/HOL/Decision_Procs/cooper_tac.ML
author paulson <lp15@cam.ac.uk>
Tue Nov 17 12:32:08 2015 +0000 (2015-11-17)
changeset 61694 6571c78c9667
parent 60754 02924903a6fd
child 62348 9a5f43dac883
permissions -rw-r--r--
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
     1 (*  Title:      HOL/Decision_Procs/cooper_tac.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 signature COOPER_TAC =
     6 sig
     7   val linz_tac: Proof.context -> bool -> int -> tactic
     8 end
     9 
    10 structure Cooper_Tac: COOPER_TAC =
    11 struct
    12 
    13 val cooper_ss = simpset_of @{context};
    14 
    15 fun prepare_for_linz q fm =
    16   let
    17     val ps = Logic.strip_params fm
    18     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
    19     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
    20     fun mk_all ((s, T), (P,n)) =
    21       if Term.is_dependent P then
    22         (HOLogic.all_const T $ Abs (s, T, P), n)
    23       else (incr_boundvars ~1 P, n-1)
    24     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
    25     val rhs = hs
    26     val np = length ps
    27     val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    28       (List.foldr HOLogic.mk_imp c rhs, np) ps
    29     val (vs, _) = List.partition (fn t => q orelse (type_of t) = @{typ nat})
    30       (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
    31     val fm2 = List.foldr mk_all2 fm' vs
    32   in (fm2, np + length vs, length rhs) end;
    33 
    34 (*Object quantifier to meta --*)
    35 fun spec_step n th = if n = 0 then th else (spec_step (n - 1) th) RS spec;
    36 
    37 (* object implication to meta---*)
    38 fun mp_step n th = if n = 0 then th else (mp_step (n - 1) th) RS mp;
    39 
    40 
    41 fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
    42   let
    43     (* Transform the term*)
    44     val (t, np, nh) = prepare_for_linz q g;
    45     (* Some simpsets for dealing with mod div abs and nat*)
    46     val mod_div_simpset =
    47       put_simpset HOL_basic_ss ctxt
    48       addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
    49           mod_add_right_eq [symmetric]
    50           div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
    51           mod_self
    52           div_by_0 mod_by_0 div_0 mod_0
    53           div_by_1 mod_by_1 div_1 mod_1
    54           Suc_eq_plus1}
    55       addsimps @{thms ac_simps}
    56       addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
    57     val simpset0 =
    58       put_simpset HOL_basic_ss ctxt
    59       addsimps @{thms mod_div_equality' Suc_eq_plus1 simp_thms}
    60       |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
    61     (* Simp rules for changing (n::int) to int n *)
    62     val simpset1 =
    63       put_simpset HOL_basic_ss ctxt
    64       addsimps @{thms zdvd_int} @ [@{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
    65         map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int}
    66       |> Splitter.add_split @{thm zdiff_int_split}
    67     (*simp rules for elimination of int n*)
    68 
    69     val simpset2 =
    70       put_simpset HOL_basic_ss ctxt
    71       addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *), @{thm int_0}, @{thm int_1}]
    72       |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
    73     (* simp rules for elimination of abs *)
    74     val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
    75     val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
    76     (* Theorem for the nat --> int transformation *)
    77     val pre_thm = Seq.hd (EVERY
    78       [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
    79        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
    80        TRY (simp_tac simpset3 1), TRY (simp_tac (put_simpset cooper_ss ctxt) 1)]
    81       (Thm.trivial ct))
    82     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
    83     (* The result of the quantifier elimination *)
    84     val (th, tac) =
    85       (case Thm.prop_of pre_thm of
    86         Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    87           let
    88             val pth = linzqe_oracle (ctxt, Envir.eta_long [] t1)
    89           in
    90             ((pth RS iffD2) RS pre_thm,
    91               assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i))
    92           end
    93       | _ => (pre_thm, assm_tac i))
    94   in resolve_tac ctxt [mp_step nh (spec_step np th)] i THEN tac end);
    95 
    96 end