src/HOL/Decision_Procs/cooper_tac.ML
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 57514 bdc2c6b40bf2
child 58963 26bf09b95dda
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     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     val thy = Proof_Context.theory_of ctxt;
    44     (* Transform the term*)
    45     val (t, np, nh) = prepare_for_linz q g;
    46     (* Some simpsets for dealing with mod div abs and nat*)
    47     val mod_div_simpset =
    48       put_simpset HOL_basic_ss ctxt
    49       addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
    50           mod_add_right_eq [symmetric]
    51           div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
    52           mod_self
    53           div_by_0 mod_by_0 div_0 mod_0
    54           div_by_1 mod_by_1 div_1 mod_1
    55           Suc_eq_plus1}
    56       addsimps @{thms ac_simps}
    57       addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
    58     val simpset0 =
    59       put_simpset HOL_basic_ss ctxt
    60       addsimps @{thms mod_div_equality' Suc_eq_plus1 simp_thms}
    61       |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
    62     (* Simp rules for changing (n::int) to int n *)
    63     val simpset1 =
    64       put_simpset HOL_basic_ss ctxt
    65       addsimps @{thms zdvd_int} @
    66         map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int zadd_int zmult_int}
    67       |> Splitter.add_split @{thm zdiff_int_split}
    68     (*simp rules for elimination of int n*)
    69 
    70     val simpset2 =
    71       put_simpset HOL_basic_ss ctxt
    72       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}]
    73       |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
    74     (* simp rules for elimination of abs *)
    75     val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
    76     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    77     (* Theorem for the nat --> int transformation *)
    78     val pre_thm = Seq.hd (EVERY
    79       [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
    80        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
    81        TRY (simp_tac simpset3 1), TRY (simp_tac (put_simpset cooper_ss ctxt) 1)]
    82       (Thm.trivial ct))
    83     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    84     (* The result of the quantifier elimination *)
    85     val (th, tac) =
    86       (case (prop_of pre_thm) of
    87         Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    88           let
    89             val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
    90           in
    91             ((pth RS iffD2) RS pre_thm,
    92               assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
    93           end
    94       | _ => (pre_thm, assm_tac i))
    95   in rtac (mp_step nh (spec_step np th)) i THEN tac end);
    96 
    97 end