# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262976382 -3600
# Node ID 89d772dae4d40b97780f2a23072a413897ad454c
# Parent  42b90994ac77e5040e2fdc2f6534c7de5b872e9d
New_relations, all works again including concat examples.

diff -r 42b90994ac77 -r 89d772dae4d4 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Fri Jan 08 15:02:12 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Jan 08 19:46:22 2010 +0100
@@ -77,32 +77,28 @@
 
 text {* raw section *}
 
-lemma nil_not_cons: 
-  shows "\<not>[] \<approx> x # xs" 
-by auto
+lemma nil_not_cons:
+  shows "\<not>[] \<approx> x # xs"
+  by auto
 
 lemma memb_cons_iff:
   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
-by (induct xs) (auto simp add: memb_def)
+  by (induct xs) (auto simp add: memb_def)
 
 lemma memb_consI1:
   shows "memb x (x # xs)"
-by (simp add: memb_def)
+  by (simp add: memb_def)
 
-lemma memb_consI2: 
+lemma memb_consI2:
   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
   by (simp add: memb_def)
 
 lemma memb_absorb:
-  shows "memb x xs \<Longrightarrow> (x # xs) \<approx> xs"
-by (induct xs) (auto simp add: memb_def)
+  shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
+  by (induct xs) (auto simp add: memb_def id_simps)
 
 text {* lifted section *}
 
-lemma fempty_not_finsert[simp]:
-  shows "{||} \<noteq> finsert x S"
-by (lifting nil_not_cons)
-
 lemma fin_finsert_iff[simp]:
   "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
 by (lifting memb_cons_iff) 
@@ -112,9 +108,10 @@
   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
   by (lifting memb_consI1, lifting memb_consI2)
 
+
 lemma finsert_absorb [simp]: 
   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
-by (lifting memb_absorb)
+  by (lifting memb_absorb)
 
 
 section {* Singletons *}
@@ -123,18 +120,22 @@
 
 lemma singleton_list_eq:
   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
-by auto
+  by (simp add: id_simps) auto
 
 text {* lifted section *}
 
+lemma fempty_not_finsert[simp]:
+  shows "{||} \<noteq> finsert x S"
+  by (lifting nil_not_cons)
+
 lemma fsingleton_eq[simp]:
   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
-by (lifting singleton_list_eq)
+  by (lifting singleton_list_eq)
 
 section {* Union *}
 
 quotient_definition
-   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
 as
   "op @"
 
@@ -244,21 +245,21 @@
 (* concat.simps(1) and concat.simps(2) contain the    *)
 (* type variables ?'a1.0 (which are turned into frees *)
 (* 'a_1                                               *)
-lemma concat1: 
+lemma concat1:
   shows "concat [] \<approx> []"
-by (simp)
+by (simp add: id_simps)
 
-lemma concat2: 
-  shows "concat (x # xs) \<approx>  x @ concat xs"
-by (simp)
+lemma concat2:
+  shows "concat (x # xs) \<approx> x @ concat xs"
+by (simp add: id_simps)
 
 lemma concat_rsp[quot_respect]:
   shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat"
 sorry
 
 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []"
-apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
-done
+  apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
+  done
 
 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
   apply (rule eq_reflection)
@@ -350,22 +351,25 @@
 apply(rule refl)
 done
 
+(* Should be true *)
+
+lemma insert_rsp2[quot_respect]:
+  "(op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) op # op #"
+apply auto
+apply (simp add: set_in_eq)
+sorry
+
+lemma append_rsp[quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
+  by (auto)
+
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
 apply(lifting concat2)
-apply(injection)
-(* The Relation is wrong to apply rep_abs_rsp *)
-thm rep_abs_rsp[of "(op \<approx> ===> op =)"]
-defer
-apply (simp only: finsert_def[simplified id_simps])
-apply (simp only: fconcat_def[simplified id_simps])
 apply(cleaning)
-(* finsert_def doesn't get folded, since rep-abs types are incorrect *)
-apply(simp add: comp_def)
-apply (simp add: fconcat_def[simplified id_simps])
+apply (simp add: finsert_def fconcat_def comp_def)
 apply cleaning
-(* The Relation is wrong again. *)
-sorry
+done
 
 text {* raw section *}
 
@@ -493,13 +497,13 @@
   "a \<in> set A \<Longrightarrow> a # A \<approx> A"
 by auto
 
-lemma cons_left_comm: 
-  "x #y # A \<approx> y # x # A"
-by auto
+lemma cons_left_comm:
+  "x # y # A \<approx> y # x # A"
+by (auto simp add: id_simps)
 
-lemma cons_left_idem: 
+lemma cons_left_idem:
   "x # x # A \<approx> x # A"
-by auto
+by (auto simp add: id_simps)
 
 lemma finite_set_raw_strong_cases:
   "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
@@ -593,10 +597,6 @@
 apply(auto)
 sorry
 
-lemma append_rsp[quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-by auto
-
 primrec
   inter_raw
 where
diff -r 42b90994ac77 -r 89d772dae4d4 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Jan 08 15:02:12 2010 +0100
+++ b/Quot/quotient_def.ML	Fri Jan 08 19:46:22 2010 +0100
@@ -40,7 +40,7 @@
 let
   val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
   val qconst_bname = Binding.name lhs_str;
-  val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs
+  val absrep_trm = Syntax.check_term lthy (absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs)
   val prop = Logic.mk_equals (lhs, absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop
   val (_, newrhs) = Primitive_Defs.abs_def prop'
diff -r 42b90994ac77 -r 89d772dae4d4 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Jan 08 15:02:12 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 08 19:46:22 2010 +0100
@@ -187,8 +187,9 @@
              val map_fun = mk_mapfun ctxt vs rty_pat       
              val result = list_comb (map_fun, args) 
            in
-             mk_fun_compose flag (absrep_const flag ctxt s', result)
-           end 
+             if tys' = [] orelse tys' = tys then absrep_const flag ctxt s'
+             else mk_fun_compose flag (absrep_const flag ctxt s', result)
+           end
     | (TFree x, TFree x') =>
         if x = x'
         then mk_identity rty
@@ -289,8 +290,9 @@
            val eqv_rel = get_equiv_rel ctxt s'
            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
          in
-           mk_rel_compose (result, eqv_rel')
-         end  
+           if tys' = [] orelse tys' = tys then eqv_rel'
+           else mk_rel_compose (result, eqv_rel')
+         end
       | _ => HOLogic.eq_const rty
 
 fun new_equiv_relation_chk ctxt (rty, qty) =
@@ -386,7 +388,7 @@
          val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
        in
          if ty = ty' then subtrm
-         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
+         else mk_babs $ (mk_resp $ new_equiv_relation ctxt (ty, ty')) $ subtrm
        end
 
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
@@ -394,7 +396,7 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
-         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_ball $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
@@ -402,22 +404,26 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
-         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_bex $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (* equalities need to be replaced by appropriate equivalence relations *) 
     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
          if ty = ty' then rtrm
-         else equiv_relation ctxt (domain_type ty, domain_type ty') 
+         else new_equiv_relation ctxt (domain_type ty, domain_type ty') 
 
   | (* in this case we just check whether the given equivalence relation is correct *) 
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
-         val exc = LIFT_MATCH "regularise (relation mismatch)"
+         fun exc rel rel' = LIFT_MATCH ("regularise (relation mismatch)\n[" ^
+           Syntax.string_of_term ctxt rel ^ " :: " ^
+           Syntax.string_of_typ ctxt (fastype_of rel) ^ "]\n[" ^
+           Syntax.string_of_term ctxt rel' ^ " :: " ^
+           Syntax.string_of_typ ctxt (fastype_of rel') ^ "]")
          val rel_ty = fastype_of rel
-         val rel' = equiv_relation ctxt (domain_type rel_ty, domain_type ty') 
+         val rel' = new_equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') 
        in 
-         if rel' aconv rel then rtrm else raise exc
+         if rel' aconv rel then rtrm else raise (exc rel rel')
        end  
 
   | (_, Const _) =>