# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271662073 -7200
# Node ID d360a26fa790ccacb97e52ff6f2636526081358f
# Parent  869d1183e0823789eb742cb7910a0976a34ce780# Parent  c22947214948334758da2e8e02f609cc87b58eda
merged

diff -r 869d1183e082 -r d360a26fa790 Attic/Quot/Examples/FSet3.thy
--- a/Attic/Quot/Examples/FSet3.thy	Mon Apr 19 09:25:31 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Mon Apr 19 09:27:53 2010 +0200
@@ -245,12 +245,6 @@
 is
  "concat"
 
-(*lemma fconcat_rsp[quot_respect]:
-  shows "((list_rel op \<approx>) ===> op \<approx>) concat concat"
-apply(auto)
-sorry
-*)
-
 (* PROBLEM: these lemmas needs to be restated, since  *)
 (* concat.simps(1) and concat.simps(2) contain the    *)
 (* type variables ?'a1.0 (which are turned into frees *)
@@ -263,9 +257,21 @@
   shows "concat (x # xs) \<approx> x @ concat xs"
 by (simp)
 
-lemma concat_rsp[quot_respect]:
+lemma concat_rsp:
+  "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y\<rbrakk> \<Longrightarrow> concat x \<approx> concat y"
+  apply (induct x y arbitrary: x' y' rule: list_induct2')
+  apply simp
+  defer defer
+  apply (simp only: concat.simps)
+  sorry
+
+lemma [quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-  sorry
+  apply (simp only: fun_rel_def)
+  apply clarify
+  apply (rule concat_rsp)
+  apply assumption+
+  done
 
 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
   apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
@@ -360,8 +366,6 @@
   apply(rule refl)
   done
 
-(* Should be true *)
-
 lemma insert_rsp2[quot_respect]:
   "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
   apply auto
@@ -709,19 +713,4 @@
 lemma "funion (funion x xa) xb = funion x (funion xa xb)"
 by (lifting append_assoc)
 
-quotient_definition
-  "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-is
-  "list_case"
-
-(* NOT SURE IF TRUE *)
-lemma list_case_rsp[quot_respect]:
-  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
-  apply (auto)
-  sorry
-
-lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"
-apply (lifting list.cases(2))
-done
-
 end
diff -r 869d1183e082 -r d360a26fa790 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 09:25:31 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 09:27:53 2010 +0200
@@ -80,6 +80,14 @@
   shows "\<not> memb x []"
   by (simp add: memb_def)
 
+lemma no_memb_nil:
+  "(\<forall>x. \<not> memb x xs) = (xs = [])"
+  by (simp add: memb_def)
+
+lemma none_memb_nil:
+  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+  by (simp add: memb_def)
+
 lemma memb_cons_iff:
   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
   by (induct xs) (auto simp add: memb_def)
@@ -162,6 +170,21 @@
   shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
   by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
 
+lemma fcard_raw_suc_memb:
+  assumes a: "fcard_raw A = Suc n"
+  shows "\<exists>a. memb a A"
+  using a
+  apply (induct A)
+  apply simp
+  apply (rule_tac x="a" in exI)
+  apply (simp add: memb_def)
+  done
+
+lemma mem_card_not_0:
+  assumes a: "memb a A"
+  shows "\<not>(fcard_raw A = 0)"
+  by (metis a fcard_raw_0 none_memb_nil)
+
 lemma fcard_raw_rsp_aux:
   assumes a: "xs \<approx> ys"
   shows "fcard_raw xs = fcard_raw ys"
@@ -208,10 +231,6 @@
   "x # x # xs \<approx> x # xs"
   by auto
 
-lemma none_memb_nil:
-  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
-  by (simp add: memb_def)
-
 lemma fset_raw_strong_cases:
   "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
   apply (induct xs)
@@ -492,6 +511,12 @@
   "fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)"
   by (lifting fcard_raw_delete)
 
+lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
+  by (lifting fcard_raw_suc_memb)
+
+lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
+  by (lifting mem_card_not_0)
+
 text {* funion *}
 
 lemma funion_simps[simp]:
diff -r 869d1183e082 -r d360a26fa790 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Apr 19 09:25:31 2010 +0200
+++ b/Nominal/Parser.thy	Mon Apr 19 09:27:53 2010 +0200
@@ -293,31 +293,49 @@
 ML {* val cheat_const_rsp = Unsynchronized.ref false *}
 
 (* nominal_datatype2 does the following things in order:
+
+Parser.thy/raw_nominal_decls
   1) define the raw datatype
   2) define the raw binding functions
+Perm.thy/define_raw_perms
   3) define permutations of the raw datatype and show that raw type is in the pt typeclass
-  4) define fv and fb_bn
+Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
+  4) define fv and fv_bn
   5) define alpha and alpha_bn
+Perm.thy/distinct_rel
   6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
+Tacs.thy/build_rel_inj
   6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)
      (left-to-right by intro rule, right-to-left by cases; simp)
+Equivp.thy/prove_eqvt
   7) prove bn_eqvt (common induction on the raw datatype)
   8) prove fv_eqvt (common induction on the raw datatype with help of above)
+Rsp.thy/build_alpha_eqvts
   9) prove alpha_eqvt and alpha_bn_eqvt
      (common alpha-induction, unfolding alpha_gen, permute of #* and =)
+Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps
  10) prove that alpha and alpha_bn are equivalence relations
      (common induction and application of 'compose' lemmas)
+Lift.thy/define_quotient_types
  11) define quotient types
+Rsp.thy/build_fvbv_rsps
  12) prove bn respects     (common induction and simp with alpha_gen)
+Rsp.thy/prove_const_rsp
  13) prove fv respects     (common induction and simp with alpha_gen)
  14) prove permute respects    (unfolds to alpha_eqvt)
+Rsp.thy/prove_alpha_bn_rsp
  15) prove alpha_bn respects
      (alpha_induct then cases then sym and trans of the relations)
+Rsp.thy/prove_alpha_alphabn
  16) show that alpha implies alpha_bn (by unduction, needed in following step)
+Rsp.thy/prove_const_rsp
  17) prove respects for all datatype constructors
      (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
+Lift.thy/quotient_lift_consts_export
  18) define lifted constructors, fv, bn, alpha_bn, permutations
+Perm.thy/define_lifted_perms
  19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
+Lift.thy/lift_thm
  20) lift permutation simplifications
  21) lift induction
  22) lift fv
@@ -325,8 +343,11 @@
  24) lift eq_iff
  25) lift alpha_distincts
  26) lift fv and bn eqvts
+Equivp.thy/prove_supports
  27) prove that union of arguments supports constructors
+Equivp.thy/prove_fs
  28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
+Equivp.thy/supp_eq
  29) prove supp = fv
 *)
 ML {*
diff -r 869d1183e082 -r d360a26fa790 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Mon Apr 19 09:25:31 2010 +0200
+++ b/Nominal/Rsp.thy	Mon Apr 19 09:27:53 2010 +0200
@@ -70,7 +70,7 @@
 *}
 
 ML {*
-fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
+fun sym_eqvts ctxt = maps (fn x => [sym OF [x]] handle _ => []) (Nominal_ThmDecls.get_eqvts_thms ctxt)
 fun all_eqvts ctxt =
   Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
 *}