moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
authorwenzelm
Mon Sep 28 22:47:34 2009 +0200 (2009-09-28 ago)
changeset 3273371618deaf777
parent 32732 d5de73f4bcb8
child 32734 06c13b2e562e
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/Tools/cong_tac.ML
     1.1 --- a/src/HOL/HOL.thy	Mon Sep 28 21:35:57 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 28 22:47:34 2009 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    "~~/src/Tools/IsaPlanner/rw_inst.ML"
     1.5    "~~/src/Tools/intuitionistic.ML"
     1.6    "~~/src/Tools/project_rule.ML"
     1.7 +  "~~/src/Tools/cong_tac.ML"
     1.8    "~~/src/Provers/hypsubst.ML"
     1.9    "~~/src/Provers/splitter.ML"
    1.10    "~~/src/Provers/classical.ML"
    1.11 @@ -240,15 +241,15 @@
    1.12    by (rule subst)
    1.13  
    1.14  
    1.15 -subsubsection {*Congruence rules for application*}
    1.16 +subsubsection {* Congruence rules for application *}
    1.17  
    1.18 -(*similar to AP_THM in Gordon's HOL*)
    1.19 +text {* Similar to @{text AP_THM} in Gordon's HOL. *}
    1.20  lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
    1.21  apply (erule subst)
    1.22  apply (rule refl)
    1.23  done
    1.24  
    1.25 -(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    1.26 +text {* Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}. *}
    1.27  lemma arg_cong: "x=y ==> f(x)=f(y)"
    1.28  apply (erule subst)
    1.29  apply (rule refl)
    1.30 @@ -259,13 +260,15 @@
    1.31  apply (rule refl)
    1.32  done
    1.33  
    1.34 -lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
    1.35 +lemma cong: "[| f = g; (x::'a) = y |] ==> f x = g y"
    1.36  apply (erule subst)+
    1.37  apply (rule refl)
    1.38  done
    1.39  
    1.40 +ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *}
    1.41  
    1.42 -subsubsection {*Equality of booleans -- iff*}
    1.43 +
    1.44 +subsubsection {* Equality of booleans -- iff *}
    1.45  
    1.46  lemma iffI: assumes "P ==> Q" and "Q ==> P" shows "P=Q"
    1.47    by (iprover intro: iff [THEN mp, THEN mp] impI assms)
     2.1 --- a/src/HOL/IsaMakefile	Mon Sep 28 21:35:57 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Sep 28 22:47:34 2009 +0200
     2.3 @@ -87,30 +87,31 @@
     2.4    $(SRC)/Provers/hypsubst.ML \
     2.5    $(SRC)/Provers/quantifier1.ML \
     2.6    $(SRC)/Provers/splitter.ML \
     2.7 -  $(SRC)/Tools/IsaPlanner/isand.ML \
     2.8 -  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
     2.9 -  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
    2.10 -  $(SRC)/Tools/IsaPlanner/zipper.ML \
    2.11 -  $(SRC)/Tools/atomize_elim.ML \
    2.12 -  $(SRC)/Tools/auto_solve.ML \
    2.13    $(SRC)/Tools/Code/code_haskell.ML \
    2.14    $(SRC)/Tools/Code/code_ml.ML \
    2.15    $(SRC)/Tools/Code/code_preproc.ML \
    2.16    $(SRC)/Tools/Code/code_printer.ML \
    2.17    $(SRC)/Tools/Code/code_target.ML \
    2.18    $(SRC)/Tools/Code/code_thingol.ML \
    2.19 +  $(SRC)/Tools/Code_Generator.thy \
    2.20 +  $(SRC)/Tools/IsaPlanner/isand.ML \
    2.21 +  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
    2.22 +  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
    2.23 +  $(SRC)/Tools/IsaPlanner/zipper.ML \
    2.24 +  $(SRC)/Tools/atomize_elim.ML \
    2.25 +  $(SRC)/Tools/auto_solve.ML \
    2.26    $(SRC)/Tools/coherent.ML \
    2.27 +  $(SRC)/Tools/cong_tac.ML \
    2.28    $(SRC)/Tools/eqsubst.ML \
    2.29    $(SRC)/Tools/induct.ML \
    2.30 +  $(SRC)/Tools/induct_tacs.ML \
    2.31    $(SRC)/Tools/intuitionistic.ML \
    2.32 -  $(SRC)/Tools/induct_tacs.ML \
    2.33 +  $(SRC)/Tools/more_conv.ML \
    2.34    $(SRC)/Tools/nbe.ML \
    2.35 +  $(SRC)/Tools/project_rule.ML \
    2.36    $(SRC)/Tools/quickcheck.ML \
    2.37 -  $(SRC)/Tools/project_rule.ML \
    2.38    $(SRC)/Tools/random_word.ML \
    2.39    $(SRC)/Tools/value.ML \
    2.40 -  $(SRC)/Tools/Code_Generator.thy \
    2.41 -  $(SRC)/Tools/more_conv.ML \
    2.42    HOL.thy \
    2.43    Tools/hologic.ML \
    2.44    Tools/recfun_codegen.ML \
    2.45 @@ -130,9 +131,9 @@
    2.46    Inductive.thy \
    2.47    Lattices.thy \
    2.48    Nat.thy \
    2.49 +  Option.thy \
    2.50    OrderedGroup.thy \
    2.51    Orderings.thy \
    2.52 -  Option.thy \
    2.53    Plain.thy \
    2.54    Power.thy \
    2.55    Predicate.thy \
    2.56 @@ -215,8 +216,8 @@
    2.57    Equiv_Relations.thy \
    2.58    Groebner_Basis.thy \
    2.59    Hilbert_Choice.thy \
    2.60 +  Int.thy \
    2.61    IntDiv.thy \
    2.62 -  Int.thy \
    2.63    List.thy \
    2.64    Main.thy \
    2.65    Map.thy \
    2.66 @@ -280,8 +281,8 @@
    2.67  
    2.68  $(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
    2.69    Archimedean_Field.thy \
    2.70 +  Complex.thy \
    2.71    Complex_Main.thy \
    2.72 -  Complex.thy \
    2.73    Deriv.thy \
    2.74    Fact.thy \
    2.75    GCD.thy \
    2.76 @@ -294,18 +295,18 @@
    2.77    MacLaurin.thy \
    2.78    Nat_Transfer.thy \
    2.79    NthRoot.thy \
    2.80 +  PReal.thy \
    2.81 +  Parity.thy \
    2.82 +  RComplete.thy \
    2.83 +  Rational.thy \
    2.84 +  Real.thy \
    2.85 +  RealDef.thy \
    2.86 +  RealPow.thy \
    2.87 +  RealVector.thy \
    2.88    SEQ.thy \
    2.89    Series.thy \
    2.90    Taylor.thy \
    2.91    Transcendental.thy \
    2.92 -  Parity.thy \
    2.93 -  PReal.thy \
    2.94 -  Rational.thy \
    2.95 -  RComplete.thy \
    2.96 -  RealDef.thy \
    2.97 -  RealPow.thy \
    2.98 -  Real.thy \
    2.99 -  RealVector.thy \
   2.100    Tools/float_syntax.ML \
   2.101    Tools/transfer.ML \
   2.102    Tools/Qelim/ferrante_rackoff_data.ML \
     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Mon Sep 28 21:35:57 2009 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Sep 28 22:47:34 2009 +0200
     3.3 @@ -228,11 +228,7 @@
     3.4          addsimprocs [perm_compose_simproc]) i,
     3.5        asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st);
     3.6  
     3.7 -
     3.8 -(* applying Stefan's smart congruence tac *)
     3.9 -fun apply_cong_tac i = 
    3.10 -    ("application of congruence",
    3.11 -     (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
    3.12 +fun apply_cong_tac i = ("application of congruence", cong_tac i);
    3.13  
    3.14  
    3.15  (* unfolds the definition of permutations     *)
     4.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 21:35:57 2009 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 22:47:34 2009 +0200
     4.3 @@ -35,7 +35,6 @@
     4.4  
     4.5    val app_bnds : term -> int -> term
     4.6  
     4.7 -  val cong_tac : int -> tactic
     4.8    val indtac : thm -> string list -> int -> tactic
     4.9    val exh_tac : (string -> thm) -> int -> tactic
    4.10  
    4.11 @@ -112,21 +111,6 @@
    4.12  fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
    4.13  
    4.14  
    4.15 -fun cong_tac i st = (case Logic.strip_assums_concl
    4.16 -  (List.nth (prems_of st, i - 1)) of
    4.17 -    _ $ (_ $ (f $ x) $ (g $ y)) =>
    4.18 -      let
    4.19 -        val cong' = Thm.lift_rule (Thm.cprem_of st i) cong;
    4.20 -        val _ $ (_ $ (f' $ x') $ (g' $ y')) =
    4.21 -          Logic.strip_assums_concl (prop_of cong');
    4.22 -        val insts = map (pairself (cterm_of (Thm.theory_of_thm st)) o
    4.23 -          apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
    4.24 -            apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
    4.25 -      in compose_tac (false, cterm_instantiate insts cong', 2) i st
    4.26 -        handle THM _ => no_tac st
    4.27 -      end
    4.28 -  | _ => no_tac st);
    4.29 -
    4.30  (* instantiate induction rule *)
    4.31  
    4.32  fun indtac indrule indnames i st =
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/cong_tac.ML	Mon Sep 28 22:47:34 2009 +0200
     5.3 @@ -0,0 +1,37 @@
     5.4 +(*  Title:      Tools/cong_tac.ML
     5.5 +    Author:     Stefan Berghofer, TU Muenchen
     5.6 +
     5.7 +Congruence tactic based on explicit instantiation.
     5.8 +*)
     5.9 +
    5.10 +signature CONG_TAC =
    5.11 +sig
    5.12 +  val cong_tac: thm -> int -> tactic
    5.13 +end;
    5.14 +
    5.15 +structure Cong_Tac: CONG_TAC =
    5.16 +struct
    5.17 +
    5.18 +fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
    5.19 +  let
    5.20 +    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
    5.21 +    val goal = Thm.term_of cgoal;
    5.22 +  in
    5.23 +    (case Logic.strip_assums_concl goal of
    5.24 +      _ $ (_ $ (f $ x) $ (g $ y)) =>
    5.25 +        let
    5.26 +          val cong' = Thm.lift_rule cgoal cong;
    5.27 +          val _ $ (_ $ (f' $ x') $ (g' $ y')) =
    5.28 +            Logic.strip_assums_concl (Thm.prop_of cong');
    5.29 +          val ps = Logic.strip_params (Thm.concl_of cong');
    5.30 +          val insts = [(f', f), (g', g), (x', x), (y', y)]
    5.31 +            |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
    5.32 +        in
    5.33 +          fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
    5.34 +            handle THM _ => no_tac st
    5.35 +        end
    5.36 +    | _ => no_tac)
    5.37 +  end);
    5.38 +
    5.39 +end;
    5.40 +