# HG changeset patch
# User boehmes
# Date 1273701231 -7200
# Node ID 3b6a8ecd3c88211aa5b4f09c84131aec97eaeb2d
# Parent  d8ea5bff3ca42bc4d1a627cb93bb955b7d12c1b9
simplified normalize_rule and moved it further down in the code

diff -r d8ea5bff3ca4 -r 3b6a8ecd3c88 src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:50 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:51 2010 +0200
@@ -26,104 +26,8 @@
 infix 2 ??
 fun (test ?? f) x = if test x then f x else x
 
-
-local
-  val all1 = @{lemma "All P == ALL x. P x" by (rule reflexive)}
-  val all2 = @{lemma "All == (%P. ALL x. P x)" by (rule reflexive)}
-  val ex1 = @{lemma "Ex P == EX x. P x" by (rule reflexive)}
-  val ex2 = @{lemma "Ex == (%P. EX x. P x)" by (rule reflexive)}
-  val let1 = @{lemma "Let c P == let x = c in P x" by (rule reflexive)}
-  val let2 = @{lemma "Let c == (%P. let x = c in P x)" by (rule reflexive)}
-  val let3 = @{lemma "Let == (%c P. let x = c in P x)" by (rule reflexive)}
-
-  fun all_abs_conv cv ctxt =
-    Conv.abs_conv (all_abs_conv cv o snd) ctxt else_conv cv ctxt
-  fun keep_conv ctxt = More_Conv.binder_conv norm_conv ctxt
-  and unfold_conv rule ctxt =
-    Conv.rewr_conv rule then_conv all_abs_conv keep_conv ctxt
-  and unfold_let_conv rule ctxt =
-    Conv.rewr_conv rule then_conv
-    all_abs_conv (fn cx => Conv.combination_conv
-      (Conv.arg_conv (norm_conv cx)) (Conv.abs_conv (norm_conv o snd) cx)) ctxt
-  and norm_conv ctxt ct =
-    (case Thm.term_of ct of
-      Const (@{const_name All}, _) $ Abs _ => keep_conv
-    | Const (@{const_name All}, _) $ _ => unfold_conv all1
-    | Const (@{const_name All}, _) => unfold_conv all2
-    | Const (@{const_name Ex}, _) $ Abs _ => keep_conv
-    | Const (@{const_name Ex}, _) $ _ => unfold_conv ex1
-    | Const (@{const_name Ex}, _) => unfold_conv ex2
-    | Const (@{const_name Let}, _) $ _ $ Abs _ => keep_conv
-    | Const (@{const_name Let}, _) $ _ $ _ => unfold_let_conv let1
-    | Const (@{const_name Let}, _) $ _ => unfold_let_conv let2
-    | Const (@{const_name Let}, _) => unfold_let_conv let3
-    | Abs _ => Conv.abs_conv (norm_conv o snd)
-    | _ $ _ => Conv.comb_conv o norm_conv
-    | _ => K Conv.all_conv) ctxt ct
-
-  fun is_normed t =
-    (case t of
-      Const (@{const_name All}, _) $ Abs (_, _, u) => is_normed u
-    | Const (@{const_name All}, _) $ _ => false
-    | Const (@{const_name All}, _) => false
-    | Const (@{const_name Ex}, _) $ Abs (_, _, u) => is_normed u
-    | Const (@{const_name Ex}, _) $ _ => false
-    | Const (@{const_name Ex}, _) => false
-    | Const (@{const_name Let}, _) $ u1 $ Abs (_, _, u2) =>
-        is_normed u1 andalso is_normed u2
-    | Const (@{const_name Let}, _) $ _ $ _ => false
-    | Const (@{const_name Let}, _) $ _ => false
-    | Const (@{const_name Let}, _) => false
-    | Abs (_, _, u) => is_normed u
-    | u1 $ u2 => is_normed u1 andalso is_normed u2
-    | _ => true)
-in
-fun norm_binder_conv ctxt ct =
-  if is_normed (Thm.term_of ct) then Conv.all_conv ct else norm_conv ctxt ct
-end
-
-fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
-fun norm_meta_def cv thm = 
-  let val thm' = Thm.combination thm (Thm.reflexive cv)
-  in Thm.transitive thm' (Thm.beta_conversion false (Thm.rhs_of thm')) end
-
-fun norm_def ctxt thm =
-  (case Thm.prop_of thm of
-    Const (@{const_name "=="}, _) $ _ $ Abs (_, T, _) =>
-      let val v = Var ((Name.uu, #maxidx (Thm.rep_thm thm) + 1), T)
-      in norm_def ctxt (norm_meta_def (cert ctxt v) thm) end
-  | @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
-      norm_def ctxt (thm RS @{thm fun_cong})
-  | _ => thm)
-
-fun atomize_conv ctxt ct =
-  (case Thm.term_of ct of
-    @{term "op ==>"} $ _ $ _ =>
-      Conv.binop_conv (atomize_conv ctxt) then_conv
-      Conv.rewr_conv @{thm atomize_imp}
-  | Const (@{const_name "=="}, _) $ _ $ _ =>
-      Conv.binop_conv (atomize_conv ctxt) then_conv
-      Conv.rewr_conv @{thm atomize_eq}
-  | Const (@{const_name all}, _) $ Abs _ =>
-      More_Conv.binder_conv atomize_conv ctxt then_conv
-      Conv.rewr_conv @{thm atomize_all}
-  | _ => Conv.all_conv) ct
-
-fun unfold_quants_conv ctxt =
-  let
-    val rules = [@{thm Ex1_def}, @{thm Ball_def}, @{thm Bex_def}]
-    val unfold_conv = Conv.try_conv (More_Conv.rewrs_conv rules)
-  in More_Conv.top_conv (K unfold_conv) ctxt end
-
-fun normalize_rule ctxt =
-  Conv.fconv_rule (
-    Thm.beta_conversion true then_conv
-    Thm.eta_conversion then_conv
-    norm_binder_conv ctxt) #>
-  norm_def ctxt #>
-  Drule.forall_intr_vars #>
-  Conv.fconv_rule (atomize_conv ctxt)
+fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
+fun if_true_conv c cv = if_conv c cv Conv.all_conv
 
 fun instantiate_free (cv, ct) =
   (Term.exists_subterm (equal (Thm.term_of cv)) o Thm.prop_of) ??
@@ -137,9 +41,6 @@
     |> (fn thm => Thm.implies_elim thm (Thm.reflexive cu))
   end
 
-fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
-fun if_true_conv c cv = if_conv c cv Conv.all_conv
-
 
 
 (* simplification of trivial let expressions (whose bound variables occur at
@@ -353,6 +254,95 @@
 
 
 
+(* further normalizations: beta/eta, universal closure, atomize *)
+
+local
+  val all1 = @{lemma "All P == ALL x. P x" by (rule reflexive)}
+  val all2 = @{lemma "All == (%P. ALL x. P x)" by (rule reflexive)}
+  val ex1 = @{lemma "Ex P == EX x. P x" by (rule reflexive)}
+  val ex2 = @{lemma "Ex == (%P. EX x. P x)" by (rule reflexive)}
+  val let1 = @{lemma "Let c P == let x = c in P x" by (rule reflexive)}
+  val let2 = @{lemma "Let c == (%P. let x = c in P x)" by (rule reflexive)}
+  val let3 = @{lemma "Let == (%c P. let x = c in P x)" by (rule reflexive)}
+
+  fun all_abs_conv cv ctxt =
+    Conv.abs_conv (all_abs_conv cv o snd) ctxt else_conv cv ctxt
+  fun keep_conv ctxt = More_Conv.binder_conv norm_conv ctxt
+  and unfold_conv rule ctxt =
+    Conv.rewr_conv rule then_conv all_abs_conv keep_conv ctxt
+  and unfold_let_conv rule ctxt =
+    Conv.rewr_conv rule then_conv
+    all_abs_conv (fn cx => Conv.combination_conv
+      (Conv.arg_conv (norm_conv cx)) (Conv.abs_conv (norm_conv o snd) cx)) ctxt
+  and norm_conv ctxt ct =
+    (case Thm.term_of ct of
+      Const (@{const_name All}, _) $ Abs _ => keep_conv
+    | Const (@{const_name All}, _) $ _ => unfold_conv all1
+    | Const (@{const_name All}, _) => unfold_conv all2
+    | Const (@{const_name Ex}, _) $ Abs _ => keep_conv
+    | Const (@{const_name Ex}, _) $ _ => unfold_conv ex1
+    | Const (@{const_name Ex}, _) => unfold_conv ex2
+    | Const (@{const_name Let}, _) $ _ $ Abs _ => keep_conv
+    | Const (@{const_name Let}, _) $ _ $ _ => unfold_let_conv let1
+    | Const (@{const_name Let}, _) $ _ => unfold_let_conv let2
+    | Const (@{const_name Let}, _) => unfold_let_conv let3
+    | Abs _ => Conv.abs_conv (norm_conv o snd)
+    | _ $ _ => Conv.comb_conv o norm_conv
+    | _ => K Conv.all_conv) ctxt ct
+
+  fun is_normed t =
+    (case t of
+      Const (@{const_name All}, _) $ Abs (_, _, u) => is_normed u
+    | Const (@{const_name All}, _) $ _ => false
+    | Const (@{const_name All}, _) => false
+    | Const (@{const_name Ex}, _) $ Abs (_, _, u) => is_normed u
+    | Const (@{const_name Ex}, _) $ _ => false
+    | Const (@{const_name Ex}, _) => false
+    | Const (@{const_name Let}, _) $ u1 $ Abs (_, _, u2) =>
+        is_normed u1 andalso is_normed u2
+    | Const (@{const_name Let}, _) $ _ $ _ => false
+    | Const (@{const_name Let}, _) $ _ => false
+    | Const (@{const_name Let}, _) => false
+    | Abs (_, _, u) => is_normed u
+    | u1 $ u2 => is_normed u1 andalso is_normed u2
+    | _ => true)
+in
+fun norm_binder_conv ctxt = if_conv is_normed Conv.all_conv (norm_conv ctxt)
+end
+
+fun norm_def ctxt thm =
+  (case Thm.prop_of thm of
+    @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
+      norm_def ctxt (thm RS @{thm fun_cong})
+  | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
+      norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
+  | _ => thm)
+
+fun atomize_conv ctxt ct =
+  (case Thm.term_of ct of
+    @{term "op ==>"} $ _ $ _ =>
+      Conv.binop_conv (atomize_conv ctxt) then_conv
+      Conv.rewr_conv @{thm atomize_imp}
+  | Const (@{const_name "=="}, _) $ _ $ _ =>
+      Conv.binop_conv (atomize_conv ctxt) then_conv
+      Conv.rewr_conv @{thm atomize_eq}
+  | Const (@{const_name all}, _) $ Abs _ =>
+      More_Conv.binder_conv atomize_conv ctxt then_conv
+      Conv.rewr_conv @{thm atomize_all}
+  | _ => Conv.all_conv) ct
+
+fun normalize_rule ctxt =
+  Conv.fconv_rule (
+    (* reduce lambda abstractions, except at known binders: *)
+    Thm.beta_conversion true then_conv
+    Thm.eta_conversion then_conv
+    norm_binder_conv ctxt) #>
+  norm_def ctxt #>
+  Drule.forall_intr_vars #>
+  Conv.fconv_rule (atomize_conv ctxt)
+
+
+
 (* lift lambda terms into additional rules *)
 
 local
@@ -361,6 +351,12 @@
   fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
   fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
 
+  fun norm_meta_def cv thm = 
+    let val thm' = Thm.combination thm (Thm.reflexive cv)
+    in Thm.transitive thm' (Thm.beta_conversion false (Thm.rhs_of thm')) end
+
+  fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
+
   val fresh_name = yield_singleton Name.variants
 
   fun used_vars cvs ct =