Nominal/Ex/Lambda.thy
author Christian Urban <urbanc@in.tum.de>
Tue, 18 Jan 2011 11:02:57 +0100
changeset 2669 1d1772a89026
parent 2667 e3f8673085b1
child 2675 68ccf847507d
permissions -rw-r--r--
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1797
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
     1
theory Lambda
2454
9ffee4eb1ae1 renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents: 2442
diff changeset
     2
imports "../Nominal2" 
1594
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
begin
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
atom_decl name
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
     7
nominal_datatype lam =
1800
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1797
diff changeset
     8
  Var "name"
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
     9
| App "lam" "lam"
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    10
| Lam x::"name" l::"lam"  bind x in l
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2425
diff changeset
    11
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    12
thm lam.distinct
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    13
thm lam.induct
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2559
diff changeset
    14
thm lam.exhaust lam.strong_exhaust
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    15
thm lam.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    16
thm lam.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    17
thm lam.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    18
thm lam.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    19
thm lam.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    20
thm lam.size_eqvt
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2425
diff changeset
    21
2666
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    22
nominal_primrec
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    23
  depth :: "lam \<Rightarrow> nat"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    24
where
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    25
  "depth (Var x) = 1"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    26
| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    27
| "depth (Lam x t) = (depth t) + 1"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    28
apply(rule_tac y="x" in lam.exhaust)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    29
apply(simp_all)[3]
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    30
apply(simp_all only: lam.distinct)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    31
apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    32
apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    33
apply(subst (asm) Abs_eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    34
apply(erule exE)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    35
apply(simp add: alphas)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    36
apply(clarify)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    37
apply(rule trans)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    38
apply(rule_tac p="p" in supp_perm_eq[symmetric])
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    39
apply(simp add: pure_supp)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    40
apply(simp add: fresh_star_def)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    41
apply(simp add: eqvt_at_def)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    42
done
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    43
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    44
termination
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    45
  apply(relation "measure size")
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    46
  apply(simp_all add: lam.size)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    47
  done
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    48
  
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    49
lemma removeAll_eqvt[eqvt]:
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    50
  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    51
by (induct xs) (auto)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    52
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    53
lemma supp_removeAll:
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    54
  fixes x::"atom"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    55
  shows "supp (removeAll x xs) = (supp xs - {x})"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    56
apply(induct xs)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    57
apply(simp_all add: supp_Nil supp_Cons)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    58
apply(rule conjI)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    59
apply(rule impI)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    60
apply(simp add: supp_atom)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    61
apply(rule impI)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    62
apply(simp add: supp_atom)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    63
apply(blast)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    64
done
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    65
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    66
nominal_primrec 
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    67
  frees_lst :: "lam \<Rightarrow> atom list"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    68
where
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    69
  "frees_lst (Var x) = [atom x]"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    70
| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    71
| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    72
apply(rule_tac y="x" in lam.exhaust)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    73
apply(simp_all)[3]
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    74
apply(simp_all only: lam.distinct)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    75
apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    76
apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    77
apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    78
apply(simp add: Abs_eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    79
apply(erule exE)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    80
apply(simp add: alphas)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    81
apply(simp add: atom_eqvt)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    82
apply(clarify)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    83
apply(rule trans)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    84
apply(rule_tac p="p" in supp_perm_eq[symmetric])
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    85
apply(simp (no_asm) add: supp_removeAll)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    86
apply(drule supp_eqvt_at)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    87
apply(simp add: finite_supp)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    88
apply(auto simp add: fresh_star_def)[1]
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    89
unfolding eqvt_at_def
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    90
apply(simp only: removeAll_eqvt atom_eqvt)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    91
done
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    92
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    93
termination
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    94
  apply(relation "measure size")
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    95
  apply(simp_all add: lam.size)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    96
  done
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    97
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    98
(* a small lemma *)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
    99
lemma
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   100
  "supp t = set (frees_lst t)"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   101
apply(induct t rule: lam.induct)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   102
apply(simp_all add: lam.supp supp_at_base)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   103
done
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   104
2669
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   105
nominal_datatype ln = 
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   106
  LNBnd nat
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   107
| LNVar name
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   108
| LNApp ln ln
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   109
| LNLam ln
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   110
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   111
fun
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   112
  lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" 
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   113
where
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   114
  "lookup [] n x = LNVar x"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   115
| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   116
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   117
lemma [eqvt]:
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   118
  shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   119
apply(induct xs arbitrary: n)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   120
apply(simp_all add: permute_pure)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   121
done
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   122
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   123
nominal_primrec
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   124
  trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   125
where
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   126
  "trans (Var x) xs = lookup xs 0 x"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   127
| "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   128
| "atom x \<sharp> xs \<Longrightarrow> trans (Lam x t) xs = LNLam (trans t (x # xs))"
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   129
apply(case_tac x)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   130
apply(simp)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   131
apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   132
apply(simp_all)[3]
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   133
apply(blast)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   134
apply(blast)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   135
apply(simp add: fresh_star_def)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   136
apply(simp_all add: lam.distinct)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   137
apply(simp add: lam.eq_iff)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   138
apply(simp add: lam.eq_iff)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   139
apply(simp add: lam.eq_iff)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   140
apply(simp add: Abs_eq_iff)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   141
apply(erule conjE)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   142
apply(erule exE)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   143
apply(simp add: alphas)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   144
apply(simp add: atom_eqvt)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   145
apply(clarify)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   146
apply(rule trans)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   147
apply(rule_tac p="p" in supp_perm_eq[symmetric])
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   148
apply(simp (no_asm) add: ln.supp)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   149
apply(drule supp_eqvt_at)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   150
apply(simp add: finite_supp)
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   151
oops
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   152
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   153
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   154
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   155
1d1772a89026 the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
parents: 2667
diff changeset
   156
2667
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   157
nominal_datatype db = 
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   158
  DBVar nat
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   159
| DBApp db db
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   160
| DBLam db
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   161
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   162
abbreviation
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   163
  mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   164
where  
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   165
  "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   166
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   167
lemma mbind_eqvt:
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   168
  fixes c::"'a::pt option"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   169
  shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   170
apply(cases c)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   171
apply(simp_all)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   172
apply(perm_simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   173
apply(rule refl)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   174
done
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   175
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   176
lemma mbind_eqvt_raw[eqvt_raw]:
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   177
  shows "(p \<bullet> option_case) \<equiv> option_case"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   178
apply(rule eq_reflection)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   179
apply(rule ext)+
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   180
apply(case_tac xb)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   181
apply(simp_all)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   182
apply(rule_tac p="-p" in permute_boolE)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   183
apply(perm_simp add: permute_minus_cancel)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   184
apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   185
apply(rule_tac p="-p" in permute_boolE)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   186
apply(perm_simp add: permute_minus_cancel)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   187
apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   188
done
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   189
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   190
fun
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   191
  index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option" 
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   192
where
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   193
  "index [] n x = None"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   194
| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   195
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   196
lemma [eqvt]:
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   197
  shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   198
apply(induct xs arbitrary: n)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   199
apply(simp_all add: permute_pure)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   200
done
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   201
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   202
ML {*
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   203
Nominal_Function_Core.trace := true
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   204
*}
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   205
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   206
(*
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   207
inductive
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   208
  trans_graph
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   209
where
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   210
  "trans_graph (Var x, xs) (index xs 0 (atom x) \<guillemotright>= (\<lambda>v. Some (DBVar v)))" 
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   211
| "\<lbrakk>trans_graph (t1, xs) (trans_sum (t1, xs)); 
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   212
    \<And>a. trans_sum (t1, xs) = Some a \<Longrightarrow> trans_graph (t2, xs) (trans_sum (t2, xs))\<rbrakk>
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   213
    \<Longrightarrow> trans_graph (App t1 t2, xs) 
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   214
       (trans_sum (t1, xs) \<guillemotright>= (\<lambda>v. trans_sum (t2, xs) \<guillemotright>= (\<lambda>va. Some (DBApp v va))))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   215
| "trans_graph (t, atom x # xs) (trans_sum (t, atom x # xs)) \<Longrightarrow>
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   216
    trans_graph (Lam x t, xs) (trans_sum (t, atom x # xs) \<guillemotright>= (\<lambda>v. Some (DBLam v)))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   217
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   218
lemma
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   219
  assumes a: "trans_graph x t"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   220
  shows "trans_graph (p \<bullet> x) (p \<bullet> t)"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   221
using a
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   222
apply(induct)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   223
apply(perm_simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   224
apply(rule trans_graph.intros)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   225
apply(perm_simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   226
apply(rule trans_graph.intros)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   227
apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   228
apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   229
defer
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   230
apply(perm_simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   231
apply(rule trans_graph.intros)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   232
apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   233
apply(rotate_tac 3)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   234
apply(drule_tac x="FOO" in meta_spec)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   235
apply(drule meta_mp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   236
prefer 2
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   237
apply(simp)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   238
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   239
equivariance trans_graph
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   240
*)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   241
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   242
(* equivariance fails at the moment
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   243
nominal_primrec
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   244
  trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   245
where
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   246
  "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   247
| "trans (App t1 t2) xs = (trans t1 xs \<guillemotright>= (\<lambda>db1. trans t2 xs \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   248
| "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   249
*)
e3f8673085b1 added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
Christian Urban <urbanc@in.tum.de>
parents: 2666
diff changeset
   250
2666
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   251
nominal_primrec
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   252
  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   253
where
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   254
  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   255
| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   256
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   257
apply(case_tac x)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   258
apply(simp)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   259
apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   260
apply(simp add: lam.eq_iff lam.distinct)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   261
apply(auto)[1]
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   262
apply(simp add: lam.eq_iff lam.distinct)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   263
apply(auto)[1]
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   264
apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   265
apply(simp_all add: lam.distinct)[5]
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   266
apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   267
apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   268
apply(simp add: lam.eq_iff)
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   269
apply(erule conjE)+
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   270
oops
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   271
2654
0f0335d91456 solved subgoals for depth and subst function
Christian Urban <urbanc@in.tum.de>
parents: 2649
diff changeset
   272
1594
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   273
end
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   274
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   275
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   276