--- a/QuotMain.thy	Tue Aug 25 00:30:23 2009 +0200
+++ b/QuotMain.thy	Tue Aug 25 10:35:28 2009 +0200
@@ -533,6 +533,14 @@
 term UNION
 thm UNION_def
 
+local_setup {*
+  make_const_def "CARD" @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term length
+term CARD
+thm CARD_def
+
 thm QUOTIENT_fset
 
 fun 
@@ -593,7 +601,7 @@
 apply(rule list_eq_sym)
 done
 
-lemma helper:
+lemma append_respects_fst:
   assumes a : "list_eq l1 l2"  
   shows "list_eq (l1 @ s) (l2 @ s)"
   using a
@@ -602,6 +610,38 @@
   apply(simp add: list_eq_sym)
 done
 
+(* This code builds the interpretation from ML level, currently only
+   for fset *)
+
+ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN
+  simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def[symmetric]}) 1 THEN
+  simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def[symmetric]}) 1) *}
+ML {* val mthdt = Method.Basic (fn _ => mthd) *}
+ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *}
+ML {* val exp = [("QUOT_TYPE",(("QUOT_TYPE_fset_i", true),
+  Expression.Named [
+   ("R","list_eq"),
+   ("Abs","Abs_fset"),
+   ("Rep","Rep_fset")
+  ]))] *}
+ML {* val bindd = ((Binding.make ("",Position.none)),([]:Attrib.src list)) *}
+ML {* val eqn1 = (bindd, "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset") *}
+ML {* val eqn2 = (bindd, "QUOT_TYPE.REP Rep_fset = REP_fset") *}
+setup {* fn thy => ProofContext.theory_of
+  (bymt (Expression.interpretation_cmd (exp, []) [eqn2,eqn1] thy)) *}
+
+(* It is eqivalent to the below:
+
+interpretation QUOT_TYPE_fset_i: QUOT_TYPE list_eq Abs_fset Rep_fset
+  where "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset"
+    and "QUOT_TYPE.REP Rep_fset = REP_fset"
+  unfolding ABS_fset_def REP_fset_def
+  apply (rule QUOT_TYPE_fset)
+  apply (simp only: ABS_fset_def[symmetric])
+  apply (simp only: REP_fset_def[symmetric])
+  done
+*)
+
 lemma yyy :
   shows "
     (
@@ -614,39 +654,27 @@
   unfolding UNION_def EMPTY_def INSERT_def
   apply(rule_tac f="(op &)" in arg_cong2)
   apply(rule_tac f="(op =)" in arg_cong2)
-  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,
-                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
-  apply(rule helper)
-  apply(rule list_eq.intros(3))
-  apply(simp only:QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
-                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
+  apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
+  apply(rule append_respects_fst)
+  apply(simp only:QUOT_TYPE_fset_i.REP_ABS_rsp)
   apply(rule list_eq_sym)
   apply(simp)
   apply(rule_tac f="(op =)" in arg_cong2)
-  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
-                  simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
-  apply(rule helper)
-  apply(rule list_eq.intros(3))
-  apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset,
-                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
+  apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
+  apply(rule append_respects_fst)
+  apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
   apply(rule list_eq_sym)
-  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
-                     simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
+  apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
   apply(rule list_eq.intros(5))
-  apply(rule list_eq.intros(3))
-  apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
-                 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
+  apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
   apply(rule list_eq_sym)
 done
 
 lemma
   shows "
-    (
      (UNION EMPTY s = s) &
-     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
-    )"
-  apply(simp add:yyy)
-  apply (unfold REP_fset_def ABS_fset_def)
-  apply (rule QUOT_TYPE.thm10[OF QUOT_TYPE_fset])
-done
+     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
+  apply (simp add: yyy)
+  apply (rule QUOT_TYPE_fset_i.thm10)
+  done