# HG changeset patch # User urbanc # Date 1133372232 -3600 # Node ID a780f9c1538b6e7a74c7ecf77de63ac80282af2e # Parent 684832c9fa620fef6aad4618f8ddea4974ff51ca changed everything until the interesting transitivity_narrowing proof. diff -r 684832c9fa62 -r a780f9c1538b src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Wed Nov 30 18:13:31 2005 +0100 +++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Nov 30 18:37:12 2005 +0100 @@ -90,7 +90,6 @@ "subst_ctxt [] Y T = []" "subst_ctxt (XT#Xs) Y T = (fst XT, subst_ty (snd XT) Y T)#(subst_ctxt Xs Y T)" - text {* valid contexts *} constdefs @@ -200,7 +199,6 @@ apply(simp add: domain_append) done - lemma fresh_implies_not_member[rule_format]: fixes \::"ty_context" shows "X\\ \ \(\T.(X,T)\(set \))" @@ -214,7 +212,6 @@ apply (induct \) apply (auto dest!: validE fresh_implies_not_member) done - section {* Subtyping *} @@ -312,55 +309,41 @@ shows "\ \ S <: T \ (pi\\) \ (pi\S) <: (pi\T)" apply(erule subtype_of_rel.induct) apply(force intro: valid_eqvt closed_in_eqvt) -(* -apply(simp) -apply(rule S_Var) -apply(rule valid_eqvt) -apply(assumption) -*) -(* FIXME: here *) -(* apply(auto intro: closed_in_eqvt valid_eqvt dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) *) apply(force intro: closed_in_eqvt valid_eqvt silly_eqvt1) apply(force intro: valid_eqvt silly_eqvt2) apply(force) apply(force intro!: S_All simp add: fresh_prod pt_fresh_bij1[OF pt_tyvrs_inst, OF at_tyvrs_inst]) done -lemma subtype_of_rel_induct_aux[rule_format]: - fixes P :: "ty_context \ ty \ ty \'a::fs_tyvrs\bool" +lemma subtype_of_rel_induct[consumes 1, case_names S_Top S_Var S_Refl S_Arrow S_All]: + fixes P :: "'a::fs_tyvrs\ty_context \ ty \ ty \bool" assumes a: "\ \ S <: T" - and a1: "\x \ S. (\ \ ok) \ (S closed_in \) \ P \ S Top x" - and a2: "\x \ X S T. (\ \ ok) \ ((X,S)\set \) \ (\ \ S <: T) \ (\z. P \ S T z) - \ P \ (TyVar X) T x" - and a3: "\x \ X. (\ \ ok) \ X\(domain \) \ P \ (TyVar X) (TyVar X) x" - and a4: "\x \ S1 S2 T1 T2. \ \ T1 <: S1 \ (\z. P \ T1 S1 z) \ \ \ S2 <: T2 \ - (\z. P \ S2 T2 z) \ P \ (S1 \ S2) (T1 \ T2) x" - and a5: "\x \ X S1 S2 T1 T2. - X\x \ X\(\,S1,T1) \ \ \ T1 <: S1 \ (\z. P \ T1 S1 z) \ ((X,T1)#\) \ S2 <: T2 - \ (\z. P ((X,T1)#\) S2 T2 z) \ P \ (\ [X<:S1].S2) (\ [X<:T1].T2) x" - shows "\(pi::tyvrs prm) (x::'a::fs_tyvrs). P (pi\\) (pi\S) (pi\T) x" -using a -proof (induct) - case (S_Top S \) - have b1: "\ \ ok" by fact - have b2: "S closed_in \" by fact - show ?case - proof (intro strip, simp) - fix pi::"tyvrs prm" and x::"'a::fs_tyvrs" + and a1: "\\ S x. (\ \ ok) \ (S closed_in \) \ P x \ S Top" + and a2: "\\ X S T x. (\ \ ok) \ ((X,S)\set \) \ (\ \ S <: T) \ (\z. P z \ S T) + \ P x \ (TyVar X) T" + and a3: "\\ X x. (\ \ ok) \ X\domain \ \ P x \ (TyVar X) (TyVar X)" + and a4: "\\ S1 S2 T1 T2 x. \ \ T1 <: S1 \ (\z. P z \ T1 S1) \ \ \ S2 <: T2 \ + (\z. P z \ S2 T2) \ P x \ (S1 \ S2) (T1 \ T2)" + and a5: "\\ X S1 S2 T1 T2 x. + X\x \ X\(\,S1,T1) \ \ \ T1 <: S1 \ (\z. P z \ T1 S1) \ ((X,T1)#\) \ S2 <: T2 + \ (\z. P z ((X,T1)#\) S2 T2) \ P x \ (\ [X<:S1].S2) (\ [X<:T1].T2)" + shows "P x \ S T" +proof - + from a have "\(pi::tyvrs prm) (x::'a::fs_tyvrs). P x (pi\\) (pi\S) (pi\T)" + proof (induct) + case (S_Top S \) + have b1: "\ \ ok" by fact + have b2: "S closed_in \" by fact from b1 have "\ (pi\\) ok" by (rule valid_eqvt) moreover from b2 have "(pi\S) closed_in (pi\\)" by (rule closed_in_eqvt) - ultimately show "P (pi \ \) (pi \ S) Top x" by (rule a1) - qed -next - case (S_Var S T X \) - have b1: "\ \ ok" by fact - have b2: "(X,S) \ set \" by fact - have b3: "\ \ S <: T" by fact - have b4: "\(pi::tyvrs prm) x. P (pi\\) (pi\S) (pi\T) x" by fact - show ?case - proof (intro strip, simp) - fix pi::"tyvrs prm" and x::"'a::fs_tyvrs" + ultimately show "P x (pi \ \) (pi \ S) (pi\Top)" by (simp add: a1) + next + case (S_Var S T X \) + have b1: "\ \ ok" by fact + have b2: "(X,S) \ set \" by fact + have b3: "\ \ S <: T" by fact + have b4: "\(pi::tyvrs prm) x. P x (pi\\) (pi\S) (pi\T)" by fact from b1 have "\ (pi\\) ok" by (rule valid_eqvt) moreover from b2 have "pi\(X,S)\pi\(set \)" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) @@ -368,47 +351,39 @@ moreover from b3 have "(pi\\) \ (pi\S) <: (pi\T)" by (rule subtype_eqvt) moreover - from b4 have "\x. P (pi\\) (pi\S) (pi\T) x" by simp + from b4 have "\x. P x (pi\\) (pi\S) (pi\T)" by simp ultimately - show "P (pi\\) (TyVar (pi\X)) (pi\T) x" by (rule a2) - qed -next - case (S_Refl X \) - have b1: "\ \ ok" by fact - have b2: "X \ domain \" by fact - show ?case - proof (intro strip, simp) - fix pi::"tyvrs prm" and x::"'a::fs_tyvrs" + show "P x (pi\\) (pi\(TyVar X)) (pi\T)" by (simp add: a2) + next + case (S_Refl X \) + have b1: "\ \ ok" by fact + have b2: "X \ domain \" by fact from b1 have "\ (pi\\) ok" by (rule valid_eqvt) moreover from b2 have "(pi\X)\pi\domain \" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) hence "(pi\X)\domain (pi\\)" by (simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst]) - ultimately show "P (pi\\) (TyVar (pi\X)) (TyVar (pi\X)) x" by (rule a3) - qed -next - case S_Arrow thus ?case by (simp, auto intro!: a4 subtype_eqvt) -next - case (S_All S1 S2 T1 T2 X \) - have b1: "\ \ T1 <: S1" by fact - have b2: "\(pi::tyvrs prm) x. P (pi\\) (pi\T1) (pi\S1) x" by fact - have b4: "((X,T1)#\) \ S2 <: T2" by fact - have b5: "\(pi::tyvrs prm) x. P (pi\((X,T1)#\)) (pi\S2) (pi\T2) x" by fact - have b3': "X\\" by fact - have b3'': "X\(T1,S1)" using b1 b3' by (rule subtype_implies_fresh) - have b3: "X\(\,S1,T1)" using b3' b3'' by (simp add: fresh_prod) - show ?case - proof (intro strip) - fix pi::"tyvrs prm" and x::"'a::fs_tyvrs" + ultimately show "P x (pi\\) (pi\(TyVar X)) (pi\(TyVar X))" by (simp add: a3) + next + case S_Arrow thus ?case by (simp, auto intro!: a4 subtype_eqvt) + next + case (S_All S1 S2 T1 T2 X \) + have b1: "\ \ T1 <: S1" by fact + have b2: "\(pi::tyvrs prm) x. P x (pi\\) (pi\T1) (pi\S1)" by fact + have b4: "((X,T1)#\) \ S2 <: T2" by fact + have b5: "\(pi::tyvrs prm) x. P x (pi\((X,T1)#\)) (pi\S2) (pi\T2)" by fact + have b3': "X\\" by fact + have b3'': "X\(T1,S1)" using b1 b3' by (rule subtype_implies_fresh) + have b3: "X\(\,S1,T1)" using b3' b3'' by (simp add: fresh_prod) have "\C::tyvrs. C\(pi\X,pi\S2,pi\T2,pi\S1,pi\T1,pi\\,x)" by (rule at_exists_fresh[OF at_tyvrs_inst], simp add: fs_tyvrs1) then obtain C::"tyvrs" where f1: "C\(pi\X)" and f2: "C\(pi\S1)" and f3: "C\(pi\T1)" and f4: "C\(pi\S2)" and f5: "C\(pi\T2)" and f6: "C\(pi\\)" and f7: "C\x" by (auto simp add: fresh_prod fresh_atm) let ?pi' = "[(C,pi\X)]@pi" - from b2 have c1: "\x. P (?pi'\\) (?pi'\T1) (?pi'\S1) x" by simp - from b5 have "\x. P (?pi'\((X,T1)#\)) (?pi'\S2) (?pi'\T2) x" by simp - hence "\x. P ((?pi'\X,?pi'\T1)#(?pi'\\)) (?pi'\S2) (?pi'\T2) x" by simp - hence c2: "\x. P ((C,?pi'\T1)#(?pi'\\)) (?pi'\S2) (?pi'\T2) x" using f1 + from b2 have c1: "\x. P x (?pi'\\) (?pi'\T1) (?pi'\S1)" by simp + from b5 have "\x. P x (?pi'\((X,T1)#\)) (?pi'\S2) (?pi'\T2)" by simp + hence "\x. P x ((?pi'\X,?pi'\T1)#(?pi'\\)) (?pi'\S2) (?pi'\T2)" by simp + hence c2: "\x. P x ((C,?pi'\T1)#(?pi'\\)) (?pi'\S2) (?pi'\T2)" using f1 by (simp only: pt_tyvrs2 calc_atm, simp) from b3 have "(pi\X)\(pi\\)" by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) @@ -431,39 +406,25 @@ hence e2: "((C,?pi'\T1)#(?pi'\\)) \ (?pi'\S2) <: (?pi'\T2)" using f1 by (simp only: pt_tyvrs2 calc_atm, simp) have fnew: "C\(?pi'\\,?pi'\S1,?pi'\T1)" using f6' f2' f3' by (simp add: fresh_prod) - have main: "P (?pi'\\) (\ [C<:(?pi'\S1)].(?pi'\S2)) (\ [C<:(?pi'\T1)].(?pi'\T2)) x" + have main: "P x (?pi'\\) (\ [C<:(?pi'\S1)].(?pi'\S2)) (\ [C<:(?pi'\T1)].(?pi'\T2))" using f7 fnew e1 c1 e2 c2 by (rule a5) have alpha1: "(\ [C<:(?pi'\S1)].(?pi'\S2)) = (pi\(\ [X<:S1].S2))" using f1 f4 f2a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) have alpha2: "(\ [C<:(?pi'\T1)].(?pi'\T2)) = (pi\(\ [X<:T1].T2))" using f1 f5 f3a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) - show "P (pi\\) (pi\(\ [X<:S1].S2)) (pi\(\ [X<:T1].T2)) x" + show "P x (pi\\) (pi\(\ [X<:S1].S2)) (pi\(\ [X<:T1].T2))" using alpha1 alpha2 f6a main by simp qed + hence "P x (([]::tyvrs prm)\\) (([]::tyvrs prm)\S) (([]::tyvrs prm)\T)" by blast + thus ?thesis by simp qed -lemma subtype_of_rel_induct[case_names S_Top S_Var S_Refl S_Arrow S_All]: - fixes P :: "ty_context \ ty \ ty \'a::fs_tyvrs\bool" - assumes a: "\ \ S <: T" - and a1: "\x \ S. (\ \ ok) \ (S closed_in \) \ P \ S Top x" - and a2: "\x \ X S T. (\ \ ok) \ ((X,S)\set \) \ (\ \ S <: T) \ (\z. P \ S T z) - \ P \ (TyVar X) T x" - and a3: "\x \ X. (\ \ ok) \ X\domain \ \ P \ (TyVar X) (TyVar X) x" - and a4: "\x \ S1 S2 T1 T2. \ \ T1 <: S1 \ (\z. P \ T1 S1 z) \ \ \ S2 <: T2 \ - (\z. P \ S2 T2 z) \ P \ (S1 \ S2) (T1 \ T2) x" - and a5: "\x \ X S1 S2 T1 T2. - X\x \ X\(\,S1,T1) \ \ \ T1 <: S1 \ (\z. P \ T1 S1 z) \ ((X,T1)#\) \ S2 <: T2 - \ (\z. P ((X,T1)#\) S2 T2 z) \ P \ (\ [X<:S1].S2) (\ [X<:T1].T2) x" - shows "P \ S T x" -using a a1 a2 a3 a4 a5 subtype_of_rel_induct_aux[of "\" "S" "T" "P" "[]" "x", simplified] by force - - section {* Two proofs for reflexivity of subtyping *} lemma subtype_reflexivity: shows "\ \ ok \ T closed_in \ \ \ \ T <: T" -proof(nominal_induct T rule: ty.induct_unsafe) - case (TAll \ X T1 T2) +proof(nominal_induct T fresh: \ rule: ty.induct_unsafe) + case (TAll X T1 T2) have i1: "\\. \ \ ok \ T1 closed_in \ \ \ \ T1 <: T1" by fact have i2: "\\. \ \ ok \ T2 closed_in \ \ \ \ T2 <: T2" by fact have f: "X\\" by fact @@ -481,13 +442,15 @@ qed qed (auto simp add: closed_in_def ty.supp supp_atm) -lemma subtype_refl: - shows "\ \ ok \ T closed_in \ \ \ \ T <: T" -apply(nominal_induct T rule: ty.induct_unsafe) +lemma subtype_reflexivity: + assumes a: "\ \ ok" + and b: "T closed_in \" + shows "\ \ T <: T" +using a b +apply(nominal_induct T fresh: \ rule: ty.induct_unsafe) apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm) -(* FIXME: the new induction method from Markus will fix this uglyness *) -apply(atomize) -apply(drule_tac x="(tyvrs, ty2)#z" in spec) +(* too bad that this cannot be found automatically *) +apply(drule_tac x="(tyvrs, ty2)#\" in meta_spec) apply(force simp add: closed_in_def) done @@ -545,7 +508,7 @@ fixes P :: "ty" and X :: "tyvrs" shows "X\(T,P) \ X\(subst_ty T Y P)" - apply (nominal_induct T rule: ty.induct_unsafe) + apply (nominal_induct T fresh: T Y P rule: ty.induct_unsafe) apply (auto simp add: fresh_prod abs_fresh) done @@ -633,8 +596,8 @@ assumes a1: "\ \ S <: T" shows "\ \ ok \ \ extends \ \ \ \ S <: T" using a1 -proof (nominal_induct \ S T rule: subtype_of_rel_induct) - case (S_Top \ \ S) +proof (nominal_induct \ S T fresh: \ rule: subtype_of_rel_induct) + case (S_Top \ S) have lh_drv_prem: "S closed_in \" by fact show "\ \ ok \ \ extends \ \ \ \ S <: Top" proof (intro strip) @@ -645,9 +608,9 @@ ultimately show "\ \ S <: Top" by force qed next - case (S_Var \ \ X S T) + case (S_Var \ X S T) have lh_drv_prem: "(X,S) \ set \" by fact - have ih: "\\. \ \ ok \ \ extends \ \ \ \ S <: T" by fact + have ih: "\\. \ \ ok \ \ extends \ \ \ \ S <: T" by fact show "\ \ ok \ \ extends \ \ \ \ TyVar X <: T" proof (intro strip) assume ok: "\ \ ok" @@ -658,7 +621,7 @@ ultimately show "\ \ TyVar X <: T" using ok by force qed next - case (S_Refl \ \ X) + case (S_Refl \ X) have lh_drv_prem: "X \ domain \" by fact show ?case proof (intro strip) @@ -671,10 +634,10 @@ next case S_Arrow thus ?case by force next - case (S_All \ \ X S1 S2 T1 T2) + case (S_All \ X S1 S2 T1 T2) have fresh: "X\\" by fact - have ih1: "\\. \ \ ok \ \ extends \ \ \ \ T1 <: S1" by fact - have ih2: "\\. \ \ ok \ \ extends ((X,T1)#\) \ \ \ S2 <: T2" by fact + have ih1: "\\. \ \ ok \ \ extends \ \ \ \ T1 <: S1" by fact + have ih2: "\\. \ \ ok \ \ extends ((X,T1)#\) \ \ \ S2 <: T2" by fact have lh_drv_prem: "\ \ T1 <: S1" by fact hence b5: "T1 closed_in \" by (simp add: subtype_implies_closed) show "\ \ ok \ \ extends \ \ \ \ \ [X<:S1].S2 <: \ [X<:T1].T2" @@ -698,19 +661,19 @@ assumes a1: "\ \ S <: T" shows "\ \ ok \ \ extends \ \ \ \ S <: T" using a1 -proof (nominal_induct \ S T rule: subtype_of_rel_induct) - case (S_Top \ \ S) thus ?case by (force intro: extends_closed) +proof (nominal_induct \ S T fresh: \ rule: subtype_of_rel_induct) + case (S_Top \ S) thus ?case by (force intro: extends_closed) next - case (S_Var \ \ X S T) thus ?case by (force simp add: extends_def) + case (S_Var \ X S T) thus ?case by (force simp add: extends_def) next - case (S_Refl \ \ X) thus ?case by (force dest: extends_domain) + case (S_Refl \ X) thus ?case by (force dest: extends_domain) next case S_Arrow thus ?case by force next - case (S_All \ \ X S1 S2 T1 T2) + case (S_All \ X S1 S2 T1 T2) have fresh: "X\\" by fact - have ih1: "\\. \ \ ok \ \ extends \ \ \ \ T1 <: S1" by fact - have ih2: "\\. \ \ ok \ \ extends ((X,T1)#\) \ \ \ S2 <: T2" by fact + have ih1: "\\. \ \ ok \ \ extends \ \ \ \ T1 <: S1" by fact + have ih2: "\ \. \ \ ok \ \ extends ((X,T1)#\) \ \ \ S2 <: T2" by fact have lh_drv_prem: "\ \ T1 <: S1" by fact hence b5: "T1 closed_in \" by (simp add: subtype_implies_closed) show "\ \ ok \ \ extends \ \ \ \ \ [X<:S1].S2 <: \ [X<:T1].T2"