Nominal/Ex/CPS/Lt.thy
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Tue, 19 Feb 2013 05:42:51 +0000
changeset 3207 d3f7c8cce53b
parent 3197 25d11b449e92
child 3231 188826f1ccdb
permissions -rw-r--r--
updated README
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
header {* The Call-by-Value Lambda Calculus *}
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
theory Lt
2898
a95a497e1f4f Make examples work with non-precompiled image
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2864
diff changeset
     3
imports "../../Nominal2"
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
begin
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
atom_decl name
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
nominal_datatype lt =
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
    Var name       ("_~"  [150] 149)
3187
b3d97424b130 added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de>
parents: 3186
diff changeset
    10
  | App lt lt         (infixl "$$" 100)
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    11
  | Lam x::"name" t::"lt"  binds  x in t
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    12
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
nominal_primrec
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    14
  subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt"  ("_ [_ ::= _]" [90, 90, 90] 90)
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
where
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    16
  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    17
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    18
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
3197
25d11b449e92 definition of an auxiliary graph in nominal-primrec definitions
Christian Urban <urbanc@in.tum.de>
parents: 3192
diff changeset
    19
  unfolding eqvt_def subst_graph_aux_def
3186
425b4c406d80 added CPS files to test (not all proofs have been completed)
Christian Urban <urbanc@in.tum.de>
parents: 3089
diff changeset
    20
  apply (simp)
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    21
  apply(rule TrueI)
3192
14c7d7e29c44 added a simproc for alpha-equivalence to the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 3187
diff changeset
    22
  using [[simproc del: alpha_lst]]
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    23
  apply(auto simp add: lt.distinct lt.eq_iff)
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
  apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    25
  apply blast
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    26
  apply(simp_all add: fresh_star_def fresh_Pair_elim)
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    27
  apply blast
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    28
  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
3186
425b4c406d80 added CPS files to test (not all proofs have been completed)
Christian Urban <urbanc@in.tum.de>
parents: 3089
diff changeset
    29
  apply(simp add: Abs_fresh_iff)
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    30
  apply(simp add: fresh_star_def fresh_Pair)
3186
425b4c406d80 added CPS files to test (not all proofs have been completed)
Christian Urban <urbanc@in.tum.de>
parents: 3089
diff changeset
    31
  apply(simp add: eqvt_at_def)
425b4c406d80 added CPS files to test (not all proofs have been completed)
Christian Urban <urbanc@in.tum.de>
parents: 3089
diff changeset
    32
  apply(simp add: perm_supp_eq fresh_star_Pair)
425b4c406d80 added CPS files to test (not all proofs have been completed)
Christian Urban <urbanc@in.tum.de>
parents: 3089
diff changeset
    33
  apply(simp add: eqvt_at_def)
425b4c406d80 added CPS files to test (not all proofs have been completed)
Christian Urban <urbanc@in.tum.de>
parents: 3089
diff changeset
    34
  apply(simp add: perm_supp_eq fresh_star_Pair)
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    35
done
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    36
2984
1b39ba5db2c1 update to 'termination (eqvt)'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2963
diff changeset
    37
termination (eqvt) by lexicographic_order
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
lemma forget[simp]:
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    40
  shows "atom x \<sharp> M \<Longrightarrow> M[x ::= s] = M"
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    41
  by (nominal_induct M avoiding: x s rule: lt.strong_induct)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
     (auto simp add: lt.fresh fresh_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    44
lemma [simp]: "supp (M[x ::= V]) <= (supp(M) - {atom x}) Un (supp V)"
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    45
  by (nominal_induct M avoiding: x V rule: lt.strong_induct)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    46
     (auto simp add: lt.supp supp_at_base, blast, blast)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    47
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    48
nominal_primrec
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    49
  isValue:: "lt => bool"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
where
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    51
  "isValue (Var x) = True"
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    52
| "isValue (Lam y N) = True"
3187
b3d97424b130 added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de>
parents: 3186
diff changeset
    53
| "isValue (A $$ B) = False"
3197
25d11b449e92 definition of an auxiliary graph in nominal-primrec definitions
Christian Urban <urbanc@in.tum.de>
parents: 3192
diff changeset
    54
  unfolding eqvt_def isValue_graph_aux_def
25d11b449e92 definition of an auxiliary graph in nominal-primrec definitions
Christian Urban <urbanc@in.tum.de>
parents: 3192
diff changeset
    55
  by (auto)
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    56
     (erule lt.exhaust, auto)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    57
2984
1b39ba5db2c1 update to 'termination (eqvt)'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2963
diff changeset
    58
termination (eqvt)
1b39ba5db2c1 update to 'termination (eqvt)'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2963
diff changeset
    59
  by (relation "measure size") (simp_all)
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    60
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    61
inductive
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    62
  eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    63
  where
3192
14c7d7e29c44 added a simproc for alpha-equivalence to the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 3187
diff changeset
    64
   evbeta: "\<lbrakk>atom x \<sharp> V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"
3187
b3d97424b130 added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de>
parents: 3186
diff changeset
    65
|  ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $$ M) \<longrightarrow>\<^isub>\<beta> (V $$ M')"
b3d97424b130 added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de>
parents: 3186
diff changeset
    66
|  ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $$ N) \<longrightarrow>\<^isub>\<beta> (M' $$ N)"
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    67
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
equivariance eval
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
nominal_inductive eval
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
done
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    73
(*lemmas [simp] = lt.supp(2)*)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    74
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    75
lemma closedev1: assumes "s \<longrightarrow>\<^isub>\<beta> t"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    76
  shows "supp t <= supp s"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    77
  using assms
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    78
    by (induct, auto simp add: lt.supp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    79
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    80
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
    81
lemma [simp]: "~ ((Lam x M) \<longrightarrow>\<^isub>\<beta> N)"
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    82
by (rule, erule eval.cases, simp_all)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    83
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    84
lemma [simp]: assumes "M \<longrightarrow>\<^isub>\<beta> N" shows "~ isValue M"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    85
using assms
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    86
by (cases, auto)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    87
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    89
inductive
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    90
  eval_star :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    91
  where
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    92
   evs1: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    93
|  evs2: "\<lbrakk>M \<longrightarrow>\<^isub>\<beta> M'; M' \<longrightarrow>\<^isub>\<beta>\<^sup>*  M'' \<rbrakk> \<Longrightarrow> M \<longrightarrow>\<^isub>\<beta>\<^sup>*  M''"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    94
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    95
lemma eval_evs: assumes *: "M \<longrightarrow>\<^isub>\<beta> M'" shows "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M'"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    96
by (rule evs2, rule *, rule evs1)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    97
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    98
lemma eval_trans[trans]:
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    99
  assumes "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   100
      and "M2  \<longrightarrow>\<^isub>\<beta>\<^sup>*  M3"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   101
  shows "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   102
  using assms
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   103
  by (induct, auto intro: evs2)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   104
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   105
lemma evs3[rule_format]: assumes "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   106
  shows "M2  \<longrightarrow>\<^isub>\<beta> M3 \<longrightarrow> M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   107
  using assms
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   108
    by (induct, auto intro: eval_evs evs2)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   109
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   110
equivariance eval_star
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   111
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   112
lemma evbeta':
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   113
  fixes x :: name
2998
f0fab367453a Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2984
diff changeset
   114
  assumes "isValue V" and "atom x\<sharp>V" and "N = (M[x ::= V])"
3187
b3d97424b130 added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de>
parents: 3186
diff changeset
   115
  shows "((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
2861
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   116
  using assms by simp (rule evs2, rule evbeta, simp_all add: evs1)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   117
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   118
end
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   119
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   120
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   121