# HG changeset patch # User Christian Urban # Date 1263604178 -3600 # Node ID 4e0b89d886ac7744d4b8ecd4f143080fd368962c # Parent 92c43c96027e9938cdf21880176c00392690f0a0 liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals diff -r 92c43c96027e -r 4e0b89d886ac Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Fri Jan 15 17:09:36 2010 +0100 +++ b/Quot/Examples/LamEx.thy Sat Jan 16 02:09:38 2010 +0100 @@ -108,44 +108,12 @@ begin quotient_definition - "perm_lam :: 'x prm \ lam \ lam" + "perm_lam :: 'x prm \ lam \ lam" as "perm::'x prm \ rlam \ rlam" end -(* lemmas that need to be lifted *) -lemma pi_var_eqvt1: - fixes pi::"'x prm" - shows "(pi \ rVar a) \ rVar (pi \ a)" - by (simp add: alpha_refl) - -lemma pi_var_eqvt2: - fixes pi::"'x prm" - shows "(pi \ rVar a) = rVar (pi \ a)" - by (simp) - -lemma pi_app_eqvt1: - fixes pi::"'x prm" - shows "(pi \ rApp t1 t2) \ rApp (pi \ t1) (pi \ t2)" - by (simp add: alpha_refl) - -lemma pi_app_eqvt2: - fixes pi::"'x prm" - shows "(pi \ rApp t1 t2) = rApp (pi \ t1) (pi \ t2)" - by (simp) - -lemma pi_lam_eqvt1: - fixes pi::"'x prm" - shows "(pi \ rLam a t) \ rLam (pi \ a) (pi \ t)" - by (simp add: alpha_refl) - -lemma pi_lam_eqvt2: - fixes pi::"'x prm" - shows "(pi \ rLam a t) = rLam (pi \ a) (pi \ t)" - by (simp add: alpha) - - lemma real_alpha: assumes a: "t = [(a,b)]\s" "a\[b].s" shows "Lam a t = Lam b s" @@ -189,38 +157,35 @@ apply (simp_all add: rlam.inject alpha_refl) done -lemma pi_var1: - fixes pi::"'x prm" - shows "pi \ Var a = Var (pi \ a)" - by (lifting pi_var_eqvt1) -lemma pi_var2: - fixes pi::"'x prm" - shows "pi \ Var a = Var (pi \ a)" - by (lifting pi_var_eqvt2) - - -lemma pi_app: - fixes pi::"'x prm" - shows "pi \ App t1 t2 = App (pi \ t1) (pi \ t2)" - by (lifting pi_app_eqvt2) +lemma lam_induct: + "\\name. P (Var name); + \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); + \name lam. P lam \ P (Lam name lam)\ + \ P lam" + by (lifting rlam.induct) -lemma pi_lam: - fixes pi::"'x prm" - shows "pi \ Lam a t = Lam (pi \ a) (pi \ t)" - by (lifting pi_lam_eqvt2) +lemma perm_lam [simp]: + fixes pi::"'a prm" + shows "pi \ Var a = Var (pi \ a)" + and "pi \ App t1 t2 = App (pi \ t1) (pi \ t2)" + and "pi \ Lam a t = Lam (pi \ a) (pi \ t)" +apply(lifting perm_rlam.simps) +done -lemma fv_var: +instance lam::pt_name +apply(default) +apply(induct_tac [!] x rule: lam_induct) +apply(simp_all add: pt_name2 pt_name3) +done + +lemma fv_lam [simp]: shows "fv (Var a) = {a}" - by (lifting rfv_var) + and "fv (App t1 t2) = fv t1 \ fv t2" + and "fv (Lam a t) = fv t - {a}" +apply(lifting rfv_var rfv_app rfv_lam) +done -lemma fv_app: - shows "fv (App t1 t2) = fv t1 \ fv t2" - by (lifting rfv_app) - -lemma fv_lam: - shows "fv (Lam a t) = fv t - {a}" - by (lifting rfv_lam) lemma a1: "a = b \ Var a = Var b" @@ -260,7 +225,7 @@ lemma var_supp1: shows "(supp (Var a)) = ((supp a)::name set)" -apply(simp add: supp_def pi_var1 var_inject) +apply(simp add: supp_def var_inject) done lemma var_supp: @@ -271,37 +236,15 @@ lemma app_supp: shows "supp (App t1 t2) = (supp t1) \ ((supp t2)::name set)" -apply(simp only: supp_def pi_app app_inject) +apply(simp only: perm_lam supp_def app_inject) apply(simp add: Collect_imp_eq Collect_neg_eq) done lemma lam_supp: shows "supp (Lam x t) = ((supp ([x].t))::name set)" -apply(simp add: supp_def pi_lam) +apply(simp add: supp_def) sorry -lemma lam_induct: - "\\name. P (Var name); - \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); - \name lam. P lam \ P (Lam name lam)\ - \ P lam" - by (lifting rlam.induct) - -instance lam::pt_name -apply(default) -apply(induct_tac x rule: lam_induct) -apply(simp add: pi_var1) -apply(simp add: pi_app) -apply(simp add: pi_lam) -apply(induct_tac x rule: lam_induct) -apply(simp add: pi_var1 pt_name2) -apply(simp add: pi_app) -apply(simp add: pi_lam pt_name2) -apply(induct_tac x rule: lam_induct) -apply(simp add: pi_var1 pt_name3) -apply(simp add: pi_app) -apply(simp add: pi_lam pt_name3) -done instance lam::fs_name apply(default) @@ -328,7 +271,7 @@ proof (induct lam rule: lam_induct) case (1 name pi) show "P a (pi \ Var name)" - apply (simp only: pi_var1) + apply (simp) apply (rule a1) done next @@ -336,7 +279,7 @@ have b1: "\(pi::name prm) a. P a (pi \ lam1)" by fact have b2: "\(pi::name prm) a. P a (pi \ lam2)" by fact show "P a (pi \ App lam1 lam2)" - apply (simp only: pi_app) + apply (simp) apply (rule a2) apply (rule b1) apply (rule b2) @@ -361,10 +304,10 @@ apply(simp add: fresh_lam) done show "P a (pi \ Lam name lam)" - apply (simp add: pi_lam) + apply (simp) apply(subst eq[symmetric]) using p - apply(simp only: pi_lam pt_name2 swap_simps) + apply(simp only: perm_lam pt_name2 swap_simps) done qed then have "P a (([]::name prm) \ lam)" by blast @@ -477,7 +420,19 @@ apply (lifting hom) done -thm bex_reg_eqv_range[OF identity_equivp, of "alpha"] +(* test test +lemma raw_hom_correct: + assumes f1: "f_var \ Respects (op= ===> op=)" + and f2: "f_app \ Respects (alpha ===> alpha ===> op= ===> op= ===> op=)" + and f3: "f_lam \ Respects ((op= ===> alpha) ===> (op= ===> op=) ===> op=)" + shows "\!hom\Respects (alpha ===> op =). + ((\x. hom (rVar x) = f_var x) \ + (\l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \ + (\x a. hom (rLam a x) = f_lam (\b. ([(a,b)]\ x)) (\b. hom ([(a,b)] \ x))))" +unfolding Bex1_def +apply(rule ex1I) +sorry +*) end diff -r 92c43c96027e -r 4e0b89d886ac Quot/QuotMain.thy --- a/Quot/QuotMain.thy Fri Jan 15 17:09:36 2010 +0100 +++ b/Quot/QuotMain.thy Sat Jan 16 02:09:38 2010 +0100 @@ -151,15 +151,15 @@ section {* Methods / Interface *} ML {* -fun mk_method1 tac thm ctxt = - SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) +fun mk_method1 tac thms ctxt = + SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) fun mk_method2 tac ctxt = SIMPLE_METHOD (HEADGOAL (tac ctxt)) *} method_setup lifting = - {* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *} + {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *} {* Lifting of theorems to quotient types. *} method_setup lifting_setup = diff -r 92c43c96027e -r 4e0b89d886ac Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Fri Jan 15 17:09:36 2010 +0100 +++ b/Quot/quotient_tacs.ML Sat Jan 16 02:09:38 2010 +0100 @@ -5,7 +5,7 @@ val all_injection_tac: Proof.context -> int -> tactic val clean_tac: Proof.context -> int -> tactic val procedure_tac: Proof.context -> thm -> int -> tactic - val lift_tac: Proof.context -> thm -> int -> tactic + val lift_tac: Proof.context -> thm list -> int -> tactic val quotient_tac: Proof.context -> int -> tactic val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic end; @@ -612,18 +612,24 @@ (* Automatic Proofs *) -val msg1 = "Regularize proof failed." -val msg2 = cat_lines ["Injection proof failed.", +val msg1 = "The regularize proof failed." +val msg2 = cat_lines ["The injection proof failed.", "This is probably due to missing respects lemmas.", "Try invoking the injection method manually to see", "which lemmas are missing."] -val msg3 = "Cleaning proof failed." +val msg3 = "The cleaning proof failed." -fun lift_tac ctxt rthm = - procedure_tac ctxt rthm - THEN' RANGE_WARN - [(regularize_tac ctxt, msg1), - (all_injection_tac ctxt, msg2), - (clean_tac ctxt, msg3)] +fun lift_tac ctxt rthms = +let + fun mk_tac rthm = + procedure_tac ctxt rthm + THEN' RANGE_WARN + [(regularize_tac ctxt, msg1), + (all_injection_tac ctxt, msg2), + (clean_tac ctxt, msg3)] +in + simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) + THEN' RANGE (map mk_tac rthms) +end end; (* structure *)