# HG changeset patch # User Cezary Kaliszyk # Date 1265362341 -3600 # Node ID 7a42cc191111ca1164bc714b1005b868e87aca78 # Parent 3664eafcad0940fee8e5d38bb6813ba571d418a4 Fixes for Bex1 removal. diff -r 3664eafcad09 -r 7a42cc191111 Quot/Examples/SigmaEx.thy --- a/Quot/Examples/SigmaEx.thy Thu Feb 04 18:09:20 2010 +0100 +++ b/Quot/Examples/SigmaEx.thy Fri Feb 05 10:32:21 2010 +0100 @@ -75,6 +75,8 @@ end + + lemma tolift: "\ fvar. \ fobj\Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). @@ -85,18 +87,16 @@ \ fpar\Respects (op = ===> op = ===> alpha_method ===> op =). \ fsgm\Respects (op = ===> (op = ===> alpha_obj) ===> op =). - Bex1 - (Respects (prod_rel (alpha_obj ===> op =) + Ex1 (\x. +(x \ (Respects (prod_rel (alpha_obj ===> op =) (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) (prod_rel ((prod_rel (op =) alpha_method) ===> op =) (alpha_method ===> op =) ) - ) - )) + )))) \ (\ (hom_o\robj \ 'a, hom_d\(char list \ rmethod) list \ 'b, hom_e\char list \ rmethod \ 'c, hom_m\rmethod \ 'd). - - (\x. hom_o (rVar x) = fvar x) \ +((\x. hom_o (rVar x) = fvar x) \ (\d. hom_o (rObj d) = fobj (hom_d d) d) \ (\a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \ (\a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \ @@ -104,14 +104,25 @@ (hom_d [] = fnil) \ (\l m. hom_e (l, m) = fpar (hom_m m) l m) \ (\x a. hom_m (rSig x a) = fsgm (\y. hom_o ([(x, y)] \ a)) (\y. [(x, y)] \ a)) -)" +)) x) " sorry -syntax +lemma test_to: "Ex1 (\x. (x \ (Respects alpha_obj)) \ P x)" +ML_prf {* prop_of (#goal (Isar.goal ())) *} +sorry +lemma test_tod: "Ex1 (P :: obj \ bool)" +apply (lifting test_to) +done + + + + +(*syntax "_expttrn" :: "pttrn => bool => bool" ("(3\\ _./ _)" [0, 10] 10) translations "\\ x. P" == "Ex (%x. P)" +*) lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar" by (simp add: a1) @@ -129,7 +140,7 @@ lemma bex1_bex1reg: "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" -apply (simp add: Bex1_def Ex1_def Bex1_rel_def in_respects) +apply (simp add: Ex1_def Bex1_rel_def in_respects) apply clarify apply auto apply (rule bexI) @@ -154,8 +165,6 @@ apply (lifting tolift) done -done - lemma tolift': "\ fvar. \ fobj\Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). diff -r 3664eafcad09 -r 7a42cc191111 Quot/QuotBase.thy --- a/Quot/QuotBase.thy Thu Feb 04 18:09:20 2010 +0100 +++ b/Quot/QuotBase.thy Fri Feb 05 10:32:21 2010 +0100 @@ -434,9 +434,9 @@ lemma bex1_rsp: assumes a: "(R ===> (op =)) f g" - shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)" + shows "Ex1 (\x. x \ Respects R \ f x) = Ex1 (\x. x \ Respects R \ g x)" using a -by (simp add: Ex1_def Bex1_def in_respects) auto +by (simp add: Ex1_def in_respects) auto (* 3 lemmas needed for cleaning of quantifiers *) lemma all_prs: @@ -536,7 +536,7 @@ done lemma bex1_bexeq_reg: "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" - apply (simp add: Bex1_def Ex1_def Bex1_rel_def in_respects) + apply (simp add: Ex1_def Bex1_rel_def in_respects) apply clarify apply auto apply (rule bexI) diff -r 3664eafcad09 -r 7a42cc191111 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Thu Feb 04 18:09:20 2010 +0100 +++ b/Quot/quotient_tacs.ML Fri Feb 05 10:32:21 2010 +0100 @@ -139,7 +139,7 @@ 0. preliminary simplification step according to ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range - 1. eliminating simple Ball/Bex/Bex1 instances (ball_reg_right bex_reg_left) + 1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left) 2. monos @@ -354,17 +354,6 @@ (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam -| Const (@{const_name "op ="},_) $ - (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm bex1_rsp} THEN' dtac @{thm QT_ex1} - -(* TODO: Check why less _ are needed then in EX/ALL cases *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $ - (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - | (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _) => rtac @{thm bexeq_rsp} THEN' quotient_tac ctxt diff -r 3664eafcad09 -r 7a42cc191111 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Thu Feb 04 18:09:20 2010 +0100 +++ b/Quot/quotient_term.ML Fri Feb 05 10:32:21 2010 +0100 @@ -389,7 +389,6 @@ val mk_babs = Const (@{const_name Babs}, dummyT) val mk_ball = Const (@{const_name Ball}, dummyT) val mk_bex = Const (@{const_name Bex}, dummyT) -val mk_bex1 = Const (@{const_name Bex1}, dummyT) val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) val mk_resp = Const (@{const_name Respects}, dummyT) @@ -474,6 +473,24 @@ else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm end + | (Const (@{const_name "Ex1"}, ty) $ + (Abs (n, _, + (Const (@{const_name "op &"}, _) $ + (Const (@{const_name "op :"}, _) $ _ $ (Const (@{const_name "Respects"}, _) $ resrel)) $ + (t $ _) + ) + )), Const (@{const_name "Ex1"}, ty') $ t') => + let + val t = incr_boundvars (~1) t + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') + val _ = tracing "bla" + in + if resrel <> needrel + then term_mismatch "regularize (Bex1)" ctxt resrel needrel + else mk_bex1_rel $ resrel $ subtrm + end + | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => let val subtrm = apply_subt (regularize_trm ctxt) (t, t') @@ -514,17 +531,6 @@ else mk_bex1_rel $ resrel $ subtrm end - | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, - Const (@{const_name "Ex1"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') - in - if resrel <> needrel - then term_mismatch "regularize (Bex1)" ctxt resrel needrel - else mk_bex1_rel $ resrel $ subtrm - end - | (* equalities need to be replaced by appropriate equivalence relations *) (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => if ty = ty' then rtrm