# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256917029 -3600
# Node ID 1dd7f7f9804045a87fc2eeb1d327c8876a280e40
# Parent  7dec34d12328980951e7eef7860fddf5efab8f0c# Parent  6ed87b3d358c9d98393edede7b1ce23340ced40e
merged

diff -r 7dec34d12328 -r 1dd7f7f98040 FSet.thy
--- a/FSet.thy	Fri Oct 30 16:35:43 2009 +0100
+++ b/FSet.thy	Fri Oct 30 16:37:09 2009 +0100
@@ -169,9 +169,9 @@
 
 (* FIXME: does not work yet for all types*)
 quotient_def (for "'a fset")
-  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
-  "fmap \<equiv> (map::('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list)"
+  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
 term map
 term fmap
@@ -309,6 +309,7 @@
 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
 by (simp add: list_eq_refl)
 
+(* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
@@ -319,16 +320,18 @@
 
 thm fold1.simps(2)
 thm list.recs(2)
+thm list.cases
+
 
 ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
-(*  prove {* build_regularize_goal ind_r_a rty rel @{context} *}
+(*prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
   ML_prf {*  fun tac ctxt =
        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
          (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
          (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *}
-  apply (tactic {* tac @{context} 1 *}) *)
+  apply (tactic {* tac @{context} 1 *})*)
 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *}
 ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
diff -r 7dec34d12328 -r 1dd7f7f98040 QuotMain.thy
--- a/QuotMain.thy	Fri Oct 30 16:35:43 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 16:37:09 2009 +0100
@@ -447,106 +447,6 @@
 *}
 
 ML {*
-(* trm \<Rightarrow> new_trm *)
-fun regularise trm rty rel lthy =
-  case trm of
-    Abs (x, T, t) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of trm;
-        val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
-        val rabs_term = (rabs $ res_term) $ lam_term;
-      in
-        rabs_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-      in
-        Term.lambda_name (x, v) rec_term
-      end
-  | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of lam_term;
-        val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
-        val rall_term = (rall $ res_term) $ lam_term;
-      in
-        rall_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term
-      in
-        Const(@{const_name "All"}, at) $ lam_term
-      end
-  | ((Const (@{const_name "All"}, at)) $ P) =>
-      let
-        val (_, [al, _]) = dest_Type (fastype_of P);
-        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
-        val v = (Free (x, al));
-        val abs = Term.lambda_name (x, v) (P $ v);
-      in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
-  | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of lam_term;
-        val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
-        val rall_term = (rall $ res_term) $ lam_term;
-      in
-        rall_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term
-      in
-        Const(@{const_name "Ex"}, at) $ lam_term
-      end
-  | ((Const (@{const_name "Ex"}, at)) $ P) =>
-      let
-        val (_, [al, _]) = dest_Type (fastype_of P);
-        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
-        val v = (Free (x, al));
-        val abs = Term.lambda_name (x, v) (P $ v);
-      in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
-  | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
-  | _ => trm
-
-*}
-
-(* my version of regularise *)
-(****************************)
-
-(* some helper functions *)
-
-
-ML {*
 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
@@ -566,47 +466,51 @@
   | _ => f trm
 *}
 
-
-(* FIXME: assumes always the typ is qty! *)
 (* FIXME: if there are more than one quotient, then you have to look up the relation *)
 ML {*
-fun my_reg rel trm =
+fun my_reg lthy rel rty trm =
   case trm of
     Abs (x, T, t) =>
-       let 
-          val ty1 = fastype_of trm
-       in
-         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm)    
-       end
-  | Const (@{const_name "All"}, ty) $ t =>
-       let 
+       if (needs_lift rty T) then
+         let
+            val rrel = tyRel T rty rel lthy
+         in
+           (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
+         end
+       else
+         Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
+  | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
+       let
           val ty1 = domain_type ty
           val ty2 = domain_type ty1
+          val rrel = tyRel T rty rel lthy
        in
-         (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)      
+         if (needs_lift rty T) then
+           (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
+         else
+           Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
-  | Const (@{const_name "Ex"}, ty) $ t =>
-       let 
+  | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
+       let
           val ty1 = domain_type ty
           val ty2 = domain_type ty1
+          val rrel = tyRel T rty rel lthy
        in
-         (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    
+         if (needs_lift rty T) then
+           (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
+         else
+           Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
-  | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
+  | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
   | _ => trm
 *}
 
-
-(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
-  trm == new_trm
-*)
-
 text {* Assumes that the given theorem is atomized *}
 ML {*
   fun build_regularize_goal thm rty rel lthy =
      Logic.mk_implies
        ((prop_of thm),
-       (regularise (prop_of thm) rty rel lthy))
+       (my_reg lthy rel rty (prop_of thm)))
 *}
 
 ML {*