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 ||
```