# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1251214670 -7200
# Node ID eac147a5eb330f33da74688033715d36d0bb5286
# Parent  54afbcf2a758c258b3b3bd7439e7c93dfd4f5080
Changed to the use of "modern interface"
  (removed the _cmd and passing of strings)

Fixed Trueprop handling and the first proof starts working properly.

diff -r 54afbcf2a758 -r eac147a5eb33 QuotMain.thy
--- a/QuotMain.thy	Tue Aug 25 14:37:11 2009 +0200
+++ b/QuotMain.thy	Tue Aug 25 17:37:50 2009 +0200
@@ -543,6 +543,40 @@
 
 thm QUOTIENT_fset
 
+(* 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_i = [((Locale.intern @{theory} "QUOT_TYPE"),(("QUOT_TYPE_fset_i", true),
+  Expression.Named [
+   ("R",@{term list_eq}),
+   ("Abs",@{term Abs_fset}),
+   ("Rep",@{term Rep_fset})
+  ]))] *}
+ML {* val bindd = ((Binding.make ("",Position.none)),([]:Attrib.src list)) *}
+ML {* val eqn1i = (bindd, @{prop "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset"}) *}
+ML {* val eqn2i = (bindd, @{prop "QUOT_TYPE.REP Rep_fset = REP_fset"}) *}
+setup {* fn thy => ProofContext.theory_of
+  (bymt (Expression.interpretation (exp_i, []) [eqn2i,eqn1i] 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
+*)
+
+
+
 fun 
   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _")
 where
@@ -550,18 +584,20 @@
 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
 
 lemma mem_respects:
-  fixes z::"nat"
+  fixes z
   assumes a: "list_eq x y"
-  shows "z memb x = z memb y"
+  shows "(z memb x) = (z memb y)"
 using a
 apply(induct)
 apply(auto)
 done
 
 
-local_setup {*
+definition "IN x xa \<equiv> x memb REP_fset xa"
+
+(*local_setup {*
   make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+*}*)
 
 term membship
 term IN
@@ -575,8 +611,7 @@
 unfolding IN_def EMPTY_def
 apply(rule_tac f="(op =) False" in arg_cong)
 apply(rule mem_respects)
-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.intros)
 done
 
@@ -610,38 +645,6 @@
   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 "
     (
@@ -694,7 +697,7 @@
           else ((build_aux f) $ (build_aux a)))
       | build_aux x =
           if is_const x then mk_rep_abs x else x
-    val concl = Thm.concl_of thm
+    val concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
   in
   HOLogic.mk_eq ((build_aux concl), concl)
 end *}
@@ -714,4 +717,17 @@
 *}
 
 ML {* val emptyt = symmetric @{thm EMPTY_def} *}
-ML {* MetaSimplifier.rewrite false [emptyt] cgoal *}
+ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *}
+
+ML {* val in_t = (symmetric @{thm IN_def}) *}
+ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *}
+
+(*theorem "(IN x EMPTY = False) = (x memb [] = False)"*)
+
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
+apply(rule_tac f="(op =)" in arg_cong2)
+unfolding IN_def EMPTY_def
+apply (rule_tac mem_respects)
+apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+
+