# HG changeset patch # User Christian Urban # Date 1269336406 -3600 # Node ID 304bd7400a47827c2f8d3627866d1753966a4c73 # Parent ac69ed8303cce4aab7b7069b15709ee772619856# Parent 75403378068b1407ec075e2f72ded20a877422bd merged diff -r ac69ed8303cc -r 304bd7400a47 Nominal/ExCoreHaskell.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/ExCoreHaskell.thy Tue Mar 23 10:26:46 2010 +0100 @@ -0,0 +1,73 @@ +theory ExCoreHaskell +imports "Parser" +begin + +(* core haskell *) + +ML {* val _ = recursive := false *} + +atom_decl var +atom_decl tvar + +(* there are types, coercion types and regular types list-data-structure *) +nominal_datatype tkind = + KStar +| KFun "tkind" "tkind" +and ckind = + CKEq "ty" "ty" +and ty = + TVar "tvar" +| TC "string" +| TApp "ty" "ty" +| TFun "string" "ty_lst" +| TAll tv::"tvar" "tkind" T::"ty" bind tv in T +| TEq "ty" "ty" "ty" +and ty_lst = + TsNil +| TsCons "ty" "ty_lst" +and co = + CC "string" +| CApp "co" "co" +| CFun "string" "co_lst" +| CAll tv::"tvar" "ckind" C::"co" bind tv in C +| CEq "co" "co" "co" +| CSym "co" +| CCir "co" "co" +| CLeft "co" +| CRight "co" +| CSim "co" +| CRightc "co" +| CLeftc "co" +| CCoe "co" "co" +and co_lst = + CsNil +| CsCons "co" "co_lst" + +(* +abbreviation + "atoms A \ atom ` A" + +nominal_datatype trm = + Var "var" +| C "string" +| LAM tv::"tvar" "kind" t::"trm" bind tv in t +| APP "trm" "ty" +| Lam v::"var" "ty" t::"trm" bind v in t +| App "trm" "trm" +| Let x::"var" "ty" "trm" t::"trm" bind x in t +| Case "trm" "assoc list" +| Cast "trm" "ty" --"ty is supposed to be a coercion type only" +and assoc = + A p::"pat" t::"trm" bind "bv p" in t +and pat = + K "string" "(tvar \ kind) list" "(var \ ty) list" +binder + bv :: "pat \ atom set" +where + "bv (K s ts vs) = (atoms (set (map fst ts))) \ (atoms (set (map fst vs)))" +*) + +end + + + diff -r ac69ed8303cc -r 304bd7400a47 Nominal/ExLF.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/ExLF.thy Tue Mar 23 10:26:46 2010 +0100 @@ -0,0 +1,27 @@ +theory ExLF +imports "Parser" +begin + +atom_decl name +atom_decl ident + +nominal_datatype kind = + Type + | KPi "ty" n::"name" k::"kind" bind n in k +and ty = + TConst "ident" + | TApp "ty" "trm" + | TPi "ty" n::"name" t::"ty" bind n in t +and trm = + Const "ident" + | Var "name" + | App "trm" "trm" + | Lam "ty" n::"name" t::"trm" bind n in t + +thm kind_ty_trm.supp + +end + + + + diff -r ac69ed8303cc -r 304bd7400a47 Nominal/ExLet.thy --- a/Nominal/ExLet.thy Tue Mar 23 10:24:12 2010 +0100 +++ b/Nominal/ExLet.thy Tue Mar 23 10:26:46 2010 +0100 @@ -11,15 +11,15 @@ Vr "name" | Ap "trm" "trm" | Lm x::"name" t::"trm" bind x in t -| Lt a::"lts" t::"trm" bind "bv a" in t +| Lt a::"lts" t::"trm" bind "bn a" in t and lts = - Nil -| Cons "name" "trm" "lts" + Lnil +| Lcons "name" "trm" "lts" binder bn where - "bn Nil = {}" -| "bn (Cons x t l) = {atom x} \ (bn l)" + "bn Lnil = {}" +| "bn (Lcons x t l) = {atom x} \ (bn l)" thm trm_lts.fv thm trm_lts.eq_iff @@ -29,6 +29,43 @@ thm trm_lts.distinct thm trm_lts.fv[simplified trm_lts.supp] +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) + apply (simp add: fresh_star_def eqvts) + 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: + "(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) + apply (rule_tac x="0::perm" in exI) + apply (simp add: fresh_star_def eqvts) + apply blast + 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 ac69ed8303cc -r 304bd7400a47 Nominal/ExLetRec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/ExLetRec.thy Tue Mar 23 10:26:46 2010 +0100 @@ -0,0 +1,74 @@ +theory ExLetRec +imports "Parser" +begin + +text {* example 3 or example 5 from Terms.thy *} + +atom_decl name + +ML {* val _ = recursive := true *} +nominal_datatype trm = + Vr "name" +| Ap "trm" "trm" +| Lm x::"name" t::"trm" bind x in t +| Lt 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 +thm trm_lts.distinct +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 (simp add: trm_lts.eq_iff alpha_gen2 set_sub) + 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: alpha_gen2 fresh_star_def eqvts) + 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 + + +end + + + diff -r ac69ed8303cc -r 304bd7400a47 Nominal/ExPS3.thy --- a/Nominal/ExPS3.thy Tue Mar 23 10:24:12 2010 +0100 +++ b/Nominal/ExPS3.thy Tue Mar 23 10:26:46 2010 +0100 @@ -29,7 +29,8 @@ thm exp_pat3.perm thm exp_pat3.induct thm exp_pat3.distinct -thm exp_pat3.fv[simplified exp_pat3.supp] +thm exp_pat3.fv +thm exp_pat3.supp (* The bindings are too complicated *) end diff -r ac69ed8303cc -r 304bd7400a47 Nominal/ExPS6.thy --- a/Nominal/ExPS6.thy Tue Mar 23 10:24:12 2010 +0100 +++ b/Nominal/ExPS6.thy Tue Mar 23 10:26:46 2010 +0100 @@ -6,6 +6,9 @@ atom_decl name +(* The binding structure is too complicated, so we cannot show equivalence *) +ML {* val _ = cheat_equivp := true *} + ML {* val _ = recursive := false *} nominal_datatype exp6 = EVar name @@ -28,6 +31,7 @@ thm exp6_pat6.perm thm exp6_pat6.induct thm exp6_pat6.distinct +thm exp6_pat6.supp end diff -r ac69ed8303cc -r 304bd7400a47 Nominal/ExTySch.thy --- a/Nominal/ExTySch.thy Tue Mar 23 10:24:12 2010 +0100 +++ b/Nominal/ExTySch.thy Tue Mar 23 10:26:46 2010 +0100 @@ -86,10 +86,10 @@ apply simp apply (rule allI) apply (rule allI) - apply(subgoal_tac "\pa. ((pa \ (fset_to_set (fmap atom (p \ fset)))) \* d \ supp (p \ TySch.All fset t) \* pa)") + apply(subgoal_tac "\pa. ((pa \ (fset_to_set (fmap atom (p \ fset)))) \* d \ supp (p \ All fset t) \* pa)") apply clarify - apply(rule_tac t="p \ TySch.All fset t" and - s="pa \ (p \ TySch.All fset t)" in subst) + apply(rule_tac t="p \ All fset t" and + s="pa \ (p \ All fset t)" in subst) apply (rule supp_perm_eq) apply assumption apply (simp only: t_tyS.perm) diff -r ac69ed8303cc -r 304bd7400a47 Nominal/LFex.thy --- a/Nominal/LFex.thy Tue Mar 23 10:24:12 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -theory LFex -imports "Parser" -begin - -atom_decl name -atom_decl ident - -nominal_datatype kind = - Type - | KPi "ty" n::"name" k::"kind" bind n in k -and ty = - TConst "ident" - | TApp "ty" "trm" - | TPi "ty" n::"name" t::"ty" bind n in t -and trm = - Const "ident" - | Var "name" - | App "trm" "trm" - | Lam "ty" n::"name" t::"trm" bind n in t - -thm kind_ty_trm.supp - -end - - - - diff -r ac69ed8303cc -r 304bd7400a47 Nominal/Manual/Term5.thy --- a/Nominal/Manual/Term5.thy Tue Mar 23 10:24:12 2010 +0100 +++ b/Nominal/Manual/Term5.thy Tue Mar 23 10:26:46 2010 +0100 @@ -289,56 +289,4 @@ lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] lemmas alpha5_DIS = alpha_dis[quot_lifted] -(* why is this not in Isabelle? *) -lemma set_sub: "{a, b} - {b} = {a} - {b}" -by auto - -lemma lets_bla: - "x \ z \ y \ z \ x \ y \(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \ (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" -apply (simp only: alpha5_INJ bv5) -apply simp -apply (rule allI) -apply (simp_all add: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) -apply (rule impI) -apply (rule impI) -apply (rule impI) -apply (simp add: set_sub) -done - -lemma lets_ok: - "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" -thm alpha5_INJ -apply (simp only: alpha5_INJ) -apply (rule_tac x="(x \ y)" in exI) -apply (simp_all add: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -apply (simp add: eqvts) -done - -lemma lets_ok3: - "x \ y \ - (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) -done - - -lemma lets_not_ok1: - "x \ y \ - (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp add: alpha5_INJ alpha_gen) -apply (simp add: permute_trm5_lts eqvts) -apply (simp add: alpha5_INJ) -done - -lemma lets_nok: - "x \ y \ x \ z \ z \ y \ - (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) -apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts) -done - end diff -r ac69ed8303cc -r 304bd7400a47 Nominal/Manual/Term5n.thy --- a/Nominal/Manual/Term5n.thy Tue Mar 23 10:24:12 2010 +0100 +++ b/Nominal/Manual/Term5n.thy Tue Mar 23 10:26:46 2010 +0100 @@ -174,55 +174,4 @@ lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] -lemma lets_bla: - "x \ z \ y \ z \ x \ y \(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \ (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" -apply (simp only: alpha5_INJ) -apply (simp only: bv5) -apply simp -done - -lemma lets_ok: - "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" -apply (simp add: alpha5_INJ) -apply (rule_tac x="(x \ y)" in exI) -apply (simp_all add: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def eqvts) -done - -lemma lets_ok3: - "x \ y \ - (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) -done - - -lemma lets_not_ok1: - "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = - (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp add: alpha5_INJ alpha_gen) -apply (rule_tac x="0::perm" in exI) -apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) -apply blast -done - -lemma distinct_helper: - shows "\(rVr5 x \5 rAp5 y z)" - apply auto - apply (erule alpha_rtrm5.cases) - apply (simp_all only: rtrm5.distinct) - done - -lemma distinct_helper2: - shows "(Vr5 x) \ (Ap5 y z)" - by (lifting distinct_helper) - -lemma lets_nok: - "x \ y \ x \ z \ z \ y \ - (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) -apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts) -done - end diff -r ac69ed8303cc -r 304bd7400a47 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Tue Mar 23 10:24:12 2010 +0100 +++ b/Nominal/ROOT.ML Tue Mar 23 10:26:46 2010 +0100 @@ -5,24 +5,17 @@ "Nominal2_Eqvt", "Nominal2_Atoms", "Nominal2_Supp", - "Test"] - -(* -no_document use_thys - ["Nominal2_Base", - "Nominal2_Eqvt", - "Nominal2_Atoms", - "Nominal2_Supp", - "Test", - "Term1", - "Term2", - "Term3", - "Term4", - "Term5", - "Term6", - "Term7", - "Term8", - "Term9", - "TySch", - "LFex"]; -*) \ No newline at end of file + "ExLam", + "ExLF", + "Ex1", + "Ex1rec", + "Ex2", + "Ex3", + "ExLet", + "ExLetRec", + "ExTySch", + "ExLeroy" +(* "ExCoreHaskell", *) +(* "ExPS3", *) +(* "ExPS6", *) + ];