--- a/Nominal/Ex/ExTySch.thy Thu Apr 08 11:52:05 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,165 +0,0 @@
-theory ExTySch
-imports "../Parser"
-begin
-
-(* Type Schemes *)
-atom_decl name
-
-ML {* val _ = alpha_type := AlphaRes *}
-nominal_datatype t =
- Var "name"
-| Fun "t" "t"
-and tyS =
- All xs::"name fset" ty::"t" bind xs in ty
-
-lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
-
-lemma size_eqvt_raw:
- "size (pi \<bullet> t :: t_raw) = size t"
- "size (pi \<bullet> ts :: tyS_raw) = size ts"
- apply (induct rule: t_raw_tyS_raw.inducts)
- apply simp_all
- done
-
-instantiation t and tyS :: size begin
-
-quotient_definition
- "size_t :: t \<Rightarrow> nat"
-is
- "size :: t_raw \<Rightarrow> nat"
-
-quotient_definition
- "size_tyS :: tyS \<Rightarrow> nat"
-is
- "size :: tyS_raw \<Rightarrow> nat"
-
-lemma size_rsp:
- "alpha_t_raw x y \<Longrightarrow> size x = size y"
- "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
- apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
- apply (simp_all only: t_raw_tyS_raw.size)
- apply (simp_all only: alphas)
- apply clarify
- apply (simp_all only: size_eqvt_raw)
- done
-
-lemma [quot_respect]:
- "(alpha_t_raw ===> op =) size size"
- "(alpha_tyS_raw ===> op =) size size"
- by (simp_all add: size_rsp)
-
-lemma [quot_preserve]:
- "(rep_t ---> id) size = size"
- "(rep_tyS ---> id) size = size"
- by (simp_all add: size_t_def size_tyS_def)
-
-instance
- by default
-
-end
-
-thm t_raw_tyS_raw.size(4)[quot_lifted]
-thm t_raw_tyS_raw.size(5)[quot_lifted]
-thm t_raw_tyS_raw.size(6)[quot_lifted]
-
-
-thm t_tyS.fv
-thm t_tyS.eq_iff
-thm t_tyS.bn
-thm t_tyS.perm
-thm t_tyS.inducts
-thm t_tyS.distinct
-ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
-
-lemma induct:
- assumes a1: "\<And>name b. P b (Var name)"
- and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
- and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
- shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
-proof -
- have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
- apply (rule t_tyS.induct)
- apply (simp add: a1)
- apply (simp)
- apply (rule allI)+
- apply (rule a2)
- apply simp
- 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> All fset t) \<sharp>* pa)")
- apply clarify
- 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)
- apply (rule a3)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2)
- apply (simp add: fin_fset_to_set)
- apply (simp add: finite_supp)
- apply (simp add: eqvts finite_supp)
- apply (subst atom_eqvt_raw[symmetric])
- apply (subst fmap_eqvt[symmetric])
- apply (subst fset_to_set_eqvt[symmetric])
- apply (simp only: fresh_star_permute_iff)
- apply (simp add: fresh_star_def)
- apply clarify
- apply (simp add: fresh_def)
- apply (simp add: t_tyS_supp)
- done
- then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
- then show ?thesis by simp
-qed
-
-lemma
- shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
- apply(simp add: t_tyS.eq_iff)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: alphas)
- apply(simp add: fresh_star_def fresh_zero_perm)
- done
-
-lemma
- shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
- apply(simp add: t_tyS.eq_iff)
- apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
- apply(simp add: alphas fresh_star_def eqvts)
- done
-
-lemma
- shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
- apply(simp add: t_tyS.eq_iff)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
-done
-
-lemma
- assumes a: "a \<noteq> b"
- shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
- using a
- apply(simp add: t_tyS.eq_iff)
- apply(clarify)
- apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
- apply auto
- done
-
-(* 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".
-*)
-
-
-end
--- a/Nominal/Ex/Test.thy Thu Apr 08 11:52:05 2010 +0200
+++ b/Nominal/Ex/Test.thy Thu Apr 08 13:04:49 2010 +0200
@@ -1,4 +1,3 @@
-(*<*)
theory Test
imports "../Parser"
begin
@@ -38,10 +37,6 @@
| "bv8 (Bar1 v x b) = {atom v}"
*)
-(* example 9 from Peter Sewell's bestiary *)
-(* run out of steam at the moment *)
-
end
-(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/TypeSchemes.thy Thu Apr 08 13:04:49 2010 +0200
@@ -0,0 +1,171 @@
+theory TypeSchemes
+imports "../Parser"
+begin
+
+section {*** Type Schemes ***}
+
+atom_decl name
+
+ML {* val _ = alpha_type := AlphaRes *}
+
+nominal_datatype ty =
+ Var "name"
+| Fun "ty" "ty"
+and tys =
+ All xs::"name fset" ty::"ty" bind 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 \<bullet> t :: ty_raw) = size t"
+ "size (pi \<bullet> 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 \<Rightarrow> nat"
+is
+ "size :: ty_raw \<Rightarrow> nat"
+
+quotient_definition
+ "size_tys :: tys \<Rightarrow> nat"
+is
+ "size :: tys_raw \<Rightarrow> nat"
+
+lemma size_rsp:
+ "alpha_ty_raw x y \<Longrightarrow> size x = size y"
+ "alpha_tys_raw a b \<Longrightarrow> 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:
+ assumes a1: "\<And>name b. P b (Var name)"
+ and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
+ and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
+ shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
+proof -
+ have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
+ apply (rule ty_tys.induct)
+ apply (simp add: a1)
+ apply (simp)
+ apply (rule allI)+
+ apply (rule a2)
+ apply simp
+ 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> All fset ty) \<sharp>* pa)")
+ apply clarify
+ apply(rule_tac t="p \<bullet> All fset ty" and
+ s="pa \<bullet> (p \<bullet> All fset ty)" in subst)
+ apply (rule supp_perm_eq)
+ apply assumption
+ apply (simp only: ty_tys.perm)
+ apply (rule a3)
+ apply(erule_tac x="(pa + p)" in allE)
+ apply simp
+ apply (simp add: eqvts eqvts_raw)
+ apply (rule at_set_avoiding2)
+ apply (simp add: fin_fset_to_set)
+ apply (simp add: finite_supp)
+ apply (simp add: eqvts finite_supp)
+ apply (subst atom_eqvt_raw[symmetric])
+ apply (subst fmap_eqvt[symmetric])
+ apply (subst fset_to_set_eqvt[symmetric])
+ apply (simp only: fresh_star_permute_iff)
+ apply (simp add: fresh_star_def)
+ apply clarify
+ apply (simp add: fresh_def)
+ apply (simp add: ty_tys_supp)
+ done
+ then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
+ then show ?thesis by simp
+qed
+
+lemma
+ shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
+ apply(simp add: ty_tys.eq_iff)
+ apply(rule_tac x="0::perm" in exI)
+ apply(simp add: alphas)
+ apply(simp add: fresh_star_def fresh_zero_perm)
+ done
+
+lemma
+ shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
+ apply(simp add: ty_tys.eq_iff)
+ apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+ apply(simp add: alphas fresh_star_def eqvts)
+ done
+
+lemma
+ shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
+ apply(simp add: ty_tys.eq_iff)
+ apply(rule_tac x="0::perm" in exI)
+ apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+done
+
+lemma
+ assumes a: "a \<noteq> b"
+ shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
+ using a
+ apply(simp add: ty_tys.eq_iff)
+ apply(clarify)
+ apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+ apply auto
+ done
+
+(* 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".
+*)
+
+
+end
--- a/Nominal/ROOT.ML Thu Apr 08 11:52:05 2010 +0200
+++ b/Nominal/ROOT.ML Thu Apr 08 13:04:49 2010 +0200
@@ -9,7 +9,7 @@
"Ex/Ex3",
"Ex/ExLet",
"Ex/ExLetRec",
- "Ex/ExTySch",
+ "Ex/TypeSchemes",
"Ex/ExLeroy",
"Ex/ExPS3",
"Ex/ExPS7",