src/Provers/quantifier1.ML
 changeset 42459 38b9f023cc34 parent 42458 5dfae6d348fd child 42460 1805c67dc7aa
```     1.1 --- a/src/Provers/quantifier1.ML	Fri Apr 22 14:53:11 2011 +0200
1.2 +++ b/src/Provers/quantifier1.ML	Fri Apr 22 15:05:04 2011 +0200
1.3 @@ -66,11 +66,11 @@
1.4  sig
1.5    val prove_one_point_all_tac: tactic
1.6    val prove_one_point_ex_tac: tactic
1.7 -  val rearrange_all: simpset -> term -> thm option
1.8 -  val rearrange_ex: simpset -> term -> thm option
1.9 -  val rearrange_ball: tactic -> simpset -> term -> thm option
1.10 -  val rearrange_bex: tactic -> simpset -> term -> thm option
1.11 -  val rearrange_Collect: tactic -> simpset -> term -> thm option
1.12 +  val rearrange_all: simpset -> cterm -> thm option
1.13 +  val rearrange_ex: simpset -> cterm -> thm option
1.14 +  val rearrange_ball: tactic -> simpset -> cterm -> thm option
1.15 +  val rearrange_bex: tactic -> simpset -> cterm -> thm option
1.16 +  val rearrange_Collect: tactic -> simpset -> cterm -> thm option
1.17  end;
1.18
1.19  functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
1.20 @@ -172,15 +172,19 @@
1.21      val Q = if n = 0 then P else renumber 0 n P;
1.22    in quant xs (qC \$ Abs (x, T, Q)) end;
1.23
1.24 -fun rearrange_all ss (F as (all as Const (q, _)) \$ Abs (x, T, P)) =
1.25 +fun rearrange_all ss ct =
1.26 +  (case term_of ct of
1.27 +    F as (all as Const (q, _)) \$ Abs (x, T, P) =>
1.28        (case extract_quant extract_imp q P of
1.29          NONE => NONE
1.30        | SOME (xs, eq, Q) =>
1.31            let val R = quantify all x T xs (Data.imp \$ eq \$ Q)
1.32            in SOME (prove_conv prove_one_point_all_tac ss (F, R)) end)
1.33 -  | rearrange_all _ _ = NONE;
1.34 +  | _ => NONE);
1.35
1.36 -fun rearrange_ball tac ss (F as Ball \$ A \$ Abs (x, T, P)) =
1.37 +fun rearrange_ball tac ss ct =
1.38 +  (case term_of ct of
1.39 +    F as Ball \$ A \$ Abs (x, T, P) =>
1.40        (case extract_imp true [] P of
1.41          NONE => NONE
1.42        | SOME (xs, eq, Q) =>
1.43 @@ -188,30 +192,36 @@
1.44            else
1.45              let val R = Data.imp \$ eq \$ Q
1.46              in SOME (prove_conv tac ss (F, Ball \$ A \$ Abs (x, T, R))) end)
1.47 -  | rearrange_ball _ _ _ = NONE;
1.48 +  | _ => NONE);
1.49
1.50 -fun rearrange_ex ss (F as (ex as Const (q, _)) \$ Abs (x, T, P)) =
1.51 +fun rearrange_ex ss ct =
1.52 +  (case term_of ct of
1.53 +    F as (ex as Const (q, _)) \$ Abs (x, T, P) =>
1.54        (case extract_quant extract_conj q P of
1.55          NONE => NONE
1.56        | SOME (xs, eq, Q) =>
1.57            let val R = quantify ex x T xs (Data.conj \$ eq \$ Q)
1.58            in SOME (prove_conv prove_one_point_ex_tac ss (F, R)) end)
1.59 -  | rearrange_ex _ _ = NONE;
1.60 +  | _ => NONE);
1.61
1.62 -fun rearrange_bex tac ss (F as Bex \$ A \$ Abs (x, T, P)) =
1.63 +fun rearrange_bex tac ss ct =
1.64 +  (case term_of ct of
1.65 +    F as Bex \$ A \$ Abs (x, T, P) =>
1.66        (case extract_conj true [] P of
1.67          NONE => NONE
1.68        | SOME (xs, eq, Q) =>
1.69            if not (null xs) then NONE
1.70            else SOME (prove_conv tac ss (F, Bex \$ A \$ Abs (x, T, Data.conj \$ eq \$ Q))))
1.71 -  | rearrange_bex _ _ _ = NONE;
1.72 +  | _ => NONE);
1.73
1.74 -fun rearrange_Collect tac ss (F as Collect \$ Abs (x, T, P)) =
1.75 +fun rearrange_Collect tac ss ct =
1.76 +  (case term_of ct of
1.77 +    F as Collect \$ Abs (x, T, P) =>
1.78        (case extract_conj true [] P of
1.79          NONE => NONE
1.80        | SOME (_, eq, Q) =>
1.81            let val R = Collect \$ Abs (x, T, Data.conj \$ eq \$ Q)
1.82            in SOME (prove_conv tac ss (F, R)) end)
1.83 -  | rearrange_Collect _ _ _ = NONE;
1.84 +  | _ => NONE);
1.85
1.86  end;
```