--- a/QuotMain.thy	Tue Sep 22 09:42:27 2009 +0200
+++ b/QuotMain.thy	Tue Sep 22 17:39:52 2009 +0200
@@ -607,16 +607,6 @@
 term UNION
 thm UNION_def
 
-(* Maybe the infrastructure should not allow this kind of definition, without showing that
-   the relation respects lenght... *)
-(* cu: what does this mean? *)
-local_setup {*
-  make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
-
-term length
-term CARD
-thm CARD_def
 
 thm QUOTIENT_fset
 
@@ -636,15 +626,131 @@
   using a by induct auto
 
 
+fun
+  card1 :: "'a list \<Rightarrow> nat"
+where
+  card1_nil: "(card1 []) = 0"
+| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
+
+local_setup {*
+  make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term card1
+term card
+thm card_def
+
+(* text {*
+ Maybe make_const_def should require a theorem that says that the particular lifted function
+ respects the relation. With it such a definition would be impossible:
+ make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*} *)
+
+lemma card1_rsp:
+  fixes a b :: "'a list"
+  assumes e: "a \<approx> b"
+  shows "card1 a = card1 b"
+  using e apply induct
+  apply (simp_all add:mem_respects)
+  done
+
+lemma card1_0:
+  fixes a :: "'a list"
+  shows "(card1 a = 0) = (a = [])"
+  apply (induct a)
+   apply (simp)
+  apply (simp_all)
+   apply meson
+  apply (simp_all)
+  done
+
+lemma not_mem_card1:
+  fixes x :: "'a"
+  fixes xs :: "'a list"
+  shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"
+  by simp
+
+
+lemma mem_cons:
+  fixes x :: "'a"
+  fixes xs :: "'a list"
+  assumes a : "x memb xs"
+  shows "x # xs \<approx> xs"
+  using a apply (induct xs)
+  apply (simp_all)
+  apply (meson)
+  apply (simp_all add: list_eq.intros(4))
+  proof -
+    fix a :: "'a"
+    fix xs :: "'a list"
+    assume a1 : "x # xs \<approx> xs"
+    assume a2 : "x memb xs"
+    have a3 : "x # a # xs \<approx> a # x # xs" using list_eq.intros(1)[of "x"] by blast
+    have a4 : "a # x # xs \<approx> a # xs" using a1 list_eq.intros(5)[of "x # xs" "xs"] by simp
+    then show "x # a # xs \<approx> a # xs" using a3 list_eq.intros(6) by blast
+  qed
+
+lemma card1_suc:
+  fixes xs :: "'a list"
+  fixes n :: "nat"
+  assumes c: "card1 xs = Suc n"
+  shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
+  using c apply (induct xs)
+   apply (simp)
+(*  apply (rule allI)*)
+  proof -
+    fix a :: "'a"
+    fix xs :: "'a list"
+    fix n :: "nat"
+    assume a1: "card1 xs = Suc n \<Longrightarrow> \<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys"
+    assume a2: "card1 (a # xs) = Suc n"
+    from a1 a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
+    apply -
+    apply (rule True_or_False [of "a memb xs", THEN disjE])
+    apply (simp_all add: card1_cons if_True simp_thms)
+  proof -
+    assume a1: "\<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys"
+    assume a2: "card1 xs = Suc n"
+    assume a3: "a memb xs"
+    from a1 obtain b ys where a5: "\<not> b memb ys \<and> xs \<approx> b # ys" by blast
+    from a2 a3 a5 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
+    apply -
+    apply (rule_tac x = "b" in exI)
+    apply (rule_tac x = "ys" in exI)
+    apply (simp_all)
+  proof -
+    assume a1: "a memb xs"
+    assume a2: "\<not> b memb ys \<and> xs \<approx> b # ys"
+    then have a3: "xs \<approx> b # ys" by simp
+    have "a # xs \<approx> xs" using a1 mem_cons[of "a" "xs"] by simp
+    then show "a # xs \<approx> b # ys" using a3 list_eq.intros(6) by blast
+  qed
+next
+  assume a2: "\<not> a memb xs"
+  from a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
+    apply -
+    apply (rule_tac x = "a" in exI)
+    apply (rule_tac x = "xs" in exI)
+    apply (simp)
+    apply (rule list_eq_sym)
+    done
+  qed
+qed
+
 lemma cons_preserves:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule QuotMain.list_eq.intros(5))
 
-(* cu: what does unlam do? *)
+
+text {*
+  unlam_def converts a definition theorem given as 'a = \lambda x. \lambda y. f (x y)'
+  to a theorem 'a x y = f (x, y)'. These are needed to rewrite right-to-left.
+*}
+
 ML {*
-fun unlam_def orig_ctxt ctxt t =
+fun unlam_def_aux orig_ctxt ctxt t =
   let val rhs = Thm.rhs_of t in
   (case try (Thm.dest_abs NONE) rhs of
     SOME (v, vt) =>
@@ -654,9 +760,11 @@
         val nv = Free(vnname, vt)
         val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv)
         val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2
-      in unlam_def orig_ctxt ctxt tnorm end
+      in unlam_def_aux orig_ctxt ctxt tnorm end
   | NONE => singleton (ProofContext.export ctxt orig_ctxt) t)
-  end
+  end;
+
+fun unlam_def ctxt t = unlam_def_aux ctxt ctxt t
 *}
 
 local_setup {*
@@ -666,7 +774,7 @@
 term membship
 term IN
 thm IN_def
-ML {* unlam_def @{context} @{context} @{thm IN_def} *}
+ML {* unlam_def @{context} @{thm IN_def} *}
 
 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
@@ -773,17 +881,20 @@
           end
       | build_aux x =
           if is_const x then maybe_mk_rep_abs x else x
-    val concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
+    val prems = (*map HOLogic.dest_Trueprop*) (Thm.prems_of thm);
+    val concl = (*HOLogic.dest_Trueprop*) (Thm.concl_of thm);
+    val concl2 = Logic.list_implies (prems, concl)
+(*    val concl2 = fold (fn a => fn c => HOLogic.mk_imp (a, c)) prems concl*)
   in
-  HOLogic.mk_eq ((build_aux concl), concl)
+  HOLogic.mk_eq ((build_aux concl2), concl2)
 end *}
 
-ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *}
-ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
-ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
-ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
-ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
-ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def CARD_def INSERT_def} *}
+ML {* val emptyt = (symmetric (unlam_def  @{context} @{thm EMPTY_def})) *}
+ML {* val in_t = (symmetric (unlam_def  @{context} @{thm IN_def})) *}
+ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *}
+ML {* val cardt =  symmetric (unlam_def @{context} @{thm card_def}) *}
+ML {* val insertt =  symmetric (unlam_def @{context} @{thm INSERT_def}) *}
+ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *}
 
 ML {*
@@ -863,11 +974,20 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 
+notation ( output) "prop" ("#_" [1000] 1000)
+
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (tactic {* print_tac "" *})
+  thm arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="]
+(*  apply (rule arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="])*)
+  apply (subst arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="])
   apply (tactic {* foo_tac' @{context} 1 *})
-  done
-
+  apply (tactic {* foo_tac' @{context} 1 *})
+  thm arg_cong2 [of "x memb []" "x memb []" False False "op ="]
+  (*apply (rule arg_cong2 [of "x memb []" "x memb []" False False "op ="])
+  done *)
+  sorry
 
 thm length_append (* Not true but worth checking that the goal is correct *)
 ML {*
@@ -878,7 +998,7 @@
 *}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* foo_tac' @{context} 1 *})
+(*  apply (tactic {* foo_tac' @{context} 1 *})*)
   sorry
 
 thm m2
@@ -890,8 +1010,8 @@
 *}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* foo_tac' @{context} 1 *})
-  done
+(*  apply (tactic {* foo_tac' @{context} 1 *})
+  done *) sorry
 
 thm list_eq.intros(4)
 ML {*
@@ -903,7 +1023,10 @@
 *}
 
 (* It is the same, but we need a name for it. *)
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
+  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (tactic {* foo_tac' @{context} 1 *})
+  sorry
 lemma zzz :
   "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))
     = (a # a # xs \<approx> a # xs)"
@@ -931,11 +1054,31 @@
   )
 *}
 
+thm sym
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm sym}))
+  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+*}
+ML {*
+  val cgoal = 
+    Toplevel.program (fn () =>
+      cterm_of @{theory} goal
+    )
+*}
+
+
 thm list_eq.intros(5)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
-  val cgoal = cterm_of @{theory} goal
+*}
+ML {*
+  val cgoal = 
+    Toplevel.program (fn () =>
+      cterm_of @{theory} goal
+    )
+*}
+ML {*
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
@@ -943,6 +1086,40 @@
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 
+
+thm list.induct
+ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *}
+
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct}))
+*}
+ML {*
+  val goal =
+    Toplevel.program (fn () =>
+      build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+    )
+*}
+ML {*
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+*}
+
+
+thm card1_suc
+
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc}))
+*}
+ML {*
+  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+*}
+ML {*
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+*}
+
+
+
 (*
 datatype obj1 =
   OVAR1 "string"