# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256134419 -7200
# Node ID d5098c950d27bb88be0a14cef6e330af2f819692
# Parent  1d0692e7ddd49501edf6de4358df3972e54d01c2
Reorganization of the construction part

diff -r 1d0692e7ddd4 -r d5098c950d27 QuotMain.thy
--- a/QuotMain.thy	Wed Oct 21 15:01:50 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 16:13:39 2009 +0200
@@ -850,13 +850,6 @@
   m1: "(x memb []) = False"
 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
 
-lemma mem_respects:
-  fixes z
-  assumes a: "list_eq x y"
-  shows "(z memb x) = (z memb y)"
-  using a by induct auto
-
-
 fun
   card1 :: "'a list \<Rightarrow> nat"
 where
@@ -877,14 +870,6 @@
  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 = [])"
@@ -937,12 +922,6 @@
 (* fold1_def is not usable, but: *)
 thm fold1.simps
 
-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))
-
 lemma fs1_strong_cases:
   fixes X :: "'a list"
   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
@@ -959,84 +938,6 @@
 term IN
 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]
-
-lemma yy:
-  shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
-unfolding IN_def EMPTY_def
-apply(rule_tac f="(op =) False" in arg_cong)
-apply(rule mem_respects)
-apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-apply(rule list_eq.intros)
-done
-
-lemma
-  shows "IN (x::nat) EMPTY = False"
-using m1
-apply -
-apply(rule yy[THEN iffD1, symmetric])
-apply(simp)
-done
-
-lemma
-  shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
-         ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
-unfolding IN_def INSERT_def
-apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
-apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
-apply(rule mem_respects)
-apply(rule list_eq.intros(3))
-apply(unfold REP_fset_def ABS_fset_def)
-apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
-apply(rule list_eq_refl)
-done
-
-lemma append_respects_fst:
-  assumes a : "list_eq l1 l2"
-  shows "list_eq (l1 @ s) (l2 @ s)"
-  using a
-  apply(induct)
-  apply(auto intro: list_eq.intros)
-  apply(simp add: list_eq_refl)
-done
-
-lemma yyy:
-  shows "
-    (
-     (UNION EMPTY s = s) &
-     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
-    ) = (
-     ((ABS_fset ([] @ REP_fset s)) = s) &
-     ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
-    )"
-  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_I_fset.thm11[symmetric])
-  apply(rule append_respects_fst)
-  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_refl)
-  apply(simp)
-  apply(rule_tac f="(op =)" in arg_cong2)
-  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
-  apply(rule append_respects_fst)
-  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_refl)
-  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
-  apply(rule list_eq.intros(5))
-  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_refl)
-done
-
-lemma
-  shows "
-     (UNION EMPTY s = s) &
-     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
-  apply (simp add: yyy)
-  apply (simp add: QUOT_TYPE_I_fset.thm10)
-  done
-
 ML {*
   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
                 @{const_name "membship"}, @{const_name "card1"},
@@ -1046,104 +947,36 @@
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
 
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
-*}
-
-ML {*
-cterm_of @{theory} (prop_of m1_novars);
-cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
-*}
-
+text {* Respectfullness *}
 
-(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
-ML {*
-  fun transconv_fset_tac' ctxt =
-    (LocalDefs.unfold_tac @{context} fset_defs) THEN
-    ObjectLogic.full_atomize_tac 1 THEN
-    REPEAT_ALL_NEW (FIRST' [
-      rtac @{thm list_eq_refl},
-      rtac @{thm cons_preserves},
-      rtac @{thm mem_respects},
-      rtac @{thm card1_rsp},
-      rtac @{thm QUOT_TYPE_I_fset.R_trans2},
-      CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
-      Cong_Tac.cong_tac @{thm cong},
-      rtac @{thm ext}
-    ]) 1
-*}
+lemma mem_respects:
+  fixes z
+  assumes a: "list_eq x y"
+  shows "(z memb x) = (z memb y)"
+  using a by induct auto
 
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
-  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-*}
-
-(*notation ( output) "prop" ("#_" [1000] 1000) *)
-notation ( output) "Trueprop" ("#_" [1000] 1000)
-
-
-prove {* (Thm.term_of cgoal2) *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
+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
 
-thm length_append (* Not true but worth checking that the goal is correct *)
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
-  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-*}
-prove {* Thm.term_of cgoal2 *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
-  sorry
-
-thm m2
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
-  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-*}
-prove {* Thm.term_of cgoal2 *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
-  done
+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))
 
-thm list_eq.intros(4)
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
-  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-  val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
-*}
-
-(* It is the same, but we need a name for it. *)
-prove zzz : {* Thm.term_of cgoal3 *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
-  done
-
-(*lemma zzz' :
-  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
-  using list_eq.intros(4) by (simp only: zzz)
-
-thm QUOT_TYPE_I_fset.REPS_same
-ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
-*)
-
-thm list_eq.intros(5)
-(* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *)
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
-  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
-*}
-prove {* Thm.term_of cgoal2 *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
-  done
-
+lemma append_respects_fst:
+  assumes a : "list_eq l1 l2"
+  shows "list_eq (l1 @ s) (l2 @ s)"
+  using a
+  apply(induct)
+  apply(auto intro: list_eq.intros)
+  apply(simp add: list_eq_refl)
+done
 
 thm list.induct
 lemma list_induct_hol4:
@@ -1178,13 +1011,8 @@
 
 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}
 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
-lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
-lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
-lemmas APPLY_RSP_II = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]
-
 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
-
 prove list_induct_tr: trm_r
 apply (atomize(full))
 apply (simp only: id_def[symmetric])
@@ -1298,6 +1126,13 @@
 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 apply (rule QUOTIENT_fset)
 apply (assumption)
+prefer 8
+apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "(op \<approx> ===> op =)" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id"]} @{context} 1 *})
+prefer 2
+apply (rule IDENTITY_QUOTIENT)
+prefer 3
+apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
+prefer 2
 sorry
 
 prove list_induct_t: trm
@@ -1331,6 +1166,171 @@
 
 ML {* @{thm fold1_def_2_r} OF [li] *}
 
+
+lemma yy:
+  shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
+unfolding IN_def EMPTY_def
+apply(rule_tac f="(op =) False" in arg_cong)
+apply(rule mem_respects)
+apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
+apply(rule list_eq.intros)
+done
+
+lemma
+  shows "IN (x::nat) EMPTY = False"
+using m1
+apply -
+apply(rule yy[THEN iffD1, symmetric])
+apply(simp)
+done
+
+lemma
+  shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
+         ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
+unfolding IN_def INSERT_def
+apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
+apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
+apply(rule mem_respects)
+apply(rule list_eq.intros(3))
+apply(unfold REP_fset_def ABS_fset_def)
+apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+apply(rule list_eq_refl)
+done
+
+lemma yyy:
+  shows "
+    (
+     (UNION EMPTY s = s) &
+     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
+    ) = (
+     ((ABS_fset ([] @ REP_fset s)) = s) &
+     ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
+    )"
+  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_I_fset.thm11[symmetric])
+  apply(rule append_respects_fst)
+  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
+  apply(rule list_eq_refl)
+  apply(simp)
+  apply(rule_tac f="(op =)" in arg_cong2)
+  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
+  apply(rule append_respects_fst)
+  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
+  apply(rule list_eq_refl)
+  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
+  apply(rule list_eq.intros(5))
+  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
+  apply(rule list_eq_refl)
+done
+
+lemma
+  shows "
+     (UNION EMPTY s = s) &
+     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
+  apply (simp add: yyy)
+  apply (simp add: QUOT_TYPE_I_fset.thm10)
+  done
+
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
+*}
+
+ML {*
+cterm_of @{theory} (prop_of m1_novars);
+cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
+*}
+
+
+(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
+ML {*
+  fun transconv_fset_tac' ctxt =
+    (LocalDefs.unfold_tac @{context} fset_defs) THEN
+    ObjectLogic.full_atomize_tac 1 THEN
+    REPEAT_ALL_NEW (FIRST' [
+      rtac @{thm list_eq_refl},
+      rtac @{thm cons_preserves},
+      rtac @{thm mem_respects},
+      rtac @{thm card1_rsp},
+      rtac @{thm QUOT_TYPE_I_fset.R_trans2},
+      CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
+      Cong_Tac.cong_tac @{thm cong},
+      rtac @{thm ext}
+    ]) 1
+*}
+
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+*}
+
+(*notation ( output) "prop" ("#_" [1000] 1000) *)
+notation ( output) "Trueprop" ("#_" [1000] 1000)
+
+
+prove {* (Thm.term_of cgoal2) *}
+  apply (tactic {* transconv_fset_tac' @{context} *})
+  done
+
+thm length_append (* Not true but worth checking that the goal is correct *)
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+*}
+prove {* Thm.term_of cgoal2 *}
+  apply (tactic {* transconv_fset_tac' @{context} *})
+  sorry
+
+thm m2
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+*}
+prove {* Thm.term_of cgoal2 *}
+  apply (tactic {* transconv_fset_tac' @{context} *})
+  done
+
+thm list_eq.intros(4)
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+  val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
+*}
+
+(* It is the same, but we need a name for it. *)
+prove zzz : {* Thm.term_of cgoal3 *}
+  apply (tactic {* transconv_fset_tac' @{context} *})
+  done
+
+(*lemma zzz' :
+  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
+  using list_eq.intros(4) by (simp only: zzz)
+
+thm QUOT_TYPE_I_fset.REPS_same
+ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
+*)
+
+thm list_eq.intros(5)
+(* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *)
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
+*}
+prove {* Thm.term_of cgoal2 *}
+  apply (tactic {* transconv_fset_tac' @{context} *})
+  done
+
 ML {*
   fun lift_theorem_fset_aux thm lthy =
     let
@@ -1360,6 +1360,7 @@
     end;
 *}
 
+(* These do not work without proper definitions to rewrite back *)
 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}