# HG changeset patch # User Christian Urban # Date 1282759680 -28800 # Node ID 3885dc2669f9052800210f700a76d2b04720383f # Parent 3772bb3bd7ce43a0b0c118ccb42e6be5b2de148a cleaned up (almost completely) the examples diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/Classical.thy Thu Aug 26 02:08:00 2010 +0800 @@ -7,8 +7,6 @@ atom_decl name atom_decl coname -declare [[STEPS = 21]] - nominal_datatype trm = Ax "name" "coname" | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 @@ -18,15 +16,15 @@ | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t -thm distinct -thm induct -thm exhaust -thm fv_defs -thm bn_defs -thm perm_simps -thm eq_iff -thm fv_bn_eqvt -thm size_eqvt +thm trm.distinct +thm trm.induct +thm trm.exhaust +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 diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/CoreHaskell.thy Thu Aug 26 02:08:00 2010 +0800 @@ -8,9 +8,10 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 21]] +declare [[STEPS = 100]] -nominal_datatype tkind = +nominal_datatype core_haskell: + tkind = KStar | KFun "tkind" "tkind" and ckind = @@ -85,31 +86,19 @@ | "bv_cvs CvsNil = []" | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" -(* can lift *) - -thm distinct -thm induct -thm exhaust -thm fv_defs -thm bn_defs -thm perm_simps -thm eq_iff -thm fv_bn_eqvt -thm size_eqvt - +(* generated theorems *) - - +thm core_haskell.distinct +thm core_haskell.induct +thm core_haskell.exhaust +thm core_haskell.fv_defs +thm core_haskell.bn_defs +thm core_haskell.perm_simps +thm core_haskell.eq_iff +thm core_haskell.fv_bn_eqvt +thm core_haskell.size_eqvt -lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) -lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] -lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm -lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff -lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts - -lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts -lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros - +(* lemma fresh_star_minus_perm: "as \* - p = as \* (p :: perm)" unfolding fresh_star_def Ball_def by auto (simp_all add: fresh_minus_perm) @@ -397,7 +386,7 @@ apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) -(* GOAL1 *) +--"GOAL1" apply(subgoal_tac "\pa. ((pa \ (atom (p \ tvar))) \ c \ supp (Abs (p \ {atom tvar}) (p \ ty)) \* pa)") apply clarify @@ -435,7 +424,7 @@ apply (simp only: supp_abs eqvts) apply blast -(* GOAL2 *) +--"GOAL2" apply(subgoal_tac "\pa. ((pa \ (atom (p \ cvar))) \ e \ supp (Abs (p \ {atom cvar}) (p \ co)) \* pa)") apply clarify @@ -474,7 +463,7 @@ apply blast -(* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *) +--"GOAL3 a copy-and-paste of Goal2 with consts and variable names changed" apply(subgoal_tac "\pa. ((pa \ (atom (p \ tvar))) \ g \ supp (Abs (p \ {atom tvar}) (p \ trm)) \* pa)") apply clarify @@ -512,7 +501,7 @@ apply (simp only: supp_abs eqvts) apply blast -(* GOAL4 a copy-and-paste *) +--"GOAL4 a copy-and-paste" apply(subgoal_tac "\pa. ((pa \ (atom (p \ cvar))) \ g \ supp (Abs (p \ {atom cvar}) (p \ trm)) \* pa)") apply clarify @@ -551,7 +540,7 @@ apply blast -(* GOAL5 a copy-and-paste *) +--"GOAL5 a copy-and-paste" apply(subgoal_tac "\pa. ((pa \ (atom (p \ var))) \ g \ supp (Abs (p \ {atom var}) (p \ trm)) \* pa)") apply clarify @@ -590,7 +579,7 @@ apply blast -(* GOAL6 a copy-and-paste *) +--"GOAL6 a copy-and-paste" apply(subgoal_tac "\pa. ((pa \ (atom (p \ var))) \ g \ supp (Abs (p \ {atom var}) (p \ trm2)) \* pa)") apply clarify @@ -629,7 +618,7 @@ apply (simp only: supp_abs eqvts) apply blast -(* MAIN ACons Goal *) +--"MAIN ACons Goal" apply(subgoal_tac "\pa. ((pa \ (set (bv (p \ pat)))) \* h \ supp (Abs_lst (p \ (bv pat)) (p \ trm)) \* pa)") apply clarify @@ -655,6 +644,7 @@ moreover have "P9 i (permute_bv 0 (0 \ pt))" and "P10 j (permute_bv_vs 0 (0 \ vars))" and "P11 k (permute_bv_tvs 0 (0 \ tvars))" and "P12 l (permute_bv_cvs 0 (0 \ cvars))" using a1 a2 a3 a4 by (blast+) ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) qed +*) section {* test about equivariance for alpha *} diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Ex1rec.thy --- a/Nominal/Ex/Ex1rec.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,40 +0,0 @@ -theory Ex1rec -imports "../NewParser" -begin - -declare [[STEPS = 9]] - -atom_decl name - -nominal_datatype lam = - Var "name" -| App "lam" "lam" -| Lam x::"name" t::"lam" bind_set x in t -| Let bp::"bp" t::"lam" bind_set "bi bp" in bp t -and bp = - Bp "name" "lam" -binder - bi::"bp \ atom set" -where - "bi (Bp x t) = {atom x}" - - -thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros - -thm lam_bp.fv -thm lam_bp.eq_iff[no_vars] -thm lam_bp.bn -thm lam_bp.perm -thm lam_bp.induct -thm lam_bp.inducts -thm lam_bp.distinct -thm lam_bp.supp -ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} -thm lam_bp.fv[simplified lam_bp.supp(1-2)] - - - -end - - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Ex2.thy --- a/Nominal/Ex/Ex2.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -theory Ex2 -imports "../NewParser" -begin - -text {* example 2 *} -declare [[STEPS = 9]] - -atom_decl name - -nominal_datatype trm = - Var "name" -| App "trm" "trm" -| Lam x::"name" t::"trm" bind_set x in t -| Let p::"pat" "trm" t::"trm" bind_set "f p" in t -and pat = - PN -| PS "name" -| PD "name" "name" -binder - f::"pat \ atom set" -where - "f PN = {}" -| "f (PD x y) = {atom x, atom y}" -| "f (PS x) = {atom x}" - -thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars] -thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars] - - - - -thm trm_pat.bn -thm trm_pat.perm -thm trm_pat.induct -thm trm_pat.distinct -thm trm_pat.fv[simplified trm_pat.supp(1-2)] - - -end - - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Ex3.thy --- a/Nominal/Ex/Ex3.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ -theory Ex3 -imports "../NewParser" -begin - -(* Example 3, identical to example 1 from Terms.thy *) - -atom_decl name - -nominal_datatype trm = - Var "name" -| App "trm" "trm" -| Lam x::"name" t::"trm" bind_set x in t -| Let p::"pat" "trm" t::"trm" bind_set "f p" in t -and pat = - PN -| PS "name" -| PD "pat" "pat" -binder - f::"pat \ atom set" -where - "f PN = {}" -| "f (PS x) = {atom x}" -| "f (PD p1 p2) = (f p1) \ (f p2)" - -thm trm_pat.fv -thm trm_pat.eq_iff -thm trm_pat.bn -thm trm_pat.perm -thm trm_pat.induct -thm trm_pat.distinct -thm trm_pat.fv[simplified trm_pat.supp(1-2)] - - - -end - - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Ex4.thy --- a/Nominal/Ex/Ex4.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,87 +0,0 @@ -theory Ex4 -imports "../NewParser" -begin - -declare [[STEPS = 5]] - -atom_decl name - -nominal_datatype trm = - Var "name" -| App "trm" "trm" -| Lam x::"name" t::"trm" bind_set x in t -| Let p::"pat" "trm" t::"trm" bind_set "f p" in t -| Foo1 p::"pat" q::"pat" t::"trm" bind_set "f p" "f q" in t -| Foo2 x::"name" p::"pat" t::"trm" bind_set x "f p" in t -and pat = - PN -| PS "name" -| PD "pat" "pat" -binder - f::"pat \ atom set" -where - "f PN = {}" -| "f (PS x) = {atom x}" -| "f (PD p1 p2) = (f p1) \ (f p2)" - -thm permute_trm_raw_permute_pat_raw.simps -thm fv_trm_raw.simps fv_pat_raw.simps fv_f_raw.simps - -thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars] - -(* -inductive - alpha_trm_raw and alpha_pat_raw and alpha_f_raw -where -(* alpha_trm_raw *) - "name = namea \ alpha_trm_raw (Var_raw name) (Var_raw namea)" -| "\alpha_trm_raw trm_raw1 trm_raw1a; alpha_trm_raw trm_raw2 trm_raw2a\ - \ alpha_trm_raw (App_raw trm_raw1 trm_raw2) (App_raw trm_raw1a trm_raw2a)" -| "\p. ({atom name}, trm_raw) \gen alpha_trm_raw fv_trm_raw p ({atom namea}, trm_rawa) \ - alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)" -| "\\p. (f_raw pat_raw, trm_raw2) \gen alpha_trm_raw fv_trm_raw p (f_raw pat_rawa, trm_raw2a); - alpha_f_raw pat_raw pat_rawa; alpha_trm_raw trm_raw1 trm_raw1a\ - \ alpha_trm_raw (Let_raw pat_raw trm_raw1 trm_raw2) (Let_raw pat_rawa trm_raw1a trm_raw2a)" -| "\\p. (f_raw pat_raw1 \ f_raw pat_raw2, trm_raw) \gen alpha_trm_raw fv_trm_raw p (f_raw pat_raw1a \ f_raw pat_raw2a, trm_rawa); - alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\ - \ alpha_trm_raw (Foo1_raw pat_raw1 pat_raw2 trm_raw) (Foo1_raw pat_raw1a pat_raw2a trm_rawa)" -| "\\p. ({atom name} \ f_raw pat_raw, trm_raw) \gen alpha_trm_raw fv_trm_raw p ({atom namea} \ f_raw pat_rawa, trm_rawa); - alpha_f_raw pat_raw pat_rawa\ - \ alpha_trm_raw (Foo2_raw name pat_raw trm_raw) (Foo2_raw namea pat_rawa trm_rawa)" - -(* alpha_pat_raw *) -| "alpha_pat_raw PN_raw PN_raw" -| "name = namea \ alpha_pat_raw (PS_raw name) (PS_raw namea)" -| "\alpha_pat_raw pat_raw1 pat_raw1a; alpha_pat_raw pat_raw2 pat_raw2a\ - \ alpha_pat_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" - -(* alpha_f_raw *) -| "alpha_f_raw PN_raw PN_raw" -| "alpha_f_raw (PS_raw name) (PS_raw namea)" -| "\alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\ - \ alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" -*) - -lemmas all = alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros - -lemma - shows "alpha_trm_raw (Foo2_raw x (PS_raw x) (Var_raw x)) - (Foo2_raw y (PS_raw y) (Var_raw y))" -apply(rule all) -apply(rule_tac x="(atom x \ atom y)" in exI) -apply(simp add: alphas) -apply(simp add: supp_at_base fresh_star_def) -apply(rule conjI) -apply(rule all) -apply(simp) -apply(perm_simp) -apply(simp) -apply(rule all) -done - - - -end - - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/ExLet.thy --- a/Nominal/Ex/ExLet.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,225 +0,0 @@ -theory ExLet -imports "../NewParser" "../../Attic/Prove" -begin - -text {* example 3 or example 5 from Terms.thy *} - -atom_decl name - -nominal_datatype trm = - Vr "name" -| Ap "trm" "trm" -| Lm x::"name" t::"trm" bind_set x in t -| Lt a::"lts" t::"trm" bind "bn a" in t -(*| L a::"lts" t1::"trm" t2::"trm" bind "bn a" in t1, bind "bn a" in t2*) -and lts = - Lnil -| Lcons "name" "trm" "lts" -binder - bn -where - "bn Lnil = []" -| "bn (Lcons x t l) = (atom x) # (bn l)" - - -thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros - -thm trm_lts.fv -thm trm_lts.eq_iff -thm trm_lts.bn -thm trm_lts.perm -thm trm_lts.induct[no_vars] -thm trm_lts.inducts[no_vars] -thm trm_lts.distinct -(*thm trm_lts.supp*) -thm trm_lts.fv[simplified trm_lts.supp(1-2)] - - -primrec - permute_bn_raw -where - "permute_bn_raw pi (Lnil_raw) = Lnil_raw" -| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \ a) t (permute_bn_raw pi l)" - -quotient_definition - "permute_bn :: perm \ lts \ lts" -is - "permute_bn_raw" - -lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" - apply simp - apply clarify - apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) - apply (rule TrueI)+ - apply simp_all - apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) - apply simp_all - done - -lemmas permute_bn = permute_bn_raw.simps[quot_lifted] - -lemma permute_bn_zero: - "permute_bn 0 a = a" - apply(induct a rule: trm_lts.inducts(2)) - apply(rule TrueI)+ - apply(simp_all add:permute_bn) - done - -lemma permute_bn_add: - "permute_bn (p + q) a = permute_bn p (permute_bn q a)" - oops - -lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" - apply(induct lts rule: trm_lts.inducts(2)) - apply(rule TrueI)+ - apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) - done - -lemma perm_bn: - "p \ bn l = bn(permute_bn p l)" - apply(induct l rule: trm_lts.inducts(2)) - apply(rule TrueI)+ - apply(simp_all add:permute_bn eqvts) - done - -lemma fv_perm_bn: - "fv_bn l = fv_bn (permute_bn p l)" - apply(induct l rule: trm_lts.inducts(2)) - apply(rule TrueI)+ - apply(simp_all add:permute_bn eqvts) - done - -lemma Lt_subst: - "supp (Abs_lst (bn lts) trm) \* q \ (Lt lts trm) = Lt (permute_bn q lts) (q \ trm)" - apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn) - apply (rule_tac x="q" in exI) - apply (simp add: alphas) - apply (simp add: perm_bn[symmetric]) - apply(rule conjI) - apply(drule supp_perm_eq) - apply(simp add: abs_eq_iff) - apply(simp add: alphas_abs alphas) - apply(drule conjunct1) - apply (simp add: trm_lts.supp) - apply(simp add: supp_abs) - apply (simp add: trm_lts.supp) - done - - -lemma fin_bn: - "finite (set (bn l))" - apply(induct l rule: trm_lts.inducts(2)) - apply(simp_all add:permute_bn eqvts) - done - -thm trm_lts.inducts[no_vars] - -lemma - fixes t::trm - and l::lts - and c::"'a::fs" - assumes a1: "\name c. P1 c (Vr name)" - and a2: "\trm1 trm2 c. \\d. P1 d trm1; \d. P1 d trm2\ \ P1 c (Ap trm1 trm2)" - and a3: "\name trm c. \atom name \ c; \d. P1 d trm\ \ P1 c (Lm name trm)" - and a4: "\lts trm c. \set (bn lts) \* c; \d. P2 d lts; \d. P1 d trm\ \ P1 c (Lt lts trm)" - and a5: "\c. P2 c Lnil" - and a6: "\name trm lts c. \\d. P1 d trm; \d. P2 d lts\ \ P2 c (Lcons name trm lts)" - shows "P1 c t" and "P2 c l" -proof - - have "(\(p::perm) (c::'a::fs). P1 c (p \ t))" and - b': "(\(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \ l)))" - apply(induct rule: trm_lts.inducts) - apply(simp) - apply(rule a1) - apply(simp) - apply(rule a2) - apply(simp) - apply(simp) - apply(simp) - apply(subgoal_tac "\q. (q \ (atom (p \ name))) \ c \ supp (Lm (p \ name) (p \ trm)) \* q") - apply(erule exE) - apply(rule_tac t="Lm (p \ name) (p \ trm)" - and s="q\ Lm (p \ name) (p \ trm)" in subst) - apply(rule supp_perm_eq) - apply(simp) - apply(simp) - apply(rule a3) - apply(simp add: atom_eqvt) - apply(subst permute_plus[symmetric]) - apply(blast) - apply(rule at_set_avoiding2_atom) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: fresh_def) - apply(simp add: trm_lts.fv[simplified trm_lts.supp]) - apply(simp) - apply(subgoal_tac "\q. (q \ set (bn (p \ lts))) \* c \ supp (Abs_lst (bn (p \ lts)) (p \ trm)) \* q") - apply(erule exE) - apply(erule conjE) - thm Lt_subst - apply(subst Lt_subst) - apply assumption - apply(rule a4) - apply(simp add:perm_bn[symmetric]) - apply(simp add: eqvts) - apply (simp add: fresh_star_def fresh_def) - apply(rotate_tac 1) - apply(drule_tac x="q + p" in meta_spec) - apply(simp) - apply(rule at_set_avoiding2) - apply(rule fin_bn) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: fresh_star_def fresh_def supp_abs) - apply(simp add: eqvts permute_bn) - apply(rule a5) - apply(simp add: permute_bn) - apply(rule a6) - apply simp - apply simp - done - then have a: "P1 c (0 \ t)" by blast - have "P2 c (permute_bn 0 (0 \ l))" using b' by blast - then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all -qed - - - -lemma lets_bla: - "x \ z \ y \ z \ x \ y \(Lt (Lcons x (Vr y) Lnil) (Vr x)) \ (Lt (Lcons x (Vr z) Lnil) (Vr x))" - by (simp add: trm_lts.eq_iff) - -lemma lets_ok: - "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" - apply (simp add: trm_lts.eq_iff) - apply (rule_tac x="(x \ y)" in exI) - apply (simp_all add: alphas eqvts supp_at_base fresh_star_def) - done - -lemma lets_ok3: - "x \ y \ - (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ - (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" - apply (simp add: alphas trm_lts.eq_iff) - done - - -lemma lets_not_ok1: - "x \ y \ - (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ - (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" - apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts) - done - -lemma lets_nok: - "x \ y \ x \ z \ z \ y \ - (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \ - (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" - apply (simp add: alphas trm_lts.eq_iff fresh_star_def) - done - - -end - - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/ExLetMult.thy --- a/Nominal/Ex/ExLetMult.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -theory ExLetMult -imports "../NewParser" -begin - -atom_decl name - -nominal_datatype trm = - Vr "name" -| Ap "trm" "trm" -| Lm x::"name" t::"trm" bind_set x in t -| Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t s -and lts = - Lnil -| Lcons "name" "trm" "lts" -binder - bn -where - "bn Lnil = []" -| "bn (Lcons x t l) = (atom x) # (bn l)" - -thm trm_lts.eq_iff -thm trm_lts.induct -thm trm_lts.fv[simplified trm_lts.supp] - - - -end - - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/ExLetRec.thy --- a/Nominal/Ex/ExLetRec.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,85 +0,0 @@ -theory ExLetRec -imports "../NewParser" -begin - - -text {* example 3 or example 5 from Terms.thy *} - -atom_decl name - -ML {* val _ = cheat_equivp := true *} - -nominal_datatype trm = - Vr "name" -| Ap "trm" "trm" -| Lm x::"name" t::"trm" bind_set x in t -| Lt a::"lts" t::"trm" bind "bn a" in a t -and lts = - Lnil -| Lcons "name" "trm" "lts" -binder - bn -where - "bn Lnil = []" -| "bn (Lcons x t l) = (atom x) # (bn l)" - -thm trm_lts.fv -thm trm_lts.eq_iff -thm trm_lts.bn -thm trm_lts.perm -thm trm_lts.induct -thm trm_lts.distinct -thm trm_lts.supp -thm trm_lts.fv[simplified trm_lts.supp] - - -(* why is this not in HOL simpset? *) -lemma set_sub: "{a, b} - {b} = {a} - {b}" -by auto - -lemma lets_bla: - "x \ z \ y \ z \ x \ y \(Lt (Lcons x (Vr y) Lnil) (Vr x)) \ (Lt (Lcons x (Vr z) Lnil) (Vr x))" - apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base) - done - -lemma lets_ok: - "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" - apply (simp add: trm_lts.eq_iff) - apply (rule_tac x="(x \ y)" in exI) - apply (simp_all add: alphas fresh_star_def eqvts supp_at_base) - done - -lemma lets_ok3: - "x \ y \ - (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ - (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" - apply (simp add: alphas trm_lts.eq_iff) - done - - -lemma lets_not_ok1: - "x \ y \ - (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ - (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" - apply (simp add: alphas trm_lts.eq_iff) - done - -lemma lets_nok: - "x \ y \ x \ z \ z \ y \ - (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \ - (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" - apply (simp add: alphas trm_lts.eq_iff fresh_star_def) - done - -lemma lets_ok4: - "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = - (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))" - apply (simp add: alphas trm_lts.eq_iff supp_at_base) - apply (rule_tac x="(x \ y)" in exI) - apply (simp add: atom_eqvt fresh_star_def) - done - -end - - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/ExPS3.thy --- a/Nominal/Ex/ExPS3.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/ExPS3.thy Thu Aug 26 02:08:00 2010 +0800 @@ -6,14 +6,11 @@ atom_decl name -ML {* val _ = cheat_equivp := true *} -ML {* val _ = cheat_alpha_bn_rsp := true *} - nominal_datatype exp = Var "name" | App "exp" "exp" -| Lam x::"name" e::"exp" bind_set x in e -| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1 +| Lam x::"name" e::"exp" bind x in e +| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind (set) x in e2, bind (set) "bp p" in e1 and pat = PVar "name" | PUnit @@ -25,16 +22,16 @@ | "bp (PUnit) = {}" | "bp (PPair p1 p2) = bp p1 \ bp p2" -thm exp_pat.fv -thm exp_pat.eq_iff -thm exp_pat.bn -thm exp_pat.perm + +thm exp_pat.distinct thm exp_pat.induct -thm exp_pat.distinct -thm exp_pat.fv -thm exp_pat.supp(1-2) - - +thm exp_pat.exhaust +thm exp_pat.fv_defs +thm exp_pat.bn_defs +thm exp_pat.perm_simps +thm exp_pat.eq_iff +thm exp_pat.fv_bn_eqvt +thm exp_pat.size_eqvt end diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/ExPS6.thy --- a/Nominal/Ex/ExPS6.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,41 +0,0 @@ -theory ExPS6 -imports "../NewParser" -begin - -(* example 6 from Peter Sewell's bestiary *) - -atom_decl name - -(* Is this binding structure supported - I think not - because e1 occurs twice as body *) - -nominal_datatype exp = - Var name -| Pair exp exp -| LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "bp p" in e1 -and pat = - PVar name -| PUnit -| PPair pat pat -binder - bp :: "pat \ atom list" -where - "bp (PVar x) = [atom x]" -| "bp (PUnit) = []" -| "bp (PPair p1 p2) = bp p1 @ bp p2" - -thm exp_pat.fv -thm exp_pat.eq_iff -thm exp_pat.bn -thm exp_pat.perm -thm exp_pat.induct -thm exp_pat.distinct -thm exp_pat.supp - - - - -end - - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/ExPS7.thy --- a/Nominal/Ex/ExPS7.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/ExPS7.thy Thu Aug 26 02:08:00 2010 +0800 @@ -11,7 +11,7 @@ Var name | Unit | Pair exp exp -| LetRec l::"lrbs" e::"exp" bind_set "bs l" in l e +| LetRec l::"lrbs" e::"exp" bind (set) "bs l" in l e and lrb = Assign name exp and lrbs = @@ -25,8 +25,6 @@ | "bs (Single a) = b a" | "bs (More a as) = (b a) \ (bs as)" -thm exp_lrb_lrbs.eq_iff -thm exp_lrb_lrbs.supp end diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/ExPS8.thy Thu Aug 26 02:08:00 2010 +0800 @@ -6,17 +6,13 @@ atom_decl name -ML {* val _ = cheat_fv_rsp := true *} -ML {* val _ = cheat_equivp := true *} -ML {* val _ = cheat_alpha_bn_rsp := true *} - nominal_datatype exp = EVar name | EUnit | EPair exp exp -| ELetRec l::lrbs e::exp bind_set "b_lrbs l" in l e +| ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e and fnclause = - K x::name p::pat f::exp bind_set "b_pat p" in f + K x::name p::pat f::exp bind (set) "b_pat p" in f and fnclauses = S fnclause | ORs fnclause fnclauses @@ -46,8 +42,6 @@ | "b_lrb (Clause fcs) = (b_fnclauses fcs)" | "b_fnclause (K x pat exp) = {atom x}" -thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv -thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff end diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/LF.thy --- a/Nominal/Ex/LF.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/LF.thy Thu Aug 26 02:08:00 2010 +0800 @@ -2,7 +2,7 @@ imports "../NewParser" begin -declare [[STEPS = 9]] +declare [[STEPS = 20]] atom_decl name atom_decl ident @@ -13,17 +13,14 @@ and ty = TConst "ident" | TApp "ty" "trm" - | TPi "ty" n::"name" t::"ty" bind n in t + | 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 -thm kind_ty_trm.supp - - - +(*thm kind_ty_trm.supp*) end diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/Lambda.thy Thu Aug 26 02:08:00 2010 +0800 @@ -5,32 +5,22 @@ atom_decl name declare [[STEPS = 21]] -class s1 -class s2 - -nominal_datatype lambda: - ('a, 'b) lam = +nominal_datatype lam = Var "name" -| App "('a::s1, 'b::s2) lam" "('a, 'b) lam" -| Lam x::"name" l::"('a, 'b) lam" bind x in l +| App "lam" "lam" +| Lam x::"name" l::"lam" bind x in l -thm distinct -thm induct -thm exhaust -thm fv_defs -thm bn_defs -thm perm_simps -thm eq_iff -thm fv_bn_eqvt -thm size_eqvt +thm lam.distinct +thm lam.induct +thm lam.exhaust +thm lam.fv_defs +thm lam.bn_defs +thm lam.perm_simps +thm lam.eq_iff +thm lam.fv_bn_eqvt +thm lam.size_eqvt -thm lam.fv -thm lam.supp -lemmas supp_fn' = lam.fv[simplified lam.supp] - -declare lam.perm[eqvt] - section {* Strong Induction Principles*} @@ -38,6 +28,7 @@ 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)" @@ -79,11 +70,12 @@ 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)" @@ -121,6 +113,7 @@ then have "P c (0 \ lam)" by blast then show "P c lam" by simp qed +*) section {* Typing *} @@ -131,6 +124,7 @@ notation TFun ("_ \ _") +(* declare ty.perm[eqvt] inductive @@ -237,7 +231,7 @@ apply(simp add: finite_supp) apply(rule_tac p="-p" in permute_boolE) apply(perm_strict_simp add: permute_minus_cancel) - (* supplied by the user *) + --"supplied by the user" apply(simp add: fresh_star_prod) apply(simp add: fresh_star_def) sorry @@ -246,86 +240,9 @@ then show "P c \ t T" by simp qed - - - - - - -inductive - tt :: "('a \ 'a \ bool) \ ('a \ 'a \ bool)" - for r :: "('a \ 'a \ bool)" -where - aa: "tt r a a" - | bb: "tt r a b ==> tt r a c" - -(* PROBLEM: derived eqvt-theorem does not conform with [eqvt] -equivariance tt *) -inductive - alpha_lam_raw' -where - a1: "name = namea \ alpha_lam_raw' (Var_raw name) (Var_raw namea)" -| a2: "\alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\ \ - alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)" -| a3: "\pi. ({atom name}, lam_raw) \gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \ - alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" - -equivariance alpha_lam_raw' - -thm eqvts_raw - -section {* size function *} - -lemma size_eqvt_raw: - fixes t::"lam_raw" - shows "size (pi \ t) = size t" - apply (induct rule: lam_raw.inducts) - apply simp_all - done - -instantiation lam :: size -begin - -quotient_definition - "size_lam :: lam \ nat" -is - "size :: lam_raw \ nat" - -lemma size_rsp: - "alpha_lam_raw x y \ size x = size y" - apply (induct rule: alpha_lam_raw.inducts) - apply (simp_all only: lam_raw.size) - apply (simp_all only: alphas) - apply clarify - apply (simp_all only: size_eqvt_raw) - done - -lemma [quot_respect]: - "(alpha_lam_raw ===> op =) size size" - by (simp_all add: size_rsp) - -lemma [quot_preserve]: - "(rep_lam ---> id) size = size" - by (simp_all add: size_lam_def) - -instance - by default - -end - -lemmas size_lam[simp] = - lam_raw.size(4)[quot_lifted] - lam_raw.size(5)[quot_lifted] - lam_raw.size(6)[quot_lifted] - -(* is this needed? *) -lemma [measure_function]: - "is_measure (size::lam\nat)" - by (rule is_measure_trivial) - section {* Matching *} definition @@ -512,6 +429,7 @@ | "match_App_raw (App_raw x y) = Some (x, y)" | "match_App_raw (Lam_raw n t) = None" +(* quotient_definition "match_App :: lam \ (lam \ lam) option" is match_App_raw @@ -547,7 +465,7 @@ apply (simp add: lam_half_inj) apply auto done - +*) (* lemma match_Lam_simps2: "atom n \ ((S :: 'a :: fs), Lam n s) \ match_Lam S (Lam n s) = Some (n, s)" @@ -627,7 +545,7 @@ lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted] *) - +(* lemma app_some: "match_App x = Some (a, b) \ x = App a b" by (induct x rule: lam.induct) (simp_all add: match_App_simps) @@ -767,7 +685,7 @@ apply (simp only: option.simps) apply (simp only: prod.simps) sorry - +*) end diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Let.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/Let.thy Thu Aug 26 02:08:00 2010 +0800 @@ -0,0 +1,224 @@ +theory Let +imports "../NewParser" +begin + +text {* example 3 or example 5 from Terms.thy *} + +atom_decl name + +nominal_datatype trm = + Var "name" +| App "trm" "trm" +| Lam x::"name" t::"trm" bind x in t +| Let a::"lts" t::"trm" bind "bn a" in t +and lts = + Lnil +| Lcons "name" "trm" "lts" +binder + bn +where + "bn Lnil = []" +| "bn (Lcons x t l) = (atom x) # (bn l)" + + +(* + +thm trm_lts.fv +thm trm_lts.eq_iff +thm trm_lts.bn +thm trm_lts.perm +thm trm_lts.induct[no_vars] +thm trm_lts.inducts[no_vars] +thm trm_lts.distinct +thm trm_lts.supp +thm trm_lts.fv[simplified trm_lts.supp(1-2)] + + +primrec + permute_bn_raw +where + "permute_bn_raw pi (Lnil_raw) = Lnil_raw" +| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \ a) t (permute_bn_raw pi l)" + +quotient_definition + "permute_bn :: perm \ lts \ lts" +is + "permute_bn_raw" + +lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" + apply simp + apply clarify + apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) + apply (rule TrueI)+ + apply simp_all + apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) + apply simp_all + done + +lemmas permute_bn = permute_bn_raw.simps[quot_lifted] + +lemma permute_bn_zero: + "permute_bn 0 a = a" + apply(induct a rule: trm_lts.inducts(2)) + apply(rule TrueI)+ + apply(simp_all add:permute_bn) + done + +lemma permute_bn_add: + "permute_bn (p + q) a = permute_bn p (permute_bn q a)" + oops + +lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" + apply(induct lts rule: trm_lts.inducts(2)) + apply(rule TrueI)+ + apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) + done + +lemma perm_bn: + "p \ bn l = bn(permute_bn p l)" + apply(induct l rule: trm_lts.inducts(2)) + apply(rule TrueI)+ + apply(simp_all add:permute_bn eqvts) + done + +lemma fv_perm_bn: + "fv_bn l = fv_bn (permute_bn p l)" + apply(induct l rule: trm_lts.inducts(2)) + apply(rule TrueI)+ + apply(simp_all add:permute_bn eqvts) + done + +lemma Lt_subst: + "supp (Abs_lst (bn lts) trm) \* q \ (Lt lts trm) = Lt (permute_bn q lts) (q \ trm)" + apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn) + apply (rule_tac x="q" in exI) + apply (simp add: alphas) + apply (simp add: perm_bn[symmetric]) + apply(rule conjI) + apply(drule supp_perm_eq) + apply(simp add: abs_eq_iff) + apply(simp add: alphas_abs alphas) + apply(drule conjunct1) + apply (simp add: trm_lts.supp) + apply(simp add: supp_abs) + apply (simp add: trm_lts.supp) + done + + +lemma fin_bn: + "finite (set (bn l))" + apply(induct l rule: trm_lts.inducts(2)) + apply(simp_all add:permute_bn eqvts) + done + +thm trm_lts.inducts[no_vars] + +lemma + fixes t::trm + and l::lts + and c::"'a::fs" + assumes a1: "\name c. P1 c (Vr name)" + and a2: "\trm1 trm2 c. \\d. P1 d trm1; \d. P1 d trm2\ \ P1 c (Ap trm1 trm2)" + and a3: "\name trm c. \atom name \ c; \d. P1 d trm\ \ P1 c (Lm name trm)" + and a4: "\lts trm c. \set (bn lts) \* c; \d. P2 d lts; \d. P1 d trm\ \ P1 c (Lt lts trm)" + and a5: "\c. P2 c Lnil" + and a6: "\name trm lts c. \\d. P1 d trm; \d. P2 d lts\ \ P2 c (Lcons name trm lts)" + shows "P1 c t" and "P2 c l" +proof - + have "(\(p::perm) (c::'a::fs). P1 c (p \ t))" and + b': "(\(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \ l)))" + apply(induct rule: trm_lts.inducts) + apply(simp) + apply(rule a1) + apply(simp) + apply(rule a2) + apply(simp) + apply(simp) + apply(simp) + apply(subgoal_tac "\q. (q \ (atom (p \ name))) \ c \ supp (Lm (p \ name) (p \ trm)) \* q") + apply(erule exE) + apply(rule_tac t="Lm (p \ name) (p \ trm)" + and s="q\ Lm (p \ name) (p \ trm)" in subst) + apply(rule supp_perm_eq) + apply(simp) + apply(simp) + apply(rule a3) + apply(simp add: atom_eqvt) + apply(subst permute_plus[symmetric]) + apply(blast) + apply(rule at_set_avoiding2_atom) + apply(simp add: finite_supp) + apply(simp add: finite_supp) + apply(simp add: fresh_def) + apply(simp add: trm_lts.fv[simplified trm_lts.supp]) + apply(simp) + apply(subgoal_tac "\q. (q \ set (bn (p \ lts))) \* c \ supp (Abs_lst (bn (p \ lts)) (p \ trm)) \* q") + apply(erule exE) + apply(erule conjE) + thm Lt_subst + apply(subst Lt_subst) + apply assumption + apply(rule a4) + apply(simp add:perm_bn[symmetric]) + apply(simp add: eqvts) + apply (simp add: fresh_star_def fresh_def) + apply(rotate_tac 1) + apply(drule_tac x="q + p" in meta_spec) + apply(simp) + apply(rule at_set_avoiding2) + apply(rule fin_bn) + apply(simp add: finite_supp) + apply(simp add: finite_supp) + apply(simp add: fresh_star_def fresh_def supp_abs) + apply(simp add: eqvts permute_bn) + apply(rule a5) + apply(simp add: permute_bn) + apply(rule a6) + apply simp + apply simp + done + then have a: "P1 c (0 \ t)" by blast + have "P2 c (permute_bn 0 (0 \ l))" using b' by blast + then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all +qed + + + +lemma lets_bla: + "x \ z \ y \ z \ x \ y \(Lt (Lcons x (Vr y) Lnil) (Vr x)) \ (Lt (Lcons x (Vr z) Lnil) (Vr x))" + by (simp add: trm_lts.eq_iff) + +lemma lets_ok: + "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" + apply (simp add: trm_lts.eq_iff) + apply (rule_tac x="(x \ y)" in exI) + apply (simp_all add: alphas eqvts supp_at_base fresh_star_def) + done + +lemma lets_ok3: + "x \ y \ + (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ + (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" + apply (simp add: alphas trm_lts.eq_iff) + done + + +lemma lets_not_ok1: + "x \ y \ + (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ + (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" + apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts) + done + +lemma lets_nok: + "x \ y \ x \ z \ z \ y \ + (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \ + (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" + apply (simp add: alphas trm_lts.eq_iff fresh_star_def) + done +*) + +end + + + diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/LetPat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/LetPat.thy Thu Aug 26 02:08:00 2010 +0800 @@ -0,0 +1,39 @@ +theory LetPat +imports "../NewParser" +begin + +declare [[STEPS = 100]] + +atom_decl name + +nominal_datatype trm = + Var "name" +| App "trm" "trm" +| Lam x::"name" t::"trm" bind (set) x in t +| Let p::"pat" "trm" t::"trm" bind (set) "f p" in t +and pat = + PN +| PS "name" +| PD "name" "name" +binder + f::"pat \ atom set" +where + "f PN = {}" +| "f (PD x y) = {atom x, atom y}" +| "f (PS x) = {atom x}" + +thm trm_pat.distinct +thm trm_pat.induct +thm trm_pat.exhaust +thm trm_pat.fv_defs +thm trm_pat.bn_defs +thm trm_pat.perm_simps +thm trm_pat.eq_iff +thm trm_pat.fv_bn_eqvt +thm trm_pat.size_eqvt + + +end + + + diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/LetRec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/LetRec.thy Thu Aug 26 02:08:00 2010 +0800 @@ -0,0 +1,36 @@ +theory LetRec +imports "../NewParser" +begin + +declare [[STEPS = 14]] + +atom_decl name + +nominal_datatype let_rec: + lam = + Var "name" +| App "lam" "lam" +| Lam x::"name" t::"lam" bind (set) x in t +| Let_Rec bp::"bp" t::"lam" bind (set) "bi bp" in bp t +and bp = + Bp "name" "lam" +binder + bi::"bp \ atom set" +where + "bi (Bp x t) = {atom x}" + +thm let_rec.distinct +thm let_rec.induct +thm let_rec.exhaust +thm let_rec.fv_defs +thm let_rec.bn_defs +thm let_rec.perm_simps +thm let_rec.eq_iff +thm let_rec.fv_bn_eqvt +thm let_rec.size_eqvt + + +end + + + diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/LetRec2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/LetRec2.thy Thu Aug 26 02:08:00 2010 +0800 @@ -0,0 +1,82 @@ +theory LetRec2 +imports "../NewParser" +begin + +atom_decl name + +nominal_datatype trm = + Vr "name" +| Ap "trm" "trm" +| Lm x::"name" t::"trm" bind (set) x in t +| Lt a::"lts" t::"trm" bind "bn a" in a t +and lts = + Lnil +| Lcons "name" "trm" "lts" +binder + bn +where + "bn Lnil = []" +| "bn (Lcons x t l) = (atom x) # (bn l)" + + +thm trm_lts.fv +thm trm_lts.eq_iff +thm trm_lts.bn +thm trm_lts.perm +thm trm_lts.induct +thm trm_lts.distinct +thm trm_lts.supp +thm trm_lts.fv[simplified trm_lts.supp] + + +(* why is this not in HOL simpset? *) +(* +lemma set_sub: "{a, b} - {b} = {a} - {b}" +by auto + +lemma lets_bla: + "x \ z \ y \ z \ x \ y \(Lt (Lcons x (Vr y) Lnil) (Vr x)) \ (Lt (Lcons x (Vr z) Lnil) (Vr x))" + apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base) + done + +lemma lets_ok: + "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" + apply (simp add: trm_lts.eq_iff) + apply (rule_tac x="(x \ y)" in exI) + apply (simp_all add: alphas fresh_star_def eqvts supp_at_base) + done + +lemma lets_ok3: + "x \ y \ + (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ + (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" + apply (simp add: alphas trm_lts.eq_iff) + done + + +lemma lets_not_ok1: + "x \ y \ + (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ + (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" + apply (simp add: alphas trm_lts.eq_iff) + done + +lemma lets_nok: + "x \ y \ x \ z \ z \ y \ + (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \ + (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" + apply (simp add: alphas trm_lts.eq_iff fresh_star_def) + done + +lemma lets_ok4: + "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = + (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))" + apply (simp add: alphas trm_lts.eq_iff supp_at_base) + apply (rule_tac x="(x \ y)" in exI) + apply (simp add: atom_eqvt fresh_star_def) + done + +end + + + diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Modules.thy --- a/Nominal/Ex/Modules.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/Modules.thy Thu Aug 26 02:08:00 2010 +0800 @@ -7,15 +7,16 @@ atom_decl name -nominal_datatype mexp = +nominal_datatype modules: + mexp = Acc "path" | Stru "body" -| Funct x::"name" "sexp" m::"mexp" bind_set x in m +| Funct x::"name" "sexp" m::"mexp" bind (set) x in m | FApp "mexp" "path" | Ascr "mexp" "sexp" and body = Empty -| Seq c::defn d::"body" bind_set "cbinders c" in d +| Seq c::"defn" d::"body" bind (set) "cbinders c" in d and defn = Type "name" "ty" | Dty "name" @@ -26,7 +27,7 @@ | SFunc "name" "sexp" "sexp" and sbody = SEmpty -| SSeq C::spec D::sbody bind_set "Cbinders C" in D +| SSeq C::"spec" D::"sbody" bind (set) "Cbinders C" in D and spec = Type1 "name" | Type2 "name" "ty" @@ -42,7 +43,7 @@ and trm = Tref1 "name" | Tref2 "path" "name" -| Lam' v::"name" "ty" M::"trm" bind_set v in M +| Lam' v::"name" "ty" M::"trm" bind (set) v in M | App' "trm" "trm" | Let' "body" "trm" binder @@ -58,15 +59,16 @@ | "Cbinders (SStru x S) = {atom x}" | "Cbinders (SVal v T) = {atom v}" -thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv -thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff -thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn -thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm -thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct -thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts -thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct -thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10) -thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)] + +thm modules.distinct +thm modules.induct +thm modules.exhaust +thm modules.fv_defs +thm modules.bn_defs +thm modules.perm_simps +thm modules.eq_iff +thm modules.fv_bn_eqvt +thm modules.size_eqvt diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/NoneExamples.thy --- a/Nominal/Ex/NoneExamples.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/NoneExamples.thy Thu Aug 26 02:08:00 2010 +0800 @@ -4,6 +4,40 @@ atom_decl name + +text {* + "Weirdo" example from Peter Sewell's bestiary. + + This example is not covered by our binding + specification. + +*} + +nominal_datatype weird = + Foo_var "name" +| Foo_pair "weird" "weird" +| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" + bind x in p1 p2, + bind y in p2 p3 + +(* e1 occurs in two bodies *) + +nominal_datatype exp = + Var name +| Pair exp exp +| LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "bp p" in e1 +and pat = + PVar name +| PUnit +| PPair pat pat +binder + bp :: "pat \ atom list" +where + "bp (PVar x) = [atom x]" +| "bp (PUnit) = []" +| "bp (PPair p1 p2) = bp p1 @ bp p2" + + (* this example binds bound names and so is not respectful *) (* diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Thu Aug 26 02:08:00 2010 +0800 @@ -4,9 +4,9 @@ atom_decl name -declare [[STEPS = 21]] +declare [[STEPS = 100]] -nominal_datatype singlelet: trm = +nominal_datatype single_let: trm = Var "name" | App "trm" "trm" | Lam x::"name" t::"trm" bind x in t @@ -21,19 +21,18 @@ where "bn (As x y t) = {atom x}" - -thm distinct -thm induct -thm exhaust -thm fv_defs -thm bn_defs -thm perm_simps -thm eq_iff -thm fv_bn_eqvt -thm size_eqvt +thm single_let.distinct +thm single_let.induct +thm single_let.exhaust +thm single_let.fv_defs +thm single_let.bn_defs +thm single_let.perm_simps +thm single_let.eq_iff +thm single_let.fv_bn_eqvt +thm single_let.size_eqvt - +(* lemma supp_fv: @@ -67,10 +66,9 @@ thm trm_assg.inducts thm trm_assg.distinct ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} +*) -(* TEMPORARY -thm trm_assg.fv[simplified trm_assg.supp(1-2)] -*) + end diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Term8.thy --- a/Nominal/Ex/Term8.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/Term8.thy Thu Aug 26 02:08:00 2010 +0800 @@ -6,21 +6,21 @@ atom_decl name -ML {* val _ = cheat_alpha_bn_rsp := true *} - nominal_datatype foo = Foo0 "name" -| Foo1 b::"bar" f::"foo" bind_set "bv b" in f +| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f and bar = Bar0 "name" -| Bar1 "name" s::"name" b::"bar" bind_set s in b +| Bar1 "name" s::"name" b::"bar" bind (set) s in b binder bv where "bv (Bar0 x) = {}" | "bv (Bar1 v x b) = {atom v}" +(* thm foo_bar.supp +*) end diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Test.thy --- a/Nominal/Ex/Test.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,40 +0,0 @@ -theory Test -imports "../NewParser" -begin - -declare [[STEPS = 4]] - -atom_decl name - -(* -nominal_datatype trm = - Vr "name" -| Ap "trm" "trm" - -thm fv_trm_raw.simps[no_vars] -*) - -(* This file contains only the examples that are not supposed to work yet. *) - - -declare [[STEPS = 2]] - - -(* example 4 from Terms.thy *) -(* fv_eqvt does not work, we need to repaire defined permute functions - defined fv and defined alpha... *) -(* lists-datastructure does not work yet *) - -nominal_datatype trm = - Vr "name" -| Ap "trm" "trm list" -| Lm x::"name" t::"trm" bind x in t - -(* -thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] -thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] -*) - -end - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/TestMorePerm.thy --- a/Nominal/Ex/TestMorePerm.thy Wed Aug 25 23:16:42 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -theory TestMorePerm -imports "../NewParser" -begin - -text {* - "Weirdo" example from Peter Sewell's bestiary. - - This example is not covered by our binding - specification. - -*} -ML {* val _ = cheat_equivp := true *} - -atom_decl name - -nominal_datatype weird = - Foo_var "name" -| Foo_pair "weird" "weird" -| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" - bind x in p1 p2, - bind y in p2 p3 - -thm alpha_weird_raw.intros[no_vars] - -thm permute_weird_raw.simps[no_vars] -thm alpha_weird_raw.intros[no_vars] -thm fv_weird_raw.simps[no_vars] - -equivariance alpha_weird_raw - - -end - - - diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/Ex/TypeSchemes.thy Thu Aug 26 02:08:00 2010 +0800 @@ -6,7 +6,7 @@ atom_decl name -declare [[STEPS = 21]] +declare [[STEPS = 100]] nominal_datatype ty = Var "name" @@ -19,74 +19,11 @@ Var2 "name" | Fun2 "ty2" "ty2" - nominal_datatype tys2 = All2 xs::"name fset" ty::"ty2" bind (res) xs in ty -lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] - - - -(* below we define manually the function for size *) - -lemma size_eqvt_raw: - "size (pi \ t :: ty_raw) = size t" - "size (pi \ ts :: tys_raw) = size ts" - apply (induct rule: ty_raw_tys_raw.inducts) - apply simp_all - done - -instantiation ty and tys :: size -begin - -quotient_definition - "size_ty :: ty \ nat" -is - "size :: ty_raw \ nat" - -quotient_definition - "size_tys :: tys \ nat" -is - "size :: tys_raw \ nat" - -lemma size_rsp: - "alpha_ty_raw x y \ size x = size y" - "alpha_tys_raw a b \ size a = size b" - apply (induct rule: alpha_ty_raw_alpha_tys_raw.inducts) - apply (simp_all only: ty_raw_tys_raw.size) - apply (simp_all only: alphas) - apply clarify - apply (simp_all only: size_eqvt_raw) - done - -lemma [quot_respect]: - "(alpha_ty_raw ===> op =) size size" - "(alpha_tys_raw ===> op =) size size" - by (simp_all add: size_rsp) - -lemma [quot_preserve]: - "(rep_ty ---> id) size = size" - "(rep_tys ---> id) size = size" - by (simp_all add: size_ty_def size_tys_def) - -instance - by default - -end - -thm ty_raw_tys_raw.size(4)[quot_lifted] -thm ty_raw_tys_raw.size(5)[quot_lifted] -thm ty_raw_tys_raw.size(6)[quot_lifted] - - -thm ty_tys.fv -thm ty_tys.eq_iff -thm ty_tys.bn -thm ty_tys.perm -thm ty_tys.inducts -thm ty_tys.distinct - +(* ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *} lemma strong_induct: @@ -278,19 +215,6 @@ done end - -(* PROBLEM: -Type schemes with separate datatypes - -nominal_datatype T = - TVar "name" -| TFun "T" "T" -nominal_datatype TyS = - TAll xs::"name list" ty::"T" bind xs in ty - -*** exception Datatype raised -*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML") -*** At command "nominal_datatype". *) diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/TypeVarsTest.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/TypeVarsTest.thy Thu Aug 26 02:08:00 2010 +0800 @@ -0,0 +1,30 @@ +theory TypeVarsTest +imports "../NewParser" +begin + +atom_decl name +declare [[STEPS = 21]] + +class s1 +class s2 + +nominal_datatype ('a, 'b) lam = + Var "name" +| App "('a::s1, 'b::s2) lam" "('a, 'b) lam" +| Lam x::"name" l::"('a, 'b) lam" bind x in l + +thm lam.distinct +thm lam.induct +thm lam.exhaust +thm lam.fv_defs +thm lam.bn_defs +thm lam.perm_simps +thm lam.eq_iff +thm lam.fv_bn_eqvt +thm lam.size_eqvt + + +end + + + diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Wed Aug 25 23:16:42 2010 +0800 +++ b/Nominal/NewParser.thy Thu Aug 26 02:08:00 2010 +0800 @@ -251,7 +251,7 @@ (* for testing porposes - to exit the procedure early *) exception TEST of Proof.context -val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 0); +val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 100); fun get_STEPS ctxt = Config.get ctxt STEPS *} @@ -259,7 +259,7 @@ setup STEPS_setup ML {* -fun nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses lthy = +fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = let (* definition of the raw datatypes *) val _ = warning "Definition of raw datatypes"; @@ -437,7 +437,6 @@ val qty_full_names = map (fst o dest_Type) qtys val qty_names = map Long_Name.base_name qty_full_names - (* defining of quotient term-constructors, binding functions, free vars functions *) val _ = warning "Defining the quotient constants" val qconstrs_descr = @@ -517,24 +516,24 @@ ||>> lift_thms qtys [] raw_exhaust_thms else raise TEST lthyA - - (* temporary theorem bindings *) + (* noting the theorems *) + + (* generating the prefix for the theorem names *) + val thms_name = + the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name + fun thms_suffix s = Binding.qualified true s thms_name + val (_, lthy9') = lthyB - |> Local_Theory.note ((@{binding "distinct"}, []), qdistincts) - ||>> Local_Theory.note ((@{binding "eq_iff"}, []), qeq_iffs) - ||>> Local_Theory.note ((@{binding "fv_defs"}, []), qfv_defs) - ||>> Local_Theory.note ((@{binding "bn_defs"}, []), qbn_defs) - ||>> Local_Theory.note ((@{binding "perm_simps"}, []), qperm_simps) - ||>> Local_Theory.note ((@{binding "fv_bn_eqvt"}, []), qfv_qbn_eqvts) - ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), qsize_eqvt) - ||>> Local_Theory.note ((@{binding "induct"}, []), [qinduct]) - ||>> Local_Theory.note ((@{binding "exhaust"}, []), qexhausts) + |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) + ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) + ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) + ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) + ||>> Local_Theory.note ((thms_suffix "perm_simps", []), qperm_simps) + ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) + ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) + ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) + ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) - - val _ = - if get_STEPS lthy > 21 - then true else raise TEST lthy9' - in (0, lthy9') end handle TEST ctxt => (0, ctxt) @@ -692,11 +691,10 @@ *} ML {* -fun nominal_datatype2_cmd (opt_thm_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = +fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = let - val (pre_typ_names, pre_typs) = split_list - (map (fn (tvs, tname, mx, _) => - (Binding.name_of tname, (tname, length tvs, mx))) dt_strs) + val pre_typs = + map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs (* this theory is used just for parsing *) val thy = ProofContext.theory_of lthy @@ -710,10 +708,8 @@ ||>> prepare_bclauses dt_strs val bclauses' = complete dt_strs bclauses - val thm_name = - the_default (Binding.name (space_implode "_" pre_typ_names)) opt_thm_name in - timeit (fn () => nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses' lthy |> snd) + timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy |> snd) end *}