LamEx.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Sun, 06 Dec 2009 06:41:52 +0100
changeset 574 06e54c862a39
parent 573 14682786c356
parent 570 6a031829319a
child 582 a082e2d138ab
permissions -rw-r--r--
merge
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
201
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory LamEx
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
imports Nominal QuotMain
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
atom_decl name
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
243
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
     7
thm abs_fresh(1)
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
     8
201
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
nominal_datatype rlam =
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
  rVar "name"
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
| rApp "rlam" "rlam"
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
| rLam "name" "rlam"
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
259
22c199522bef Optimization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 258
diff changeset
    14
print_theorems
201
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
243
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    16
function
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    17
  rfv :: "rlam \<Rightarrow> name set"
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    18
where
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    19
  rfv_var: "rfv (rVar a) = {a}"
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    20
| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)"
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    21
| rfv_lam: "rfv (rLam a t) = (rfv t) - {a}"
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    22
sorry
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    23
247
e83a6e452843 Lemmas about fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 246
diff changeset
    24
termination rfv sorry
243
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    25
271
1b57f99737fe Alpha.induct now lifts automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 270
diff changeset
    26
inductive
246
6da7d538e5e0 changed the order of rfv and reformulated a3 with rfv
Christian Urban <urbanc@in.tum.de>
parents: 245
diff changeset
    27
  alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
6da7d538e5e0 changed the order of rfv and reformulated a3 with rfv
Christian Urban <urbanc@in.tum.de>
parents: 245
diff changeset
    28
where
6da7d538e5e0 changed the order of rfv and reformulated a3 with rfv
Christian Urban <urbanc@in.tum.de>
parents: 245
diff changeset
    29
  a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
6da7d538e5e0 changed the order of rfv and reformulated a3 with rfv
Christian Urban <urbanc@in.tum.de>
parents: 245
diff changeset
    30
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
6da7d538e5e0 changed the order of rfv and reformulated a3 with rfv
Christian Urban <urbanc@in.tum.de>
parents: 245
diff changeset
    31
| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
6da7d538e5e0 changed the order of rfv and reformulated a3 with rfv
Christian Urban <urbanc@in.tum.de>
parents: 245
diff changeset
    32
259
22c199522bef Optimization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 258
diff changeset
    33
print_theorems
22c199522bef Optimization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 258
diff changeset
    34
271
1b57f99737fe Alpha.induct now lifts automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 270
diff changeset
    35
lemma alpha_refl:
286
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    36
  fixes t::"rlam"
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    37
  shows "t \<approx> t"
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    38
  apply(induct t rule: rlam.induct)
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    39
  apply(simp add: a1)
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    40
  apply(simp add: a2)
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    41
  apply(rule a3)
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    42
  apply(subst pt_swap_bij'')
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    43
  apply(rule pt_name_inst)
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    44
  apply(rule at_name_inst)
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    45
  apply(simp)
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    46
  apply(simp)
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    47
  done
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    48
534
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 515
diff changeset
    49
lemma alpha_equivp:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 515
diff changeset
    50
  shows "equivp alpha"
271
1b57f99737fe Alpha.induct now lifts automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 270
diff changeset
    51
sorry
1b57f99737fe Alpha.induct now lifts automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 270
diff changeset
    52
201
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
quotient lam = rlam / alpha
534
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 515
diff changeset
    54
  apply(rule alpha_equivp)
286
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
    55
  done
201
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
203
7384115df9fd added equiv-thm to the quot_info
Christian Urban <urbanc@in.tum.de>
parents: 201
diff changeset
    57
print_quotients
7384115df9fd added equiv-thm to the quot_info
Christian Urban <urbanc@in.tum.de>
parents: 201
diff changeset
    58
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
    59
quotient_def 
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    60
  Var :: "name \<Rightarrow> lam"
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    61
where
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    62
  "Var \<equiv> rVar"
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    63
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
    64
quotient_def 
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    65
  App :: "lam \<Rightarrow> lam \<Rightarrow> lam"
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    66
where
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    67
  "App \<equiv> rApp"
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    68
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
    69
quotient_def 
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    70
  Lam :: "name \<Rightarrow> lam \<Rightarrow> lam"
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    71
where
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
    72
  "Lam \<equiv> rLam"
201
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
218
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 203
diff changeset
    74
thm Var_def
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 203
diff changeset
    75
thm App_def
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 203
diff changeset
    76
thm Lam_def
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 203
diff changeset
    77
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
    78
quotient_def 
243
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    79
  fv :: "lam \<Rightarrow> name set"
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    80
where
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    81
  "fv \<equiv> rfv"
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
    82
570
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    83
ML {*
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    84
local
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    85
   fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    86
   fun pp_list xs = Pretty.list "[" "]" xs
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    87
   fun pp_str s   = Pretty.str s
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    88
   fun pp_qstr s = Pretty.quote (pp_str s)
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    89
   fun pp_int i   = pp_str (string_of_int i)
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    90
   fun pp_sort S = pp_list (map pp_qstr S)
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    91
   fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    92
in
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    93
fun raw_pp_typ (TVar ((a, i), S)) =
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    94
       pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    95
   | raw_pp_typ (TFree (a, S)) =
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    96
       pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    97
   | raw_pp_typ (Type (a, tys)) =
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    98
       pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
    99
end *}
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   100
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   101
ML {*
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   102
PolyML.addPrettyPrinter
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   103
  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   104
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   105
*}
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   106
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   107
typ "name set" 
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   108
typ "name => bool"
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   109
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   110
ML {* @{typ "name set"} *}
6a031829319a added more to IntEx2
Christian Urban <urbanc@in.tum.de>
parents: 567
diff changeset
   111
243
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   112
thm fv_def
22715cab3995 added fv-function
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   113
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   114
(* definition of overloaded permutation function *)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   115
(* for the lifted type lam                       *)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   116
overloading
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   117
  perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   118
begin
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   119
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 267
diff changeset
   120
quotient_def 
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   121
  perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   122
where
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   123
  "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   124
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   125
end
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   126
238
e9cc3a3aa5d1 Tried manually lifting real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 237
diff changeset
   127
(*quotient_def (for lam)
e9cc3a3aa5d1 Tried manually lifting real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 237
diff changeset
   128
  abs_fun_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
e9cc3a3aa5d1 Tried manually lifting real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 237
diff changeset
   129
where
e9cc3a3aa5d1 Tried manually lifting real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 237
diff changeset
   130
  "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"*)
e9cc3a3aa5d1 Tried manually lifting real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 237
diff changeset
   131
e9cc3a3aa5d1 Tried manually lifting real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 237
diff changeset
   132
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   133
thm perm_lam_def
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   134
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   135
(* lemmas that need to lift *)
234
811f17de4031 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 233
diff changeset
   136
lemma pi_var_com:
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   137
  fixes pi::"'x prm"
234
811f17de4031 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 233
diff changeset
   138
  shows "(pi\<bullet>rVar a) \<approx> rVar (pi\<bullet>a)"
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   139
  sorry
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   140
234
811f17de4031 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 233
diff changeset
   141
lemma pi_app_com:
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   142
  fixes pi::"'x prm"
234
811f17de4031 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 233
diff changeset
   143
  shows "(pi\<bullet>rApp t1 t2) \<approx> rApp (pi\<bullet>t1) (pi\<bullet>t2)"
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   144
  sorry
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   145
234
811f17de4031 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 233
diff changeset
   146
lemma pi_lam_com:
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   147
  fixes pi::"'x prm"
234
811f17de4031 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 233
diff changeset
   148
  shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   149
  sorry
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   150
451
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   151
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   152
201
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
lemma real_alpha:
451
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   154
  assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
201
1ac36993cc71 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
  shows "Lam a t = Lam b s"
451
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   156
using a
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   157
unfolding fresh_def supp_def
217
9cc87d02190a First experiments with Lambda
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 203
diff changeset
   158
sorry
9cc87d02190a First experiments with Lambda
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 203
diff changeset
   159
508
fac6069d8e80 Made your version work again with LIST_REL_EQ.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 501
diff changeset
   160
lemma perm_rsp[quotient_rsp]:
286
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
   161
  "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   162
  apply(auto)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   163
  (* this is propably true if some type conditions are imposed ;o) *)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   164
  sorry
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   165
451
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   166
lemma fresh_rsp:
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   167
  "(op = ===> alpha ===> op =) fresh fresh"
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   168
  apply(auto)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   169
  (* this is probably only true if some type conditions are imposed *)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   170
  sorry
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   171
508
fac6069d8e80 Made your version work again with LIST_REL_EQ.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 501
diff changeset
   172
lemma rVar_rsp[quotient_rsp]:
451
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   173
  "(op = ===> alpha) rVar rVar"
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   174
by (auto intro:a1)
234
811f17de4031 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 233
diff changeset
   175
508
fac6069d8e80 Made your version work again with LIST_REL_EQ.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 501
diff changeset
   176
lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
451
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   177
by (auto intro:a2)
234
811f17de4031 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 233
diff changeset
   178
508
fac6069d8e80 Made your version work again with LIST_REL_EQ.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 501
diff changeset
   179
lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
229
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   180
  apply(auto)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   181
  apply(rule a3)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   182
  apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   183
  apply(rule sym)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   184
  apply(rule trans)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   185
  apply(rule pt_name3)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   186
  apply(rule at_ds1[OF at_name_inst])
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   187
  apply(simp add: pt_name1)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   188
  apply(assumption)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   189
  apply(simp add: abs_fresh)
13f985a93dbc fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
parents: 225
diff changeset
   190
  done
217
9cc87d02190a First experiments with Lambda
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 203
diff changeset
   191
508
fac6069d8e80 Made your version work again with LIST_REL_EQ.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 501
diff changeset
   192
lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv"
247
e83a6e452843 Lemmas about fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 246
diff changeset
   193
  sorry
217
9cc87d02190a First experiments with Lambda
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 203
diff changeset
   194
285
8ebdef196fd5 Infrastructure for polymorphic types
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 273
diff changeset
   195
lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
8ebdef196fd5 Infrastructure for polymorphic types
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 273
diff changeset
   196
apply (auto)
8ebdef196fd5 Infrastructure for polymorphic types
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 273
diff changeset
   197
apply (erule alpha.cases)
8ebdef196fd5 Infrastructure for polymorphic types
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 273
diff changeset
   198
apply (simp_all add: rlam.inject alpha_refl)
8ebdef196fd5 Infrastructure for polymorphic types
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 273
diff changeset
   199
done
8ebdef196fd5 Infrastructure for polymorphic types
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 273
diff changeset
   200
217
9cc87d02190a First experiments with Lambda
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 203
diff changeset
   201
ML {* val qty = @{typ "lam"} *}
458
44a70e69ef92 Code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 451
diff changeset
   202
ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *}
271
1b57f99737fe Alpha.induct now lifts automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 270
diff changeset
   203
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   204
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   205
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
508
fac6069d8e80 Made your version work again with LIST_REL_EQ.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 501
diff changeset
   206
ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *}
237
80f1df49b940 More tests in Lam
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 234
diff changeset
   207
376
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   208
lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   209
apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   210
done
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   211
376
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   212
lemma pi_app: "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   213
apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *})
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   214
done
376
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   215
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   216
lemma pi_lam: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   217
apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *})
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   218
done
249
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   219
376
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   220
lemma fv_var: "fv (Var (a\<Colon>name)) = {a}"
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   221
apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *})
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   222
done
376
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   223
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   224
lemma fv_app: "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   225
apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *})
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   226
done
249
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   227
376
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   228
lemma fv_lam: "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   229
apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   230
done
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   231
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   232
lemma a1: "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   233
apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *})
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   234
done
376
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   235
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   236
lemma a2: "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   237
apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *})
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   238
done
376
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   239
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   240
lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   241
apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   242
done
286
Christian Urban <urbanc@in.tum.de>
parents: 285
diff changeset
   243
378
86fba2c4eeef All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 376
diff changeset
   244
lemma alpha_cases: "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
86fba2c4eeef All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 376
diff changeset
   245
     \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
86fba2c4eeef All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 376
diff changeset
   246
     \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   247
    \<Longrightarrow> P"
378
86fba2c4eeef All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 376
diff changeset
   248
apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *})
86fba2c4eeef All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 376
diff changeset
   249
done
86fba2c4eeef All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 376
diff changeset
   250
86fba2c4eeef All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 376
diff changeset
   251
lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   252
     \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   253
     \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   254
        \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   255
    \<Longrightarrow> qxb qx qxa"
378
86fba2c4eeef All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 376
diff changeset
   256
apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *})
86fba2c4eeef All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 376
diff changeset
   257
done
252
e30997c88050 Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 251
diff changeset
   258
376
e99c0334d8bf lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 370
diff changeset
   259
lemma var_inject: "(Var a = Var b) = (a = b)"
370
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   260
apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *})
09e28d4c19aa Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 292
diff changeset
   261
done
285
8ebdef196fd5 Infrastructure for polymorphic types
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 273
diff changeset
   262
451
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   263
lemma lam_induct:" \<lbrakk>\<And>name. P (Var name); \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   264
              \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   265
apply (tactic {* lift_tac_lam @{context} @{thm rlam.induct} 1 *})
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   266
done
586e3dc4afdb Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 445
diff changeset
   267
249
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   268
lemma var_supp:
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   269
  shows "supp (Var a) = ((supp a)::name set)"
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   270
  apply(simp add: supp_def)
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   271
  apply(simp add: pi_var)
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   272
  apply(simp add: var_inject)
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   273
  done
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   274
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   275
lemma var_fresh:
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   276
  fixes a::"name"
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   277
  shows "(a\<sharp>(Var b)) = (a\<sharp>b)"
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   278
  apply(simp add: fresh_def)
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   279
  apply(simp add: var_supp)
7dec34d12328 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de>
parents: 247
diff changeset
   280
  done
247
e83a6e452843 Lemmas about fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 246
diff changeset
   281