Nominal/Ex/Lambda.thy
author Christian Urban <urbanc@in.tum.de>
Sat, 17 Dec 2011 17:08:47 +0000
branchNominal2-Isabelle2011-1
changeset 3071 11f6a561eb4b
parent 2995 6d2859aeebba
permissions -rw-r--r--
cleaned examples for stable branch
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
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
     2
imports 
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
     3
  "../Nominal2"
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
     4
  "~~/src/HOL/Library/Monad_Syntax"
1594
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
begin
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
2885
1264f2a21ea9 some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
parents: 2868
diff changeset
     7
1594
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
atom_decl name
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    10
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
    11
  Var "name"
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    12
| App "lam" "lam"
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
    13
| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2425
diff changeset
    14
2868
2b8e387d2dfc got rid of the boolean flag in the raw_equivariance function
Christian Urban <urbanc@in.tum.de>
parents: 2860
diff changeset
    15
2951
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    16
section {* Simple examples from Norrish 2004 *}
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    17
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    18
nominal_primrec 
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    19
  is_app :: "lam \<Rightarrow> bool"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    20
where
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    21
  "is_app (Var x) = False"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    22
| "is_app (App t1 t2) = True"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    23
| "is_app (Lam [x]. t) = False"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    24
apply(simp add: eqvt_def is_app_graph_def)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    25
apply (rule, perm_simp, rule)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    26
apply(rule TrueI)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    27
apply(rule_tac y="x" in lam.exhaust)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    28
apply(auto)[3]
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    29
apply(all_trivials)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    30
done
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    31
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
    32
termination (eqvt) by lexicographic_order
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
    33
2974
b95a2065aa10 generated the partial eqvt-theorem for functions
Christian Urban <urbanc@in.tum.de>
parents: 2973
diff changeset
    34
thm is_app_def
2975
c62e26830420 preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
Christian Urban <urbanc@in.tum.de>
parents: 2974
diff changeset
    35
thm is_app.eqvt
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
    36
2975
c62e26830420 preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
Christian Urban <urbanc@in.tum.de>
parents: 2974
diff changeset
    37
thm eqvts
2951
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    38
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    39
nominal_primrec 
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    40
  rator :: "lam \<Rightarrow> lam option"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    41
where
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    42
  "rator (Var x) = None"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    43
| "rator (App t1 t2) = Some t1"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    44
| "rator (Lam [x]. t) = None"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    45
apply(simp add: eqvt_def rator_graph_def)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    46
apply (rule, perm_simp, rule)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    47
apply(rule TrueI)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    48
apply(rule_tac y="x" in lam.exhaust)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    49
apply(auto)[3]
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    50
apply(simp_all)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    51
done
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    52
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
    53
termination (eqvt) by lexicographic_order
2951
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    54
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    55
nominal_primrec 
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    56
  rand :: "lam \<Rightarrow> lam option"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    57
where
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    58
  "rand (Var x) = None"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    59
| "rand (App t1 t2) = Some t2"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    60
| "rand (Lam [x]. t) = None"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    61
apply(simp add: eqvt_def rand_graph_def)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    62
apply (rule, perm_simp, rule)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    63
apply(rule TrueI)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    64
apply(rule_tac y="x" in lam.exhaust)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    65
apply(auto)[3]
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    66
apply(simp_all)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    67
done
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    68
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
    69
termination (eqvt) by lexicographic_order
2951
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    70
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    71
nominal_primrec 
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    72
  is_eta_nf :: "lam \<Rightarrow> bool"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    73
where
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    74
  "is_eta_nf (Var x) = True"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    75
| "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    76
| "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> 
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    77
                             ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    78
apply(simp add: eqvt_def is_eta_nf_graph_def)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    79
apply (rule, perm_simp, rule)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    80
apply(rule TrueI)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    81
apply(rule_tac y="x" in lam.exhaust)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    82
apply(auto)[3]
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    83
apply(simp_all)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    84
apply(erule_tac c="()" in Abs_lst1_fcb2')
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    85
apply(simp_all add: pure_fresh fresh_star_def)[3]
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    86
apply(simp add: eqvt_at_def conj_eqvt)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    87
apply(perm_simp)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    88
apply(rule refl)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    89
apply(simp add: eqvt_at_def conj_eqvt)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    90
apply(perm_simp)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    91
apply(rule refl)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    92
done
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    93
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
    94
termination (eqvt) by lexicographic_order
2951
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    95
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    96
nominal_datatype path = Left | Right | In
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    97
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    98
section {* Paths to a free variables *} 
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    99
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   100
instance path :: pure
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   101
apply(default)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   102
apply(induct_tac "x::path" rule: path.induct)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   103
apply(simp_all)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   104
done
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   105
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   106
nominal_primrec 
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   107
  var_pos :: "name \<Rightarrow> lam \<Rightarrow> (path list) set"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   108
where
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   109
  "var_pos y (Var x) = (if y = x then {[]} else {})"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   110
| "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   111
| "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   112
apply(simp add: eqvt_def var_pos_graph_def)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   113
apply (rule, perm_simp, rule)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   114
apply(rule TrueI)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   115
apply(case_tac x)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   116
apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   117
apply(auto simp add: fresh_star_def)[3]
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   118
apply(simp_all)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   119
apply(erule conjE)+
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   120
apply(erule_tac Abs_lst1_fcb2)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   121
apply(simp add: pure_fresh)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   122
apply(simp add: fresh_star_def)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   123
apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   124
apply(perm_simp)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   125
apply(rule refl)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   126
apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   127
apply(perm_simp)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   128
apply(rule refl)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   129
done
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   130
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   131
termination (eqvt) by lexicographic_order
2951
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   132
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   133
lemma var_pos1:
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   134
  assumes "atom y \<notin> supp t"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   135
  shows "var_pos y t = {}"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   136
using assms
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   137
apply(induct t rule: var_pos.induct)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   138
apply(simp_all add: lam.supp supp_at_base fresh_at_base)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   139
done
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   140
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   141
lemma var_pos2:
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   142
  shows "var_pos y (Lam [y].t) = {}"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   143
apply(rule var_pos1)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   144
apply(simp add: lam.supp)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   145
done
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   146
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   147
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   148
text {* strange substitution operation *}
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   149
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   150
nominal_primrec
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   151
  subst' :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::== _]" [90, 90, 90] 90)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   152
where
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   153
  "(Var x)[y ::== s] = (if x = y then s else (Var x))"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   154
| "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   155
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])"
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   156
  apply(simp add: eqvt_def subst'_graph_def)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   157
  apply (rule, perm_simp, rule)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   158
  apply(rule TrueI)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   159
  apply(case_tac x)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   160
  apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   161
  apply(auto simp add: fresh_star_def)[3]
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   162
  apply(simp_all)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   163
  apply(erule conjE)+
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   164
  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   165
  apply(simp_all add: Abs_fresh_iff)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   166
  apply(simp add: fresh_star_def fresh_Pair)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   167
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   168
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   169
done
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   170
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   171
termination (eqvt) by lexicographic_order
2951
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   172
d75b3d8529e7 added some relatively simple examples from paper by Norrish
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
   173
2868
2b8e387d2dfc got rid of the boolean flag in the raw_equivariance function
Christian Urban <urbanc@in.tum.de>
parents: 2860
diff changeset
   174
section {* free name function *}
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   175
2860
25a7f421a3ba added a test that every function must be of pt-sort
Christian Urban <urbanc@in.tum.de>
parents: 2858
diff changeset
   176
text {* first returns an atom list *}
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   177
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   178
nominal_primrec 
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   179
  frees_lst :: "lam \<Rightarrow> atom list"
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   180
where
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   181
  "frees_lst (Var x) = [atom x]"
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   182
| "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   183
| "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
2868
2b8e387d2dfc got rid of the boolean flag in the raw_equivariance function
Christian Urban <urbanc@in.tum.de>
parents: 2860
diff changeset
   184
  unfolding eqvt_def
2b8e387d2dfc got rid of the boolean flag in the raw_equivariance function
Christian Urban <urbanc@in.tum.de>
parents: 2860
diff changeset
   185
  unfolding frees_lst_graph_def
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   186
  apply (rule, perm_simp, rule)
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   187
apply(rule TrueI)
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   188
apply(rule_tac y="x" in lam.exhaust)
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   189
apply(auto)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   190
apply (erule_tac c="()" in Abs_lst1_fcb2)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   191
apply(simp add: supp_removeAll fresh_def)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   192
apply(simp add: fresh_star_def fresh_Unit)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   193
apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   194
apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   195
done
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   196
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   197
termination (eqvt) by lexicographic_order
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   198
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   199
text {* a small test lemma *}
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   200
lemma shows "supp t = set (frees_lst t)"
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   201
  by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base)
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   202
2860
25a7f421a3ba added a test that every function must be of pt-sort
Christian Urban <urbanc@in.tum.de>
parents: 2858
diff changeset
   203
text {* second returns an atom set - therefore needs an invariant *}
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   204
2821
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
   205
nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
   206
  frees_set :: "lam \<Rightarrow> atom set"
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
   207
where
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
   208
  "frees_set (Var x) = {atom x}"
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
   209
| "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
   210
| "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
2845
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   211
  apply(simp add: eqvt_def frees_set_graph_def)
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   212
  apply(rule, perm_simp, rule)
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   213
  apply(erule frees_set_graph.induct)
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   214
  apply(auto)[9]
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   215
  apply(rule_tac y="x" in lam.exhaust)
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   216
  apply(auto)[3]
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   217
  apply(simp)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   218
  apply(erule_tac c="()" in Abs_lst1_fcb2)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   219
  apply(simp add: fresh_minus_atom_set)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   220
  apply(simp add: fresh_star_def fresh_Unit)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   221
  apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   222
  apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
2845
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   223
  done
2821
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
   224
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   225
termination (eqvt) 
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   226
  by lexicographic_order
2821
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
   227
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   228
lemma "frees_set t = supp t"
2845
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   229
  by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base)
2821
c7d4bd9e89e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
parents: 2819
diff changeset
   230
2868
2b8e387d2dfc got rid of the boolean flag in the raw_equivariance function
Christian Urban <urbanc@in.tum.de>
parents: 2860
diff changeset
   231
section {* height function *}
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2425
diff changeset
   232
2666
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   233
nominal_primrec
2678
494b859bfc16 defined height as a function that returns an integer
Christian Urban <urbanc@in.tum.de>
parents: 2675
diff changeset
   234
  height :: "lam \<Rightarrow> int"
2666
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   235
where
2678
494b859bfc16 defined height as a function that returns an integer
Christian Urban <urbanc@in.tum.de>
parents: 2675
diff changeset
   236
  "height (Var x) = 1"
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   237
| "height (App t1 t2) = max (height t1) (height t2) + 1"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   238
| "height (Lam [x].t) = height t + 1"
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   239
  apply(simp add: eqvt_def height_graph_def)
2791
5d0875b7ed3e Simple eqvt proofs with perm_simps for clarity
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2789
diff changeset
   240
  apply (rule, perm_simp, rule)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   241
  apply(rule TrueI)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   242
  apply(rule_tac y="x" in lam.exhaust)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   243
  apply(auto)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   244
  apply (erule_tac c="()" in Abs_lst1_fcb2)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   245
  apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   246
  done
2666
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   247
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   248
termination (eqvt)
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   249
  by lexicographic_order
2666
324a5d1289a3 added a few examples of functions to Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2664
diff changeset
   250
  
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2685
diff changeset
   251
thm height.simps
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2685
diff changeset
   252
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   253
  
2868
2b8e387d2dfc got rid of the boolean flag in the raw_equivariance function
Christian Urban <urbanc@in.tum.de>
parents: 2860
diff changeset
   254
section {* capture-avoiding substitution *}
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   255
2675
68ccf847507d defined properly substitution
Christian Urban <urbanc@in.tum.de>
parents: 2669
diff changeset
   256
nominal_primrec
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   257
  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
2675
68ccf847507d defined properly substitution
Christian Urban <urbanc@in.tum.de>
parents: 2669
diff changeset
   258
where
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   259
  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   260
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   261
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
2791
5d0875b7ed3e Simple eqvt proofs with perm_simps for clarity
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2789
diff changeset
   262
  unfolding eqvt_def subst_graph_def
5d0875b7ed3e Simple eqvt proofs with perm_simps for clarity
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2789
diff changeset
   263
  apply (rule, perm_simp, rule)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   264
  apply(rule TrueI)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   265
  apply(auto simp add: lam.distinct lam.eq_iff)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   266
  apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   267
  apply(blast)+
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   268
  apply(simp_all add: fresh_star_def fresh_Pair_elim)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   269
  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   270
  apply(simp_all add: Abs_fresh_iff)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   271
  apply(simp add: fresh_star_def fresh_Pair)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   272
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   273
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
2675
68ccf847507d defined properly substitution
Christian Urban <urbanc@in.tum.de>
parents: 2669
diff changeset
   274
done
68ccf847507d defined properly substitution
Christian Urban <urbanc@in.tum.de>
parents: 2669
diff changeset
   275
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   276
termination (eqvt)
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   277
  by lexicographic_order
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   278
2975
c62e26830420 preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
Christian Urban <urbanc@in.tum.de>
parents: 2974
diff changeset
   279
thm subst.eqvt
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   280
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   281
lemma forget:
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   282
  shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
2845
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   283
  by (nominal_induct t avoiding: x s rule: lam.strong_induct)
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   284
     (auto simp add: lam.fresh fresh_at_base)
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   285
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   286
text {* same lemma but with subst.induction *}
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   287
lemma forget2:
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   288
  shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
2845
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   289
  by (induct t x s rule: subst.induct)
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   290
     (auto simp add: lam.fresh fresh_at_base fresh_Pair)
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   291
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   292
lemma fresh_fact:
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   293
  fixes z::"name"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   294
  assumes a: "atom z \<sharp> s"
2845
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   295
      and b: "z = y \<or> atom z \<sharp> t"
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   296
  shows "atom z \<sharp> t[y ::= s]"
2845
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   297
  using a b
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   298
  by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   299
      (auto simp add: lam.fresh fresh_at_base)
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   300
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   301
lemma substitution_lemma:  
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   302
  assumes a: "x \<noteq> y" "atom x \<sharp> u"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   303
  shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   304
using a 
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   305
by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   306
   (auto simp add: fresh_fact forget)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   307
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   308
lemma subst_rename: 
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   309
  assumes a: "atom y \<sharp> t"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   310
  shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   311
using a 
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   312
apply (nominal_induct t avoiding: x y s rule: lam.strong_induct)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   313
apply (auto simp add: lam.fresh fresh_at_base)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   314
done
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   315
2767
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   316
lemma height_ge_one:
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   317
  shows "1 \<le> (height e)"
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   318
by (induct e rule: lam.induct) (simp_all)
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   319
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   320
theorem height_subst:
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   321
  shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   322
proof (nominal_induct e avoiding: x e' rule: lam.strong_induct)
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   323
  case (Var y)
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   324
  have "1 \<le> height e'" by (rule height_ge_one)
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   325
  then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   326
next
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   327
  case (Lam y e1)
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   328
  hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   329
  moreover
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   330
  have vc: "atom y\<sharp>x" "atom y\<sharp>e'" by fact+ (* usual variable convention *)
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   331
  ultimately show "height ((Lam [y]. e1)[x::=e']) \<le> height (Lam [y]. e1) - 1 + height e'" by simp
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   332
next
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   333
  case (App e1 e2)
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   334
  hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')"
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   335
    and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by simp_all
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   336
  then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'"  by simp
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   337
qed
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   338
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   339
subsection {* single-step beta-reduction *}
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   340
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   341
inductive 
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   342
  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   343
where
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   344
  b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   345
| b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   346
| b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   347
| b4[intro]: "atom x \<sharp> s \<Longrightarrow> App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   348
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   349
equivariance beta
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   350
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   351
nominal_inductive beta
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   352
  avoids b4: "x"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   353
  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   354
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   355
text {* One-Reduction *}
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   356
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   357
inductive 
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   358
  One :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>1 _" [80,80] 80)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   359
where
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   360
  o1[intro]: "Var x \<longrightarrow>1 Var x"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   361
| o2[intro]: "\<lbrakk>t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>1 App t2 s2"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   362
| o3[intro]: "t1 \<longrightarrow>1 t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>1 Lam [x].t2"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   363
| o4[intro]: "\<lbrakk>atom x \<sharp> (s1, s2); t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   364
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   365
equivariance One
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   366
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   367
nominal_inductive One 
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   368
  avoids o3: "x"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   369
      |  o4: "x"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   370
  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   371
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   372
lemma One_refl:
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   373
  shows "t \<longrightarrow>1 t"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   374
by (nominal_induct t rule: lam.strong_induct) (auto)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   375
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   376
lemma One_subst: 
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   377
  assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   378
  shows "t1[x ::= s1] \<longrightarrow>1 t2[x ::= s2]" 
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   379
using a 
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   380
apply(nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   381
apply(auto simp add: substitution_lemma fresh_at_base fresh_fact fresh_Pair)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   382
done
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   383
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   384
lemma better_o4_intro:
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   385
  assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   386
  shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]"
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   387
proof -
2685
1df873b63cb2 added obtain_fresh lemma; tuned Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2683
diff changeset
   388
  obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" by (rule obtain_fresh)
2683
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   389
  have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   390
    by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   391
  also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt)
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   392
  also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric])
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   393
  finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   394
qed
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   395
42c0d011a177 ported some of the old proofs to serve as testcases
Christian Urban <urbanc@in.tum.de>
parents: 2678
diff changeset
   396
section {* Locally Nameless Terms *}
2678
494b859bfc16 defined height as a function that returns an integer
Christian Urban <urbanc@in.tum.de>
parents: 2675
diff changeset
   397
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
   398
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
   399
  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
   400
| 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
   401
| 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
   402
| 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
   403
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
   404
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
   405
  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
   406
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
   407
  "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
   408
| "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
   409
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   410
lemma supp_lookup:
2824
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   411
  shows "supp (lookup xs n x) \<subseteq> {atom x}"
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   412
  apply(induct arbitrary: n rule: lookup.induct)
2824
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   413
  apply(simp add: ln.supp supp_at_base)
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   414
  apply(simp add: ln.supp pure_supp)
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   415
  done
2824
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   416
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   417
lemma supp_lookup_in:
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   418
  shows "x \<in> set xs \<Longrightarrow> supp (lookup xs n x) = {}"
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   419
  by (induct arbitrary: n rule: lookup.induct)(auto simp add: ln.supp pure_supp)
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   420
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   421
lemma supp_lookup_notin:
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   422
  shows "x \<notin> set xs \<Longrightarrow> supp (lookup xs n x) = {atom x}"
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   423
  by (induct arbitrary: n rule: lookup.induct) (auto simp add: ln.supp pure_supp supp_at_base)
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   424
2829
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   425
lemma supp_lookup_fresh:
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   426
  shows "atom ` set xs \<sharp>* lookup xs n x"
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   427
  by (case_tac "x \<in> set xs") (auto simp add: fresh_star_def fresh_def supp_lookup_in supp_lookup_notin)
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   428
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   429
lemma lookup_eqvt[eqvt]:
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
   430
  shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
2767
94f6f70e3067 New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2765
diff changeset
   431
  by (induct xs arbitrary: n) (simp_all add: permute_pure)
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
   432
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   433
text {* Function that translates lambda-terms into locally nameless terms *}
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   434
2826
Christian Urban <urbanc@in.tum.de>
parents: 2825
diff changeset
   435
nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
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
   436
  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
   437
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
   438
  "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
   439
| "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
2685
1df873b63cb2 added obtain_fresh lemma; tuned Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2683
diff changeset
   440
| "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
2829
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   441
  apply (simp add: eqvt_def trans_graph_def)
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   442
  apply (rule, perm_simp, rule)
2824
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   443
  apply (erule trans_graph.induct)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   444
  apply (auto simp add: ln.fresh)[3]
2829
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   445
  apply (simp add: supp_lookup_fresh)
2824
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   446
  apply (simp add: fresh_star_def ln.fresh)
44d937e8ae78 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2822
diff changeset
   447
  apply (simp add: ln.fresh fresh_star_def)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   448
  apply(auto)[1]
2829
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   449
  apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   450
  apply (auto simp add: fresh_star_def)[3]
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   451
  apply(simp_all)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   452
  apply(erule conjE)+
2948
b0b2adafb6d2 made the tests go through again
Christian Urban <urbanc@in.tum.de>
parents: 2945
diff changeset
   453
  apply (erule_tac c="xsa" in Abs_lst1_fcb2')
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   454
  apply (simp add: fresh_star_def)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   455
  apply (simp add: fresh_star_def)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   456
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   457
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
2829
0acb0b8f4106 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2828
diff changeset
   458
  done
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
   459
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   460
termination (eqvt)
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   461
  by lexicographic_order
2827
394664816e24 defined the "count-bound-variables-occurences" function which has an accumulator like trans
Christian Urban <urbanc@in.tum.de>
parents: 2826
diff changeset
   462
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   463
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   464
text {* count the occurences of lambdas in a term *}
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   465
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   466
nominal_primrec
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   467
  cntlams :: "lam  \<Rightarrow> nat"
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   468
where
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   469
  "cntlams (Var x) = 0"
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   470
| "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   471
| "cntlams (Lam [x]. t) = Suc (cntlams t)"
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   472
  apply(simp add: eqvt_def cntlams_graph_def)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   473
  apply(rule, perm_simp, rule)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   474
  apply(rule TrueI)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   475
  apply(rule_tac y="x" in lam.exhaust)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   476
  apply(auto)[3]
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   477
  apply(all_trivials)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   478
  apply(simp)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   479
  apply(simp)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   480
  apply(erule_tac c="()" in Abs_lst1_fcb2')
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   481
  apply(simp add: pure_fresh)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   482
  apply(simp add: fresh_star_def pure_fresh)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   483
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   484
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   485
  done
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   486
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   487
termination (eqvt)
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   488
  by lexicographic_order
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   489
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   490
2860
25a7f421a3ba added a test that every function must be of pt-sort
Christian Urban <urbanc@in.tum.de>
parents: 2858
diff changeset
   491
text {* count the bound-variable occurences in a lambda-term *}
2827
394664816e24 defined the "count-bound-variables-occurences" function which has an accumulator like trans
Christian Urban <urbanc@in.tum.de>
parents: 2826
diff changeset
   492
2828
81276d5c7438 cbvs can be easily defined without an invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2827
diff changeset
   493
nominal_primrec
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   494
  cntbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
2827
394664816e24 defined the "count-bound-variables-occurences" function which has an accumulator like trans
Christian Urban <urbanc@in.tum.de>
parents: 2826
diff changeset
   495
where
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   496
  "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   497
| "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   498
| "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   499
  apply(simp add: eqvt_def cntbvs_graph_def)
2828
81276d5c7438 cbvs can be easily defined without an invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2827
diff changeset
   500
  apply(rule, perm_simp, rule)
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   501
  apply(rule TrueI)
2828
81276d5c7438 cbvs can be easily defined without an invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2827
diff changeset
   502
  apply(case_tac x)
81276d5c7438 cbvs can be easily defined without an invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2827
diff changeset
   503
  apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   504
  apply(auto simp add: fresh_star_def)[3]
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   505
  apply(all_trivials)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   506
  apply(simp)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   507
  apply(simp)
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   508
  apply(simp)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   509
  apply(erule conjE)
2912
3c363a5070a5 copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom
Christian Urban <urbanc@in.tum.de>
parents: 2902
diff changeset
   510
  apply(erule Abs_lst1_fcb2')
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   511
  apply(simp add: pure_fresh fresh_star_def)
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   512
  apply(simp add: fresh_star_def)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   513
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   514
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
2828
81276d5c7438 cbvs can be easily defined without an invariant
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2827
diff changeset
   515
  done
2827
394664816e24 defined the "count-bound-variables-occurences" function which has an accumulator like trans
Christian Urban <urbanc@in.tum.de>
parents: 2826
diff changeset
   516
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   517
termination (eqvt)
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   518
  by lexicographic_order
2827
394664816e24 defined the "count-bound-variables-occurences" function which has an accumulator like trans
Christian Urban <urbanc@in.tum.de>
parents: 2826
diff changeset
   519
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   520
section {* De Bruijn Terms *}
2827
394664816e24 defined the "count-bound-variables-occurences" function which has an accumulator like trans
Christian Urban <urbanc@in.tum.de>
parents: 2826
diff changeset
   521
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
   522
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
   523
  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
   524
| 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
   525
| 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
   526
2792
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   527
instance db :: pure
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   528
  apply default
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   529
  apply (induct_tac x rule: db.induct)
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   530
  apply (simp_all add: permute_pure)
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   531
  done
2795
929bd2dd1ab2 DeBruijn translation in a simplifier friendly way
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2794
diff changeset
   532
929bd2dd1ab2 DeBruijn translation in a simplifier friendly way
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2794
diff changeset
   533
lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"
929bd2dd1ab2 DeBruijn translation in a simplifier friendly way
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2794
diff changeset
   534
  unfolding fresh_def supp_set[symmetric]
2845
a99f488a96bb Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2843
diff changeset
   535
  by (induct xs) (auto simp add: supp_of_finite_insert supp_at_base supp_set_empty)
2795
929bd2dd1ab2 DeBruijn translation in a simplifier friendly way
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2794
diff changeset
   536
2800
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   537
fun
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   538
  vindex :: "name list \<Rightarrow> name \<Rightarrow> nat \<Rightarrow> db option" 
2792
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   539
where
2800
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   540
  "vindex [] v n = None"
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   541
| "vindex (h # t) v n = (if v = h then (Some (DBVar n)) else (vindex t v (Suc n)))"
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   542
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   543
lemma vindex_eqvt[eqvt]:
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   544
  "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)"
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   545
  by (induct l arbitrary: n) (simp_all add: permute_pure)
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   546
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   547
nominal_primrec
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   548
  transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option"
2800
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   549
where
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   550
  "transdb (Var x) l = vindex l x 0"
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   551
| "transdb (App t1 t2) xs = 
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2948
diff changeset
   552
      Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
2942
fac8895b109a Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2941
diff changeset
   553
| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   554
  unfolding eqvt_def transdb_graph_def
2792
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   555
  apply (rule, perm_simp, rule)
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   556
  apply(rule TrueI)
2792
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   557
  apply (case_tac x)
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   558
  apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   559
  apply (auto simp add: fresh_star_def fresh_at_list)[3]
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   560
  apply(simp_all)
2942
fac8895b109a Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2941
diff changeset
   561
  apply(elim conjE)
2912
3c363a5070a5 copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom
Christian Urban <urbanc@in.tum.de>
parents: 2902
diff changeset
   562
  apply (erule_tac c="xsa" in Abs_lst1_fcb2')
2902
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   563
  apply (simp add: pure_fresh)
9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Christian Urban <urbanc@in.tum.de>
parents: 2891
diff changeset
   564
  apply(simp add: fresh_star_def fresh_at_list)
2942
fac8895b109a Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2941
diff changeset
   565
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+
2792
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   566
  done
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   567
2973
d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
parents: 2972
diff changeset
   568
termination (eqvt)
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   569
  by lexicographic_order
2792
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   570
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   571
lemma transdb_eqvt[eqvt]:
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   572
  "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)"
2942
fac8895b109a Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2941
diff changeset
   573
  apply (nominal_induct t avoiding: l rule: lam.strong_induct)
2800
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   574
  apply (simp add: vindex_eqvt)
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   575
  apply (simp_all add: permute_pure)
2797
6750964a69bf equivariance of db_trans
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2796
diff changeset
   576
  apply (simp add: fresh_at_list)
2822
23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
parents: 2821
diff changeset
   577
  apply (subst transdb.simps)
2797
6750964a69bf equivariance of db_trans
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2796
diff changeset
   578
  apply (simp add: fresh_at_list[symmetric])
2800
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   579
  apply (drule_tac x="name # l" in meta_spec)
6e518b436740 DB translation using index; easier to reason about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2799
diff changeset
   580
  apply auto
2797
6750964a69bf equivariance of db_trans
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2796
diff changeset
   581
  done
6750964a69bf equivariance of db_trans
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2796
diff changeset
   582
2792
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   583
lemma db_trans_test:
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   584
  assumes a: "y \<noteq> x"
2858
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   585
  shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = 
de6b601c8d3d added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de>
parents: 2852
diff changeset
   586
  Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
2795
929bd2dd1ab2 DeBruijn translation in a simplifier friendly way
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2794
diff changeset
   587
  using a by simp
2792
c4ed08a7454a Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2791
diff changeset
   588
2841
f8d660de0cf7 Eval can be defined with additional freshness
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2840
diff changeset
   589
lemma supp_subst:
2972
84afb941df53 moved eqvt for Option.map
Christian Urban <urbanc@in.tum.de>
parents: 2951
diff changeset
   590
  shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s"
84afb941df53 moved eqvt for Option.map
Christian Urban <urbanc@in.tum.de>
parents: 2951
diff changeset
   591
  by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)
2841
f8d660de0cf7 Eval can be defined with additional freshness
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2840
diff changeset
   592
f8d660de0cf7 Eval can be defined with additional freshness
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2840
diff changeset
   593
lemma var_fresh_subst:
f8d660de0cf7 Eval can be defined with additional freshness
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2840
diff changeset
   594
  "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])"
f8d660de0cf7 Eval can be defined with additional freshness
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2840
diff changeset
   595
  by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base)
f8d660de0cf7 Eval can be defined with additional freshness
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2840
diff changeset
   596
1594
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   597
end
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   598
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   599
892fcdb96c96 Move LamEx out of Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   600