Quot/Nominal/Terms.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 05 Feb 2010 15:09:49 +0100
changeset 1073 53350d409473
parent 1058 afedef46d3ab
child 1083 30550327651a
permissions -rw-r--r--
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory Terms
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
     2
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
atom_decl name
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
text {* primrec seems to be genarally faster than fun *}
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
section {*** lets with binding patterns ***}
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    11
datatype rtrm1 =
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    12
  rVr1 "name"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    13
| rAp1 "rtrm1" "rtrm1"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    14
| rLm1 "name" "rtrm1"        --"name is bound in trm1"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    15
| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
and bp =
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
  BUnit
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
| BVr "name"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
| BPr "bp" "bp"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
(* to be given by the user *)
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
    22
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
primrec 
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
  bv1
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
where
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
  "bv1 (BUnit) = {}"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    27
| "bv1 (BVr x) = {atom x}"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
(* needs to be calculated by the package *)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
primrec 
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    32
  rfv_trm1 and rfv_bp
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
where
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    34
  "rfv_trm1 (rVr1 x) = {atom x}"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    35
| "rfv_trm1 (rAp1 t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2)"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    36
| "rfv_trm1 (rLm1 x t) = (rfv_trm1 t) - {atom x}"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    37
| "rfv_trm1 (rLt1 bp t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2 - bv1 bp)"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    38
| "rfv_bp (BUnit) = {}"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    39
| "rfv_bp (BVr x) = {atom x}"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    40
| "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
(* needs to be stated by the package *)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
instantiation 
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    44
  rtrm1 and bp :: pt
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
begin
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
primrec
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    48
  permute_rtrm1 and permute_bp
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
where
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    50
  "permute_rtrm1 pi (rVr1 a) = rVr1 (pi \<bullet> a)"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    51
| "permute_rtrm1 pi (rAp1 t1 t2) = rAp1 (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    52
| "permute_rtrm1 pi (rLm1 a t) = rLm1 (pi \<bullet> a) (permute_rtrm1 pi t)"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    53
| "permute_rtrm1 pi (rLt1 bp t1 t2) = rLt1 (permute_bp pi bp) (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    54
| "permute_bp pi (BUnit) = BUnit"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    55
| "permute_bp pi (BVr a) = BVr (pi \<bullet> a)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    56
| "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    57
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    58
lemma pt_rtrm1_bp_zero:
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    59
  fixes t::rtrm1
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    60
  and   b::bp
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    61
  shows "0 \<bullet> t = t"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    62
  and   "0 \<bullet> b = b"
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    63
apply(induct t and b rule: rtrm1_bp.inducts)
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    64
apply(simp_all)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    65
done
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    66
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    67
lemma pt_rtrm1_bp_plus:
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    68
  fixes t::rtrm1
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    69
  and   b::bp
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    70
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    71
  and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    72
apply(induct t and b rule: rtrm1_bp.inducts)
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    73
apply(simp_all)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    74
done
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    75
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    76
instance
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    77
apply default
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    78
apply(simp_all add: pt_rtrm1_bp_zero pt_rtrm1_bp_plus)
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
    79
done
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
end
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
inductive
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    84
  alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
where
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    86
  a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    87
| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    88
| a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    89
| a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    90
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
    91
lemma alpha1_inj:
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    92
"(rVr1 a \<approx>1 rVr1 b) = (a = b)"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    93
"(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    94
"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s)))"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    95
"(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))))"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    96
apply -
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    97
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    98
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
    99
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   100
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   101
done
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   102
1030
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   103
(* Shouyld we derive it? But bv is given by the user? *)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   104
lemma bv1_eqvt[eqvt]:
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   105
  shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   106
  apply (induct x)
1043
534d4c604f80 fixed proofs that broke because of eqvt
Christian Urban <urbanc@in.tum.de>
parents: 1039
diff changeset
   107
apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
1030
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   108
done
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   109
1031
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   110
lemma rfv_trm1_eqvt[eqvt]:
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   111
  shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   112
  apply (induct t)
1043
534d4c604f80 fixed proofs that broke because of eqvt
Christian Urban <urbanc@in.tum.de>
parents: 1039
diff changeset
   113
  apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
1031
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   114
  done
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   115
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   116
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   117
lemma alpha1_eqvt:
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   118
  shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
1031
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   119
  apply (induct t s rule: alpha1.inducts)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   120
  apply (simp_all add:eqvts alpha1_inj)
1033
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   121
  apply (erule exE)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   122
  apply (rule_tac x="pi \<bullet> pia" in exI)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   123
  apply (simp add: alpha_gen)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   124
  apply(erule conjE)+
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   125
  apply(rule conjI)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   126
  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
1043
534d4c604f80 fixed proofs that broke because of eqvt
Christian Urban <urbanc@in.tum.de>
parents: 1039
diff changeset
   127
  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt rfv_trm1_eqvt)
1033
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   128
  apply(rule conjI)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   129
  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
1043
534d4c604f80 fixed proofs that broke because of eqvt
Christian Urban <urbanc@in.tum.de>
parents: 1039
diff changeset
   130
  apply(simp add: atom_eqvt Diff_eqvt rfv_trm1_eqvt insert_eqvt empty_eqvt)
1033
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   131
  apply(simp add: permute_eqvt[symmetric])
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   132
  apply (erule exE)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   133
  apply (rule_tac x="pi \<bullet> pia" in exI)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   134
  apply (simp add: alpha_gen)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   135
  apply(erule conjE)+
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   136
  apply(rule conjI)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   137
  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
1043
534d4c604f80 fixed proofs that broke because of eqvt
Christian Urban <urbanc@in.tum.de>
parents: 1039
diff changeset
   138
  apply(simp add: rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
1033
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   139
  apply(rule conjI)
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   140
  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
1043
534d4c604f80 fixed proofs that broke because of eqvt
Christian Urban <urbanc@in.tum.de>
parents: 1039
diff changeset
   141
  apply(simp add: atom_eqvt rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
1033
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   142
  apply(simp add: permute_eqvt[symmetric])
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   143
  done
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   145
lemma alpha1_equivp: "equivp alpha1" 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   146
  sorry
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   148
quotient_type trm1 = rtrm1 / alpha1
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
  by (rule alpha1_equivp)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
1028
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   151
quotient_definition
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   152
  "Vr1 :: name \<Rightarrow> trm1"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   153
as
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   154
  "rVr1"
41fc4d3fc764 First experiments in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 976
diff changeset
   155
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   156
quotient_definition
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   157
  "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   158
as
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   159
  "rAp1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   160
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   161
quotient_definition
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   162
  "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   163
as
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   164
  "rLm1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   165
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   166
quotient_definition
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   167
  "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   168
as
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   169
  "rLt1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   170
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   171
quotient_definition
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   172
  "fv_trm1 :: trm1 \<Rightarrow> atom set"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   173
as
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   174
  "rfv_trm1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   175
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   176
lemma alpha_rfv1:
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   177
  shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   178
  apply(induct rule: alpha1.induct)
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   179
  apply(simp_all add: alpha_gen.simps)
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   180
  done
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   181
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   182
lemma [quot_respect]:
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   183
 "(op = ===> alpha1) rVr1 rVr1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   184
 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   185
 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   186
 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   187
apply (auto intro: alpha1.intros)
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   188
apply(rule a3) apply (rule_tac x="0" in exI)
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   189
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   190
apply(rule a4) apply assumption apply (rule_tac x="0" in exI)
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   191
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   192
done
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   193
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   194
lemma [quot_respect]:
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   195
  "(op = ===> alpha1 ===> alpha1) permute permute"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   196
apply auto
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   197
apply (rule alpha1_eqvt)
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   198
apply simp
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   199
done
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   200
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   201
lemma [quot_respect]:
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   202
  "(alpha1 ===> op =) rfv_trm1 rfv_trm1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   203
apply (simp add: alpha_rfv1)
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   204
done
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   205
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   206
lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   207
lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   208
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   209
instantiation trm1 and bp :: pt
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   210
begin
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   211
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   212
quotient_definition
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   213
  "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   214
as
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   215
  "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   216
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   217
instance
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   218
apply default
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   219
apply(induct_tac [!] x rule: trm1_bp_inducts(1))
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   220
apply(simp_all add: permute_rtrm1_permute_bp.simps[quot_lifted])
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   221
done
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   222
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   223
end
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   224
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   225
lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   226
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   227
lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted]
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   228
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   229
lemmas fv_trm1_eqvt = rfv_trm1_eqvt[quot_lifted]
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   230
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   231
lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   232
1031
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   233
lemma lm1_supp_pre:
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   234
  shows "(supp (atom x, t)) supports (Lm1 x t) "
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   235
apply(simp add: supports_def)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   236
apply(fold fresh_def)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   237
apply(simp add: fresh_Pair swap_fresh_fresh)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   238
apply(clarify)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   239
apply(subst swap_at_base_simps(3))
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   240
apply(simp_all add: fresh_atom)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   241
done
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   242
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   243
lemma lt1_supp_pre:
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   244
  shows "(supp (x, t, s)) supports (Lt1 t x s) "
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   245
apply(simp add: supports_def)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   246
apply(fold fresh_def)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   247
apply(simp add: fresh_Pair swap_fresh_fresh)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   248
done
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   249
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   250
lemma bp_supp: "finite (supp (bp :: bp))"
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   251
  apply (induct bp)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   252
  apply(simp_all add: supp_def)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   253
  apply (fold supp_def)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   254
  apply (simp add: supp_at_base)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   255
  apply(simp add: Collect_imp_eq)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   256
  apply(simp add: Collect_neg_eq[symmetric])
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   257
  apply (fold supp_def)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   258
  apply (simp)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   259
  done
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   260
1030
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   261
instance trm1 :: fs
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   262
apply default
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   263
apply(induct_tac x rule: trm1_bp_inducts(1))
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   264
apply(simp_all)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   265
apply(simp add: supp_def alpha1_INJ eqvts)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   266
apply(simp add: supp_def[symmetric] supp_at_base)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   267
apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   268
apply(simp add: Collect_imp_eq Collect_neg_eq)
1031
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   269
apply(rule supports_finite)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   270
apply(rule lm1_supp_pre)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   271
apply(simp add: supp_Pair supp_atom)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   272
apply(rule supports_finite)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   273
apply(rule lt1_supp_pre)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   274
apply(simp add: supp_Pair supp_atom bp_supp)
bcf6e7d20c20 More ingredients in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1030
diff changeset
   275
done
1030
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   276
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   277
lemma supp_fv:
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   278
  shows "supp t = fv_trm1 t"
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   279
apply(induct t rule: trm1_bp_inducts(1))
1030
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   280
apply(simp_all)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   281
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   282
apply(simp only: supp_at_base[simplified supp_def])
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   283
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   284
apply(simp add: Collect_imp_eq Collect_neg_eq)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   285
apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   286
apply(simp add: supp_Abs fv_trm1)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   287
apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   288
apply(simp add: alpha1_INJ)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   289
apply(simp add: Abs_eq_iff)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   290
apply(simp add: alpha_gen.simps)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   291
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   292
apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   293
apply(simp add: supp_Abs fv_trm1)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   294
apply(simp (no_asm) add: supp_def)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   295
apply(simp add: alpha1_INJ)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   296
apply(simp add: Abs_eq_iff)
1033
dce45db16063 Some cleaning and eqvt proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1032
diff changeset
   297
apply(simp add: alpha_gen)
1030
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   298
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   299
apply(simp add: Collect_imp_eq Collect_neg_eq)
07f97267a392 Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1029
diff changeset
   300
done
1029
5f098a0d2daa More in Terms
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1028
diff changeset
   301
1032
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   302
lemma trm1_supp:
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   303
  "supp (Vr1 x) = {atom x}"
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   304
  "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   305
  "supp (Lm1 x t) = (supp t) - {atom x}"
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   306
  "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   307
  by (simp_all only: supp_fv fv_trm1)
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   308
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   309
lemma trm1_induct_strong:
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   310
  assumes "\<And>name b. P b (Vr1 name)"
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   311
  and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   312
  and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   313
  and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   314
  shows   "P a rtrma"
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   315
sorry
1032
135bf399c036 The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1031
diff changeset
   316
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   317
section {*** lets with single assignments ***}
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   318
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   319
datatype trm2 =
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   320
  Vr2 "name"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   321
| Ap2 "trm2" "trm2"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   322
| Lm2 "name" "trm2"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   323
| Lt2 "assign" "trm2"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   324
and assign =
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   325
  As "name" "trm2"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   326
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   327
(* to be given by the user *)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   328
primrec 
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   329
  bv2
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   330
where
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   331
  "bv2 (As x t) = {atom x}"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   332
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   333
(* needs to be calculated by the package *)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   334
primrec
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   335
  fv_trm2 and fv_assign
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   336
where
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   337
  "fv_trm2 (Vr2 x) = {atom x}"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   338
| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   339
| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {atom x}"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   340
| "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   341
| "fv_assign (As x t) = (fv_trm2 t)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   342
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   343
(* needs to be stated by the package *)
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   344
instantiation 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   345
  trm2 and assign :: pt
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   346
begin
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   347
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   348
primrec
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   349
  permute_trm2 and permute_assign
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   350
where
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   351
  "permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   352
| "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   353
| "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   354
| "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   355
| "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   356
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   357
lemma pt_trm2_assign_zero:
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   358
  fixes t::trm2
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   359
  and   b::assign
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   360
  shows "0 \<bullet> t = t"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   361
  and   "0 \<bullet> b = b"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   362
apply(induct t and b rule: trm2_assign.inducts)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   363
apply(simp_all)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   364
done
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   365
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   366
lemma pt_trm2_assign_plus:
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   367
  fixes t::trm2
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   368
  and   b::assign
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   369
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   370
  and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   371
apply(induct t and b rule: trm2_assign.inducts)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   372
apply(simp_all)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   373
done
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   374
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   375
instance
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   376
apply default
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   377
apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   378
done
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   379
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   380
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   381
end
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   382
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   383
inductive
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   384
  alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   385
where
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   386
  a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   387
| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   388
| a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and> 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   389
            (fv_trm2 t - {atom a})\<sharp>* pi \<and> 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   390
            (pi \<bullet> t) \<approx>2 s \<and> 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   391
            (pi \<bullet> a) = b)
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   392
       \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   393
| a4: "\<exists>pi. (
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   394
         fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   395
         (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and>
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   396
         pi \<bullet> t1 = t2       (* \<and> (pi \<bullet> b1 = b2) *)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   397
       ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   398
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   399
lemma alpha2_equivp: "equivp alpha2" 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   400
  sorry
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   401
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   402
quotient_type qtrm2 = trm2 / alpha2
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   403
  by (rule alpha2_equivp)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   404
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
section {*** lets with many assignments ***}
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   406
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   407
datatype trm3 =
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   408
  Vr3 "name"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   409
| Ap3 "trm3" "trm3"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   410
| Lm3 "name" "trm3"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   411
| Lt3 "assigns" "trm3"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   412
and assigns =
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   413
  ANil
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   414
| ACons "name" "trm3" "assigns"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   415
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   416
(* to be given by the user *)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   417
primrec 
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   418
  bv3
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   419
where
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   420
  "bv3 ANil = {}"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   421
| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   422
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   423
primrec
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   424
  fv_trm3 and fv_assigns
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   425
where
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   426
  "fv_trm3 (Vr3 x) = {atom x}"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   427
| "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   428
| "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {atom x}"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   429
| "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   430
| "fv_assigns (ANil) = {}"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   431
| "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   432
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   433
(* needs to be stated by the package *)
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   434
instantiation
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   435
 trm3 and assigns :: pt
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   436
begin
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   437
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   438
primrec
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   439
  permute_trm3 and permute_assigns
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   440
where
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   441
  "permute_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   442
| "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   443
| "permute_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (permute_trm3 pi t)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   444
| "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   445
| "permute_assigns pi (ANil) = ANil"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   446
| "permute_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (permute_trm3 pi t) (permute_assigns pi as)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   447
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   448
lemma pt_trm3_assigns_zero:
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   449
  fixes t::trm3
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   450
  and   b::assigns
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   451
  shows "0 \<bullet> t = t"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   452
  and   "0 \<bullet> b = b"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   453
apply(induct t and b rule: trm3_assigns.inducts)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   454
apply(simp_all)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   455
done
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   456
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   457
lemma pt_trm3_assigns_plus:
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   458
  fixes t::trm3
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   459
  and   b::assigns
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   460
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   461
  and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   462
apply(induct t and b rule: trm3_assigns.inducts)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   463
apply(simp_all)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   464
done
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   465
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   466
instance
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   467
apply default
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   468
apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   469
done
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   470
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   471
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   472
end
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   473
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   474
inductive
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   475
  alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   476
where
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   477
  a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   478
| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   479
| a3: "\<exists>pi. (fv_trm3 t - {atom a} = fv_trm3 s - {atom b} \<and> 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   480
             (fv_trm3 t - {atom a})\<sharp>* pi \<and> 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   481
             (pi \<bullet> t) \<approx>3 s \<and> 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   482
             (pi \<bullet> a) = b)
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   483
       \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   484
| a4: "\<exists>pi. (
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   485
         fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and>
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   486
         (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and>
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   487
         pi \<bullet> t1 = t2      (* \<and> (pi \<bullet> b1 = b2)  *)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   488
       ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   489
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   490
lemma alpha3_equivp: "equivp alpha3" 
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   491
  sorry
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   492
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   493
quotient_type qtrm3 = trm3 / alpha3
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   494
  by (rule alpha3_equivp)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   495
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   496
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   497
section {*** lam with indirect list recursion ***}
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   498
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   499
datatype trm4 =
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   500
  Vr4 "name"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   501
| Ap4 "trm4" "trm4 list"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   502
| Lm4 "name" "trm4"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   503
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   504
thm trm4.recs
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   505
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   506
primrec
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   507
  fv_trm4 and fv_trm4_list
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   508
where
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   509
  "fv_trm4 (Vr4 x) = {atom x}"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   510
| "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   511
| "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {atom x}"
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   512
| "fv_trm4_list ([]) = {}"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   513
| "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   514
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   515
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   516
(* needs to be stated by the package *)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   517
(* there cannot be a clause for lists, as *) 
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   518
(* permuteutations are  already defined in Nominal (also functions, options, and so on) *)
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   519
instantiation
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   520
  trm4 :: pt
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   521
begin
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   522
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   523
(* does not work yet *)
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   524
primrec
963
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   525
  permute_trm4  and permute_trm4_list
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   526
where
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   527
  "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"
963
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   528
| "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute_trm4_list pi ts)"
957
080bd6f1607c mostly ported Terms.thy to new Nominal
Christian Urban <urbanc@in.tum.de>
parents: 950
diff changeset
   529
| "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)"
963
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   530
| "permute_trm4_list pi ([]) = []"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   531
| "permute_trm4_list pi (t#ts) = (permute_trm4 pi t) # (permute_trm4_list pi ts)"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   532
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   533
lemma pt_trm4_list_zero:
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   534
  fixes t::trm4
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   535
  and   ts::"trm4 list"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   536
  shows "0 \<bullet> t = t"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   537
  and   "permute_trm4_list 0 ts = ts"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   538
apply(induct t and ts rule: trm4.inducts)
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   539
apply(simp_all)
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   540
done
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   541
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   542
lemma pt_trm4_list_plus:
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   543
  fixes t::trm4
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   544
  and   ts::"trm4 list"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   545
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   546
  and   "(permute_trm4_list (p + q) ts) = permute_trm4_list p (permute_trm4_list q ts)"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   547
apply(induct t and ts rule: trm4.inducts)
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   548
apply(simp_all)
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   549
done
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   550
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   551
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   552
instance
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   553
apply(default)
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   554
apply(simp_all add: pt_trm4_list_zero pt_trm4_list_plus)
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   555
done
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   556
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   557
end
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   558
963
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   559
(* "repairing" of the permute function *)
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   560
lemma repaired:
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   561
  fixes ts::"trm4 list"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   562
  shows "permute_trm4_list p ts = p \<bullet> ts"
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   563
  apply(induct ts)
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   564
  apply(simp_all)
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   565
  done
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   566
976
Christian Urban <urbanc@in.tum.de>
parents: 963
diff changeset
   567
thm permute_trm4_permute_trm4_list.simps
963
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   568
thm permute_trm4_permute_trm4_list.simps[simplified repaired]
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   569
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   570
inductive
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   571
    alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   572
and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) 
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   573
where
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   574
  a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   575
| a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
963
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   576
| a4: "\<exists>pi. (fv_trm4 t - {atom a} = fv_trm4 s - {atom b} \<and> 
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   577
            (fv_trm4 t - {atom a})\<sharp>* pi \<and> 
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   578
            (pi \<bullet> t) \<approx>4 s \<and> 
caed1462c951 completely ported
Christian Urban <urbanc@in.tum.de>
parents: 957
diff changeset
   579
            (pi \<bullet> a) = b)
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   580
       \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   581
| a5: "[] \<approx>4list []"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   582
| a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   583
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   584
lemma alpha4_equivp: "equivp alpha4" sorry
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   585
lemma alpha4list_equivp: "equivp alpha4list" sorry
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   586
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   587
quotient_type 
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   588
  qtrm4 = trm4 / alpha4 and
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   589
  qtrm4list = "trm4 list" / alpha4list
1042
5a3bc323661c Minor fix.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1041
diff changeset
   590
  by (simp_all add: alpha4_equivp alpha4list_equivp)
1036
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   591
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   592
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   593
datatype rtrm5 =
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   594
  rVr5 "name"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   595
| rAp5 "rtrm5" "rtrm5"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   596
| rLt5 "rlts" "rtrm5"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   597
and rlts =
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   598
  rLnil
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   599
| rLcons "name" "rtrm5" "rlts"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   600
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   601
primrec
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   602
  rbv5
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   603
where
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   604
  "rbv5 rLnil = {}"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   605
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   606
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   607
primrec
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   608
  rfv_trm5 and rfv_lts
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   609
where
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   610
  "rfv_trm5 (rVr5 n) = {atom n}"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   611
| "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   612
| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - rbv5 lts) \<union> (rfv_lts lts - rbv5 lts)"
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   613
| "rfv_lts (rLnil) = {}"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   614
| "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   615
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   616
instantiation
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   617
  rtrm5 and rlts :: pt
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   618
begin
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   619
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   620
primrec
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   621
  permute_rtrm5 and permute_rlts
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   622
where
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   623
  "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   624
| "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   625
| "permute_rtrm5 pi (rLt5 ls t) = rLt5 (permute_rlts pi ls) (permute_rtrm5 pi t)"
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   626
| "permute_rlts pi (rLnil) = rLnil"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   627
| "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   628
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   629
lemma pt_rtrm5_zero:
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   630
  fixes t::rtrm5
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   631
  and   l::rlts
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   632
  shows "0 \<bullet> t = t"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   633
  and   "0 \<bullet> l = l"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   634
apply(induct t and l rule: rtrm5_rlts.inducts)
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   635
apply(simp_all)
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   636
done
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   637
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   638
lemma pt_rtrm5_plus:
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   639
  fixes t::rtrm5
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   640
  and   l::rlts
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   641
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   642
  and   "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   643
apply(induct t and l rule: rtrm5_rlts.inducts)
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   644
apply(simp_all)
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   645
done
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   646
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   647
instance
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   648
apply default
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   649
apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   650
done
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   651
950
98764f25f012 added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   652
end
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   653
1036
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   654
inductive
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   655
  alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   656
and
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   657
  alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   658
where
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   659
  a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   660
| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   661
| a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2)); 
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   662
        \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))\<rbrakk>
1036
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   663
        \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1035
diff changeset
   664
| a4: "rLnil \<approx>l rLnil"
1040
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   665
| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   666
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   667
print_theorems
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   668
1040
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   669
lemma alpha5_inj:
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   670
  "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   671
  "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   672
  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2))) \<and>
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   673
         (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))))"
1040
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   674
  "rLnil \<approx>l rLnil"
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   675
  "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
1040
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   676
apply -
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   677
apply (simp_all add: alpha5_alphalts.intros)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   678
apply rule
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   679
apply (erule alpha5.cases)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   680
apply (simp_all add: alpha5_alphalts.intros)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   681
apply rule
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   682
apply (erule alpha5.cases)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   683
apply (simp_all add: alpha5_alphalts.intros)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   684
apply rule
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   685
apply (erule alpha5.cases)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   686
apply (simp_all add: alpha5_alphalts.intros)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   687
apply rule
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   688
apply (erule alphalts.cases)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   689
apply (simp_all add: alpha5_alphalts.intros)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   690
done
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   691
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   692
lemma alpha5_equivps:
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   693
  shows "equivp alpha5"
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   694
  and   "equivp alphalts"
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   695
sorry
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   696
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   697
quotient_type
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   698
  trm5 = rtrm5 / alpha5
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   699
and
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   700
  lts = rlts / alphalts
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   701
  by (auto intro: alpha5_equivps)
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   702
1046
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   703
quotient_definition
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   704
  "Vr5 :: name \<Rightarrow> trm5"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   705
as
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   706
  "rVr5"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   707
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   708
quotient_definition
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   709
  "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   710
as
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   711
  "rAp5"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   712
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   713
quotient_definition
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   714
  "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   715
as
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   716
  "rLt5"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   717
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   718
quotient_definition
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   719
  "Lnil :: lts"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   720
as
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   721
  "rLnil"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   722
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   723
quotient_definition
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   724
  "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   725
as
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   726
  "rLcons"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   727
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   728
quotient_definition
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   729
   "fv_trm5 :: trm5 \<Rightarrow> atom set"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   730
as
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   731
  "rfv_trm5"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   732
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   733
quotient_definition
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   734
   "fv_lts :: lts \<Rightarrow> atom set"
1046
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   735
as
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   736
  "rfv_lts"
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   737
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   738
quotient_definition
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   739
   "bv5 :: lts \<Rightarrow> atom set"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   740
as
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   741
  "rbv5"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   742
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   743
lemma alpha5_rfv:
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   744
  "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   745
  "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   746
  apply(induct rule: alpha5_alphalts.inducts)
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   747
  apply(simp_all add: alpha_gen)
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   748
  done
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   749
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   750
lemma [quot_respect]:
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   751
"(op = ===> alpha5 ===> alpha5) permute permute"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   752
"(op = ===> alphalts ===> alphalts) permute permute"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   753
"(op = ===> alpha5) rVr5 rVr5"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   754
"(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   755
"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   756
"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   757
"(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   758
"(alpha5 ===> op =) rfv_trm5 rfv_trm5"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   759
"(alphalts ===> op =) rfv_lts rfv_lts"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   760
"(alphalts ===> op =) rbv5 rbv5"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   761
sorry
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   762
1053
b1ca92ea3a86 proved that bv for lists respects alpha for terms
Christian Urban <urbanc@in.tum.de>
parents: 1051
diff changeset
   763
lemma bv_list_rsp:
1055
34220518cccf Simplified the proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1054
diff changeset
   764
  shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
34220518cccf Simplified the proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1054
diff changeset
   765
apply(induct rule: alpha5_alphalts.inducts(2))
1053
b1ca92ea3a86 proved that bv for lists respects alpha for terms
Christian Urban <urbanc@in.tum.de>
parents: 1051
diff changeset
   766
apply(simp_all)
b1ca92ea3a86 proved that bv for lists respects alpha for terms
Christian Urban <urbanc@in.tum.de>
parents: 1051
diff changeset
   767
done
b1ca92ea3a86 proved that bv for lists respects alpha for terms
Christian Urban <urbanc@in.tum.de>
parents: 1051
diff changeset
   768
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   769
1053
b1ca92ea3a86 proved that bv for lists respects alpha for terms
Christian Urban <urbanc@in.tum.de>
parents: 1051
diff changeset
   770
lemma 
b1ca92ea3a86 proved that bv for lists respects alpha for terms
Christian Urban <urbanc@in.tum.de>
parents: 1051
diff changeset
   771
  shows "(alphalts ===> op =) rbv5 rbv5"
b1ca92ea3a86 proved that bv for lists respects alpha for terms
Christian Urban <urbanc@in.tum.de>
parents: 1051
diff changeset
   772
  by (simp add: bv_list_rsp)
b1ca92ea3a86 proved that bv for lists respects alpha for terms
Christian Urban <urbanc@in.tum.de>
parents: 1051
diff changeset
   773
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   774
lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   775
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   776
instantiation trm5 and lts :: pt
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   777
begin
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   778
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   779
quotient_definition
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   780
  "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   781
as
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   782
  "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   783
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   784
quotient_definition
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   785
  "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   786
as
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   787
  "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   788
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   789
lemma trm5_lts_zero:
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   790
  "0 \<bullet> (x\<Colon>trm5) = x"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   791
  "0 \<bullet> (y\<Colon>lts) = y"
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   792
apply(induct x and y rule: trm5_lts_inducts)
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   793
apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   794
done
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   795
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   796
lemma trm5_lts_plus:
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   797
  "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   798
  "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   799
apply(induct x and y rule: trm5_lts_inducts)
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   800
apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   801
done
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   802
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   803
instance
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   804
apply default
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   805
apply (simp_all add: trm5_lts_zero trm5_lts_plus)
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   806
done
1040
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   807
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   808
end
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   809
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   810
lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   811
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   812
lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   813
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   814
lemmas bv5[simp] = rbv5.simps[quot_lifted]
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   815
1073
53350d409473 Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1058
diff changeset
   816
lemmas fv_trm5_lts[simp] = rfv_trm5_rfv_lts.simps[quot_lifted]
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   817
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   818
lemma lets_ok:
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   819
  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   820
apply (subst alpha5_INJ)
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   821
apply (rule conjI)
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   822
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   823
apply (simp only: alpha_gen)
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   824
apply (simp add: permute_trm5_lts fresh_star_def)
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   825
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   826
apply (simp only: alpha_gen)
1052
c1b469325033 Finished remains on the let proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1051
diff changeset
   827
apply (simp add: permute_trm5_lts fresh_star_def)
c1b469325033 Finished remains on the let proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1051
diff changeset
   828
done
1050
e8bb5f85e510 Lets are ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1046
diff changeset
   829
1058
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   830
lemma lets_ok2:
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   831
  "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   832
   (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   833
apply (subst alpha5_INJ)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   834
apply (rule conjI)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   835
apply (rule_tac x="0 :: perm" in exI)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   836
apply (simp only: alpha_gen)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   837
apply (simp add: permute_trm5_lts fresh_star_def)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   838
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   839
apply (simp only: alpha_gen)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   840
apply (simp add: permute_trm5_lts fresh_star_def)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   841
done
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   842
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   843
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   844
lemma lets_not_ok1:
1056
a9135d300fbf Lets different.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1055
diff changeset
   845
  "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   846
             (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   847
apply (subst alpha5_INJ(3))
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   848
apply(clarify)
1056
a9135d300fbf Lets different.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1055
diff changeset
   849
apply (simp add: alpha_gen)
a9135d300fbf Lets different.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1055
diff changeset
   850
apply (simp add: permute_trm5_lts fresh_star_def)
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   851
apply (simp add: alpha5_INJ(5))
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   852
apply(clarify)
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   853
apply (simp add: alpha5_INJ(2))
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   854
apply (simp only: alpha5_INJ(1))
1056
a9135d300fbf Lets different.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1055
diff changeset
   855
done
a9135d300fbf Lets different.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1055
diff changeset
   856
1058
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   857
lemma distinct_helper:
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   858
  shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   859
  apply auto
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   860
  apply (erule alpha5.cases)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   861
  apply (simp_all only: rtrm5.distinct)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   862
  done
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   863
1058
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   864
lemma distinct_helper2:
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   865
  shows "(Vr5 x) \<noteq> (Ap5 y z)"
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   866
  by (lifting distinct_helper)
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   867
1058
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   868
lemma lets_nok:
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   869
  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   870
   (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   871
   (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   872
apply (subst alpha5_INJ)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   873
apply (simp only: alpha_gen permute_trm5_lts fresh_star_def)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   874
apply (subst alpha5_INJ(5))
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   875
apply (subst alpha5_INJ(5))
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   876
apply (simp add: distinct_helper2)
afedef46d3ab More let-rec experiments
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1057
diff changeset
   877
done
1057
f81b506f62a7 proposal for an alpha equivalence
Christian Urban <urbanc@in.tum.de>
parents: 1056
diff changeset
   878
1048
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   879
text {* type schemes *} 
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   880
datatype ty = 
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   881
  Var "name" 
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   882
| Fun "ty" "ty"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   883
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   884
instantiation
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   885
  ty :: pt
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   886
begin
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   887
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   888
primrec
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   889
  permute_ty 
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   890
where
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   891
  "permute_ty pi (Var a) = Var (pi \<bullet> a)"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   892
| "permute_ty pi (Fun T1 T2) = Fun (permute_ty pi T1) (permute_ty pi T2)"
1046
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   893
1048
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   894
lemma pt_ty_zero:
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   895
  fixes T::ty
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   896
  shows "0 \<bullet> T = T"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   897
apply(induct T rule: ty.inducts)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   898
apply(simp_all)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   899
done
1046
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   900
1048
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   901
lemma pt_ty_plus:
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   902
  fixes T::ty
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   903
  shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   904
apply(induct T rule: ty.inducts)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   905
apply(simp_all)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   906
done
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   907
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   908
instance
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   909
apply default
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   910
apply(simp_all add: pt_ty_zero pt_ty_plus)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   911
done
1046
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   912
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
   913
end
1048
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   914
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   915
datatype tyS = 
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   916
  All "name set" "ty" 
1046
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   917
1048
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   918
instantiation
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   919
  tyS :: pt
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   920
begin
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   921
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   922
primrec
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   923
  permute_tyS 
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   924
where
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   925
  "permute_tyS pi (All xs T) = All (pi \<bullet> xs) (pi \<bullet> T)"
1046
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   926
1048
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   927
lemma pt_tyS_zero:
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   928
  fixes T::tyS
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   929
  shows "0 \<bullet> T = T"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   930
apply(induct T rule: tyS.inducts)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   931
apply(simp_all)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   932
done
1046
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   933
1048
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   934
lemma pt_tyS_plus:
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   935
  fixes T::tyS
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   936
  shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   937
apply(induct T rule: tyS.inducts)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   938
apply(simp_all)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   939
done
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   940
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   941
instance
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   942
apply default
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   943
apply(simp_all add: pt_tyS_zero pt_tyS_plus)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   944
done
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   945
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   946
end
1046
159c7a9cd575 Definitions for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1044
diff changeset
   947
1040
632467a97dd8 alpha5 pseudo-injective
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1036
diff changeset
   948
1048
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   949
abbreviation
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   950
  "atoms xs \<equiv> {atom x| x. x \<in> xs}"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   951
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   952
primrec
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   953
  rfv_ty
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   954
where
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   955
  "rfv_ty (Var n) = {atom n}"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   956
| "rfv_ty (Fun T1 T2) = (rfv_ty T1) \<union> (rfv_ty T2)"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   957
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   958
primrec
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   959
  rfv_tyS
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   960
where 
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   961
  "rfv_tyS (All xs T) = (rfv_ty T - atoms xs)"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   962
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   963
inductive
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   964
  alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   965
where
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   966
  a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) rfv_ty pi (atoms xs2, T2)) 
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   967
        \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   968
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   969
lemma
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   970
  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   971
  apply(rule a1)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   972
  apply(simp add: alpha_gen)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   973
  apply(rule_tac x="0::perm" in exI)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   974
  apply(simp add: fresh_star_def)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   975
  done
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   976
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   977
lemma
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   978
  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   979
  apply(rule a1)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   980
  apply(simp add: alpha_gen)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   981
  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   982
  apply(simp add: fresh_star_def)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   983
  done
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   984
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   985
lemma
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   986
  shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   987
  apply(rule a1)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   988
  apply(simp add: alpha_gen)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   989
  apply(rule_tac x="0::perm" in exI)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   990
  apply(simp add: fresh_star_def)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   991
  done
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   992
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   993
lemma
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   994
  assumes a: "a \<noteq> b"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   995
  shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   996
  using a
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   997
  apply(clarify)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   998
  apply(erule alpha_tyS.cases)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
   999
  apply(simp add: alpha_gen)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
  1000
  apply(erule conjE)+
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
  1001
  apply(erule exE)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
  1002
  apply(erule conjE)+
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
  1003
  apply(clarify)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
  1004
  apply(simp)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
  1005
  apply(simp add: fresh_star_def)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
  1006
  apply(auto)
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
  1007
  done
1051
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1050 1049
diff changeset
  1008
1048
f5e037fd7c01 added type-scheme example
Christian Urban <urbanc@in.tum.de>
parents: 1044
diff changeset
  1009
1035
3a60a028cfc5 Starting with a let-rec example.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1033
diff changeset
  1010
end