equal
deleted
inserted
replaced
40 fixes pi:: "name prm" |
40 fixes pi:: "name prm" |
41 assumes a: "valid \<Gamma>" |
41 assumes a: "valid \<Gamma>" |
42 shows "valid (pi\<bullet>\<Gamma>)" |
42 shows "valid (pi\<bullet>\<Gamma>)" |
43 using a |
43 using a |
44 apply(induct) |
44 apply(induct) |
45 apply(auto simp add: fresh_eqvt) |
45 apply(auto simp add: fresh_bij) |
46 done |
46 done |
47 |
47 |
48 (* typing judgements *) |
48 (* typing judgements *) |
49 consts |
49 consts |
50 typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" |
50 typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" |
74 have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst]) |
74 have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst]) |
75 ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>" |
75 ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>" |
76 using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) |
76 using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) |
77 next |
77 next |
78 case (t3 \<Gamma> \<sigma> \<tau> a t) |
78 case (t3 \<Gamma> \<sigma> \<tau> a t) |
79 moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt) |
79 moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij) |
80 ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force |
80 ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force |
81 qed (auto) |
81 qed (auto) |
82 |
82 |
83 lemma typing_induct[consumes 1, case_names t1 t2 t3]: |
83 lemma typing_induct[consumes 1, case_names t1 t2 t3]: |
84 fixes P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool" |
84 fixes P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool" |