src/Pure/Tools/find_theorems.ML
changeset 31042 d452117ba564
parent 30822 8aac4b974280
child 31684 d5d830979a54
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Wed May 06 09:08:47 2009 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed May 06 10:55:47 2009 +1000
     1.3 @@ -7,7 +7,7 @@
     1.4  signature FIND_THEOREMS =
     1.5  sig
     1.6    datatype 'term criterion =
     1.7 -    Name of string | Intro | Elim | Dest | Solves | Simp of 'term |
     1.8 +    Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
     1.9      Pattern of 'term
    1.10    val tac_limit: int ref
    1.11    val limit: int ref
    1.12 @@ -24,11 +24,12 @@
    1.13  (** search criteria **)
    1.14  
    1.15  datatype 'term criterion =
    1.16 -  Name of string | Intro | Elim | Dest | Solves | Simp of 'term |
    1.17 +  Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
    1.18    Pattern of 'term;
    1.19  
    1.20  fun read_criterion _ (Name name) = Name name
    1.21    | read_criterion _ Intro = Intro
    1.22 +  | read_criterion _ IntroIff = IntroIff
    1.23    | read_criterion _ Elim = Elim
    1.24    | read_criterion _ Dest = Dest
    1.25    | read_criterion _ Solves = Solves
    1.26 @@ -42,6 +43,7 @@
    1.27      (case c of
    1.28        Name name => Pretty.str (prfx "name: " ^ quote name)
    1.29      | Intro => Pretty.str (prfx "intro")
    1.30 +    | IntroIff => Pretty.str (prfx "introiff")
    1.31      | Elim => Pretty.str (prfx "elim")
    1.32      | Dest => Pretty.str (prfx "dest")
    1.33      | Solves => Pretty.str (prfx "solves")
    1.34 @@ -74,17 +76,40 @@
    1.35  
    1.36  fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
    1.37  
    1.38 +(* Note: ("op =" : "bool --> bool --> bool") does not exist in Pure. *)
    1.39 +fun is_Iff c =
    1.40 +  (case dest_Const c of
    1.41 +     ("op =", ty) =>
    1.42 +       (ty
    1.43 +        |> strip_type
    1.44 +        |> swap
    1.45 +        |> (op ::)
    1.46 +        |> map (fst o dest_Type)
    1.47 +        |> forall (curry (op =) "bool")
    1.48 +        handle TYPE _ => false)
    1.49 +   | _ => false);
    1.50 +
    1.51  (*extract terms from term_src, refine them to the parts that concern us,
    1.52    if po try match them against obj else vice versa.
    1.53    trivial matches are ignored.
    1.54    returns: smallest substitution size*)
    1.55 -fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src =
    1.56 +fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src =
    1.57    let
    1.58      val thy = ProofContext.theory_of ctxt;
    1.59  
    1.60 +    val chkmatch = obj |> (if po then rpair else pair) #> Pattern.matches thy;
    1.61      fun matches pat =
    1.62 -      is_nontrivial thy pat andalso
    1.63 -      Pattern.matches thy (if po then (pat, obj) else (obj, pat));
    1.64 +      let
    1.65 +        val jpat = ObjectLogic.drop_judgment thy pat;
    1.66 +        val c = Term.head_of jpat;
    1.67 +        val pats =
    1.68 +          if Term.is_Const c
    1.69 +          then if doiff andalso is_Iff c
    1.70 +               then pat :: map (ObjectLogic.ensure_propT thy) ((snd o strip_comb) jpat)
    1.71 +                    |> filter (is_nontrivial thy)
    1.72 +               else [pat]
    1.73 +          else [];
    1.74 +      in filter chkmatch pats end;
    1.75  
    1.76      fun substsize pat =
    1.77        let val (_, subst) =
    1.78 @@ -96,7 +121,9 @@
    1.79  
    1.80      val match_thm = matches o refine_term;
    1.81    in
    1.82 -    map (substsize o refine_term) (filter match_thm (extract_terms term_src))
    1.83 +    map match_thm (extract_terms term_src)
    1.84 +    |> flat
    1.85 +    |> map substsize
    1.86      |> bestmatch
    1.87    end;
    1.88  
    1.89 @@ -117,7 +144,7 @@
    1.90        hd o Logic.strip_imp_prems);
    1.91      val prems = Logic.prems_of_goal goal 1;
    1.92  
    1.93 -    fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm;
    1.94 +    fun try_subst prem = is_matching_thm false extract_dest ctxt true prem thm;
    1.95      val successful = prems |> map_filter try_subst;
    1.96    in
    1.97      (*if possible, keep best substitution (one with smallest size)*)
    1.98 @@ -127,11 +154,11 @@
    1.99      then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
   1.100    end;
   1.101  
   1.102 -fun filter_intro ctxt goal (_, thm) =
   1.103 +fun filter_intro doiff ctxt goal (_, thm) =
   1.104    let
   1.105      val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl);
   1.106      val concl = Logic.concl_of_goal goal 1;
   1.107 -    val ss = is_matching_thm extract_intro ctxt true concl thm;
   1.108 +    val ss = is_matching_thm doiff extract_intro ctxt true concl thm;
   1.109    in
   1.110      if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
   1.111    end;
   1.112 @@ -148,7 +175,7 @@
   1.113        val rule_tree = combine rule_mp rule_concl;
   1.114        fun goal_tree prem = combine prem goal_concl;
   1.115        fun try_subst prem =
   1.116 -        is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
   1.117 +        is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree;
   1.118        val successful = prems |> map_filter try_subst;
   1.119      in
   1.120      (*elim rules always have assumptions, so an elim with one
   1.121 @@ -183,7 +210,7 @@
   1.122      val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt);
   1.123      val extract_simp =
   1.124        (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
   1.125 -    val ss = is_matching_thm extract_simp ctxt false t thm;
   1.126 +    val ss = is_matching_thm false extract_simp ctxt false t thm;
   1.127    in
   1.128      if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
   1.129    end;
   1.130 @@ -233,7 +260,8 @@
   1.131    | filter_crit _ NONE Elim = err_no_goal "elim"
   1.132    | filter_crit _ NONE Dest = err_no_goal "dest"
   1.133    | filter_crit _ NONE Solves = err_no_goal "solves"
   1.134 -  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
   1.135 +  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro false ctxt (fix_goal goal))
   1.136 +  | filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal))
   1.137    | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
   1.138    | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
   1.139    | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
   1.140 @@ -428,6 +456,7 @@
   1.141  val criterion =
   1.142    P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
   1.143    P.reserved "intro" >> K Intro ||
   1.144 +  P.reserved "introiff" >> K IntroIff ||
   1.145    P.reserved "elim" >> K Elim ||
   1.146    P.reserved "dest" >> K Dest ||
   1.147    P.reserved "solves" >> K Solves ||