Nominal/TySch.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Sat, 20 Mar 2010 10:12:09 +0100
changeset 1562 41294e4fc870
parent 1561 c3dca6e600c8
child 1568 2311a9fc4624
permissions -rw-r--r--
Size experiments.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
theory TySch
1525
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
     2
imports "Parser" "../Attic/Prove" "FSet"
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
begin
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
atom_decl name
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
1477
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
     7
ML {* val _ = cheat_fv_rsp := false *}
1561
c3dca6e600c8 Use 'alpha_bn_refl' to get rid of one of the sorrys.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1553
diff changeset
     8
ML {* val _ = cheat_alpha_bn_rsp := false *}
1477
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
     9
ML {* val _ = cheat_equivp := false *}
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    10
1477
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
    11
nominal_datatype t =
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
    12
  Var "name"
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
    13
| Fun "t" "t"
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
    14
and tyS =
1525
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
    15
  All xs::"name fset" ty::"t" bind xs in ty
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
1562
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    17
lemma size_eqvt: "size (pi \<bullet> x) = size x"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    18
sorry (* Can this be shown? *)
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    19
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    20
instantiation t and tyS :: size begin
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    21
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    22
quotient_definition
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    23
  "size_t :: t \<Rightarrow> nat"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    24
is
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    25
  "size :: t_raw \<Rightarrow> nat"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    26
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    27
quotient_definition
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    28
  "size_tyS :: tyS \<Rightarrow> nat"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    29
is
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    30
  "size :: tyS_raw \<Rightarrow> nat"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    31
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    32
lemma size_rsp:
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    33
  "alpha_t_raw x y \<Longrightarrow> size x = size y"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    34
  "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    35
  apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    36
  apply (simp_all only: t_raw_tyS_raw.size)
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    37
  apply (simp_all only: alpha_gen)
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    38
  apply clarify
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    39
  apply (simp_all only: size_eqvt)
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    40
  done
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    41
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    42
lemma [quot_respect]:
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    43
  "(alpha_t_raw ===> op =) size size"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    44
  "(alpha_tyS_raw ===> op =) size size"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    45
  by (simp_all add: size_rsp)
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    46
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    47
lemma [quot_preserve]:
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    48
  "(rep_t ---> id) size = size"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    49
  "(rep_tyS ---> id) size = size"
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    50
  by (simp_all add: size_t_def size_tyS_def)
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    51
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    52
instance
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    53
  by default
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    54
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    55
end
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    56
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    57
thm t_raw_tyS_raw.size(4)[quot_lifted]
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    58
thm t_raw_tyS_raw.size(5)[quot_lifted]
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    59
thm t_raw_tyS_raw.size(6)[quot_lifted]
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    60
41294e4fc870 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    61
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    62
thm t_tyS.fv
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    63
thm t_tyS.eq_iff
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    64
thm t_tyS.bn
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    65
thm t_tyS.perm
1525
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
    66
thm t_tyS.inducts
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    67
thm t_tyS.distinct
1534
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1530
diff changeset
    68
ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
1430
ccbcebef56f3 Trying to prove atom_image_fresh_swap
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1277
diff changeset
    69
1553
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1547
diff changeset
    70
lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
1525
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
    71
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
    72
lemma induct:
1537
0b21101157b1 Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1534
diff changeset
    73
  assumes a1: "\<And>name b. P b (Var name)"
0b21101157b1 Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1534
diff changeset
    74
  and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
1538
6853ce305118 Working on TySch strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1537
diff changeset
    75
  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
1539
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    76
  shows "P (a :: 'a :: pt) t \<and> P' d ts "
1537
0b21101157b1 Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1534
diff changeset
    77
proof -
1539
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    78
  have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
1538
6853ce305118 Working on TySch strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1537
diff changeset
    79
    apply (rule t_tyS.induct)
1537
0b21101157b1 Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1534
diff changeset
    80
    apply (simp add: a1)
1539
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    81
    apply (simp)
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    82
    apply (rule allI)+
1538
6853ce305118 Working on TySch strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1537
diff changeset
    83
    apply (rule a2)
1539
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    84
    apply simp
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    85
    apply simp
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    86
    apply (rule allI)
1538
6853ce305118 Working on TySch strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1537
diff changeset
    87
    apply (rule allI)
1539
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    88
    apply(subgoal_tac "\<exists>new::name fset. fset_to_set (fmap atom new) \<sharp>* (d, All (p \<bullet> fset) (p \<bullet> t))
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    89
                                      \<and> fcard new = fcard fset")
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    90
    apply clarify
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    91
    (*apply(rule_tac t="p \<bullet> All fset t" and 
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    92
                   s="(((p \<bullet> fset) \<leftrightarrow> new) + p) \<bullet> All fset t" in subst)
1538
6853ce305118 Working on TySch strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1537
diff changeset
    93
    apply (rule a3)
1539
78d0adf8a086 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1538
diff changeset
    94
    apply simp_all*)
1537
0b21101157b1 Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1534
diff changeset
    95
    sorry
1538
6853ce305118 Working on TySch strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1537
diff changeset
    96
  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
6853ce305118 Working on TySch strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1537
diff changeset
    97
  then show ?thesis by simp
1537
0b21101157b1 Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1534
diff changeset
    98
qed
1525
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
    99
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   100
lemma
1525
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
   101
  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   102
  apply(simp add: t_tyS.eq_iff)
1477
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
   103
  apply(rule_tac x="0::perm" in exI)
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   104
  apply(simp add: alpha_gen)
1477
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
   105
  apply(auto)
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
   106
  apply(simp add: fresh_star_def fresh_zero_perm)
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   107
  done
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   108
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   109
lemma
1525
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
   110
  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   111
  apply(simp add: t_tyS.eq_iff)
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   112
  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
1510
be911e869fde Added fv,bn,distinct,perm to the simplifier.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1498
diff changeset
   113
  apply(simp add: alpha_gen fresh_star_def eqvts)
1477
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
   114
  apply auto
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   115
  done
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   116
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   117
lemma
1525
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
   118
  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   119
  apply(simp add: t_tyS.eq_iff)
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   120
  apply(rule_tac x="0::perm" in exI)
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   121
  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
1477
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
   122
oops
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   123
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   124
lemma
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   125
  assumes a: "a \<noteq> b"
1525
bf321f16d025 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1515
diff changeset
   126
  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   127
  using a
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   128
  apply(simp add: t_tyS.eq_iff)
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   129
  apply(clarify)
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   130
  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
1477
4ac3485899e1 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1430
diff changeset
   131
  apply auto
1271
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   132
  done
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   133
393aced4801d Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   134
end