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;