# HG changeset patch # User Cezary Kaliszyk # Date 1260548546 -3600 # Node ID e68f501f76d04106029c6ba6220a171e13c6ae79 # Parent a9e55e1ef64c44a8c116924d63e4cf65e2953469# Parent 7b74d77a61aaeae98b6ca0112c1763f517acf218 Merge + Added LarryInt & Fset3 to tests. diff -r 7b74d77a61aa -r e68f501f76d0 Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Fri Dec 11 17:03:52 2009 +0100 +++ b/Quot/Examples/FSet3.thy Fri Dec 11 17:22:26 2009 +0100 @@ -22,7 +22,8 @@ quotient fset = "'a list" / "list_eq" by (rule list_eq_equivp) -lemma not_nil_equiv_cons: "\[] \ a # A" sorry +lemma not_nil_equiv_cons: "\[] \ a # A" +unfolding list_eq_def by auto (* The 2 lemmas below are different from the ones in QuotList *) lemma nil_rsp[quot_respect]: diff -r 7b74d77a61aa -r e68f501f76d0 Quot/Examples/IntEx2.thy --- a/Quot/Examples/IntEx2.thy Fri Dec 11 17:03:52 2009 +0100 +++ b/Quot/Examples/IntEx2.thy Fri Dec 11 17:22:26 2009 +0100 @@ -194,8 +194,8 @@ (simp) lemma add: - "(ABS_int (x,y)) + (ABS_int (u,v)) = - (ABS_int (x + u, y + v))" + "(abs_int (x,y)) + (abs_int (u,v)) = + (abs_int (x + u, y + v))" apply(simp add: plus_int_def) apply(fold plus_raw.simps) apply(rule Quotient_rel_abs[OF Quotient_int]) diff -r 7b74d77a61aa -r e68f501f76d0 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Fri Dec 11 17:03:52 2009 +0100 +++ b/Quot/QuotMain.thy Fri Dec 11 17:22:26 2009 +0100 @@ -17,14 +17,14 @@ begin definition - ABS::"'a \ 'b" + abs::"'a \ 'b" where - "ABS x \ Abs (R x)" + "abs x \ Abs (R x)" definition - REP::"'b \ 'a" + rep::"'b \ 'a" where - "REP a = Eps (Rep a)" + "rep a = Eps (Rep a)" lemma lem9: shows "R (Eps (R x)) = R x" @@ -36,9 +36,9 @@ qed theorem thm10: - shows "ABS (REP a) \ a" + shows "abs (rep a) \ a" apply (rule eq_reflection) - unfolding ABS_def REP_def + unfolding abs_def rep_def proof - from rep_prop obtain x where eq: "Rep a = R x" by auto @@ -50,9 +50,9 @@ show "Abs (R (Eps (Rep a))) = a" by simp qed -lemma REP_refl: - shows "R (REP a) (REP a)" -unfolding REP_def +lemma rep_refl: + shows "R (rep a) (rep a)" +unfolding rep_def by (simp add: equivp[simplified equivp_def]) lemma lem7: @@ -64,21 +64,21 @@ done theorem thm11: - shows "R r r' = (ABS r = ABS r')" -unfolding ABS_def + shows "R r r' = (abs r = abs r')" +unfolding abs_def by (simp only: equivp[simplified equivp_def] lem7) -lemma REP_ABS_rsp: - shows "R f (REP (ABS g)) = R f g" - and "R (REP (ABS g)) f = R g f" +lemma rep_abs_rsp: + shows "R f (rep (abs g)) = R f g" + and "R (rep (abs g)) f = R g f" by (simp_all add: thm10 thm11) lemma Quotient: - "Quotient R ABS REP" + "Quotient R abs rep" apply(unfold Quotient_def) apply(simp add: thm10) -apply(simp add: REP_refl) +apply(simp add: rep_refl) apply(subst thm11[symmetric]) apply(simp add: equivp[simplified equivp_def]) done diff -r 7b74d77a61aa -r e68f501f76d0 Quot/ROOT.ML --- a/Quot/ROOT.ML Fri Dec 11 17:03:52 2009 +0100 +++ b/Quot/ROOT.ML Fri Dec 11 17:22:26 2009 +0100 @@ -4,8 +4,10 @@ ["QuotMain", "Examples/FSet", "Examples/FSet2", + "Examples/FSet3", "Examples/IntEx", "Examples/IntEx2", "Examples/LFex", "Examples/LamEx", - "Examples/LarryDatatype"]; + "Examples/LarryDatatype", + "Examples/LarryInt"]; diff -r 7b74d77a61aa -r e68f501f76d0 Quot/quotient.ML --- a/Quot/quotient.ML Fri Dec 11 17:03:52 2009 +0100 +++ b/Quot/quotient.ML Fri Dec 11 17:22:26 2009 +0100 @@ -132,12 +132,12 @@ val rep = Const (rep_name, abs_ty --> rep_ty) (* ABS and REP definitions *) - val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) - val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) + val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT ) + val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT ) val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) - val ABS_name = Binding.prefix_name "ABS_" qty_name - val REP_name = Binding.prefix_name "REP_" qty_name + val ABS_name = Binding.prefix_name "abs_" qty_name + val REP_name = Binding.prefix_name "rep_" qty_name val (((ABS, ABS_def), (REP, REP_def)), lthy2) = lthy1 |> define (ABS_name, NoSyn, ABS_trm) ||>> define (REP_name, NoSyn, REP_trm) diff -r 7b74d77a61aa -r e68f501f76d0 Quot/quotient_def.ML --- a/Quot/quotient_def.ML Fri Dec 11 17:03:52 2009 +0100 +++ b/Quot/quotient_def.ML Fri Dec 11 17:22:26 2009 +0100 @@ -31,18 +31,18 @@ fun get_fun_aux lthy s fs = case (maps_lookup (ProofContext.theory_of lthy) s) of SOME info => list_comb (Const (#mapfun info, dummyT), fs) - | NONE => raise + | NONE => raise (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])) fun get_const flag lthy _ qty = (* FIXME: check here that _ and qty are related *) -let +let val thy = ProofContext.theory_of lthy val qty_name = Long_Name.base_name (fst (dest_Type qty)) in case flag of - absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) - | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) + absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) + | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) end @@ -53,17 +53,17 @@ fun get_fun flag lthy (rty, qty) = if rty = qty then mk_identity qty else - case (rty, qty) of + case (rty, qty) of (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => let val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') val fs_ty2 = get_fun flag lthy (ty2, ty2') - in + in get_fun_aux lthy "fun" [fs_ty1, fs_ty2] - end + end | (Type (s, []), Type (s', [])) => if s = s' - then mk_identity qty + then mk_identity qty else get_const flag lthy rty qty | (Type (s, tys), Type (s', tys')) => if s = s' @@ -71,7 +71,7 @@ else get_const flag lthy rty qty | (TFree x, TFree x') => if x = x' - then mk_identity qty + then mk_identity qty else raise (LIFT_MATCH "get_fun") | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") | _ => raise (LIFT_MATCH "get_fun")