# HG changeset patch # User Christian Urban # Date 1281776081 -28800 # Node ID c670a849af65c174d821cb47db518b9ab332258b # Parent f2f611daf48011c069875105d54bfee19e2a020d more experiments with lifting diff -r f2f611daf480 -r c670a849af65 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Thu Aug 12 21:29:35 2010 +0800 +++ b/Nominal-General/nominal_library.ML Sat Aug 14 16:54:41 2010 +0800 @@ -55,6 +55,9 @@ (* transformations of premises in inductions *) val transform_prem1: Proof.context -> string list -> thm -> thm val transform_prem2: Proof.context -> string list -> thm -> thm + + (* transformation into the object logic *) + val atomize: thm -> thm end @@ -256,6 +259,9 @@ map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm +(* transformes a theorem into one of the object logic *) +val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars + end (* structure *) diff -r f2f611daf480 -r c670a849af65 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Thu Aug 12 21:29:35 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Sat Aug 14 16:54:41 2010 +0800 @@ -21,39 +21,29 @@ where "bn (As x y t) = {atom x}" +(* can lift *) +thm distinct +thm trm_raw_assg_raw.inducts +thm fv_defs -thm alpha_sym_thms -thm alpha_trans_thms -thm size_eqvt -thm size_simps -thm size_rsp -thm alpha_bn_imps -thm distinct +(* cannot lift yet *) thm eq_iff thm eq_iff_simps -thm fv_defs thm perm_simps thm perm_laws +thm trm_raw_assg_raw.size(9 - 16) + +(* rsp lemmas *) +thm size_rsp thm funs_rsp thm constrs_rsp +thm permute_rsp declare constrs_rsp[quot_respect] -(* declare funs_rsp[quot_respect] *) - -typ trm -typ assg -term Var -term App -term Baz -term bn -term fv_trm -term alpha_bn - -lemma [quot_respect]: - "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" -apply(simp) -sorry +declare funs_rsp[quot_respect] +declare size_rsp[quot_respect] +declare permute_rsp[quot_respect] ML {* val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} @@ -67,29 +57,113 @@ val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} *} -thm perm_defs[no_vars] +instantiation trm and assg :: size +begin + +quotient_definition + "size_trm :: trm \ nat" +is "size :: trm_raw \ nat" + +quotient_definition + "size_assg :: assg \ nat" +is "size :: assg_raw \ nat" + +instance .. + +end + +ML {* + val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} +*} + + + +instantiation trm and assg :: pt +begin + +quotient_definition + "permute_trm :: perm => trm => trm" + is "permute :: perm \ trm_raw \ trm_raw" + +quotient_definition + "permute_assg :: perm => assg => assg" + is "permute :: perm \ assg_raw \ assg_raw" + +lemma qperm_laws: + fixes t::trm and a::assg + shows "permute 0 t = t" + and "permute 0 a = a" +sorry + +instance +apply(default) +sorry + +end + + +(* +lemma [quot_respect]: + "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw" +apply(simp) +sorry +*) + +ML {* + val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]} +*} + +ML {* + val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} +*} + + +(* +instance trm :: size .. +instance assg :: size .. + +lemma "(size (Var x)) = 0" +apply(descending) +apply(rule trm_raw_assg_raw.size(9 - 16)) +apply(simp) +*) + +ML {* + val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} +*} + +section {* NOT *} + + +ML {* + val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} +*} + + +ML {* + val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} +*} + +ML {* + val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} +*} + + +ML {* + val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} +*} instance trm :: pt sorry instance assg :: pt sorry -lemma b1: - "p \ Var name = Var (p \ name)" - "p \ App trm1 trm2 = App (p \ trm1) (p \ trm2)" - "p \ Lam name trm = Lam (p \ name) (p \ trm)" - "p \ Let assg trm = Let (p \ assg) (p \ trm)" - "p \ Foo name1 name2 trm1 trm2 trm3 = - Foo (p \ name1) (p \ name2) (p \ trm1) (p \ trm2) (p \ trm3)" - "p \ Bar name1 name2 trm = Bar (p \ name1) (p \ name2) (p \ trm)" - "p \ Baz name trm1 trm2 = Baz (p \ name) (p \ trm1) (p \ trm2)" - "p \ As name1 name2 trm = As (p \ name1) (p \ name2) (p \ trm)" -sorry + + -(* -ML {* - val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_defs} -*} -*) + + + + thm eq_iff[no_vars] diff -r f2f611daf480 -r c670a849af65 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Thu Aug 12 21:29:35 2010 +0800 +++ b/Nominal/NewParser.thy Sat Aug 14 16:54:41 2010 +0800 @@ -438,15 +438,19 @@ then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 else raise TEST lthy6 - (* auxiliary lemmas for respectfulness proofs *) - val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs + (* respectfulness proofs *) + val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 + val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct (raw_size_thms @ raw_size_eqvt) lthy6 + |> map mk_funs_rsp val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros - (alpha_bn_imp_thms @ raw_funs_rsp) lthy6 + (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 + + val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt (* defining the quotient type *) val _ = warning "Declaring the quotient types" @@ -508,13 +512,10 @@ ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) - ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) - ||>> Local_Theory.note ((@{binding "size_simps"}, []), raw_size_thms) ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp) ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp) - ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms) - ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms) - + ||>> Local_Theory.note ((@{binding "permute_rsp"}, []), alpha_permute_rsp) + val _ = if get_STEPS lthy > 17 then true else raise TEST lthy8' diff -r f2f611daf480 -r c670a849af65 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Thu Aug 12 21:29:35 2010 +0800 +++ b/Nominal/nominal_dt_alpha.ML Sat Aug 14 16:54:41 2010 +0800 @@ -30,7 +30,8 @@ val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list - val resolve_fun_rel: thm -> thm + val mk_funs_rsp: thm -> thm + val mk_alpha_permute_rsp: thm -> thm end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = @@ -559,21 +560,21 @@ (** proves the equivp predicate for all alphas **) -val equivp_intro = - @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y. R x y --> (!z. R y z --> R x z)|] ==> equivp R" - by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)} +val transp_def' = + @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" + by (rule eq_reflection, auto simp add: transp_def)} fun raw_prove_equivp alphas refl symm trans ctxt = let - val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars - val refl' = map atomize refl - val symm' = map atomize symm - val trans' = map atomize trans + val refl' = map (fold_rule @{thms reflp_def} o atomize) refl + val symm' = map (fold_rule @{thms symp_def} o atomize) symm + val trans' = map (fold_rule [transp_def'] o atomize) trans + fun prep_goal t = HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) in Goal.prove_multi ctxt [] [] (map prep_goal alphas) - (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac equivp_intro THEN' + (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) end @@ -613,10 +614,11 @@ let val arg_ty = domain_type o fastype_of val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms + fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y) - val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) fvs - val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) bns - val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => HOLogic.mk_eq (t2 $ x, t2 $ y))) alpha_bn_trms fv_bns + val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs + val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) + val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) @@ -690,17 +692,28 @@ end -(* resolve with @{thm fun_relI} *) +(* transformation of the natural rsp-lemmas into the standard form *) + +val fun_rsp = @{lemma + "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp} + +fun mk_funs_rsp thm = + thm + |> atomize + |> single + |> curry (op OF) fun_rsp -fun resolve_fun_rel thm = -let - val fun_rel = @{thm fun_relI} - val thm' = forall_intr_vars thm - val cinsts = Thm.match (cprem_of fun_rel 1, cprop_of thm') - val fun_rel' = Thm.instantiate cinsts fun_rel -in - thm' COMP fun_rel' -end + +val permute_rsp = @{lemma + "(!x y p. R x y --> R (permute p x) (permute p y)) + ==> ((op =) ===> R ===> R) permute permute" by simp} + +fun mk_alpha_permute_rsp thm = + thm + |> atomize + |> single + |> curry (op OF) permute_rsp + end (* structure *)