--- /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 \<equiv> 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 \<times> kind) list" "(var \<times> ty) list"
+binder
+ bv :: "pat \<Rightarrow> atom set"
+where
+ "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
+*)
+
+end
+
+
+
--- /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
+
+
+
+
--- 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} \<union> (bn l)"
+ "bn Lnil = {}"
+| "bn (Lcons x t l) = {atom x} \<union> (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 \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (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 \<leftrightarrow> y)" in exI)
+ apply (simp_all add: alphas)
+ apply (simp add: fresh_star_def eqvts)
+ done
+
+lemma lets_ok3:
+ "x \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (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 \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (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
--- /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} \<union> (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 \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (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 \<leftrightarrow> y)" in exI)
+ apply (simp_all add: alpha_gen2 fresh_star_def eqvts)
+ done
+
+lemma lets_ok3:
+ "x \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (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 \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (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 \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (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
+
+
+
--- 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
--- 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
--- 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 "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> TySch.All fset t) \<sharp>* pa)")
+ apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset t) \<sharp>* pa)")
apply clarify
- apply(rule_tac t="p \<bullet> TySch.All fset t" and
- s="pa \<bullet> (p \<bullet> TySch.All fset t)" in subst)
+ apply(rule_tac t="p \<bullet> All fset t" and
+ s="pa \<bullet> (p \<bullet> All fset t)" in subst)
apply (rule supp_perm_eq)
apply assumption
apply (simp only: t_tyS.perm)
--- 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
-
-
-
-
--- 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 \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (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 \<leftrightarrow> 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 \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (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 \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (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 \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (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
--- 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 \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (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 \<leftrightarrow> y)" in exI)
-apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def eqvts)
-done
-
-lemma lets_ok3:
- "x \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (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 "\<not>(rVr5 x \<approx>5 rAp5 y z)"
- apply auto
- apply (erule alpha_rtrm5.cases)
- apply (simp_all only: rtrm5.distinct)
- done
-
-lemma distinct_helper2:
- shows "(Vr5 x) \<noteq> (Ap5 y z)"
- by (lifting distinct_helper)
-
-lemma lets_nok:
- "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (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
--- 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", *)
+ ];