diff -r a30d0bb76869 -r 9f667f6da04f Nominal/CPS/Lt.thy --- a/Nominal/CPS/Lt.thy Thu Jun 16 21:23:38 2011 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,131 +0,0 @@ -header {* The Call-by-Value Lambda Calculus *} -theory Lt -imports Nominal2 -begin - -atom_decl name - -nominal_datatype lt = - Var name ("_~" [150] 149) - | Abs x::"name" t::"lt" bind x in t - | App lt lt (infixl "$" 100) - -nominal_primrec - subst :: "lt \ lt \ name \ lt" ("_[_'/_]" [200,0,0] 190) -where - "(y~)[L/x] = (if y = x then L else y~)" -| "atom y\L \ atom y\x \ (Abs y M)[L/x] = Abs y (M[L/x])" -| "(M $ N)[L/x] = M[L/x] $ N[L/x]" - unfolding eqvt_def subst_graph_def - apply(perm_simp) - apply(auto) - apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) - apply(simp_all add: fresh_star_def fresh_Pair) - apply blast+ - apply (erule Abs_lst1_fcb) - apply (simp_all add: Abs_fresh_iff)[2] - apply(drule_tac a="atom (ya)" in fresh_eqvt_at) - apply(simp add: finite_supp fresh_Pair) - apply(simp_all add: fresh_Pair Abs_fresh_iff) - apply(subgoal_tac "(atom y \ atom ya) \ La = La") - apply(subgoal_tac "(atom y \ atom ya) \ xa = xa") - apply(simp add: atom_eqvt eqvt_at_def Abs1_eq_iff swap_commute) - apply (simp_all add: swap_fresh_fresh) - done - -termination - by (relation "measure (\(t, _, _). size t)") - (simp_all add: lt.size) - -lemma subst_eqvt[eqvt]: - shows "p\(M[V/(x::name)]) = (p\M)[(p\V)/(p\x)]" - by (induct M V x rule: subst.induct) (simp_all) - -lemma forget[simp]: - shows "atom x \ M \ M[s/x] = M" - by (nominal_induct M avoiding: x s rule: lt.strong_induct) - (auto simp add: lt.fresh fresh_at_base) - -lemma [simp]: "supp ( M[V/(x::name)] ) <= (supp(M) - {atom x}) Un (supp V)" - by (nominal_induct M avoiding: x V rule: lt.strong_induct) - (auto simp add: lt.supp supp_at_base, blast, blast) - -nominal_primrec - isValue:: "lt => bool" -where - "isValue (Var x) = True" -| "isValue (Abs y N) = True" -| "isValue (A $ B) = False" - unfolding eqvt_def isValue_graph_def - by (perm_simp, auto) - (erule lt.exhaust, auto) - -termination - by (relation "measure size") - (simp_all add: lt.size) - -lemma is_Value_eqvt[eqvt]: - shows "p\(isValue (M::lt)) = isValue (p\M)" - by (induct M rule: lt.induct) (simp_all add: eqvts) - -inductive - eval :: "[lt, lt] \ bool" (" _ \\<^isub>\ _" [80,80] 80) - where - evbeta: "\atom x\V; isValue V\ \ ((Abs x M) $ V) \\<^isub>\ (M[V/x])" -| ev1: "\isValue V; M \\<^isub>\ M' \ \ (V $ M) \\<^isub>\ (V $ M')" -| ev2: "M \\<^isub>\ M' \ (M $ N) \\<^isub>\ (M' $ N)" - -equivariance eval - -nominal_inductive eval -done - -(*lemmas [simp] = lt.supp(2)*) - -lemma closedev1: assumes "s \\<^isub>\ t" - shows "supp t <= supp s" - using assms - by (induct, auto simp add: lt.supp) - - -lemma [simp]: "~ ((Abs x M) \\<^isub>\ N)" -by (rule, erule eval.cases, simp_all) - -lemma [simp]: assumes "M \\<^isub>\ N" shows "~ isValue M" -using assms -by (cases, auto) - - -inductive - eval_star :: "[lt, lt] \ bool" (" _ \\<^isub>\\<^sup>* _" [80,80] 80) - where - evs1: "M \\<^isub>\\<^sup>* M" -| evs2: "\M \\<^isub>\ M'; M' \\<^isub>\\<^sup>* M'' \ \ M \\<^isub>\\<^sup>* M''" - -lemma eval_evs: assumes *: "M \\<^isub>\ M'" shows "M \\<^isub>\\<^sup>* M'" -by (rule evs2, rule *, rule evs1) - -lemma eval_trans[trans]: - assumes "M1 \\<^isub>\\<^sup>* M2" - and "M2 \\<^isub>\\<^sup>* M3" - shows "M1 \\<^isub>\\<^sup>* M3" - using assms - by (induct, auto intro: evs2) - -lemma evs3[rule_format]: assumes "M1 \\<^isub>\\<^sup>* M2" - shows "M2 \\<^isub>\ M3 \ M1 \\<^isub>\\<^sup>* M3" - using assms - by (induct, auto intro: eval_evs evs2) - -equivariance eval_star - -lemma evbeta': - fixes x :: name - assumes "isValue V" and "atom x\V" and "N = (M[V/x])" - shows "((Abs x M) $ V) \\<^isub>\\<^sup>* N" - using assms by simp (rule evs2, rule evbeta, simp_all add: evs1) - -end - - -