# HG changeset patch # User Christian Urban # Date 1271112812 -7200 # Node ID 56cebe7f8e247b05f6b32ea2fd526d39b188762e # Parent 4135198bbb8afddff9f62d5d5cec3f2d1bc85248 some small tunings (incompleted work in Lambda.thy) diff -r 4135198bbb8a -r 56cebe7f8e24 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue Apr 13 00:47:57 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Tue Apr 13 00:53:32 2010 +0200 @@ -141,6 +141,18 @@ apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) done +lemma + shows "valid Gamma \ valid (p \ Gamma)" +ML_prf {* +val ({names, ...}, {raw_induct, intrs, elims, ...}) = + Inductive.the_inductive @{context} (Sign.intern_const @{theory} "valid") +*} +apply(tactic {* rtac raw_induct 1 *}) +apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) +apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) +done + + thm eqvts thm eqvts_raw @@ -151,8 +163,20 @@ | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" -thm typing.induct -ML {* Inductive.get_monos @{context} *} + +ML {* Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *} + +lemma + shows "Gamma \ t : T \ (p \ Gamma) \ (p \ t) : (p \ T)" +ML_prf {* +val ({names, ...}, {raw_induct, intrs, elims, ...}) = + Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") +*} +apply(tactic {* rtac raw_induct 1 *}) +apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) +apply(perm_strict_simp) +apply(rule typing.intros) +oops lemma uu[eqvt]: assumes a: "Gamma \ t : T" @@ -168,10 +192,13 @@ apply(rule impI) prefer 2 apply(rule impI) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) +apply(simp) +apply(auto)[1] +apply(simp) apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) done +(* inductive typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) where @@ -188,6 +215,37 @@ apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) done +*) + +ML {* +val inductive_atomize = @{thms induct_atomize}; + +val atomize_conv = + MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) + (HOL_basic_ss addsimps inductive_atomize); +val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); +fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 + (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); +*} + +ML {* +val ({names, ...}, {raw_induct, intrs, elims, ...}) = + Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") +*} + +ML {* val ind_params = Inductive.params_of raw_induct *} +ML {* val raw_induct = atomize_induct @{context} raw_induct; *} +ML {* val elims = map (atomize_induct @{context}) elims; *} +ML {* val monos = Inductive.get_monos @{context}; *} + +lemma + shows "Gamma \ t : T \ (p \ Gamma) \ (p \ t) : (p \ T)" +apply(tactic {* rtac raw_induct 1 *}) +apply(tactic {* my_tac @{context} intrs 1 *}) +apply(perm_strict_simp) +apply(rule typing.intros) +oops + thm eqvts thm eqvts_raw diff -r 4135198bbb8a -r 56cebe7f8e24 Nominal/FSet.thy --- a/Nominal/FSet.thy Tue Apr 13 00:47:57 2010 +0200 +++ b/Nominal/FSet.thy Tue Apr 13 00:53:32 2010 +0200 @@ -43,8 +43,7 @@ quotient_definition fin ("_ |\| _" [50, 51] 50) where - "fin :: 'a \ 'a fset \ bool" -is "memb" + "fin :: 'a \ 'a fset \ bool" is "memb" abbreviation fnotin :: "'a \ 'a fset \ bool" ("_ |\| _" [50, 51] 50) @@ -63,7 +62,7 @@ shows "(op = ===> op \ ===> op \) op # op #" by simp -section {* Augmenting a set -- @{const finsert} *} +section {* Augmenting an fset -- @{const finsert} *} lemma nil_not_cons: shows