# HG changeset patch
# User boehmes
# Date 1256120386 -7200
# Node ID 69780aef0531f5750f36212f39c513bfaeb1efe1
# Parent  cffdb7b2849864084a9df96fb0b70fe9f328a835
proper handling of single literal case,
added explicit exception,
unfolding of distinct respects equal elements,
made SML/NJ happy

diff -r cffdb7b28498 -r 69780aef0531 src/HOL/SMT/Tools/smt_monomorph.ML
--- a/src/HOL/SMT/Tools/smt_monomorph.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_monomorph.ML	Wed Oct 21 12:19:46 2009 +0200
@@ -32,7 +32,7 @@
 fun consts_of ts = AList.group (op =) (fold Term.add_consts ts [])
   |> filter_out (ignored o fst)
 
-val join_consts = curry (AList.join (op =) (K (merge (op =))))
+fun join_consts cs ds = AList.join (op =) (K (merge (op =))) (cs, ds)
 fun diff_consts cs ds = 
   let fun diff (n, Ts) =
     (case AList.lookup (op =) cs n of
@@ -55,7 +55,7 @@
 fun proper_match ps env =
   forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps
 
-val eq_tab = eq_set (op =) o pairself Vartab.dest
+fun eq_tab (tab1, tab2) = eq_set (op =) (Vartab.dest tab1, Vartab.dest tab2)
 
 fun specialize thy cs is ((r, ps), ces) (ts, ns) =
   let
diff -r cffdb7b28498 -r 69780aef0531 src/HOL/SMT/Tools/z3_model.ML
--- a/src/HOL/SMT/Tools/z3_model.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_model.ML	Wed Oct 21 12:19:46 2009 +0200
@@ -82,12 +82,12 @@
 fun spaced p = p --| space
 
 val key = spaced (lift name) #-> lift' ident
-val mapping = spaced (this "->")
+fun mapping st = spaced (this "->") st
 fun in_braces p = spaced ($$ "{") |-- p --| spaced ($$ "}")
 
-val bool_expr =
-  this "true" >> K @{term True} ||
-  this "false" >> K @{term False}
+fun bool_expr st =
+ (this "true" >> K @{term True} ||
+  this "false" >> K @{term False}) st
 
 fun number_expr T =
   let
@@ -95,7 +95,7 @@
     fun frac n d = Const (@{const_name divide}, T --> T --> T) $ n $ d
   in num :|-- (fn n => Scan.optional ($$ "/" |-- num >> frac n) n) end
 
-val value = this "val!" |-- lift nat_num
+fun value st = (this "val!" |-- lift nat_num) st
 fun value_expr T = value #-> lift' (get_value T)
 
 val domT = Term.domain_type
diff -r cffdb7b28498 -r 69780aef0531 src/HOL/SMT/Tools/z3_proof.ML
--- a/src/HOL/SMT/Tools/z3_proof.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_proof.ML	Wed Oct 21 12:19:46 2009 +0200
@@ -192,9 +192,11 @@
 
 val variables =
   par (this "vars" |-- bsep1 (par ((lift name >> K "x") --| blank -- sort)))
-val patterns = bsep (par ((this ":pat" || this ":nopat") |-- bsep1 (lift id)))
-val quant_kind =
-  this "forall" >> K T.mk_forall || this "exists" >> K T.mk_exists
+fun patterns st =
+  bsep (par ((this ":pat" || this ":nopat") |-- bsep1 (lift id))) st
+fun quant_kind st =
+ (this "forall" >> K T.mk_forall ||
+  this "exists" >> K T.mk_exists) st
 fun quantifier thy = par (quant_kind --| blank --
   variables --| patterns --| blank -- arg thy) >>
   (fn ((q, vs), body) => fold_rev (q thy) vs body)
diff -r cffdb7b28498 -r 69780aef0531 src/HOL/SMT/Tools/z3_proof_rules.ML
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Wed Oct 21 12:19:46 2009 +0200
@@ -386,52 +386,55 @@
 
   datatype conj_disj = CONJ | DISJ | NCON | NDIS
   fun kind_of t =
-    if is_conj t then CONJ
-    else if is_disj t then DISJ
-    else if is_neg' is_conj t then NCON
-    else if is_neg' is_disj t then NDIS
-    else CONJ (*allows to prove equalities with single literals on each side*)
+    if is_conj t then SOME CONJ
+    else if is_disj t then SOME DISJ
+    else if is_neg' is_conj t then SOME NCON
+    else if is_neg' is_disj t then SOME NDIS
+    else NONE
 in
 fun prove_conj_disj_eq ct =
   let val cp = Thm.dest_binop ct
   in
     (case pairself (kind_of o Thm.term_of) cp of
-      (CONJ, CONJ) => prove_eq true true cp
-    | (CONJ, NDIS) => prove_eq true false cp
-    | (DISJ, DISJ) => contrapos1 (prove_eq false false) cp
-    | (DISJ, NCON) => contrapos2 (prove_eq false true) cp
-    | (NCON, NCON) => contrapos1 (prove_eq true true) cp
-    | (NCON, DISJ) => contrapos3 (prove_eq true false) cp
-    | (NDIS, NDIS) => prove_eq false false cp
-    | (NDIS, CONJ) => prove_eq false true cp)
+      (SOME CONJ, SOME CONJ) => prove_eq true true cp
+    | (SOME CONJ, SOME NDIS) => prove_eq true false cp
+    | (SOME CONJ, NONE) => prove_eq true true cp
+    | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp
+    | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp
+    | (SOME DISJ, NONE) => contrapos1 (prove_eq false false) cp
+    | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp
+    | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp
+    | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp
+    | (SOME NDIS, SOME NDIS) => prove_eq false false cp
+    | (SOME NDIS, SOME CONJ) => prove_eq false true cp
+    | (SOME NDIS, NONE) => prove_eq false true cp
+    | _ => raise CTERM ("prove_conj_disj_eq", [ct]))
   end
 end
 
 (** unfolding of distinct **)
 
 local
-  val distinct1 = @{lemma "distinct [] == ~False" by simp}
-  val distinct2 = @{lemma "distinct [x] == ~False" by simp}
-  val distinct3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
+  val set1 = @{lemma "x ~: set [] == ~False" by simp}
+  val set2 = @{lemma "x ~: set [x] == False" by simp}
+  val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
+  val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
+  val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
+
+  fun set_conv ct =
+    (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
+    (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
+
+  val dist1 = @{lemma "distinct [] == ~False" by simp}
+  val dist2 = @{lemma "distinct [x] == ~False" by simp}
+  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
     by simp}
 
-  val set1 = @{lemma "x ~: set [] == ~False" by simp}
-  val set2 = @{lemma "x ~: set [y] == x ~= y" by simp}
-  val set3 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
-
   fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
-
-  fun unfold_conv rule1 rule2 rule3 sub_conv =
-    let
-      fun uconv ct =
-       (Conv.rewr_conv rule1 else_conv
-        Conv.rewr_conv rule2 else_conv
-       (Conv.rewr_conv rule3 then_conv binop_conv sub_conv uconv)) ct
-    in uconv end
-
-  val set_conv = unfold_conv set1 set2 set3 Conv.all_conv
 in
-val unfold_distinct_conv = unfold_conv distinct1 distinct2 distinct3 set_conv
+fun unfold_distinct_conv ct =
+  (More_Conv.rewrs_conv [dist1, dist2] else_conv
+  (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
 end
 
 
diff -r cffdb7b28498 -r 69780aef0531 src/HOL/SMT/Tools/z3_proof_terms.ML
--- a/src/HOL/SMT/Tools/z3_proof_terms.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_terms.ML	Wed Oct 21 12:19:46 2009 +0200
@@ -143,8 +143,8 @@
     fun dec (i, v) = if i = 0 then NONE else SOME (i - 1, v)
   in mk_preterm (Thm.capply cq (Thm.cabs cv ct), map_filter dec vs) end
 in
-val mk_forall = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat All})
-val mk_exists = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat Ex})
+fun mk_forall thy = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat All}) thy
+fun mk_exists thy = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat Ex}) thy
 end