# HG changeset patch # User Christian Urban # Date 1310546878 -3600 # Node ID fa37c2a33812f52cb6a769b2be0217dee5debac5 # Parent d8a6b424f80aec01f475d04ab485071d4369db7f slight tuning diff -r d8a6b424f80a -r fa37c2a33812 Nominal/Ex/LetSimple2.thy --- a/Nominal/Ex/LetSimple2.thy Tue Jul 12 03:12:32 2011 +0900 +++ b/Nominal/Ex/LetSimple2.thy Wed Jul 13 09:47:58 2011 +0100 @@ -2,6 +2,19 @@ imports "../Nominal2" begin +(* +ML {* + val lemma = + Term_XML.Encode.term #> + YXML.string_of_body #> + translate_string (fn c => if ord c < 10 then "\\00" ^ string_of_int (ord c) else c) #> + quote #> prefix "lemma " #> + Markup.markup Markup.sendback #> writeln +*} + +ML {* lemma @{prop "x == x"} *} +*) + atom_decl name nominal_datatype trm = @@ -37,20 +50,20 @@ thm trm_assn.perm_bn_simps thm alpha_bn_raw.cases - +thm trm_assn.alpha_refl +thm trm_assn.alpha_sym +thm trm_assn.alpha_trans lemmas alpha_bn_cases[consumes 1] = alpha_bn_raw.cases[quot_lifted] lemma alpha_bn_refl: "alpha_bn x x" - by (induct x rule: trm_assn.inducts(2)) - (rule TrueI, auto simp add: trm_assn.eq_iff) + by(rule trm_assn.alpha_refl) + lemma alpha_bn_sym: "alpha_bn x y \ alpha_bn y x" - apply(erule alpha_bn_cases) - apply(auto) - done + by (rule trm_assn.alpha_sym) lemma alpha_bn_trans: "alpha_bn x y \ alpha_bn y z \ alpha_bn x z" - sorry + using trm_assn.alpha_trans by metis lemma k: "A \ A \ A" by blast @@ -133,6 +146,9 @@ apply(simp_all add: eqvt_at_def) done +(* assn-function prevents automatic discharge +termination by lexicographic_order +*) nominal_primrec subst_trm :: "trm \ name \ trm \ trm" ("_ [_ ::= _]" [90, 90, 90] 90) @@ -166,7 +182,8 @@ lemma cheat: "P" sorry -nominal_primrec (invariant "\x y. case x of Inl x1 \ True | Inr x2 \ \p. (permute_bn p x2) = x2 \ (p \ y) = y") +nominal_primrec + (invariant "\x y. case x of Inl x1 \ True | Inr x2 \ \p. (permute_bn p x2) = x2 \ (p \ y) = y") height_trm2 :: "trm \ nat" and height_assn2 :: "assn \ nat" where @@ -174,7 +191,7 @@ | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)" | "height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)" | "height_assn2 (Assn x t) = (height_trm2 t)" - thm height_trm2_height_assn2_graph.intros + thm height_trm2_height_assn2_graph.intros[no_vars] thm height_trm2_height_assn2_graph_def apply (simp only: eqvt_def height_trm2_height_assn2_graph_def) apply (rule, perm_simp, rule) @@ -299,14 +316,14 @@ nominal_primrec (default "sum_case (\x. Inl undefined) (\x. Inr undefined)") - subst_trm :: "trm \ name \ trm \ trm" ("_ [_ ::trm= _]" [90, 90, 90] 90) and - subst_assn :: "assn \ name \ trm \ assn" ("_ [_ ::assn= _]" [90, 90, 90] 90) + subst_trm2 :: "trm \ name \ trm \ trm" ("_ [_ ::trm2= _]" [90, 90, 90] 90) and + subst_assn2 :: "assn \ name \ trm \ assn" ("_ [_ ::assn2= _]" [90, 90, 90] 90) where - "(Var x)[y ::trm= s] = (if x = y then s else (Var x))" -| "(App t1 t2)[y ::trm= s] = App (t1[y ::trm= s]) (t2[y ::trm= s])" -| "(set (bn as)) \* (y, s) \ (Let as t)[y ::trm= s] = Let (ast[y ::assn= s]) (t[y ::trm= s])" -| "(Assn x t)[y ::assn= s] = Assn x (t[y ::trm= s])" -apply(subgoal_tac "\p x r. subst_trm_subst_assn_graph x r \ subst_trm_subst_assn_graph (p \ x) (p \ r)") + "(Var x)[y ::trm2= s] = (if x = y then s else (Var x))" +| "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])" +| "(set (bn as)) \* (y, s) \ (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])" +| "(Assn x t)[y ::assn2= s] = Assn x (t[y ::trm2= s])" +apply(subgoal_tac "\p x r. subst_trm2_subst_assn2_graph x r \ subst_trm2_subst_assn2_graph (p \ x) (p \ r)") apply(simp add: eqvt_def) apply(rule allI) apply(simp add: permute_fun_def permute_bool_def) @@ -336,31 +353,41 @@ apply(rule_tac y="a" in trm_assn.exhaust(2)) apply(simp) apply(blast) - apply(simp_all)[7] - prefer 2 +--"compatibility" + apply(all_trivials) + apply(simp) apply(simp) prefer 2 apply(simp) + thm Inl_inject + apply(drule Inl_inject) + apply(rule arg_cong) + back + apply (simp only: meta_eq_to_obj_eq[OF subst_trm2_def, symmetric, unfolded fun_eq_iff]) + apply (simp only: meta_eq_to_obj_eq[OF subst_assn2_def, symmetric, unfolded fun_eq_iff]) + apply (subgoal_tac "eqvt_at (\ast. subst_assn2 ast ya sa) ast") + apply (subgoal_tac "eqvt_at (\asta. subst_assn2 asta ya sa) asta") + apply (subgoal_tac "eqvt_at (\t. subst_trm2 t ya sa) t") + apply (subgoal_tac "eqvt_at (\ta. subst_trm2 ta ya sa) ta") + apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (ast, y, s))") + apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (asta, ya, sa))") + apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (t, y, s))") + apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (ta, ya, sa))") + defer + apply(simp add: Abs_eq_iff alphas) + apply(clarify) + apply(rule eqvt_at_perm) apply(simp) - apply (simp only: meta_eq_to_obj_eq[OF subst_trm_def, symmetric, unfolded fun_eq_iff]) - apply (simp only: meta_eq_to_obj_eq[OF subst_assn_def, symmetric, unfolded fun_eq_iff]) - apply (subgoal_tac "eqvt_at (\ast. subst_assn ast ya sa) ast") - apply (subgoal_tac "eqvt_at (\asta. subst_assn asta ya sa) asta") - apply (subgoal_tac "eqvt_at (\t. subst_trm t ya sa) t") - apply (subgoal_tac "eqvt_at (\ta. subst_trm ta ya sa) ta") - apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inr (ast, ya, sa))") - apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inr (asta, ya, sa))") - apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inl (t, ya, sa))") - apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inl (ta, ya, sa))") - defer + apply(simp add: subst_trm2_def) + apply(simp add: eqvt_at_def) defer defer defer defer defer apply(rule conjI) - apply (subgoal_tac "subst_assn ast ya sa= subst_assn asta ya sa") - apply (subgoal_tac "subst_trm t ya sa = subst_trm ta ya sa") + apply (subgoal_tac "subst_assn2 ast ya sa= subst_assn2 asta ya sa") + apply (subgoal_tac "subst_trm2 t ya sa = subst_trm2 ta ya sa") apply(simp) apply(erule_tac conjE)+ apply(erule alpha_bn_cases) diff -r d8a6b424f80a -r fa37c2a33812 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue Jul 12 03:12:32 2011 +0900 +++ b/Nominal/Nominal2.thy Wed Jul 13 09:47:58 2011 +0100 @@ -328,7 +328,7 @@ val alpha_bn_rsp = raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms - val raw_perm_bn_rsp =raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps + val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps (* noting the quot_respects lemmas *) val (_, lthy6) = @@ -408,7 +408,7 @@ val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, - qalpha_refl_thms ], lthyB) = + qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) = lthy9a |>>> lift_thms qtys [] alpha_distincts ||>>> lift_thms qtys eq_iff_simps alpha_eq_iff @@ -423,6 +423,8 @@ ||>>> lift_thms qtys [] raw_size_thms ||>>> lift_thms qtys [] raw_perm_bn_simps ||>>> lift_thms qtys [] alpha_refl_thms + ||>>> lift_thms qtys [] alpha_sym_thms + ||>>> lift_thms qtys [] alpha_trans_thms val qinducts = Project_Rule.projections lthyB qinduct @@ -512,6 +514,10 @@ ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) + ||>> Local_Theory.note ((thms_suffix "alpha_refl", []), qalpha_refl_thms) + ||>> Local_Theory.note ((thms_suffix "alpha_sym", []), qalpha_sym_thms) + ||>> Local_Theory.note ((thms_suffix "alpha_trans", []), qalpha_trans_thms) + in lthy9' end