--- 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)} *}