src/HOL/Tools/function_package/fundef_package.ML
changeset 23473 997bca36d4fe
parent 23203 a5026e73cfcf
child 23819 2040846d1bbe
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Jun 21 23:49:26 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Jun 22 10:23:37 2007 +0200
     1.3 @@ -190,6 +190,76 @@
     1.4      DatatypeHooks.add case_cong_hook
     1.5      #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
     1.6  
     1.7 +(* ad-hoc method to convert elimination-style goals to existential statements *)
     1.8 +
     1.9 +fun insert_int_goal thy subg st =
    1.10 +    let
    1.11 +      val goal = hd (prems_of st)
    1.12 +      val (ps, imp) = dest_all_all goal
    1.13 +      val cps = map (cterm_of thy) ps
    1.14 +
    1.15 +      val imp_subg = fold (fn p => fn t => betapply (t,p)) ps subg
    1.16 +      val new_subg = implies $ imp_subg $ imp
    1.17 +                      |> fold_rev mk_forall ps
    1.18 +                      |> cterm_of thy 
    1.19 +                      |> assume 
    1.20 +
    1.21 +      val sg2 = imp_subg
    1.22 +                 |> fold_rev mk_forall ps
    1.23 +                 |> cterm_of thy 
    1.24 +                 |> assume
    1.25 +
    1.26 +      val t' = new_subg
    1.27 +                |> fold forall_elim cps
    1.28 +                |> flip implies_elim (fold forall_elim cps sg2)
    1.29 +                |> fold_rev forall_intr cps
    1.30 +
    1.31 +      val st' = implies_elim st t'
    1.32 +                 |> implies_intr (cprop_of sg2)
    1.33 +                 |> implies_intr (cprop_of new_subg)
    1.34 +    in
    1.35 +      Seq.single st'
    1.36 +    end
    1.37 +
    1.38 +fun mk_cases_statement thy t =
    1.39 +    let
    1.40 +      fun mk_clause t = 
    1.41 +          let 
    1.42 +            val (qs, imp) = dest_all_all t
    1.43 +          in 
    1.44 +            Logic.strip_imp_prems imp
    1.45 +             |> map (ObjectLogic.atomize_term thy)
    1.46 +             |> foldr1 HOLogic.mk_conj
    1.47 +             |> fold_rev (fn Free (v,T) => fn t => HOLogic.mk_exists (v,T,t)) qs
    1.48 +          end
    1.49 +
    1.50 +      val (ps, imp) = dest_all_all t
    1.51 +    in 
    1.52 +      Logic.strip_imp_prems imp
    1.53 +       |> map mk_clause
    1.54 +       |> foldr1 HOLogic.mk_disj
    1.55 +       |> HOLogic.mk_Trueprop
    1.56 +       |> fold_rev lambda ps
    1.57 +    end
    1.58 +
    1.59 +fun elim_to_cases1 ctxt st =
    1.60 +    let
    1.61 +      val thy = theory_of_thm st
    1.62 +      val [subg] = prems_of st
    1.63 +      val cex = mk_cases_statement thy subg
    1.64 +    in
    1.65 +      (insert_int_goal thy cex
    1.66 +       THEN REPEAT_ALL_NEW (Tactic.ematch_tac [disjE, exE, conjE]) 1
    1.67 +       THEN REPEAT (Goal.assume_rule_tac ctxt 1)
    1.68 +    (*   THEN REPEAT (etac thin_rl 1)*)) st
    1.69 +    end
    1.70 +
    1.71 +fun elim_to_cases_tac ctxt = SELECT_GOAL (elim_to_cases1 ctxt)
    1.72 +
    1.73 +val elim_to_cases_setup = Method.add_methods
    1.74 +  [("elim_to_cases", Method.ctxt_args (Method.SIMPLE_METHOD' o elim_to_cases_tac),
    1.75 +    "convert elimination-style goal to a disjunction of existentials")]
    1.76 +
    1.77  (* setup *)
    1.78  
    1.79  val setup =
    1.80 @@ -198,6 +268,7 @@
    1.81        "declaration of congruence rule for function definitions")]
    1.82    #> setup_case_cong_hook
    1.83    #> FundefRelation.setup
    1.84 +  #> elim_to_cases_setup
    1.85  
    1.86  val get_congs = FundefCommon.get_fundef_congs o Context.Theory
    1.87