# HG changeset patch # User Cezary Kaliszyk # Date 1268897575 -3600 # Node ID 2ff84b1f551f047e64000ac9569acd0a260802ee # Parent 1c9931e5039a7d700b1b4714a8ecb67a47b8d4f1 Rename bound variables + minor cleaning. diff -r 1c9931e5039a -r 2ff84b1f551f Nominal/Fv.thy --- a/Nominal/Fv.thy Thu Mar 18 08:03:42 2010 +0100 +++ b/Nominal/Fv.thy Thu Mar 18 08:32:55 2010 +0100 @@ -754,16 +754,6 @@ | SOME i => i *} -ML {* -fun rename_vars fnctn thm = -let - val vars = Term.add_vars (prop_of thm) [] - val nvars = map (Var o ((apfst o apfst) fnctn)) vars -in - Thm.certify_instantiate ([], (vars ~~ nvars)) thm -end -*} - lemma not_in_union: "c \ a \ b \ (c \ a \ c \ b)" by auto diff -r 1c9931e5039a -r 2ff84b1f551f Nominal/LFex.thy --- a/Nominal/LFex.thy Thu Mar 18 08:03:42 2010 +0100 +++ b/Nominal/LFex.thy Thu Mar 18 08:32:55 2010 +0100 @@ -37,14 +37,14 @@ lemma supp_eqs: "supp Type = {}" - "supp rkind = fv_kind rkind \ supp (KPi rty name rkind) = supp rty \ supp (Abs {atom name} rkind)" + "supp kind = fv_kind kind \ supp (KPi ty name kind) = supp ty \ supp (Abs {atom name} kind)" "supp (TConst i) = {atom i}" "supp (TApp A M) = supp A \ supp M" - "supp rty2 = fv_ty rty2 \ supp (TPi rty1 name rty2) = supp rty1 \ supp (Abs {atom name} rty2)" + "supp ty2 = fv_ty ty2 \ supp (TPi ty1 name ty2) = supp ty1 \ supp (Abs {atom name} ty2)" "supp (Const i) = {atom i}" "supp (Var x) = {atom x}" "supp (App M N) = supp M \ supp N" - "supp rtrm = fv_trm rtrm \ supp (Lam rty name rtrm) = supp rty \ supp (Abs {atom name} rtrm)" + "supp trm = fv_trm trm \ supp (Lam ty name trm) = supp ty \ supp (Abs {atom name} trm)" apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm) apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen) apply(simp_all only: ex_out) @@ -64,7 +64,7 @@ apply(simp_all add: supp_Abs) done -lemma supp_rkind_rty_rtrm: +lemma supp_kind_ty_trm: "supp Type = {}" "supp (KPi A x K) = supp A \ (supp K - {atom x})" "supp (TConst i) = {atom i}" diff -r 1c9931e5039a -r 2ff84b1f551f Nominal/Lift.thy --- a/Nominal/Lift.thy Thu Mar 18 08:03:42 2010 +0100 +++ b/Nominal/Lift.thy Thu Mar 18 08:32:55 2010 +0100 @@ -3,14 +3,45 @@ begin ML {* -fun lift_thm ctxt thm = +fun rename_vars fnctn thm = +let + val vars = Term.add_vars (prop_of thm) [] + val nvars = map (Var o ((apfst o apfst) fnctn)) vars +in + Thm.certify_instantiate ([], (vars ~~ nvars)) thm +end +*} + +ML {* +fun un_raws name = let fun un_raw name = unprefix "_raw" name handle Fail _ => name fun add_under names = hd names :: (map (prefix "_") (tl names)) - fun un_raws name = implode (map un_raw (add_under (space_explode "_" name))) +in + implode (map un_raw (add_under (space_explode "_" name))) +end +*} + +(* Similar to Tools/IsaPlanner/rw_tools.ML *) +ML {* +fun rename_term_bvars (Abs(s, ty, t)) = (Abs(un_raws s, ty, rename_term_bvars t)) + | rename_term_bvars (a $ b) = (rename_term_bvars a) $ (rename_term_bvars b) + | rename_term_bvars x = x; + +fun rename_thm_bvars th = +let + val t = Thm.prop_of th +in + Thm.rename_boundvars t (rename_term_bvars t) th +end; +*} + +ML {* +fun lift_thm ctxt thm = +let val un_raw_names = rename_vars un_raws in - un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))) + rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))) end *} diff -r 1c9931e5039a -r 2ff84b1f551f Nominal/Test.thy --- a/Nominal/Test.thy Thu Mar 18 08:03:42 2010 +0100 +++ b/Nominal/Test.thy Thu Mar 18 08:32:55 2010 +0100 @@ -43,7 +43,7 @@ apply(simp only: infinite_Un) apply(simp only: Collect_disj_eq) apply(simp only: supp_def[symmetric]) -apply(rule_tac t="supp (Lm name lm_raw)" and s="supp (Abs {atom name} lm_raw)" in subst) +apply(rule_tac t="supp (Lm name lm)" and s="supp (Abs {atom name} lm)" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: lm_perm) apply(simp only: permute_ABS) @@ -68,8 +68,8 @@ lemma assumes a0: "finite (supp c)" and a1: "\name c. P c (Vr name)" - and a2: "\lm_raw1 lm_raw2 c. \\d. P d lm_raw1; \d. P d lm_raw2\ \ P c (Ap lm_raw1 lm_raw2)" - and a3: "\name lm_raw c. \\d. P d lm_raw\ \ P c (Lm name lm_raw)" + and a2: "\lm1 lm2 c. \\d. P d lm1; \d. P d lm2\ \ P c (Ap lm1 lm2)" + and a3: "\name lm c. \\d. P d lm\ \ P c (Lm name lm)" shows "P c lm" proof - have "\p c. P c (p \ lm)" @@ -80,11 +80,11 @@ apply(rule a2) apply(assumption) apply(assumption) - apply(subgoal_tac "\new::name. (atom new) \ (c, Lm (p \ name) (p \ lm_raw)) + apply(subgoal_tac "\new::name. (atom new) \ (c, Lm (p \ name) (p \ lm)) \ sort_of (atom new) = sort_of (atom name)") apply(erule exE) - apply(rule_tac t="(p \ Lm name lm_raw)" and - s="((((atom (p \ name)) \ (atom new)) + p) \ Lm name lm_raw)" in subst) + apply(rule_tac t="(p \ Lm name lm)" and + s="((((atom (p \ name)) \ (atom new)) + p) \ Lm name lm)" in subst) apply(simp) apply(subst lm_perm) apply(subst (2) lm_perm) @@ -150,7 +150,7 @@ apply(simp only: infinite_Un) apply(simp only: Collect_disj_eq) (* LAM case *) -apply(rule_tac t="supp (LAM name lam_raw)" and s="supp (Abs {atom name} lam_raw)" in subst) +apply(rule_tac t="supp (LAM name lam)" and s="supp (Abs {atom name} lam)" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: lam_bp_perm) apply(simp only: permute_ABS) @@ -162,7 +162,7 @@ apply(simp only: eqvts) apply(simp only: supp_Abs) (* LET case *) -apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \ fv_bi bp_raw" in subst) +apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \ fv_bi bp" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: lam_bp_perm) apply(simp only: permute_ABS) @@ -239,7 +239,7 @@ apply(simp only: infinite_Un) apply(simp only: Collect_disj_eq) (* LAM case *) -apply(rule_tac t="supp (LAM' name lam'_raw)" and s="supp (Abs {atom name} lam'_raw)" in subst) +apply(rule_tac t="supp (LAM' name lam')" and s="supp (Abs {atom name} lam')" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: lam'_bp'_perm) apply(simp only: permute_ABS) @@ -251,8 +251,8 @@ apply(simp only: eqvts) apply(simp only: supp_Abs) (* LET case *) -apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and - s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst) +apply(rule_tac t="supp (LET' bp' lam')" and + s="supp (Abs (bi' bp') (bp', lam'))" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: lam'_bp'_perm) apply(simp only: permute_ABS) @@ -325,7 +325,7 @@ apply(simp only: infinite_Un) apply(simp only: Collect_disj_eq) (* LAM case *) -apply(rule_tac t="supp (Lam name trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst) +apply(rule_tac t="supp (Lam name trm')" and s="supp (Abs {atom name} trm')" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: trm'_pat'_perm) apply(simp only: permute_ABS) @@ -337,8 +337,8 @@ apply(simp only: eqvts) apply(simp only: supp_Abs) (* LET case *) -apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)" - and s="supp (Abs (f pat'_raw) trm'_raw2) \ supp trm'_raw1 \ fv_f pat'_raw" in subst) +apply(rule_tac t="supp (Let pat' trm'1 trm'2)" + and s="supp (Abs (f pat') trm'2) \ supp trm'1 \ fv_f pat'" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: trm'_pat'_perm) apply(simp only: permute_ABS) @@ -460,7 +460,7 @@ 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(rule_tac t="supp (All fun t)" and s="supp (Abs (atom ` fun) t)" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: t_tyS_perm) apply(simp only: permute_ABS) diff -r 1c9931e5039a -r 2ff84b1f551f Nominal/TySch.thy --- a/Nominal/TySch.thy Thu Mar 18 08:03:42 2010 +0100 +++ b/Nominal/TySch.thy Thu Mar 18 08:32:55 2010 +0100 @@ -9,7 +9,6 @@ ML {* val _ = cheat_equivp := false *} ML {* val _ = cheat_fv_eqvt := false *} ML {* val _ = cheat_alpha_eqvt := false *} -ML {* val _ = recursive := false *} nominal_datatype t = Var "name" @@ -24,68 +23,6 @@ thm t_tyS_induct thm t_tyS_distinct -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 - -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 - -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 - -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_eq_iff) -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_eq_iff) -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_eq_iff) -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)) = All {b, a} (Fun (Var a) (Var b))" apply(simp add: t_tyS_eq_iff) @@ -120,5 +57,4 @@ apply auto done - end