# HG changeset patch # User Cezary Kaliszyk # Date 1268822458 -3600 # Node ID 4ac3485899e182247e346fc211470e539af41bac # Parent e911dae2073745472106f9869c53bd598322f58a Updated Type Schemes to automatic lifting. One goal is not true because of the restriction. diff -r e911dae20737 -r 4ac3485899e1 Nominal/TySch.thy --- a/Nominal/TySch.thy Wed Mar 17 11:20:24 2010 +0100 +++ b/Nominal/TySch.thy Wed Mar 17 11:40:58 2010 +0100 @@ -1,99 +1,123 @@ theory TySch -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +imports "Parser" "../Attic/Prove" begin atom_decl name -text {* type schemes *} -datatype ty = - Var "name" -| Fun "ty" "ty" +ML {* val _ = cheat_fv_rsp := false *} +ML {* val _ = cheat_const_rsp := false *} +ML {* val _ = cheat_equivp := false *} +ML {* val _ = cheat_fv_eqvt := false *} +ML {* val _ = cheat_alpha_eqvt := false *} +ML {* val _ = recursive := false *} -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.ty") 1 *} -print_theorems - -datatype tyS = - All "name set" "ty" +nominal_datatype t = + Var "name" +| Fun "t" "t" +and tyS = + All xs::"name set" ty::"t" bind xs in ty -lemma support_image: "supp (atom ` (s :: (('a :: at) set))) = supp s" -apply (simp add: supp_def) -apply (simp add: eqvts eqvts_raw) -(* apply (metis COMBC_def Collect_def Collect_mem_eq atom_name_def_raw finite finite_imageI obtain_at_base rangeI)*) -sorry +thm t_tyS_fv +thm t_tyS_inject +thm t_tyS_bn +thm t_tyS_perm +thm t_tyS_induct +thm t_tyS_distinct -lemma atom_image_swap_fresh: "\a \ atom ` (fn :: ('a :: at) set); b \ atom ` fn\ \ (a \ b) \ fn = fn" -apply (simp add: fresh_def) -apply (simp add: support_image) -apply (fold fresh_def) -apply (simp add: swap_fresh_fresh) -done - -lemma "\a \ atom ` fun; a \ t; b \ atom ` fun; b \ t\ \ All ((a \ b) \ fun) t = All fun t" -apply (simp add: atom_image_swap_fresh) +lemma supports: + "(supp (atom i)) supports (Var i)" + "(supp A \ supp M) supports (Fun A M)" +apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh t_tyS_perm) +apply clarify +apply(simp_all add: fresh_atom) done -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *} -print_theorems +lemma fs: + "finite (supp (x\t)) \ finite (supp (z\tyS))" +apply(induct rule: t_tyS_induct) +apply(rule supports_finite) +apply(rule supports) +apply(simp add: supp_atom) +apply(rule supports_finite) +apply(rule supports) +apply(simp add: supp_atom) +sorry -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty") - [[[[]], [[], []]]] *} -print_theorems +instance t and tyS :: fs +apply default +apply (simp_all add: fs) +sorry + +(* Should be moved to a proper place *) +lemma infinite_Un: + shows "infinite (S \ T) \ infinite S \ infinite T" + by simp -(* -Doesnot work yet since we do not refer to fv_ty -local_setup {* define_raw_fv (Datatype.the_info @{theory} "TySch.tyS") [[[[], []]]] *} -print_theorems -*) - -primrec - fv_tyS -where - "fv_tyS (All xs T) = (fv_ty T - atom ` xs)" - -inductive - alpha_tyS :: "tyS \ tyS \ bool" ("_ \tyS _" [100, 100] 100) -where - a1: "\pi. ((atom ` xs1, T1) \gen (op =) fv_ty pi (atom ` xs2, T2)) - \ All xs1 T1 \tyS All xs2 T2" +lemma supp_fv_t_tyS: + shows "supp T = fv_t T" + and "supp S = fv_tyS S" +apply(induct T and S rule: t_tyS_inducts) +apply(simp_all add: t_tyS_fv) +(* VarTS case *) +apply(simp only: supp_def) +apply(simp only: t_tyS_perm) +apply(simp only: t_tyS_inject) +apply(simp only: supp_def[symmetric]) +apply(simp only: supp_at_base) +(* FunTS case *) +apply(simp only: supp_def) +apply(simp only: t_tyS_perm) +apply(simp only: t_tyS_inject) +apply(simp only: de_Morgan_conj) +apply(simp only: Collect_disj_eq) +apply(simp only: infinite_Un) +apply(simp only: Collect_disj_eq) +(* All case *) +apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst) +apply(simp (no_asm) only: supp_def) +apply(simp only: t_tyS_perm) +apply(simp only: permute_ABS) +apply(simp only: t_tyS_inject) +apply(simp only: Abs_eq_iff) +apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) +apply(simp only: alpha_gen) +apply(simp only: supp_eqvt[symmetric]) +apply(simp only: eqvts) +apply(simp only: supp_Abs) +done lemma - shows "All {a, b} (Fun (Var a) (Var b)) \tyS All {b, a} (Fun (Var a) (Var b))" - apply(rule a1) + shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" + apply(simp add: t_tyS_inject) + apply(rule_tac x="0::perm" in exI) apply(simp add: alpha_gen) - apply(rule_tac x="0::perm" in exI) - apply(simp add: fresh_star_def) + apply(auto) + apply(simp add: fresh_star_def fresh_zero_perm) done lemma - shows "All {a, b} (Fun (Var a) (Var b)) \tyS All {a, b} (Fun (Var b) (Var a))" - apply(rule a1) - apply(simp add: alpha_gen) + shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))" + apply(simp add: t_tyS_inject) apply(rule_tac x="(atom a \ atom b)" in exI) - apply(simp add: fresh_star_def) + apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts) + apply auto done lemma - shows "All {a, b, c} (Fun (Var a) (Var b)) \tyS All {a, b} (Fun (Var a) (Var b))" - apply(rule a1) - apply(simp add: alpha_gen) + shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))" + apply(simp add: t_tyS_inject) apply(rule_tac x="0::perm" in exI) - apply(simp add: fresh_star_def) - done + apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject) +oops lemma assumes a: "a \ b" - shows "\(All {a, b} (Fun (Var a) (Var b)) \tyS All {c} (Fun (Var c) (Var c)))" + shows "\(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))" using a + apply(simp add: t_tyS_inject) apply(clarify) - apply(erule alpha_tyS.cases) - apply(simp add: alpha_gen) - apply(erule conjE)+ - apply(erule exE) - apply(erule conjE)+ - apply(clarify) - apply(simp) - apply(simp add: fresh_star_def) - apply(auto) + apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject) + apply auto done