src/HOL/Tools/SMT/smt_translate.ML
changeset 37124 fe22fc54b876
parent 36899 bcd6fce5bf06
child 39298 5aefb5bc8a93
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed May 26 11:59:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed May 26 15:34:47 2010 +0200
     1.3 @@ -119,13 +119,19 @@
     1.4        if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
     1.5    | group_quant _ Ts t = (Ts, t)
     1.6  
     1.7 -fun dest_pat ts (Const (@{const_name pat}, _) $ t) = SPat (rev (t :: ts))
     1.8 -  | dest_pat ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (t :: ts))
     1.9 -  | dest_pat ts (Const (@{const_name andpat}, _) $ p $ t) = dest_pat (t::ts) p
    1.10 -  | dest_pat _ t = raise TERM ("dest_pat", [t])
    1.11 +fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
    1.12 +  | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
    1.13 +  | dest_pat t = raise TERM ("dest_pat", [t])
    1.14 +
    1.15 +fun dest_pats [] = I
    1.16 +  | dest_pats ts =
    1.17 +      (case map dest_pat ts |> split_list ||> distinct (op =) of
    1.18 +        (ps, [true]) => cons (SPat ps)
    1.19 +      | (ps, [false]) => cons (SNoPat ps)
    1.20 +      | _ => raise TERM ("dest_pats", ts))
    1.21  
    1.22  fun dest_trigger (@{term trigger} $ tl $ t) =
    1.23 -      (map (dest_pat []) (HOLogic.dest_list tl), t)
    1.24 +      (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
    1.25    | dest_trigger t = ([], t)
    1.26  
    1.27  fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
    1.28 @@ -143,9 +149,9 @@
    1.29  
    1.30  (* enforce a strict separation between formulas and terms *)
    1.31  
    1.32 -val term_eq_rewr = @{lemma "x term_eq y == x = y" by (simp add: term_eq_def)}
    1.33 +val term_eq_rewr = @{lemma "term_eq x y == x = y" by (simp add: term_eq_def)}
    1.34  
    1.35 -val term_bool = @{lemma "~(True term_eq False)" by (simp add: term_eq_def)}
    1.36 +val term_bool = @{lemma "~(term_eq True False)" by (simp add: term_eq_def)}
    1.37  val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
    1.38  
    1.39  
    1.40 @@ -210,11 +216,10 @@
    1.41  
    1.42      and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
    1.43        | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
    1.44 -      | in_pat ((c as Const (@{const_name andpat}, _)) $ p $ t) =
    1.45 -          c $ in_pat p $ in_term t
    1.46        | in_pat t = raise TERM ("in_pat", [t])
    1.47  
    1.48 -    and in_pats p = in_list @{typ pattern} in_pat p
    1.49 +    and in_pats ps =
    1.50 +      in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
    1.51  
    1.52      and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
    1.53        | in_trig t = in_form t