Proved concat_empty.
--- a/Quot/Examples/AbsRepTest.thy Thu Jan 07 16:51:38 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy Fri Jan 08 10:08:01 2010 +0100
@@ -135,7 +135,7 @@
apply(simp add: Quotient_abs_rep[OF a])
done
-lemma set_in_eq: "(\<forall>e. ((e \<in> A) = (e \<in> B))) \<equiv> A = B"
+lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
apply (rule eq_reflection)
apply auto
done
@@ -145,77 +145,6 @@
apply(simp only: set_map set_in_eq)
done
-lemma quotient_compose_list_pre:
- "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =
- ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>
- (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and>
- abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
- apply rule
- apply rule
- apply rule
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply rule
- apply (rule equivp_reflp[OF fset_equivp])
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply(rule)
- apply rule
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply rule
- apply (rule equivp_reflp[OF fset_equivp])
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
- apply (metis Quotient_rel[OF Quotient_fset])
- apply (auto)[1]
- apply (subgoal_tac "map abs_fset r = map abs_fset b")
- prefer 2
- apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
- apply (subgoal_tac "map abs_fset s = map abs_fset ba")
- prefer 2
- apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
- apply (simp add: map_rel_cong)
- apply rule
- apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"])
- apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply rule
- prefer 2
- apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"])
- apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply (erule conjE)+
- apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
- prefer 2
- apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)
- apply (rule map_rel_cong)
- apply (assumption)
- done
-
-lemma quotient_compose_list:
- shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1))
- (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
- unfolding Quotient_def comp_def
- apply (rule)+
- apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
- apply (rule)
- apply (rule)
- apply (rule)
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply (rule)
- apply (rule equivp_reflp[OF fset_equivp])
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply rule
- apply rule
-apply(rule quotient_compose_list_pre)
-done
-
lemma quotient_compose_list_gen_pre:
assumes a: "equivp r2"
and b: "Quotient r2 abs2 rep2"
--- a/Quot/Examples/FSet3.thy Thu Jan 07 16:51:38 2010 +0100
+++ b/Quot/Examples/FSet3.thy Fri Jan 08 10:08:01 2010 +0100
@@ -260,36 +260,95 @@
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)
+ apply auto
+ done
+
+lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
+ unfolding list_eq.simps
+ apply(simp only: set_map set_in_eq)
+ done
+
+lemma quotient_compose_list_pre:
+ "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r s =
+ ((list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r r \<and>
+ (list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) s s \<and>
+ abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
+ apply rule
+ apply rule
+ apply rule
+ apply (rule list_rel_refl)
+ apply (metis equivp_def fset_equivp)
+ apply rule
+ apply (rule equivp_reflp[OF fset_equivp])
+ apply (rule list_rel_refl)
+ apply (metis equivp_def fset_equivp)
+ apply(rule)
+ apply rule
+ apply (rule list_rel_refl)
+ apply (metis equivp_def fset_equivp)
+ apply rule
+ apply (rule equivp_reflp[OF fset_equivp])
+ apply (rule list_rel_refl)
+ apply (metis equivp_def fset_equivp)
+ apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
+ apply (metis Quotient_rel[OF Quotient_fset])
+ apply (auto simp only:)[1]
+ apply (subgoal_tac "map abs_fset r = map abs_fset b")
+ prefer 2
+ apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
+ apply (subgoal_tac "map abs_fset s = map abs_fset ba")
+ prefer 2
+ apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
+ apply (simp only: map_rel_cong)
+ apply rule
+ apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"])
+ apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
+ apply (rule list_rel_refl)
+ apply (metis equivp_def fset_equivp)
+ apply rule
+ prefer 2
+ apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"])
+ apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
+ apply (rule list_rel_refl)
+ apply (metis equivp_def fset_equivp)
+ apply (erule conjE)+
+ apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
+ prefer 2
+ apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)
+ apply (rule map_rel_cong)
+ apply (assumption)
+ done
+
+lemma quotient_compose_list[quot_thm]:
+ shows "Quotient ((list_rel op \<approx>) OO (op \<approx>) OO (list_rel op \<approx>))
+ (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
+ unfolding Quotient_def comp_def
+ apply (rule)+
+ apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
+ apply (rule)
+ apply (rule)
+ apply (rule)
+ apply (rule list_rel_refl)
+ apply (metis equivp_def fset_equivp)
+ apply (rule)
+ apply (rule equivp_reflp[OF fset_equivp])
+ apply (rule list_rel_refl)
+ apply (metis equivp_def fset_equivp)
+ apply rule
+ apply rule
+ apply(rule quotient_compose_list_pre)
+ done
+
lemma fconcat_empty:
shows "fconcat {||} = {||}"
-apply(lifting_setup concat1)
-apply(regularize)
-defer
+apply(lifting concat1)
apply(cleaning)
apply(simp add: comp_def)
-apply(cleaning)
apply(fold fempty_def[simplified id_simps])
apply(rule refl)
-apply(injection)
-apply(rule apply_rsp[of "(list_rel (op \<approx>)) OO (op \<approx>) OO (list_rel (op \<approx>))" _ _ "op \<approx>" "concat" _ "[]" "((map rep_fset \<circ> rep_fset) ((abs_fset \<circ> map abs_fset) []))"])
-prefer 2
-ML_prf {* fun dest_comb (f $ a) = (f, a) *}
-apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (fst o dest_comb) 1 *})
-prefer 3
-apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (snd o dest_comb) 1 *})
-apply(rule rep_abs_rsp[of _ "(abs_fset \<circ> map abs_fset)" "(map rep_fset \<circ> rep_fset)"])
-prefer 3
-apply(rule rep_abs_rsp[of _ "((map rep_fset \<circ> rep_fset) ---> abs_fset)" "(abs_fset \<circ> map abs_fset) ---> rep_fset"])
-prefer 2
-apply(rule concat_rsp)
-prefer 3
-apply(injection)
-prefer 2
-apply(thin_tac "Quot_True {||}")
-apply(unfold Quotient_def)
-
-apply(auto)
-sorry
+done
lemma fconcat_insert:
shows "fconcat (finsert x S) = x |\<union>| fconcat S"
--- a/Quot/QuotScript.thy Thu Jan 07 16:51:38 2010 +0100
+++ b/Quot/QuotScript.thy Fri Jan 08 10:08:01 2010 +0100
@@ -502,6 +502,13 @@
using a b unfolding Respects_def
by simp
+lemma abs_o_rep:
+ assumes a: "Quotient r absf repf"
+ shows "absf o repf = id"
+ apply(rule ext)
+ apply(simp add: Quotient_abs_rep[OF a])
+ done
+
lemma fun_rel_eq_rel:
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"