src/CCL/Wfd.thy
author wenzelm
Sat, 22 Oct 2016 21:10:02 +0200
changeset 64350 3af8566788e7
parent 63120 629a4c5e953e
child 69593 3dda49e08b9d
permissions -rw-r--r--
remote_builds has PAR-SEQ semantics of old isatest-makedist; tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     1
(*  Title:      CCL/Wfd.thy
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 289
diff changeset
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
     6
section \<open>Well-founded relations in CCL\<close>
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     7
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     8
theory Wfd
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     9
imports Trancl Type Hered
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    10
begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    12
definition Wfd :: "[i set] \<Rightarrow> o"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    13
  where "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R \<longrightarrow> y:P) \<longrightarrow> x:P) \<longrightarrow> (ALL a. a:P)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    15
definition wf :: "[i set] \<Rightarrow> i set"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    16
  where "wf(R) == {x. x:R \<and> Wfd(R)}"
57521
b14c0794f97f modernized definitions;
wenzelm
parents: 56245
diff changeset
    17
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    18
definition wmap :: "[i\<Rightarrow>i,i set] \<Rightarrow> i set"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    19
  where "wmap(f,R) == {p. EX x y. p=<x,y> \<and> <f(x),f(y)> : R}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
57521
b14c0794f97f modernized definitions;
wenzelm
parents: 56245
diff changeset
    21
definition lex :: "[i set,i set] => i set"      (infixl "**" 70)
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    22
  where "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> \<and> (<a,a'> : ra | (a=a' \<and> <b,b'> : rb))}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
57521
b14c0794f97f modernized definitions;
wenzelm
parents: 56245
diff changeset
    24
definition NatPR :: "i set"
b14c0794f97f modernized definitions;
wenzelm
parents: 56245
diff changeset
    25
  where "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    27
definition ListPR :: "i set \<Rightarrow> i set"
57521
b14c0794f97f modernized definitions;
wenzelm
parents: 56245
diff changeset
    28
  where "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    29
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    30
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    31
lemma wfd_induct:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    32
  assumes 1: "Wfd(R)"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    33
    and 2: "\<And>x. ALL y. <y,x>: R \<longrightarrow> P(y) \<Longrightarrow> P(x)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    34
  shows "P(a)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    35
  apply (rule 1 [unfolded Wfd_def, rule_format, THEN CollectD])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    36
  using 2 apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    37
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    38
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    39
lemma wfd_strengthen_lemma:
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    40
  assumes 1: "\<And>x y.<x,y> : R \<Longrightarrow> Q(x)"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    41
    and 2: "ALL x. (ALL y. <y,x> : R \<longrightarrow> y : P) \<longrightarrow> x : P"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    42
    and 3: "\<And>x. Q(x) \<Longrightarrow> x:P"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    43
  shows "a:P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    44
  apply (rule 2 [rule_format])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    45
  using 1 3
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    46
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    47
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    48
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
    49
method_setup wfd_strengthen = \<open>
63120
629a4c5e953e embedded content may be delimited via cartouches;
wenzelm
parents: 61966
diff changeset
    50
  Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
58971
8c9a319821b3 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    51
    SIMPLE_METHOD' (fn i =>
59780
23b67731f4f0 support 'for' fixes in rule_tac etc.;
wenzelm
parents: 59763
diff changeset
    52
      Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] [] @{thm wfd_strengthen_lemma} i
59755
f8d164ab0dc1 more position information;
wenzelm
parents: 59582
diff changeset
    53
        THEN assume_tac ctxt (i + 1)))
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
    54
\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    55
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    56
lemma wf_anti_sym: "\<lbrakk>Wfd(r); <a,x>:r; <x,a>:r\<rbrakk> \<Longrightarrow> P"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    57
  apply (subgoal_tac "ALL x. <a,x>:r \<longrightarrow> <x,a>:r \<longrightarrow> P")
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    58
   apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    59
  apply (erule wfd_induct)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    60
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    61
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    62
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    63
lemma wf_anti_refl: "\<lbrakk>Wfd(r); <a,a>: r\<rbrakk> \<Longrightarrow> P"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    64
  apply (rule wf_anti_sym)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    65
  apply assumption+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    66
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    67
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    68
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
    69
subsection \<open>Irreflexive transitive closure\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    70
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    71
lemma trancl_wf:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    72
  assumes 1: "Wfd(R)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    73
  shows "Wfd(R^+)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    74
  apply (unfold Wfd_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    75
  apply (rule allI ballI impI)+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    76
(*must retain the universal formula for later use!*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    77
  apply (rule allE, assumption)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    78
  apply (erule mp)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    79
  apply (rule 1 [THEN wfd_induct])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    80
  apply (rule impI [THEN allI])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    81
  apply (erule tranclE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    82
   apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    83
  apply (erule spec [THEN mp, THEN spec, THEN mp])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    84
   apply assumption+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    85
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    86
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    87
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
    88
subsection \<open>Lexicographic Ordering\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    89
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    90
lemma lexXH:
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    91
  "p : ra**rb \<longleftrightarrow> (EX a a' b b'. p = <<a,b>,<a',b'>> \<and> (<a,a'> : ra | a=a' \<and> <b,b'> : rb))"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    92
  unfolding lex_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    93
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    94
lemma lexI1: "<a,a'> : ra \<Longrightarrow> <<a,b>,<a',b'>> : ra**rb"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    95
  by (blast intro!: lexXH [THEN iffD2])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    96
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
    97
lemma lexI2: "<b,b'> : rb \<Longrightarrow> <<a,b>,<a,b'>> : ra**rb"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    98
  by (blast intro!: lexXH [THEN iffD2])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    99
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   100
lemma lexE:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   101
  assumes 1: "p : ra**rb"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   102
    and 2: "\<And>a a' b b'. \<lbrakk><a,a'> : ra; p=<<a,b>,<a',b'>>\<rbrakk> \<Longrightarrow> R"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   103
    and 3: "\<And>a b b'. \<lbrakk><b,b'> : rb; p = <<a,b>,<a,b'>>\<rbrakk> \<Longrightarrow> R"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   104
  shows R
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   105
  apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   106
  using 2 3
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   107
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   108
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   109
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   110
lemma lex_pair: "\<lbrakk>p : r**s; \<And>a a' b b'. p = <<a,b>,<a',b'>> \<Longrightarrow> P\<rbrakk> \<Longrightarrow>P"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   111
  apply (erule lexE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   112
   apply blast+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   113
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   114
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   115
lemma lex_wf:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   116
  assumes 1: "Wfd(R)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   117
    and 2: "Wfd(S)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   118
  shows "Wfd(R**S)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   119
  apply (unfold Wfd_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   120
  apply safe
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   121
  apply (wfd_strengthen "\<lambda>x. EX a b. x=<a,b>")
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   122
   apply (blast elim!: lex_pair)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   123
  apply (subgoal_tac "ALL a b.<a,b>:P")
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   124
   apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   125
  apply (rule 1 [THEN wfd_induct, THEN allI])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   126
  apply (rule 2 [THEN wfd_induct, THEN allI]) back
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   127
  apply (fast elim!: lexE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   128
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   129
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   130
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   131
subsection \<open>Mapping\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   132
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   133
lemma wmapXH: "p : wmap(f,r) \<longleftrightarrow> (EX x y. p=<x,y> \<and> <f(x),f(y)> : r)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   134
  unfolding wmap_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   135
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   136
lemma wmapI: "<f(a),f(b)> : r \<Longrightarrow> <a,b> : wmap(f,r)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   137
  by (blast intro!: wmapXH [THEN iffD2])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   138
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   139
lemma wmapE: "\<lbrakk>p : wmap(f,r); \<And>a b. \<lbrakk><f(a),f(b)> : r; p=<a,b>\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   140
  by (blast dest!: wmapXH [THEN iffD1])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   141
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   142
lemma wmap_wf:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   143
  assumes 1: "Wfd(r)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   144
  shows "Wfd(wmap(f,r))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   145
  apply (unfold Wfd_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   146
  apply clarify
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   147
  apply (subgoal_tac "ALL b. ALL a. f (a) = b \<longrightarrow> a:P")
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   148
   apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   149
  apply (rule 1 [THEN wfd_induct, THEN allI])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   150
  apply clarify
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   151
  apply (erule spec [THEN mp])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   152
  apply (safe elim!: wmapE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   153
  apply (erule spec [THEN mp, THEN spec, THEN mp])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   154
   apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   155
   apply (rule refl)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   156
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   157
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   158
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   159
subsection \<open>Projections\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   160
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   161
lemma wfstI: "<xa,ya> : r \<Longrightarrow> <<xa,xb>,<ya,yb>> : wmap(fst,r)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   162
  apply (rule wmapI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   163
  apply simp
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   164
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   165
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   166
lemma wsndI: "<xb,yb> : r \<Longrightarrow> <<xa,xb>,<ya,yb>> : wmap(snd,r)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   167
  apply (rule wmapI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   168
  apply simp
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   169
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   170
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   171
lemma wthdI: "<xc,yc> : r \<Longrightarrow> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   172
  apply (rule wmapI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   173
  apply simp
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   174
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   175
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   176
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   177
subsection \<open>Ground well-founded relations\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   178
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   179
lemma wfI: "\<lbrakk>Wfd(r);  a : r\<rbrakk> \<Longrightarrow> a : wf(r)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   180
  unfolding wf_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   181
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   182
lemma Empty_wf: "Wfd({})"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   183
  unfolding Wfd_def by (blast elim: EmptyXH [THEN iffD1, THEN FalseE])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   184
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   185
lemma wf_wf: "Wfd(wf(R))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   186
  unfolding wf_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   187
  apply (rule_tac Q = "Wfd(R)" in excluded_middle [THEN disjE])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   188
   apply simp_all
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   189
  apply (rule Empty_wf)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   190
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   191
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   192
lemma NatPRXH: "p : NatPR \<longleftrightarrow> (EX x:Nat. p=<x,succ(x)>)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   193
  unfolding NatPR_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   194
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   195
lemma ListPRXH: "p : ListPR(A) \<longleftrightarrow> (EX h:A. EX t:List(A).p=<t,h$t>)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   196
  unfolding ListPR_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   197
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   198
lemma NatPRI: "x : Nat \<Longrightarrow> <x,succ(x)> : NatPR"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   199
  by (auto simp: NatPRXH)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   200
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   201
lemma ListPRI: "\<lbrakk>t : List(A); h : A\<rbrakk> \<Longrightarrow> <t,h $ t> : ListPR(A)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   202
  by (auto simp: ListPRXH)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   203
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   204
lemma NatPR_wf: "Wfd(NatPR)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   205
  apply (unfold Wfd_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   206
  apply clarify
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   207
  apply (wfd_strengthen "\<lambda>x. x:Nat")
47966
b8a94ed1646e eliminated obsolete fastsimp;
wenzelm
parents: 47432
diff changeset
   208
   apply (fastforce iff: NatPRXH)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   209
  apply (erule Nat_ind)
47966
b8a94ed1646e eliminated obsolete fastsimp;
wenzelm
parents: 47432
diff changeset
   210
   apply (fastforce iff: NatPRXH)+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   211
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   212
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   213
lemma ListPR_wf: "Wfd(ListPR(A))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   214
  apply (unfold Wfd_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   215
  apply clarify
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   216
  apply (wfd_strengthen "\<lambda>x. x:List (A)")
47966
b8a94ed1646e eliminated obsolete fastsimp;
wenzelm
parents: 47432
diff changeset
   217
   apply (fastforce iff: ListPRXH)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   218
  apply (erule List_ind)
47966
b8a94ed1646e eliminated obsolete fastsimp;
wenzelm
parents: 47432
diff changeset
   219
   apply (fastforce iff: ListPRXH)+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   220
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   221
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   222
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   223
subsection \<open>General Recursive Functions\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   224
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   225
lemma letrecT:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   226
  assumes 1: "a : A"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   227
    and 2: "\<And>p g. \<lbrakk>p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x)\<rbrakk> \<Longrightarrow> h(p,g) : D(p)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   228
  shows "letrec g x be h(x,g) in g(a) : D(a)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   229
  apply (rule 1 [THEN rev_mp])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   230
  apply (rule wf_wf [THEN wfd_induct])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   231
  apply (subst letrecB)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   232
  apply (rule impI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   233
  apply (erule 2)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   234
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   235
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   236
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   237
lemma SPLITB: "SPLIT(<a,b>,B) = B(a,b)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   238
  unfolding SPLIT_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   239
  apply (rule set_ext)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   240
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   241
  done
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
   242
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   243
lemma letrec2T:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   244
  assumes "a : A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   245
    and "b : B"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   246
    and "\<And>p q g. \<lbrakk>p:A; q:B;
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   247
              ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y)\<rbrakk> \<Longrightarrow> 
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   248
                h(p,q,g) : D(p,q)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   249
  shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   250
  apply (unfold letrec2_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   251
  apply (rule SPLITB [THEN subst])
41526
54b4686704af eliminated global prems;
wenzelm
parents: 38500
diff changeset
   252
  apply (assumption | rule letrecT pairT splitT assms)+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   253
  apply (subst SPLITB)
41526
54b4686704af eliminated global prems;
wenzelm
parents: 38500
diff changeset
   254
  apply (assumption | rule ballI SubtypeI assms)+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   255
  apply (rule SPLITB [THEN subst])
41526
54b4686704af eliminated global prems;
wenzelm
parents: 38500
diff changeset
   256
  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   257
    erule bspec SubtypeE sym [THEN subst])+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   258
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   259
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   260
lemma lem: "SPLIT(<a,<b,c>>,\<lambda>x xs. SPLIT(xs,\<lambda>y z. B(x,y,z))) = B(a,b,c)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   261
  by (simp add: SPLITB)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   262
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   263
lemma letrec3T:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   264
  assumes "a : A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   265
    and "b : B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   266
    and "c : C"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   267
    and "\<And>p q r g. \<lbrakk>p:A; q:B; r:C;
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   268
       ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}.
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   269
                                                        g(x,y,z) : D(x,y,z) \<rbrakk> \<Longrightarrow>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   270
                h(p,q,r,g) : D(p,q,r)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   271
  shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   272
  apply (unfold letrec3_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   273
  apply (rule lem [THEN subst])
41526
54b4686704af eliminated global prems;
wenzelm
parents: 38500
diff changeset
   274
  apply (assumption | rule letrecT pairT splitT assms)+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   275
  apply (simp add: SPLITB)
41526
54b4686704af eliminated global prems;
wenzelm
parents: 38500
diff changeset
   276
  apply (assumption | rule ballI SubtypeI assms)+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   277
  apply (rule lem [THEN subst])
41526
54b4686704af eliminated global prems;
wenzelm
parents: 38500
diff changeset
   278
  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   279
    erule bspec SubtypeE sym [THEN subst])+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   280
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   281
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   282
lemmas letrecTs = letrecT letrec2T letrec3T
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   283
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   284
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   285
subsection \<open>Type Checking for Recursive Calls\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   286
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   287
lemma rcallT:
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   288
  "\<lbrakk>ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);  
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   289
    g(a) : D(a) \<Longrightarrow> g(a) : E;  a:A;  <a,p>:wf(R)\<rbrakk> \<Longrightarrow> g(a) : E"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   290
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   291
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   292
lemma rcall2T:
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   293
  "\<lbrakk>ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y);
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   294
    g(a,b) : D(a,b) \<Longrightarrow> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R)\<rbrakk> \<Longrightarrow> g(a,b) : E"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   295
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   296
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   297
lemma rcall3T:
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   298
  "\<lbrakk>ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z);
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   299
    g(a,b,c) : D(a,b,c) \<Longrightarrow> g(a,b,c) : E;
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   300
    a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R)\<rbrakk> \<Longrightarrow> g(a,b,c) : E"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   301
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   302
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   303
lemmas rcallTs = rcallT rcall2T rcall3T
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   304
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   305
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   306
subsection \<open>Instantiating an induction hypothesis with an equality assumption\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   307
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   308
lemma hyprcallT:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   309
  assumes 1: "g(a) = b"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   310
    and 2: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x)"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   311
    and 3: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) \<Longrightarrow> b=g(a) \<Longrightarrow> g(a) : D(a) \<Longrightarrow> P"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   312
    and 4: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) \<Longrightarrow> a:A"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   313
    and 5: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) \<Longrightarrow> <a,p>:wf(R)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   314
  shows P
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   315
  apply (rule 3 [OF 2, OF 1 [symmetric]])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   316
  apply (rule rcallT [OF 2])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   317
    apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   318
   apply (rule 4 [OF 2])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   319
  apply (rule 5 [OF 2])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   320
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   321
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   322
lemma hyprcall2T:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   323
  assumes 1: "g(a,b) = c"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   324
    and 2: "ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y)"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   325
    and 3: "\<lbrakk>c = g(a,b); g(a,b) : D(a,b)\<rbrakk> \<Longrightarrow> P"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   326
    and 4: "a:A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   327
    and 5: "b:B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   328
    and 6: "<<a,b>,<p,q>>:wf(R)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   329
  shows P
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   330
  apply (rule 3)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   331
    apply (rule 1 [symmetric])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   332
  apply (rule rcall2T)
23467
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   333
      apply (rule 2)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   334
     apply assumption
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   335
    apply (rule 4)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   336
   apply (rule 5)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   337
  apply (rule 6)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   338
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   339
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   340
lemma hyprcall3T:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   341
  assumes 1: "g(a,b,c) = d"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   342
    and 2: "ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z)"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   343
    and 3: "\<lbrakk>d = g(a,b,c); g(a,b,c) : D(a,b,c)\<rbrakk> \<Longrightarrow> P"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   344
    and 4: "a:A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   345
    and 5: "b:B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   346
    and 6: "c:C"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   347
    and 7: "<<a,<b,c>>,<p,<q,r>>> : wf(R)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   348
  shows P
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   349
  apply (rule 3)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   350
   apply (rule 1 [symmetric])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   351
  apply (rule rcall3T)
23467
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   352
       apply (rule 2)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   353
      apply assumption
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   354
     apply (rule 4)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   355
    apply (rule 5)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   356
   apply (rule 6)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22846
diff changeset
   357
  apply (rule 7)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   358
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   359
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   360
lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   361
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   362
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   363
subsection \<open>Rules to Remove Induction Hypotheses after Type Checking\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   364
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   365
lemma rmIH1: "\<lbrakk>ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P\<rbrakk> \<Longrightarrow> P" .
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   366
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   367
lemma rmIH2: "\<lbrakk>ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P\<rbrakk> \<Longrightarrow> P" .
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   368
  
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   369
lemma rmIH3:
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   370
 "\<lbrakk>ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); P\<rbrakk> \<Longrightarrow> P" .
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   371
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   372
lemmas rmIHs = rmIH1 rmIH2 rmIH3
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   373
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   374
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   375
subsection \<open>Lemmas for constructors and subtypes\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   376
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   377
(* 0-ary constructors do not need additional rules as they are handled *)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   378
(*                                      correctly by applying SubtypeI *)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   379
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   380
lemma Subtype_canTs:
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   381
  "\<And>a b A B P. a : {x:A. b:{y:B(a).P(<x,y>)}} \<Longrightarrow> <a,b> : {x:Sigma(A,B).P(x)}"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   382
  "\<And>a A B P. a : {x:A. P(inl(x))} \<Longrightarrow> inl(a) : {x:A+B. P(x)}"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   383
  "\<And>b A B P. b : {x:B. P(inr(x))} \<Longrightarrow> inr(b) : {x:A+B. P(x)}"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   384
  "\<And>a P. a : {x:Nat. P(succ(x))} \<Longrightarrow> succ(a) : {x:Nat. P(x)}"
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   385
  "\<And>h t A P. h : {x:A. t : {y:List(A).P(x$y)}} \<Longrightarrow> h$t : {x:List(A).P(x)}"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   386
  by (assumption | rule SubtypeI canTs icanTs | erule SubtypeE)+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   387
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   388
lemma letT: "\<lbrakk>f(t):B; \<not>t=bot\<rbrakk> \<Longrightarrow> let x be t in f(x) : B"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   389
  apply (erule letB [THEN ssubst])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   390
  apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   391
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   392
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   393
lemma applyT2: "\<lbrakk>a:A; f : Pi(A,B)\<rbrakk> \<Longrightarrow> f ` a  : B(a)"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   394
  apply (erule applyT)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   395
  apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   396
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   397
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   398
lemma rcall_lemma1: "\<lbrakk>a:A; a:A \<Longrightarrow> P(a)\<rbrakk> \<Longrightarrow> a : {x:A. P(x)}"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   399
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   400
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   401
lemma rcall_lemma2: "\<lbrakk>a:{x:A. Q(x)}; \<lbrakk>a:A; Q(a)\<rbrakk> \<Longrightarrow> P(a)\<rbrakk> \<Longrightarrow> a : {x:A. P(x)}"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   402
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   403
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   404
lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   405
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   406
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   407
subsection \<open>Typechecking\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   408
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   409
ML \<open>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   410
local
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   411
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   412
val type_rls =
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   413
  @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   414
  @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   415
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 51798
diff changeset
   416
fun bvars (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) l = bvars t (s::l)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   417
  | bvars _ l = l
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   418
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 51798
diff changeset
   419
fun get_bno l n (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
38500
d5477ee35820 more antiquotations
haftmann
parents: 36319
diff changeset
   420
  | get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t
d5477ee35820 more antiquotations
haftmann
parents: 36319
diff changeset
   421
  | get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
d5477ee35820 more antiquotations
haftmann
parents: 36319
diff changeset
   422
  | get_bno l n (Const(@{const_name mem},_) $ t $ _) = get_bno l n t
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   423
  | get_bno l n (t $ s) = get_bno l n t
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   424
  | get_bno l n (Bound m) = (m-length(l),n)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   425
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   426
(* Not a great way of identifying induction hypothesis! *)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59499
diff changeset
   427
fun could_IH x = Term.could_unify(x,hd (Thm.prems_of @{thm rcallT})) orelse
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59499
diff changeset
   428
                 Term.could_unify(x,hd (Thm.prems_of @{thm rcall2T})) orelse
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59499
diff changeset
   429
                 Term.could_unify(x,hd (Thm.prems_of @{thm rcall3T}))
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   430
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   431
fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   432
  let val bvs = bvars Bi []
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 32283
diff changeset
   433
      val ihs = filter could_IH (Logic.strip_assums_hyp Bi)
59755
f8d164ab0dc1 more position information;
wenzelm
parents: 59582
diff changeset
   434
      val rnames = map (fn x =>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   435
                    let val (a,b) = get_bno [] 0 x
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41526
diff changeset
   436
                    in (nth bvs a, b) end) ihs
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   437
      fun try_IHs [] = no_tac
59755
f8d164ab0dc1 more position information;
wenzelm
parents: 59582
diff changeset
   438
        | try_IHs ((x,y)::xs) =
f8d164ab0dc1 more position information;
wenzelm
parents: 59582
diff changeset
   439
            tac [((("g", 0), Position.none), x)] (nth rls (y - 1)) i ORELSE (try_IHs xs)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   440
  in try_IHs rnames end)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   441
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   442
fun is_rigid_prog t =
58976
b38a54bbfbd6 tuned whitespace;
wenzelm
parents: 58975
diff changeset
   443
  (case (Logic.strip_assums_concl t) of
b38a54bbfbd6 tuned whitespace;
wenzelm
parents: 58975
diff changeset
   444
    (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) =>
b38a54bbfbd6 tuned whitespace;
wenzelm
parents: 58975
diff changeset
   445
      null (Term.add_vars a [])
b38a54bbfbd6 tuned whitespace;
wenzelm
parents: 58975
diff changeset
   446
  | _ => false)
b38a54bbfbd6 tuned whitespace;
wenzelm
parents: 58975
diff changeset
   447
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   448
in
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   449
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   450
fun rcall_tac ctxt i =
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
   451
  let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps [] rl i THEN assume_tac ctxt i
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   452
  in IHinst tac @{thms rcallTs} i end
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58977
diff changeset
   453
  THEN eresolve_tac ctxt @{thms rcall_lemmas} i
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   454
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58889
diff changeset
   455
fun raw_step_tac ctxt prems i =
59499
14095f771781 misc tuning;
wenzelm
parents: 59498
diff changeset
   456
  assume_tac ctxt i ORELSE
14095f771781 misc tuning;
wenzelm
parents: 59498
diff changeset
   457
  resolve_tac ctxt (prems @ type_rls) i ORELSE
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58889
diff changeset
   458
  rcall_tac ctxt i ORELSE
59499
14095f771781 misc tuning;
wenzelm
parents: 59498
diff changeset
   459
  ematch_tac ctxt @{thms SubtypeE} i ORELSE
14095f771781 misc tuning;
wenzelm
parents: 59498
diff changeset
   460
  match_tac ctxt @{thms SubtypeI} i
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   461
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   462
fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
58976
b38a54bbfbd6 tuned whitespace;
wenzelm
parents: 58975
diff changeset
   463
    if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   464
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   465
fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   466
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   467
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   468
(*** Clean up Correctness Condictions ***)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   469
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   470
fun clean_ccs_tac ctxt =
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
   471
  let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps [] rl i THEN assume_tac ctxt i in
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   472
    TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58977
diff changeset
   473
      eresolve_tac ctxt ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 47966
diff changeset
   474
      hyp_subst_tac ctxt))
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   475
  end
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   476
27221
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   477
fun gen_ccs_tac ctxt rls i =
31328dc30196 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 27208
diff changeset
   478
  SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
   479
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   480
end
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   481
\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   482
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   483
method_setup typechk = \<open>
58971
8c9a319821b3 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   484
  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (typechk_tac ctxt ths))
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   485
\<close>
58971
8c9a319821b3 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   486
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   487
method_setup clean_ccs = \<open>
58971
8c9a319821b3 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   488
  Scan.succeed (SIMPLE_METHOD o clean_ccs_tac)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   489
\<close>
58971
8c9a319821b3 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   490
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   491
method_setup gen_ccs = \<open>
58971
8c9a319821b3 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   492
  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (gen_ccs_tac ctxt ths))
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   493
\<close>
58971
8c9a319821b3 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   494
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   495
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   496
subsection \<open>Evaluation\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   497
57945
cacb00a569e0 prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents: 57521
diff changeset
   498
named_theorems eval "evaluation rules"
cacb00a569e0 prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents: 57521
diff changeset
   499
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   500
ML \<open>
32282
853ef99c04cc FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
wenzelm
parents: 32211
diff changeset
   501
fun eval_tac ths =
57945
cacb00a569e0 prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents: 57521
diff changeset
   502
  Subgoal.FOCUS_PREMS (fn {context = ctxt, prems, ...} =>
cacb00a569e0 prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents: 57521
diff changeset
   503
    let val eval_rules = Named_Theorems.get ctxt @{named_theorems eval}
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58977
diff changeset
   504
    in DEPTH_SOLVE_1 (resolve_tac ctxt (ths @ prems @ rev eval_rules) 1) end)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   505
\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   506
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   507
method_setup eval = \<open>
47432
e1576d13e933 more standard method setup;
wenzelm
parents: 45294
diff changeset
   508
  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   509
\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   510
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   511
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   512
lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   513
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   514
lemma applyV [eval]:
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   515
  assumes "f \<longlongrightarrow> lam x. b(x)"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   516
    and "b(a) \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   517
  shows "f ` a \<longlongrightarrow> c"
41526
54b4686704af eliminated global prems;
wenzelm
parents: 38500
diff changeset
   518
  unfolding apply_def by (eval assms)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   519
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   520
lemma letV:
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   521
  assumes 1: "t \<longlongrightarrow> a"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   522
    and 2: "f(a) \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   523
  shows "let x be t in f(x) \<longlongrightarrow> c"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   524
  apply (unfold let_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   525
  apply (rule 1 [THEN canonical])
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   526
  apply (tactic \<open>
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58977
diff changeset
   527
    REPEAT (DEPTH_SOLVE_1 (resolve_tac @{context} (@{thms assms} @ @{thms eval_rls}) 1 ORELSE
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   528
      eresolve_tac @{context} @{thms substitute} 1))\<close>)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   529
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   530
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   531
lemma fixV: "f(fix(f)) \<longlongrightarrow> c \<Longrightarrow> fix(f) \<longlongrightarrow> c"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   532
  apply (unfold fix_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   533
  apply (rule applyV)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   534
   apply (rule lamV)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   535
  apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   536
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   537
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   538
lemma letrecV:
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   539
  "h(t,\<lambda>y. letrec g x be h(x,g) in g(y)) \<longlongrightarrow> c \<Longrightarrow>  
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   540
                 letrec g x be h(x,g) in g(t) \<longlongrightarrow> c"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   541
  apply (unfold letrec_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   542
  apply (assumption | rule fixV applyV  lamV)+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   543
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   544
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   545
lemmas [eval] = letV letrecV fixV
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   546
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   547
lemma V_rls [eval]:
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   548
  "true \<longlongrightarrow> true"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   549
  "false \<longlongrightarrow> false"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   550
  "\<And>b c t u. \<lbrakk>b\<longlongrightarrow>true; t\<longlongrightarrow>c\<rbrakk> \<Longrightarrow> if b then t else u \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   551
  "\<And>b c t u. \<lbrakk>b\<longlongrightarrow>false; u\<longlongrightarrow>c\<rbrakk> \<Longrightarrow> if b then t else u \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   552
  "\<And>a b. <a,b> \<longlongrightarrow> <a,b>"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   553
  "\<And>a b c t h. \<lbrakk>t \<longlongrightarrow> <a,b>; h(a,b) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> split(t,h) \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   554
  "zero \<longlongrightarrow> zero"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   555
  "\<And>n. succ(n) \<longlongrightarrow> succ(n)"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   556
  "\<And>c n t u. \<lbrakk>n \<longlongrightarrow> zero; t \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> ncase(n,t,u) \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   557
  "\<And>c n t u x. \<lbrakk>n \<longlongrightarrow> succ(x); u(x) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> ncase(n,t,u) \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   558
  "\<And>c n t u. \<lbrakk>n \<longlongrightarrow> zero; t \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> nrec(n,t,u) \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   559
  "\<And>c n t u x. \<lbrakk>n\<longlongrightarrow>succ(x); u(x,nrec(x,t,u))\<longlongrightarrow>c\<rbrakk> \<Longrightarrow> nrec(n,t,u)\<longlongrightarrow>c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   560
  "[] \<longlongrightarrow> []"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   561
  "\<And>h t. h$t \<longlongrightarrow> h$t"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   562
  "\<And>c l t u. \<lbrakk>l \<longlongrightarrow> []; t \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> lcase(l,t,u) \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   563
  "\<And>c l t u x xs. \<lbrakk>l \<longlongrightarrow> x$xs; u(x,xs) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> lcase(l,t,u) \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   564
  "\<And>c l t u. \<lbrakk>l \<longlongrightarrow> []; t \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> lrec(l,t,u) \<longlongrightarrow> c"
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   565
  "\<And>c l t u x xs. \<lbrakk>l\<longlongrightarrow>x$xs; u(x,xs,lrec(xs,t,u))\<longlongrightarrow>c\<rbrakk> \<Longrightarrow> lrec(l,t,u)\<longlongrightarrow>c"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   566
  unfolding data_defs by eval+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   567
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   568
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   569
subsection \<open>Factorial\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   570
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   571
schematic_goal
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   572
  "letrec f n be ncase(n,succ(zero),\<lambda>x. nrec(n,zero,\<lambda>y g. nrec(f(x),g,\<lambda>z h. succ(h))))  
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   573
   in f(succ(succ(zero))) \<longlongrightarrow> ?a"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   574
  by eval
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   575
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   576
schematic_goal
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   577
  "letrec f n be ncase(n,succ(zero),\<lambda>x. nrec(n,zero,\<lambda>y g. nrec(f(x),g,\<lambda>z h. succ(h))))  
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   578
   in f(succ(succ(succ(zero)))) \<longlongrightarrow> ?a"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   579
  by eval
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   580
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   581
subsection \<open>Less Than Or Equal\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   582
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   583
schematic_goal
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   584
  "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   585
   in f(<succ(zero), succ(zero)>) \<longlongrightarrow> ?a"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   586
  by eval
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   587
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   588
schematic_goal
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   589
  "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   590
   in f(<succ(zero), succ(succ(succ(succ(zero))))>) \<longlongrightarrow> ?a"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   591
  by eval
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   592
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   593
schematic_goal
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   594
  "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   595
   in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) \<longlongrightarrow> ?a"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   596
  by eval
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   597
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   598
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   599
subsection \<open>Reverse\<close>
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   600
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   601
schematic_goal
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   602
  "letrec id l be lcase(l,[],\<lambda>x xs. x$id(xs))  
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   603
   in id(zero$succ(zero)$[]) \<longlongrightarrow> ?a"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   604
  by eval
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   605
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   606
schematic_goal
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58976
diff changeset
   607
  "letrec rev l be lcase(l,[],\<lambda>x xs. lrec(rev(xs),x$[],\<lambda>y ys g. y$g))  
61966
e90c42077767 more symbols;
wenzelm
parents: 61337
diff changeset
   608
   in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) \<longlongrightarrow> ?a"
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   609
  by eval
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   610
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   611
end