Nominal/Ex/TypeSchemes.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 01 Jun 2011 16:13:42 +0900
changeset 2801 5ecb857e9de7
parent 2787 1a6593bc494d
child 2803 04f7c4ce8588
child 2804 db0ed02eba6e
permissions -rw-r--r--
proved subst for All constructor in type schemes.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory TypeSchemes
2454
9ffee4eb1ae1 renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents: 2451
diff changeset
     2
imports "../Nominal2"
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
section {*** Type Schemes ***}
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
2709
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
     7
2556
8ed62410236e added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
     8
atom_decl name 
8ed62410236e added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
     9
2486
b4ea19604b0b cleaned up two examples
Christian Urban <urbanc@in.tum.de>
parents: 2480
diff changeset
    10
(* defined as a single nominal datatype *)
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
nominal_datatype ty =
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
  Var "name"
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
| Fun "ty" "ty"
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
and tys =
2714
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
    16
  All xs::"name fset" ty::"ty" bind (set+) xs in ty
2434
92dc6cfa3a95 automatic lifting
Christian Urban <urbanc@in.tum.de>
parents: 2424
diff changeset
    17
2468
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
    18
thm ty_tys.distinct
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
    19
thm ty_tys.induct
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2611
diff changeset
    20
thm ty_tys.inducts
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2611
diff changeset
    21
thm ty_tys.exhaust ty_tys.strong_exhaust
2468
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
    22
thm ty_tys.fv_defs
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
    23
thm ty_tys.bn_defs
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
    24
thm ty_tys.perm_simps
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
    25
thm ty_tys.eq_iff
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
    26
thm ty_tys.fv_bn_eqvt
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
    27
thm ty_tys.size_eqvt
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
    28
thm ty_tys.supports
2493
2e174807c891 added postprocessed fresh-lemmas for constructors
Christian Urban <urbanc@in.tum.de>
parents: 2486
diff changeset
    29
thm ty_tys.supp
2494
11133eb76f61 added Foo1 to explore a contrived example
Christian Urban <urbanc@in.tum.de>
parents: 2493
diff changeset
    30
thm ty_tys.fresh
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    32
fun
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    33
  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    34
where
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    35
  "lookup [] Y = Var Y"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    36
| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    37
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    38
lemma lookup_eqvt[eqvt]:
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    39
  shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    40
apply(induct Ts T rule: lookup.induct)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    41
apply(simp_all)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    42
done
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    43
2709
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    44
lemma test:
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    45
  assumes a: "f x = Inl y"
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    46
  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    47
using a 
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    48
apply(frule_tac p="p" in permute_boolI)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    49
apply(simp (no_asm_use) only: eqvts)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    50
apply(subst (asm) permute_fun_app_eq)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    51
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    52
apply(simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    53
done
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    54
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    55
lemma test2:
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    56
  assumes a: "f x = Inl y"
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    57
  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    58
using a 
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    59
apply(frule_tac p="p" in permute_boolI)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    60
apply(simp (no_asm_use) only: eqvts)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    61
apply(subst (asm) permute_fun_app_eq)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    62
back
2709
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    63
apply(simp)
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    64
done
2709
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
    65
2727
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
    66
lemma helper:
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
    67
  assumes "A - C = A - D"
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
    68
  and "B - C = B - D"
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
    69
  and "E \<subseteq> A \<union> B"
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
    70
  shows "E - C = E - D"
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
    71
using assms
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
    72
by blast
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
    73
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    74
nominal_primrec
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    75
    subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    76
and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    77
where
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    78
  "subst \<theta> (Var X) = lookup \<theta> X"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    79
| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    80
| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    81
apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    82
apply(simp add: eqvt_def)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    83
apply(rule allI)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    84
apply(simp add: permute_fun_def permute_bool_def)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    85
apply(rule ext)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    86
apply(rule ext)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    87
apply(rule iffI)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    88
apply(drule_tac x="p" in meta_spec)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    89
apply(drule_tac x="- p \<bullet> x" in meta_spec)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    90
apply(drule_tac x="- p \<bullet> xa" in meta_spec)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    91
apply(simp)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    92
apply(drule_tac x="-p" in meta_spec)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    93
apply(drule_tac x="x" in meta_spec)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    94
apply(drule_tac x="xa" in meta_spec)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    95
apply(simp)
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
    96
--"Eqvt One way"
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    97
thm subst_substs_graph.induct
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    98
thm subst_substs_graph.intros
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
    99
thm Projl.simps
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   100
apply(erule subst_substs_graph.induct)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   101
apply(perm_simp)
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   102
apply(rule subst_substs_graph.intros)
2709
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   103
thm subst_substs_graph.cases
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   104
apply(erule subst_substs_graph.cases)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   105
apply(simp (no_asm_use) only: eqvts)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   106
apply(subst test)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   107
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   108
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   109
apply(rotate_tac 1)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   110
apply(erule subst_substs_graph.cases)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   111
apply(subst test)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   112
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   113
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   114
apply(perm_simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   115
apply(rule subst_substs_graph.intros)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   116
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   117
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   118
apply(subst test)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   119
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   120
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   121
apply(perm_simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   122
apply(rule subst_substs_graph.intros)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   123
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   124
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   125
apply(simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   126
--"A"
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   127
apply(simp (no_asm_use) only: eqvts)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   128
apply(subst test)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   129
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   130
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   131
apply(rotate_tac 1)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   132
apply(erule subst_substs_graph.cases)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   133
apply(subst test)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   134
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   135
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   136
apply(perm_simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   137
apply(rule subst_substs_graph.intros)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   138
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   139
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   140
apply(subst test)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   141
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   142
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   143
apply(perm_simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   144
apply(rule subst_substs_graph.intros)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   145
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   146
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   147
apply(simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   148
--"A"
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   149
apply(simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   150
apply(erule subst_substs_graph.cases)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   151
apply(simp (no_asm_use) only: eqvts)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   152
apply(subst test)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   153
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   154
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   155
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   156
apply(rule subst_substs_graph.intros)
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   157
apply (simp add: eqvts)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   158
apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   159
apply (simp add: image_eqvt eqvts_raw eqvts)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   160
apply (simp add: fresh_star_permute_iff)
2709
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   161
apply(perm_simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   162
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   163
apply(simp (no_asm_use) only: eqvts)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   164
apply(subst test)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   165
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   166
back
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   167
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   168
apply(rule subst_substs_graph.intros)
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   169
apply (simp add: eqvts)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   170
apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   171
apply (simp add: image_eqvt eqvts_raw eqvts)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   172
apply (simp add: fresh_star_permute_iff)
2709
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   173
apply(perm_simp)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   174
apply(assumption)
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   175
apply(simp)
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   176
--"Eqvt done"
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   177
apply (case_tac x)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   178
apply simp apply clarify 
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   179
apply (rule_tac y="b" in ty_tys.exhaust(1))
2787
1a6593bc494d added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 2728
diff changeset
   180
apply (auto)[1]
1a6593bc494d added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 2728
diff changeset
   181
apply (auto)[1]
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   182
apply simp apply clarify 
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   183
apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))
2787
1a6593bc494d added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 2728
diff changeset
   184
apply (auto)[1]
1a6593bc494d added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 2728
diff changeset
   185
apply (auto)[5]
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   186
--"LAST GOAL"
2787
1a6593bc494d added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
parents: 2728
diff changeset
   187
apply(simp del: ty_tys.eq_iff)
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   188
apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   189
apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   190
apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
2709
eb4a2f4078ae some experiments
Christian Urban <urbanc@in.tum.de>
parents: 2707
diff changeset
   191
defer
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   192
apply (simp add: eqvt_at_def subst_def)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   193
apply rule
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   194
apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)")
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   195
apply (subst test2)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   196
apply (drule_tac x="(\<theta>', T)" in meta_spec)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   197
apply assumption
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   198
apply simp
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   199
--"We require that for Inl it returns Inl. It doesn't work for undefined, but it does work for the following"
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   200
 apply (subgoal_tac "\<And>y. \<exists>z. (\<lambda>x. THE_default (sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined) x) (subst_substs_graph x)) (Inl y) = (Inl z)")
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   201
prefer 2
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   202
apply (simp add: THE_default_def)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   203
apply (case_tac "Ex1 (subst_substs_graph (Inl y))")
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   204
prefer 2
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   205
apply simp
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   206
apply (simp add: the1_equality)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   207
apply auto[1]
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   208
apply (erule_tac x="x" in allE)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   209
apply simp
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   210
apply(cases rule: subst_substs_graph.cases)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   211
apply assumption
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   212
apply (rule_tac x="lookup \<theta> X" in exI)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   213
apply clarify
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   214
apply (rule the1_equality)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   215
apply metis apply assumption
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   216
apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   217
                  (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   218
apply clarify
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   219
apply (rule the1_equality)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   220
apply metis apply assumption
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   221
apply clarify
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   222
--"This is exactly the assumption for the properly defined function"
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   223
defer
2714
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   224
apply (simp only: Abs_eq_res_set)
2727
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   225
apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   226
apply (subst (asm) Abs_eq_iff2)
2714
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   227
apply (clarify)
2711
ec1a7ef740b8 Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2710
diff changeset
   228
apply (simp add: alphas)
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   229
apply (clarify)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   230
apply (rule trans)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   231
apply(rule_tac p="p" in supp_perm_eq[symmetric])
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   232
apply(rule fresh_star_supp_conv)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   233
thm fresh_star_perm_set_conv
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   234
apply(drule fresh_star_perm_set_conv)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   235
apply (rule finite_Diff)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   236
apply (rule finite_supp)
2714
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   237
apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. subst \<theta>' T)")
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   238
apply (metis Un_absorb2 fresh_star_Un)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   239
apply (simp add: fresh_star_Un)
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   240
apply (rule conjI)
2714
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   241
apply (simp (no_asm) add: fresh_star_def)
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   242
2711
ec1a7ef740b8 Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2710
diff changeset
   243
apply rule
ec1a7ef740b8 Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2710
diff changeset
   244
apply(simp (no_asm) only: Abs_fresh_iff)
ec1a7ef740b8 Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2710
diff changeset
   245
apply(clarify)
2714
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   246
apply auto[1]
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   247
apply (simp add: fresh_star_def fresh_def)
2728
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   248
2714
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   249
apply (simp (no_asm) add: fresh_star_def)
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   250
apply rule
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   251
apply auto[1]
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   252
apply(simp (no_asm) only: Abs_fresh_iff)
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   253
apply(clarify)
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   254
apply auto[1]
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   255
apply(drule_tac a="atom x" in fresh_eqvt_at)
2711
ec1a7ef740b8 Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2710
diff changeset
   256
apply (simp add: supp_Pair finite_supp)
ec1a7ef740b8 Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2710
diff changeset
   257
apply (simp add: fresh_Pair)
2728
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   258
apply(auto simp add: Abs_fresh_iff fresh_star_def)[2]
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   259
apply (simp add: fresh_def)
2710
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   260
apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   261
prefer 2
7eebe0d5d298 Experiments with functions
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2709
diff changeset
   262
apply (rule perm_supp_eq)
2714
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   263
apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'")
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   264
apply (auto simp add: fresh_star_def)[1]
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   265
apply (simp add: fresh_star_Un fresh_star_def)
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   266
apply blast
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   267
apply(simp add: eqvt_at_def inter_eqvt supp_eqvt)
908750991c2f Experiments with substitution on set+
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2711
diff changeset
   268
apply (simp only: Abs_eq_res_set[symmetric])
2727
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   269
apply (simp add: Abs_eq_iff alphas)
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   270
apply rule
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   271
prefer 2
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   272
apply (rule_tac x="0 :: perm" in exI)
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   273
apply (simp add: fresh_star_zero)
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   274
apply (rule helper)
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   275
prefer 3
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   276
apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)")
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   277
apply simp
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   278
apply (subst supp_Pair[symmetric])
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   279
apply (rule supp_eqvt_at)
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   280
apply (simp add: eqvt_at_def)
2728
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   281
apply (thin_tac " p \<bullet> atom ` fset xs \<inter> supp (p \<bullet> T) = atom ` fset xsa \<inter> supp (p \<bullet> T)")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   282
apply (thin_tac "supp T - atom ` fset xs \<inter> supp T = supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   283
apply (thin_tac "supp p \<subseteq> atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   284
apply (thin_tac "(atom ` fset xsa \<inter> supp (p \<bullet> T) - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   285
apply (thin_tac "atom ` fset xs \<sharp>* \<theta>'")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   286
apply (thin_tac "atom ` fset xsa \<sharp>* \<theta>'")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   287
apply (thin_tac "(supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* p")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   288
apply (rule)
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   289
apply (subgoal_tac "\<forall>p. p \<bullet> subst \<theta>' T = subst (p \<bullet> \<theta>') (p \<bullet> T)")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   290
apply (erule_tac x="p" in allE)
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   291
apply (erule_tac x="pa + p" in allE)
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   292
apply (metis permute_plus)
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   293
apply assumption
2727
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   294
apply (simp add: supp_Pair finite_supp)
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   295
prefer 2 apply blast
c10b56d226ce further experiments with typeschemes subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2722
diff changeset
   296
prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI)
2728
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   297
apply (rule_tac s="supp \<theta>'" in trans)
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   298
apply (subgoal_tac "(p \<bullet> atom ` fset xs) \<sharp>* \<theta>'")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   299
apply (auto simp add: fresh_star_def fresh_def)[1]
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   300
apply (subgoal_tac "supp p \<sharp>* \<theta>'")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   301
apply (metis fresh_star_permute_iff)
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   302
apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* \<theta>'")
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   303
apply (auto simp add: fresh_star_def)[1]
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   304
apply (simp add: fresh_star_Un)
1feef59f3aa4 typeschemes/subst
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2727
diff changeset
   305
apply (auto simp add: fresh_star_def fresh_def)[1]
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   306
oops
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   307
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   308
section {* defined as two separate nominal datatypes *}
2486
b4ea19604b0b cleaned up two examples
Christian Urban <urbanc@in.tum.de>
parents: 2480
diff changeset
   309
2308
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2181
diff changeset
   310
nominal_datatype ty2 =
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2181
diff changeset
   311
  Var2 "name"
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2181
diff changeset
   312
| Fun2 "ty2" "ty2"
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2181
diff changeset
   313
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2181
diff changeset
   314
nominal_datatype tys2 =
2634
3ce1089cdbf3 changed res keyword to set+ for restrictions; comment by a referee
Christian Urban <urbanc@in.tum.de>
parents: 2630
diff changeset
   315
  All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents: 2308
diff changeset
   316
2468
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
   317
thm tys2.distinct
2630
8268b277d240 automated all strong induction lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2622
diff changeset
   318
thm tys2.induct tys2.strong_induct
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2611
diff changeset
   319
thm tys2.exhaust tys2.strong_exhaust
2468
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
   320
thm tys2.fv_defs
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
   321
thm tys2.bn_defs
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
   322
thm tys2.perm_simps
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
   323
thm tys2.eq_iff
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
   324
thm tys2.fv_bn_eqvt
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
   325
thm tys2.size_eqvt
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
   326
thm tys2.supports
2493
2e174807c891 added postprocessed fresh-lemmas for constructors
Christian Urban <urbanc@in.tum.de>
parents: 2486
diff changeset
   327
thm tys2.supp
2494
11133eb76f61 added Foo1 to explore a contrived example
Christian Urban <urbanc@in.tum.de>
parents: 2493
diff changeset
   328
thm tys2.fresh
2468
7b1470b55936 moved a proof to Abs
Christian Urban <urbanc@in.tum.de>
parents: 2454
diff changeset
   329
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   330
fun
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   331
  lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   332
where
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   333
  "lookup2 [] Y = Var2 Y"
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   334
| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"
2556
8ed62410236e added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   335
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   336
lemma lookup2_eqvt[eqvt]:
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   337
  shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
2801
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   338
  by (induct Ts T rule: lookup2.induct) simp_all
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   339
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   340
nominal_primrec
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   341
  subst  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   342
where
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   343
  "subst \<theta> (Var2 X) = lookup2 \<theta> X"
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   344
| "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
2801
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   345
  unfolding eqvt_def subst_graph_def
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   346
  apply (rule, perm_simp, rule)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   347
  apply(case_tac x)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   348
  apply(simp)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   349
  apply(rule_tac y="b" in ty2.exhaust)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   350
  apply(blast)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   351
  apply(blast)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   352
  apply(simp_all add: ty2.distinct)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   353
  done
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   354
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   355
termination
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   356
  apply(relation "measure (size o snd)")
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   357
  apply(simp_all add: ty2.size)
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   358
  done
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   359
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   360
lemma subst_eqvt[eqvt]:
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   361
  shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)"
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   362
apply(induct \<theta> T rule: subst.induct)
2707
747ebf2f066d made eqvt-proof explicit in the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2676
diff changeset
   363
apply(simp_all add: lookup2_eqvt)
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   364
done
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   365
2801
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   366
lemma supp_fun_app2_eqvt:
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   367
  assumes e: "eqvt f"
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   368
  shows "supp (f a b) \<subseteq> supp a \<union> supp b"
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   369
  using supp_fun_app_eqvt[OF e] supp_fun_app
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   370
  by blast
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   371
 
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   372
lemma supp_subst:
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   373
  "supp (subst \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   374
  apply (rule supp_fun_app2_eqvt)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   375
  unfolding eqvt_def by (simp add: eqvts_raw)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   376
 
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   377
lemma fresh_star_inter1:
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   378
  "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   379
  unfolding fresh_star_def by blast
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   380
 
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   381
nominal_primrec
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   382
  substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   383
where
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   384
  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"
2801
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   385
  unfolding eqvt_def substs_graph_def
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   386
  apply (rule, perm_simp, rule)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   387
  apply auto[1]
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   388
  apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   389
  apply auto
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   390
  apply (subst (asm) Abs_eq_res_set)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   391
  apply (subst (asm) Abs_eq_iff2)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   392
  apply (clarify)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   393
  apply (simp add: alphas)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   394
  apply (clarify)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   395
  apply (rule trans)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   396
  apply(rule_tac p="p" in supp_perm_eq[symmetric])
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   397
  apply(rule fresh_star_supp_conv)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   398
  apply(drule fresh_star_perm_set_conv)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   399
  apply (rule finite_Diff)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   400
  apply (rule finite_supp)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   401
  apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* ([atom ` fset xs]res. subst \<theta>' t)")
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   402
  apply (metis Un_absorb2 fresh_star_Un)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   403
  apply (subst fresh_star_Un)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   404
  apply (rule conjI)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   405
  apply (simp (no_asm) add: fresh_star_def)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   406
  apply (rule)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   407
  apply (simp add: Abs_fresh_iff)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   408
  apply (simp add: fresh_star_def)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   409
  apply (rule)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   410
  apply (simp (no_asm) add: Abs_fresh_iff)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   411
  apply auto[1]
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   412
  apply (simp add: fresh_def supp_Abs)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   413
  apply (rule contra_subsetD)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   414
  apply (rule supp_subst)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   415
  apply auto[1]
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   416
  apply simp
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   417
  apply (subst Abs_eq_iff)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   418
  apply (rule_tac x="0::perm" in exI)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   419
  apply (subgoal_tac "p \<bullet> subst \<theta>' t = subst \<theta>' (p \<bullet> t)")
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   420
  prefer 2
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   421
  apply (subgoal_tac "\<theta>' = p \<bullet> \<theta>'")
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   422
  apply (simp add: subst_eqvt)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   423
  apply (rule sym)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   424
  apply (rule perm_supp_eq)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   425
  apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* \<theta>'")
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   426
  apply (metis Diff_partition fresh_star_Un)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   427
  apply (simp add: fresh_star_Un fresh_star_inter1)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   428
  apply (simp add: alphas fresh_star_zero)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   429
  apply auto[1]
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   430
  apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   431
  apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   432
  apply (drule subsetD[OF supp_subst])
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   433
  apply auto[1]
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   434
  apply (simp add: fresh_star_def fresh_def)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   435
  apply (subgoal_tac "x \<in> supp(p \<bullet> t)")
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   436
  apply (smt IntI inf_le1 inter_eqvt subsetD supp_eqvt)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   437
  apply (rotate_tac 6)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   438
  apply (drule sym)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   439
  apply (simp add: subst_eqvt)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   440
  apply (drule subsetD[OF supp_subst])
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   441
  apply auto[1]
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   442
  apply (rotate_tac 2)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   443
  apply (subst (asm) fresh_star_permute_iff[symmetric])
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   444
  apply (simp add: fresh_star_def fresh_def)
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   445
  apply blast
5ecb857e9de7 proved subst for All constructor in type schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2787
diff changeset
   446
  done
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   447
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   448
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   449
text {* Some Tests about Alpha-Equality *}
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   450
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   451
lemma
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   452
  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   453
  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   454
  apply(rule_tac x="0::perm" in exI)
2676
028d5511c15f some tryes about substitution over type-schemes
Christian Urban <urbanc@in.tum.de>
parents: 2634
diff changeset
   455
  apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   456
  done
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   457
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   458
lemma
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   459
  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
2566
a59d8e1e3a17 moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
parents: 2556
diff changeset
   460
  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   461
  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
2566
a59d8e1e3a17 moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
parents: 2556
diff changeset
   462
  apply(simp add: alphas fresh_star_def supp_at_base ty_tys.supp)
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   463
  done
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   464
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   465
lemma
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   466
  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
2566
a59d8e1e3a17 moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
parents: 2556
diff changeset
   467
  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   468
  apply(rule_tac x="0::perm" in exI)
2566
a59d8e1e3a17 moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
parents: 2556
diff changeset
   469
  apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   470
done
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   471
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   472
lemma
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   473
  assumes a: "a \<noteq> b"
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   474
  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   475
  using a
2566
a59d8e1e3a17 moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
parents: 2556
diff changeset
   476
  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   477
  apply(clarify)
2566
a59d8e1e3a17 moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
parents: 2556
diff changeset
   478
  apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   479
  apply auto
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   480
  done
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   481
2566
a59d8e1e3a17 moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
parents: 2556
diff changeset
   482
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   483
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   484
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   485
end