# HG changeset patch # User Christian Urban # Date 1293009205 0 # Node ID e44551d067e6dfd1a585bfab2a3c0c96b77d0ee4 # Parent dd7490fdd998222dd02c9fbf60808f032ef57876 properly exported strong exhaust theorem; cleaned up some examples diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/Ex/Classical.thy Wed Dec 22 09:13:25 2010 +0000 @@ -2,7 +2,7 @@ imports "../Nominal2" begin -(* example from my Urban's PhD *) +(* example from Urban's PhD *) atom_decl name atom_decl coname @@ -19,12 +19,16 @@ thm trm.distinct thm trm.induct thm trm.exhaust +thm trm.strong_exhaust +thm trm.strong_exhaust[simplified] thm trm.fv_defs thm trm.bn_defs thm trm.perm_simps thm trm.eq_iff thm trm.fv_bn_eqvt thm trm.size_eqvt +thm trm.supp +thm trm.supp[simplified] diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/CoreHaskell2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/CoreHaskell2.thy Wed Dec 22 09:13:25 2010 +0000 @@ -0,0 +1,79 @@ +theory CoreHaskell2 +imports "../Nominal2" +begin + +(* Core Haskell by John Matthews *) + +atom_decl var +atom_decl cvar +atom_decl tvar + + +nominal_datatype kinds: + Kind = + Klifted + | Kunlifted + | Kopen + | Karrow Kind Kind + | Keq Ty Ty +and Ty = + Tvar tvar + | Tcon string + | Tapp Ty Ty + | Tforall pb::PBind ty::Ty bind "bind_pb pb" in ty +and PBind = + Pbind tvar Kind +binder + bind_pb +where + "bind_pb (Pbind tv k) = [atom tv]" + +nominal_datatype expressions: + Bind = + Vb var Ty + | Tb tvar Kind +and Exp = + Var var + | Dcon string + | App Exp Exp + | Appt Exp Ty + | Lam b::Bind e::Exp bind "bind_b b" in e +binder + bind_b +where + "bind_b (Vb v ty) = [atom v]" +| "bind_b (Tb tv kind) = [atom tv]" + +thm kinds.distinct +thm kinds.induct +thm kinds.inducts +thm kinds.exhaust +thm kinds.strong_exhaust +thm kinds.fv_defs +thm kinds.bn_defs +thm kinds.perm_simps +thm kinds.eq_iff +thm kinds.fv_bn_eqvt +thm kinds.size_eqvt +thm kinds.supports +thm kinds.fsupp +thm kinds.supp +thm kinds.fresh + +thm expressions.distinct +thm expressions.induct +thm expressions.inducts +thm expressions.exhaust +thm expressions.fv_defs +thm expressions.bn_defs +thm expressions.perm_simps +thm expressions.eq_iff +thm expressions.fv_bn_eqvt +thm expressions.size_eqvt +thm expressions.supports +thm expressions.fsupp +thm expressions.supp +thm expressions.fresh + +end + diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/Datatypes.thy --- a/Nominal/Ex/Datatypes.thy Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/Ex/Datatypes.thy Wed Dec 22 09:13:25 2010 +0000 @@ -17,6 +17,7 @@ thm Maybe.distinct thm Maybe.induct thm Maybe.exhaust +thm Maybe.strong_exhaust thm Maybe.fv_defs thm Maybe.bn_defs thm Maybe.perm_simps @@ -27,6 +28,9 @@ (* using a datatype inside a nominal_datatype + + the datatype needs to be shown to be an instance + of the pure class (this is usually trivial) *) atom_decl name @@ -55,6 +59,7 @@ thm baz.distinct thm baz.induct thm baz.exhaust +thm baz.strong_exhaust thm baz.fv_defs thm baz.bn_defs thm baz.perm_simps diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/LF.thy --- a/Nominal/Ex/LF.thy Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/Ex/LF.thy Wed Dec 22 09:13:25 2010 +0000 @@ -2,25 +2,40 @@ imports "../Nominal2" begin -declare [[STEPS = 100]] - atom_decl name atom_decl ident -nominal_datatype kind = - Type - | KPi "ty" n::"name" k::"kind" bind n in k +nominal_datatype lf: + kind = + Type + | KPi "ty" n::"name" k::"kind" bind n in k and ty = - TConst "ident" - | TApp "ty" "trm" - | TPi "ty" n::"name" ty::"ty" bind n in ty + TConst "ident" + | TApp "ty" "trm" + | TPi "ty" n::"name" ty::"ty" bind n in ty and trm = - Const "ident" - | Var "name" - | App "trm" "trm" - | Lam "ty" n::"name" t::"trm" bind n in t + Const "ident" + | Var "name" + | App "trm" "trm" + | Lam "ty" n::"name" t::"trm" bind n in t -(*thm kind_ty_trm.supp*) +thm lf.distinct +thm lf.induct +thm lf.inducts +thm lf.exhaust +thm lf.strong_exhaust +thm lf.fv_defs +thm lf.bn_defs +thm lf.perm_simps +thm lf.eq_iff +thm lf.fv_bn_eqvt +thm lf.size_eqvt +thm lf.supports +thm lf.fsupp +thm lf.supp +thm lf.fresh +thm lf.fresh[simplified] + end diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/Ex/Lambda.thy Wed Dec 22 09:13:25 2010 +0000 @@ -3,7 +3,6 @@ begin atom_decl name -declare [[STEPS = 100]] nominal_datatype lam = Var "name" @@ -12,53 +11,27 @@ thm lam.distinct thm lam.induct -thm lam.exhaust +thm lam.exhaust lam.strong_exhaust thm lam.fv_defs thm lam.bn_defs thm lam.perm_simps thm lam.eq_iff -thm lam.eq_iff[folded alphas] thm lam.fv_bn_eqvt thm lam.size_eqvt -section {* Strong Exhausts Lemma and Strong Induction Lemma via Induct_schema *} - -lemma strong_exhaust: - fixes c::"'a::fs" - assumes "\name. \y = Var name\ \ P" - and "\lam1 lam2. \y = App lam1 lam2\ \ P" - and "\name lam. \atom name \ c; y = Lam name lam\ \ P" - shows "P" -apply(rule_tac y="y" in lam.exhaust) -apply(rule assms(1)) -apply(assumption) -apply(rule assms(2)) -apply(assumption) -apply(subgoal_tac "\q. (q \ (atom name)) \ c \ supp (Lam name lam) \* q") -apply(erule exE) -apply(erule conjE) -apply(rule assms(3)) -apply(simp add: atom_eqvt) -apply(clarify) -apply(drule supp_perm_eq[symmetric]) -apply(simp) -apply(rule at_set_avoiding2_atom) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: lam.fresh) -done +section {* Strong Induction Lemma via Induct_schema *} lemma strong_induct: fixes c::"'a::fs" assumes a1: "\name c. P c (Var name)" and a2: "\lam1 lam2 c. \\d. P d lam1; \d. P d lam2\ \ P c (App lam1 lam2)" - and a3: "\name lam c. \atom name \ c; \d. P d lam\ \ P c (Lam name lam)" + and a3: "\name lam c. \{atom name} \* c; \d. P d lam\ \ P c (Lam name lam)" shows "P c lam" using assms apply(induction_schema) -apply(rule_tac y="lam" in strong_exhaust) +apply(rule_tac y="lam" in lam.strong_exhaust) apply(blast) apply(blast) apply(blast) @@ -66,99 +39,6 @@ apply(simp_all add: lam.size) done -section {* Strong Induction Principles*} - -(* - Old way of establishing strong induction - principles by chosing a fresh name. -*) -(* -lemma - fixes c::"'a::fs" - assumes a1: "\name c. P c (Var name)" - and a2: "\lam1 lam2 c. \\d. P d lam1; \d. P d lam2\ \ P c (App lam1 lam2)" - and a3: "\name lam c. \atom name \ c; \d. P d lam\ \ P c (Lam name lam)" - shows "P c lam" -proof - - have "\p. P c (p \ lam)" - apply(induct lam arbitrary: c rule: lam.induct) - apply(perm_simp) - apply(rule a1) - apply(perm_simp) - apply(rule a2) - apply(assumption) - apply(assumption) - apply(subgoal_tac "\new::name. (atom new) \ (c, Lam (p \ name) (p \ lam))") - defer - apply(simp add: fresh_def) - apply(rule_tac X="supp (c, Lam (p \ name) (p \ lam))" in obtain_at_base) - apply(simp add: supp_Pair finite_supp) - apply(blast) - apply(erule exE) - apply(rule_tac t="p \ Lam name lam" and - s="(((p \ name) \ new) + p) \ Lam name lam" in subst) - apply(simp del: lam.perm) - apply(subst lam.perm) - apply(subst (2) lam.perm) - apply(rule flip_fresh_fresh) - apply(simp add: fresh_def) - apply(simp only: supp_fn') - apply(simp) - apply(simp add: fresh_Pair) - apply(simp) - apply(rule a3) - apply(simp add: fresh_Pair) - apply(drule_tac x="((p \ name) \ new) + p" in meta_spec) - apply(simp) - done - then have "P c (0 \ lam)" by blast - then show "P c lam" by simp -qed -*) -(* - New way of establishing strong induction - principles by using a appropriate permutation. -*) -(* -lemma - fixes c::"'a::fs" - assumes a1: "\name c. P c (Var name)" - and a2: "\lam1 lam2 c. \\d. P d lam1; \d. P d lam2\ \ P c (App lam1 lam2)" - and a3: "\name lam c. \atom name \ c; \d. P d lam\ \ P c (Lam name lam)" - shows "P c lam" -proof - - have "\p. P c (p \ lam)" - apply(induct lam arbitrary: c rule: lam.induct) - apply(perm_simp) - apply(rule a1) - apply(perm_simp) - apply(rule a2) - apply(assumption) - apply(assumption) - apply(subgoal_tac "\q. (q \ {p \ atom name}) \* c \ supp (p \ Lam name lam) \* q") - apply(erule exE) - apply(rule_tac t="p \ Lam name lam" and - s="q \ p \ Lam name lam" in subst) - defer - apply(simp) - apply(rule a3) - apply(simp add: eqvts fresh_star_def) - apply(drule_tac x="q + p" in meta_spec) - apply(simp) - apply(rule at_set_avoiding2) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(perm_simp) - apply(simp add: fresh_star_def fresh_def supp_fn') - apply(rule supp_perm_eq) - apply(simp) - done - then have "P c (0 \ lam)" by blast - then show "P c lam" by simp -qed -*) - section {* Typing *} nominal_datatype ty = diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/Ex/Let.thy Wed Dec 22 09:13:25 2010 +0000 @@ -18,7 +18,6 @@ "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)" -thm at_set_avoiding2 thm trm_assn.fv_defs thm trm_assn.eq_iff thm trm_assn.bn_defs @@ -28,28 +27,8 @@ thm trm_assn.distinct thm trm_assn.supp thm trm_assn.fresh -thm trm_assn.exhaust[where y="t", no_vars] - -lemmas permute_bn = permute_bn_raw.simps[quot_lifted] - -lemma uu: - shows "alpha_bn as (permute_bn p as)" -apply(induct as rule: trm_assn.inducts(2)) -apply(auto)[4] -apply(simp add: permute_bn) -apply(simp add: trm_assn.eq_iff) -apply(simp add: permute_bn) -apply(simp add: trm_assn.eq_iff) -done - -lemma tt: - shows "(p \ bn as) = bn (permute_bn p as)" -apply(induct as rule: trm_assn.inducts(2)) -apply(auto)[4] -apply(simp add: permute_bn trm_assn.bn_defs) -apply(simp add: permute_bn trm_assn.bn_defs) -apply(simp add: atom_eqvt) -done +thm trm_assn.exhaust +thm trm_assn.strong_exhaust lemma strong_exhaust1: fixes c::"'a::fs" @@ -58,41 +37,18 @@ and "\name trm. \{atom name} \* c; y = Lam name trm\ \ P" and "\assn trm. \set (bn assn) \* c; y = Let assn trm\ \ P" shows "P" -apply(rule_tac y="y" in trm_assn.exhaust(1)) +apply(rule_tac y="y" in trm_assn.strong_exhaust(1)) apply(rule assms(1)) apply(assumption) apply(rule assms(2)) apply(assumption) -apply(subgoal_tac "\q. (q \ {atom name}) \* c \ supp (Lam name trm) \* q") -apply(erule exE) -apply(erule conjE) apply(rule assms(3)) -apply(perm_simp) +apply(assumption) apply(assumption) -apply(drule supp_perm_eq[symmetric]) -apply(simp) -apply(rule at_set_avoiding2) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: trm_assn.fresh fresh_star_def) -apply(subgoal_tac "\q. (q \ (set (bn assn))) \* (c::'a::fs) \ supp ([bn assn]lst.trm) \* q") -apply(erule exE) -apply(erule conjE) -apply(simp add: set_eqvt) -apply(subst (asm) tt) -apply(rule_tac assms(4)) -apply(simp) -apply(simp add: trm_assn.eq_iff) -apply(drule supp_perm_eq[symmetric]) -apply(simp) -apply(simp add: tt uu) -apply(rule at_set_avoiding2) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: Abs_fresh_star) -done +apply(rule assms(4)) +apply(assumption) +apply(assumption) +sorry lemma strong_exhaust2: diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/SystemFOmega.thy --- a/Nominal/Ex/SystemFOmega.thy Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/Ex/SystemFOmega.thy Wed Dec 22 09:13:25 2010 +0000 @@ -18,9 +18,9 @@ nominal_datatype ty = TVar tvar | TFun ty ty -| TAll a::tvar kind t::ty bind a in t -| TEx a::tvar kind t::ty bind a in t -| TLam a::tvar kind t::ty bind a in t +| TAll a::tvar kind t::ty bind a in t +| TEx a::tvar kind t::ty bind a in t +| TLam a::tvar kind t::ty bind a in t | TApp ty ty | TRec trec and trec = @@ -29,20 +29,50 @@ nominal_datatype trm = Var var -| Lam x::var ty t::trm bind x in t +| Lam x::var ty t::trm bind x in t | App trm trm | Dot trm label -| LAM a::tvar kind t::trm bind a in t +| LAM a::tvar kind t::trm bind a in t | APP trm ty | Pack ty trm -| Unpack a::tvar x::var trm t::trm bind a x in t +| Unpack a::tvar x::var trm t::trm bind a x in t | Rec rec and rec = RNil | RCons label trm rec +thm ty_trec.distinct +thm ty_trec.induct +thm ty_trec.inducts +thm ty_trec.exhaust +thm ty_trec.strong_exhaust +thm ty_trec.fv_defs +thm ty_trec.bn_defs +thm ty_trec.perm_simps +thm ty_trec.eq_iff +thm ty_trec.fv_bn_eqvt +thm ty_trec.size_eqvt +thm ty_trec.supports +thm ty_trec.fsupp +thm ty_trec.supp +thm ty_trec.fresh +thm trm_rec.distinct +thm trm_rec.induct +thm trm_rec.inducts +thm trm_rec.exhaust +thm trm_rec.strong_exhaust +thm trm_rec.fv_defs +thm trm_rec.bn_defs +thm trm_rec.perm_simps +thm trm_rec.eq_iff +thm trm_rec.fv_bn_eqvt +thm trm_rec.size_eqvt +thm trm_rec.supports +thm trm_rec.fsupp +thm trm_rec.supp +thm trm_rec.fresh end diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/Ex/TypeSchemes.thy Wed Dec 22 09:13:25 2010 +0000 @@ -9,8 +9,6 @@ (* defined as a single nominal datatype *) -thm finite_set - nominal_datatype ty = Var "name" | Fun "ty" "ty" @@ -19,7 +17,8 @@ thm ty_tys.distinct thm ty_tys.induct -thm ty_tys.exhaust +thm ty_tys.inducts +thm ty_tys.exhaust ty_tys.strong_exhaust thm ty_tys.fv_defs thm ty_tys.bn_defs thm ty_tys.perm_simps @@ -41,7 +40,7 @@ thm tys2.distinct thm tys2.induct -thm tys2.exhaust +thm tys2.exhaust tys2.strong_exhaust thm tys2.fv_defs thm tys2.bn_defs thm tys2.perm_simps @@ -52,39 +51,13 @@ thm tys2.supp thm tys2.fresh - -lemma strong_exhaust: - fixes c::"'a::fs" - assumes "\names ty. \fset (map_fset atom names) \* c; y = All2 names ty\ \ P" - shows "P" -apply(rule_tac y="y" in tys2.exhaust) -apply(rename_tac names ty2) -apply(subgoal_tac "\q. (q \ (fset (map_fset atom names))) \* c \ supp (All2 names ty2) \* q") -apply(erule exE) -apply(perm_simp) -apply(erule conjE) -apply(rule assms(1)) -apply(assumption) -apply(clarify) -apply(drule supp_perm_eq[symmetric]) -apply(simp) -apply(rule at_set_avoiding2) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp) -apply(simp add: fresh_star_def) -apply(simp add: tys2.fresh) -done - - lemma strong_induct: fixes c::"'a::fs" assumes "\names ty2 c. fset (map_fset atom names) \* c \ P c (All2 names ty2)" shows "P c tys" using assms apply(induction_schema) -apply(rule_tac y="tys" in strong_exhaust) +apply(rule_tac y="tys" in tys2.strong_exhaust) apply(blast) apply(relation "measure (\(x,y). size y)") apply(simp_all add: tys2.size) diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/TypeVarsTest.thy --- a/Nominal/Ex/TypeVarsTest.thy Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/Ex/TypeVarsTest.thy Wed Dec 22 09:13:25 2010 +0000 @@ -2,6 +2,13 @@ imports "../Nominal2" begin +(* a nominal datatype with type variables and sorts *) + + +(* the sort constraints need to be attached to the *) +(* first occurence of the type variables on the *) +(* left-hand side *) + atom_decl name class s1 @@ -10,14 +17,20 @@ instance nat :: s1 .. instance int :: s2 .. -nominal_datatype ('a, 'b) lam = +nominal_datatype ('a, 'b, 'c) lam = Var "name" -| App "('a::s1, 'b::s2) lam" "('a, 'b) lam" -| Lam x::"name" l::"('a, 'b) lam" bind x in l +| App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam" +| Lam x::"name" l::"('a, 'b, 'c) lam" bind x in l +| Foo "'a" "'b" +| Bar x::"'c" l::"('a, 'b, 'c) lam" bind x in l + +term Foo +term Bar thm lam.distinct thm lam.induct -thm lam.exhaust +thm lam.exhaust +thm lam.strong_exhaust thm lam.fv_defs thm lam.bn_defs thm lam.perm_simps diff -r dd7490fdd998 -r e44551d067e6 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/Nominal2.thy Wed Dec 22 09:13:25 2010 +0000 @@ -307,6 +307,7 @@ RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) (prems' ~~ bclausesss) exhausts')] end) + |> ProofContext.export lthy'' lthy end *} @@ -847,6 +848,7 @@ ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) + ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms) ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) diff -r dd7490fdd998 -r e44551d067e6 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Tue Dec 21 10:28:08 2010 +0000 +++ b/Nominal/ROOT.ML Wed Dec 22 09:13:25 2010 +0000 @@ -25,4 +25,5 @@ (*"Ex/Foo1", "Ex/Foo2",*) "Ex/CoreHaskell" + "Ex/CoreHaskell2" ];