src/ZF/UNITY/GenPrefix.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46953 2b6e55924af3
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26060
diff changeset
     1
(*  Title:      ZF/UNITY/GenPrefix.thy
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
d9320fb0a570 New files
ehmety
parents:
diff changeset
     3
    Copyright   2001  University of Cambridge
d9320fb0a570 New files
ehmety
parents:
diff changeset
     4
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26060
diff changeset
     5
<xs,ys>:gen_prefix(r)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26060
diff changeset
     6
  if ys = xs' @ zs where length(xs) = length(xs')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26060
diff changeset
     7
  and corresponding elements of xs, xs' are pairwise related by r
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
     8
d9320fb0a570 New files
ehmety
parents:
diff changeset
     9
Based on Lex/Prefix
d9320fb0a570 New files
ehmety
parents:
diff changeset
    10
*)
d9320fb0a570 New files
ehmety
parents:
diff changeset
    11
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    12
header{*Charpentier's Generalized Prefix Relation*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    13
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    14
theory GenPrefix
26060
cd89870aa92f imports Main;
wenzelm
parents: 26056
diff changeset
    15
imports Main
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    16
begin
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    17
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    18
definition (*really belongs in ZF/Trancl*)
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    19
  part_order :: "[i, i] => o"  where
14055
a3f592e3f4bd Further tweaks of ZF/UNITY
paulson
parents: 14046
diff changeset
    20
  "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
a3f592e3f4bd Further tweaks of ZF/UNITY
paulson
parents: 14046
diff changeset
    21
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    22
consts
d9320fb0a570 New files
ehmety
parents:
diff changeset
    23
  gen_prefix :: "[i, i] => i"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    24
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    25
inductive
d9320fb0a570 New files
ehmety
parents:
diff changeset
    26
  (* Parameter A is the domain of zs's elements *)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    27
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    28
  domains "gen_prefix(A, r)" \<subseteq> "list(A)*list(A)"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    29
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    30
  intros
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    31
    Nil:     "<[],[]>:gen_prefix(A, r)"
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    32
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    33
    prepend: "[| <xs,ys>:gen_prefix(A, r);  <x,y>:r; x \<in> A; y \<in> A |]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26060
diff changeset
    34
              ==> <Cons(x,xs), Cons(y,ys)>: gen_prefix(A, r)"
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    35
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    36
    append:  "[| <xs,ys>:gen_prefix(A, r); zs:list(A) |]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26060
diff changeset
    37
              ==> <xs, ys@zs>:gen_prefix(A, r)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    38
    type_intros app_type list.Nil list.Cons
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    39
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    40
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    41
  prefix :: "i=>i"  where
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    42
  "prefix(A) == gen_prefix(A, id(A))"
d9320fb0a570 New files
ehmety
parents:
diff changeset
    43
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    44
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    45
  strict_prefix :: "i=>i"  where
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    46
  "strict_prefix(A) == prefix(A) - id(list(A))"
d9320fb0a570 New files
ehmety
parents:
diff changeset
    47
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    48
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    49
(* less or equal and greater or equal over prefixes *)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    50
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    51
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    52
  pfixLe :: "[i, i] => o"  (infixl "pfixLe" 50)  where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    53
  "xs pfixLe ys == <xs, ys>:gen_prefix(nat, Le)"
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    54
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    55
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    56
  pfixGe :: "[i, i] => o"  (infixl "pfixGe" 50)  where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    57
  "xs pfixGe ys == <xs, ys>:gen_prefix(nat, Ge)"
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
    58
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    59
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    60
lemma reflD:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    61
 "[| refl(A, r); x \<in> A |] ==> <x,x>:r"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    62
apply (unfold refl_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    63
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    64
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    65
(*** preliminary lemmas ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    66
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    67
lemma Nil_gen_prefix: "xs \<in> list(A) ==> <[], xs> \<in> gen_prefix(A, r)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    68
by (drule gen_prefix.append [OF gen_prefix.Nil], simp)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    69
declare Nil_gen_prefix [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    70
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    71
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    72
lemma gen_prefix_length_le: "<xs,ys> \<in> gen_prefix(A, r) ==> length(xs) \<le> length(ys)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    73
apply (erule gen_prefix.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    74
apply (subgoal_tac [3] "ys \<in> list (A) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    75
apply (auto dest: gen_prefix.dom_subset [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    76
            intro: le_trans simp add: length_app)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    77
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    78
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    79
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    80
lemma Cons_gen_prefix_aux:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    81
  "[| <xs', ys'> \<in> gen_prefix(A, r) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    82
   ==> (\<forall>x xs. x \<in> A \<longrightarrow> xs'= Cons(x,xs) \<longrightarrow>
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    83
       (\<exists>y ys. y \<in> A & ys' = Cons(y,ys) &
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    84
       <x,y>:r & <xs, ys> \<in> gen_prefix(A, r)))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    85
apply (erule gen_prefix.induct)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    86
prefer 3 apply (force intro: gen_prefix.append, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    87
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    88
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    89
lemma Cons_gen_prefixE:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    90
  "[| <Cons(x,xs), zs> \<in> gen_prefix(A, r);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    91
    !!y ys. [|zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r;
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    92
      <xs,ys> \<in> gen_prefix(A, r) |] ==> P |] ==> P"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    93
apply (frule gen_prefix.dom_subset [THEN subsetD], auto)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    94
apply (blast dest: Cons_gen_prefix_aux)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    95
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    96
declare Cons_gen_prefixE [elim!]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
    97
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    98
lemma Cons_gen_prefix_Cons:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
    99
"(<Cons(x,xs),Cons(y,ys)> \<in> gen_prefix(A, r))
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   100
  \<longleftrightarrow> (x \<in> A & y \<in> A & <x,y>:r & <xs,ys> \<in> gen_prefix(A, r))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   101
apply (auto intro: gen_prefix.prepend)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   102
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   103
declare Cons_gen_prefix_Cons [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   104
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   105
(** Monotonicity of gen_prefix **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   106
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   107
lemma gen_prefix_mono2: "r<=s ==> gen_prefix(A, r) \<subseteq> gen_prefix(A, s)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   108
apply clarify
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   109
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   110
apply (erule rev_mp)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   111
apply (erule gen_prefix.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   112
apply (auto intro: gen_prefix.append)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   113
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   114
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   115
lemma gen_prefix_mono1: "A<=B ==>gen_prefix(A, r) \<subseteq> gen_prefix(B, r)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   116
apply clarify
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   117
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   118
apply (erule rev_mp)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   119
apply (erule_tac P = "y \<in> list (A) " in rev_mp)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   120
apply (erule_tac P = "xa \<in> list (A) " in rev_mp)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   121
apply (erule gen_prefix.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   122
apply (simp (no_asm_simp))
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   123
apply clarify
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   124
apply (erule ConsE)+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   125
apply (auto dest: gen_prefix.dom_subset [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   126
            intro: gen_prefix.append list_mono [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   127
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   128
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   129
lemma gen_prefix_mono: "[| A \<subseteq> B; r \<subseteq> s |] ==> gen_prefix(A, r) \<subseteq> gen_prefix(B, s)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   130
apply (rule subset_trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   131
apply (rule gen_prefix_mono1)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   132
apply (rule_tac [2] gen_prefix_mono2, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   133
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   134
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   135
(*** gen_prefix order ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   136
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   137
(* reflexivity *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   138
lemma refl_gen_prefix: "refl(A, r) ==> refl(list(A), gen_prefix(A, r))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   139
apply (unfold refl_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   140
apply (induct_tac "x", auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   141
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   142
declare refl_gen_prefix [THEN reflD, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   143
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   144
(* Transitivity *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   145
(* A lemma for proving gen_prefix_trans_comp *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   146
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   147
lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   148
   \<forall>zs. <xs @ ys, zs> \<in> gen_prefix(A, r) \<longrightarrow> <xs, zs>: gen_prefix(A, r)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   149
apply (erule list.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   150
apply (auto dest: gen_prefix.dom_subset [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   151
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   152
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   153
(* Lemma proving transitivity and more*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   154
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   155
lemma gen_prefix_trans_comp [rule_format (no_asm)]:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   156
     "<x, y>: gen_prefix(A, r) ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   157
   (\<forall>z \<in> list(A). <y,z> \<in> gen_prefix(A, s)\<longrightarrow><x, z> \<in> gen_prefix(A, s O r))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   158
apply (erule gen_prefix.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   159
apply (auto elim: ConsE simp add: Nil_gen_prefix)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   160
apply (subgoal_tac "ys \<in> list (A) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   161
prefer 2 apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   162
apply (drule_tac xs = ys and r = s in append_gen_prefix, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   163
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   164
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   165
lemma trans_comp_subset: "trans(r) ==> r O r \<subseteq> r"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   166
by (auto dest: transD)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   167
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   168
lemma trans_gen_prefix: "trans(r) ==> trans(gen_prefix(A,r))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   169
apply (simp (no_asm) add: trans_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   170
apply clarify
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   171
apply (rule trans_comp_subset [THEN gen_prefix_mono2, THEN subsetD], assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   172
apply (rule gen_prefix_trans_comp)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   173
apply (auto dest: gen_prefix.dom_subset [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   174
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   175
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   176
lemma trans_on_gen_prefix:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   177
 "trans(r) ==> trans[list(A)](gen_prefix(A, r))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   178
apply (drule_tac A = A in trans_gen_prefix)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   179
apply (unfold trans_def trans_on_def, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   180
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   181
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   182
lemma prefix_gen_prefix_trans:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   183
    "[| <x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   184
      ==>  <x, z> \<in> gen_prefix(A, r)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   185
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   186
apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in right_comp_id [THEN subst])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   187
apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   188
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   189
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   190
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   191
lemma gen_prefix_prefix_trans:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   192
"[| <x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   193
  ==>  <x, z> \<in> gen_prefix(A, r)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   194
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   195
apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in left_comp_id [THEN subst])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   196
apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   197
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   198
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   199
(** Antisymmetry **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   200
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   201
lemma nat_le_lemma [rule_format]: "n \<in> nat ==> \<forall>b \<in> nat. n #+ b \<le> n \<longrightarrow> b = 0"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   202
by (induct_tac "n", auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   203
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   204
lemma antisym_gen_prefix: "antisym(r) ==> antisym(gen_prefix(A, r))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   205
apply (simp (no_asm) add: antisym_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   206
apply (rule impI [THEN allI, THEN allI])
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   207
apply (erule gen_prefix.induct, blast)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   208
apply (simp add: antisym_def, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   209
txt{*append case is hardest*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   210
apply clarify
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   211
apply (subgoal_tac "length (zs) = 0")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   212
apply (subgoal_tac "ys \<in> list (A) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   213
prefer 2 apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   214
apply (drule_tac psi = "<ys @ zs, xs> \<in> gen_prefix (A,r) " in asm_rl)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   215
apply simp
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   216
apply (subgoal_tac "length (ys @ zs) = length (ys) #+ length (zs) &ys \<in> list (A) &xs \<in> list (A) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   217
prefer 2 apply (blast intro: length_app dest: gen_prefix.dom_subset [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   218
apply (drule gen_prefix_length_le)+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   219
apply clarify
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   220
apply simp
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   221
apply (drule_tac j = "length (xs) " in le_trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   222
apply blast
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   223
apply (auto intro: nat_le_lemma)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   224
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   225
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   226
(*** recursion equations ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   227
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   228
lemma gen_prefix_Nil: "xs \<in> list(A) ==> <xs, []> \<in> gen_prefix(A,r) \<longleftrightarrow> (xs = [])"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   229
by (induct_tac "xs", auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   230
declare gen_prefix_Nil [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   231
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   232
lemma same_gen_prefix_gen_prefix:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   233
 "[| refl(A, r);  xs \<in> list(A) |] ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   234
    <xs@ys, xs@zs>: gen_prefix(A, r) \<longleftrightarrow> <ys,zs> \<in> gen_prefix(A, r)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   235
apply (unfold refl_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   236
apply (induct_tac "xs")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   237
apply (simp_all (no_asm_simp))
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   238
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   239
declare same_gen_prefix_gen_prefix [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   240
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   241
lemma gen_prefix_Cons: "[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   242
    <xs, Cons(y,ys)> \<in> gen_prefix(A,r)  \<longleftrightarrow>
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   243
      (xs=[] | (\<exists>z zs. xs=Cons(z,zs) & z \<in> A & <z,y>:r & <zs,ys> \<in> gen_prefix(A,r)))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   244
apply (induct_tac "xs", auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   245
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   246
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   247
lemma gen_prefix_take_append: "[| refl(A,r);  <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   248
      ==>  <xs@zs, take(length(xs), ys) @ zs> \<in> gen_prefix(A, r)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   249
apply (erule gen_prefix.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   250
apply (simp (no_asm_simp))
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   251
apply (frule_tac [!] gen_prefix.dom_subset [THEN subsetD], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   252
apply (frule gen_prefix_length_le)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   253
apply (subgoal_tac "take (length (xs), ys) \<in> list (A) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   254
apply (simp_all (no_asm_simp) add: diff_is_0_iff [THEN iffD2] take_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   255
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   256
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   257
lemma gen_prefix_append_both: "[| refl(A, r);  <xs,ys> \<in> gen_prefix(A,r);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   258
         length(xs) = length(ys); zs \<in> list(A) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   259
      ==>  <xs@zs, ys @ zs> \<in> gen_prefix(A, r)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   260
apply (drule_tac zs = zs in gen_prefix_take_append, assumption+)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   261
apply (subgoal_tac "take (length (xs), ys) =ys")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   262
apply (auto intro!: take_all dest: gen_prefix.dom_subset [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   263
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   264
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   265
(*NOT suitable for rewriting since [y] has the form y#ys*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   266
lemma append_cons_conv: "xs \<in> list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   267
by (auto simp add: app_assoc)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   268
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   269
lemma append_one_gen_prefix_lemma [rule_format]:
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   270
     "[| <xs,ys> \<in> gen_prefix(A, r);  refl(A, r) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   271
      ==> length(xs) < length(ys) \<longrightarrow>
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   272
          <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   273
apply (erule gen_prefix.induct, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   274
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   275
apply (simp_all add: length_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   276
(* Append case is hardest *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   277
apply (frule gen_prefix_length_le [THEN le_iff [THEN iffD1]])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   278
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   279
apply (subgoal_tac "length (xs) :nat&length (ys) :nat &length (zs) :nat")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   280
prefer 2 apply (blast intro: length_type, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   281
apply (simp_all add: nth_append length_type length_app)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   282
apply (rule conjI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   283
apply (blast intro: gen_prefix.append)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   284
apply (erule_tac V = "length (xs) < length (ys) \<longrightarrow>?u" in thin_rl)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   285
apply (erule_tac a = zs in list.cases, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   286
apply (rule_tac P1 = "%x. <?u (x), ?v>:?w" in nat_diff_split [THEN iffD2])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   287
apply auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   288
apply (simplesubst append_cons_conv)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   289
apply (rule_tac [2] gen_prefix.append)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   290
apply (auto elim: ConsE simp add: gen_prefix_append_both)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   291
done
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   292
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   293
lemma append_one_gen_prefix: "[| <xs,ys>: gen_prefix(A, r);  length(xs) < length(ys);  refl(A, r) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   294
      ==> <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   295
apply (blast intro: append_one_gen_prefix_lemma)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   296
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   297
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   298
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   299
(** Proving the equivalence with Charpentier's definition **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   300
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   301
lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) ==>
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   302
  \<forall>ys \<in> list(A). \<forall>i \<in> nat. i < length(xs)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   303
          \<longrightarrow> <xs, ys>: gen_prefix(A, r) \<longrightarrow> <nth(i, xs), nth(i, ys)>:r"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   304
apply (induct_tac "xs", simp, clarify)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   305
apply simp
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   306
apply (erule natE, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   307
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   308
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   309
lemma gen_prefix_imp_nth: "[| <xs,ys> \<in> gen_prefix(A,r); i < length(xs)|]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   310
      ==> <nth(i, xs), nth(i, ys)>:r"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   311
apply (cut_tac A = A in gen_prefix.dom_subset)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   312
apply (rule gen_prefix_imp_nth_lemma)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   313
apply (auto simp add: lt_nat_in_nat)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   314
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   315
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   316
lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) ==>
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   317
  \<forall>ys \<in> list(A). length(xs) \<le> length(ys)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   318
      \<longrightarrow> (\<forall>i. i < length(xs) \<longrightarrow> <nth(i, xs), nth(i,ys)>:r)
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   319
      \<longrightarrow> <xs, ys> \<in> gen_prefix(A, r)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   320
apply (induct_tac "xs")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   321
apply (simp_all (no_asm_simp))
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   322
apply clarify
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   323
apply (erule_tac a = ys in list.cases, simp)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   324
apply (force intro!: nat_0_le simp add: lt_nat_in_nat)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   325
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   326
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   327
lemma gen_prefix_iff_nth: "(<xs,ys> \<in> gen_prefix(A,r)) \<longleftrightarrow>
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   328
      (xs \<in> list(A) & ys \<in> list(A) & length(xs) \<le> length(ys) &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   329
      (\<forall>i. i < length(xs) \<longrightarrow> <nth(i,xs), nth(i, ys)>: r))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   330
apply (rule iffI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   331
apply (frule gen_prefix.dom_subset [THEN subsetD])
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   332
apply (frule gen_prefix_length_le, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   333
apply (rule_tac [2] nth_imp_gen_prefix)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   334
apply (drule gen_prefix_imp_nth)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   335
apply (auto simp add: lt_nat_in_nat)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   336
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   337
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   338
(** prefix is a partial order: **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   339
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   340
lemma refl_prefix: "refl(list(A), prefix(A))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   341
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   342
apply (rule refl_gen_prefix)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   343
apply (auto simp add: refl_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   344
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   345
declare refl_prefix [THEN reflD, simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   346
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   347
lemma trans_prefix: "trans(prefix(A))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   348
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   349
apply (rule trans_gen_prefix)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   350
apply (auto simp add: trans_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   351
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   352
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   353
lemmas prefix_trans = trans_prefix [THEN transD]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   354
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   355
lemma trans_on_prefix: "trans[list(A)](prefix(A))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   356
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   357
apply (rule trans_on_gen_prefix)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   358
apply (auto simp add: trans_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   359
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   360
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   361
lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   362
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   363
(* Monotonicity of "set" operator WRT prefix *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   364
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   365
lemma set_of_list_prefix_mono:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   366
"<xs,ys> \<in> prefix(A) ==> set_of_list(xs) \<subseteq> set_of_list(ys)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   367
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   368
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   369
apply (erule gen_prefix.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   370
apply (subgoal_tac [3] "xs \<in> list (A) &ys \<in> list (A) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   371
prefer 4 apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   372
apply (auto simp add: set_of_list_append)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   373
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   374
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   375
(** recursion equations **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   376
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   377
lemma Nil_prefix: "xs \<in> list(A) ==> <[],xs> \<in> prefix(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   378
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   379
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   380
apply (simp (no_asm_simp) add: Nil_gen_prefix)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   381
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   382
declare Nil_prefix [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   383
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   384
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   385
lemma prefix_Nil: "<xs, []> \<in> prefix(A) \<longleftrightarrow> (xs = [])"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   386
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   387
apply (unfold prefix_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   388
apply (frule gen_prefix.dom_subset [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   389
apply (drule_tac psi = "<xs, []> \<in> gen_prefix (A, id (A))" in asm_rl)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   390
apply (simp add: gen_prefix_Nil)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   391
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   392
declare prefix_Nil [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   393
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   394
lemma Cons_prefix_Cons:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   395
"<Cons(x,xs), Cons(y,ys)> \<in> prefix(A) \<longleftrightarrow> (x=y & <xs,ys> \<in> prefix(A) & y \<in> A)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   396
apply (unfold prefix_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   397
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   398
declare Cons_prefix_Cons [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   399
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   400
lemma same_prefix_prefix:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   401
"xs \<in> list(A)==> <xs@ys,xs@zs> \<in> prefix(A) \<longleftrightarrow> (<ys,zs> \<in> prefix(A))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   402
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   403
apply (subgoal_tac "refl (A,id (A))")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   404
apply (simp (no_asm_simp))
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   405
apply (auto simp add: refl_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   406
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   407
declare same_prefix_prefix [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   408
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   409
lemma same_prefix_prefix_Nil: "xs \<in> list(A) ==> <xs@ys,xs> \<in> prefix(A) \<longleftrightarrow> (<ys,[]> \<in> prefix(A))"
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   410
apply (rule_tac P = "%x. <?u, x>:?v \<longleftrightarrow> ?w (x) " in app_right_Nil [THEN subst])
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   411
apply (rule_tac [2] same_prefix_prefix, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   412
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   413
declare same_prefix_prefix_Nil [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   414
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   415
lemma prefix_appendI:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   416
"[| <xs,ys> \<in> prefix(A); zs \<in> list(A) |] ==> <xs,ys@zs> \<in> prefix(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   417
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   418
apply (erule gen_prefix.append, assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   419
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   420
declare prefix_appendI [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   421
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   422
lemma prefix_Cons:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   423
"[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   424
  <xs,Cons(y,ys)> \<in> prefix(A) \<longleftrightarrow>
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   425
  (xs=[] | (\<exists>zs. xs=Cons(y,zs) & <zs,ys> \<in> prefix(A)))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   426
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   427
apply (auto simp add: gen_prefix_Cons)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   428
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   429
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   430
lemma append_one_prefix:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   431
  "[| <xs,ys> \<in> prefix(A); length(xs) < length(ys) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   432
  ==> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   433
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   434
apply (subgoal_tac "refl (A, id (A))")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   435
apply (simp (no_asm_simp) add: append_one_gen_prefix)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   436
apply (auto simp add: refl_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   437
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   438
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   439
lemma prefix_length_le:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   440
"<xs,ys> \<in> prefix(A) ==> length(xs) \<le> length(ys)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   441
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   442
apply (blast dest: gen_prefix_length_le)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   443
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   444
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   445
lemma prefix_type: "prefix(A)<=list(A)*list(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   446
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   447
apply (blast intro!: gen_prefix.dom_subset)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   448
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   449
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   450
lemma strict_prefix_type:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   451
"strict_prefix(A) \<subseteq> list(A)*list(A)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   452
apply (unfold strict_prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   453
apply (blast intro!: prefix_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   454
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   455
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   456
lemma strict_prefix_length_lt_aux:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   457
     "<xs,ys> \<in> prefix(A) ==> xs\<noteq>ys \<longrightarrow> length(xs) < length(ys)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   458
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   459
apply (erule gen_prefix.induct, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   460
apply (subgoal_tac [!] "ys \<in> list(A) & xs \<in> list(A)")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   461
apply (auto dest: gen_prefix.dom_subset [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   462
            simp add: length_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   463
apply (subgoal_tac "length (zs) =0")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   464
apply (drule_tac [2] not_lt_imp_le)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   465
apply (rule_tac [5] j = "length (ys) " in lt_trans2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   466
apply auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   467
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   468
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   469
lemma strict_prefix_length_lt:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   470
     "<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   471
apply (unfold strict_prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   472
apply (rule strict_prefix_length_lt_aux [THEN mp])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   473
apply (auto dest: prefix_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   474
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   475
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   476
(*Equivalence to the definition used in Lex/Prefix.thy*)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   477
lemma prefix_iff:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   478
    "<xs,zs> \<in> prefix(A) \<longleftrightarrow> (\<exists>ys \<in> list(A). zs = xs@ys) & xs \<in> list(A)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   479
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   480
apply (auto simp add: gen_prefix_iff_nth lt_nat_in_nat nth_append nth_type app_type length_app)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   481
apply (subgoal_tac "drop (length (xs), zs) \<in> list (A) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   482
apply (rule_tac x = "drop (length (xs), zs) " in bexI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   483
apply safe
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   484
 prefer 2 apply (simp add: length_type drop_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   485
apply (rule nth_equalityI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   486
apply (simp_all (no_asm_simp) add: nth_append app_type drop_type length_app length_drop)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   487
apply (rule nat_diff_split [THEN iffD2], simp_all, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   488
apply (drule_tac i = "length (zs) " in leI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   489
apply (force simp add: le_subset_iff, safe)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   490
apply (subgoal_tac "length (xs) #+ (i #- length (xs)) = i")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   491
apply (subst nth_drop)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   492
apply (simp_all (no_asm_simp) add: leI split add: nat_diff_split)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   493
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   494
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   495
lemma prefix_snoc:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   496
"[|xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   497
   <xs, ys@[y]> \<in> prefix(A) \<longleftrightarrow> (xs = ys@[y] | <xs,ys> \<in> prefix(A))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   498
apply (simp (no_asm) add: prefix_iff)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   499
apply (rule iffI, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   500
apply (erule_tac xs = ysa in rev_list_elim, simp)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   501
apply (simp add: app_type app_assoc [symmetric])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   502
apply (auto simp add: app_assoc app_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   503
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   504
declare prefix_snoc [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   505
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   506
lemma prefix_append_iff [rule_format]: "zs \<in> list(A) ==> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A).
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   507
   (<xs, ys@zs> \<in> prefix(A)) \<longleftrightarrow>
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   508
  (<xs,ys> \<in> prefix(A) | (\<exists>us. xs = ys@us & <us,zs> \<in> prefix(A)))"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   509
apply (erule list_append_induct, force, clarify)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   510
apply (rule iffI)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   511
apply (simp add: add: app_assoc [symmetric])
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   512
apply (erule disjE)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   513
apply (rule disjI2)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   514
apply (rule_tac x = "y @ [x]" in exI)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   515
apply (simp add: add: app_assoc [symmetric], force+)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   516
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   517
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   518
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   519
(*Although the prefix ordering is not linear, the prefixes of a list
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   520
  are linearly ordered.*)
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   521
lemma common_prefix_linear_lemma [rule_format]: "[| zs \<in> list(A); xs \<in> list(A); ys \<in> list(A) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   522
   ==> <xs, zs> \<in> prefix(A) \<longrightarrow> <ys,zs> \<in> prefix(A)
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   523
  \<longrightarrow><xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   524
apply (erule list_append_induct, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   525
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   526
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   527
lemma common_prefix_linear: "[|<xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   528
      ==> <xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   529
apply (cut_tac prefix_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   530
apply (blast del: disjCI intro: common_prefix_linear_lemma)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   531
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   532
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   533
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   534
(*** pfixLe, pfixGe \<in> properties inherited from the translations ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   535
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   536
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   537
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   538
(** pfixLe **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   539
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   540
lemma refl_Le: "refl(nat,Le)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   541
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   542
apply (unfold refl_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   543
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   544
declare refl_Le [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   545
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   546
lemma antisym_Le: "antisym(Le)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   547
apply (unfold antisym_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   548
apply (auto intro: le_anti_sym)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   549
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   550
declare antisym_Le [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   551
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   552
lemma trans_on_Le: "trans[nat](Le)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   553
apply (unfold trans_on_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   554
apply (blast intro: le_trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   555
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   556
declare trans_on_Le [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   557
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   558
lemma trans_Le: "trans(Le)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   559
apply (unfold trans_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   560
apply (blast intro: le_trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   561
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   562
declare trans_Le [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   563
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   564
lemma part_order_Le: "part_order(nat,Le)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   565
by (unfold part_order_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   566
declare part_order_Le [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   567
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   568
lemma pfixLe_refl: "x \<in> list(nat) ==> x pfixLe x"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   569
by (blast intro: refl_gen_prefix [THEN reflD] refl_Le)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   570
declare pfixLe_refl [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   571
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   572
lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   573
by (blast intro: trans_gen_prefix [THEN transD] trans_Le)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   574
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   575
lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   576
by (blast intro: antisym_gen_prefix [THEN antisymE] antisym_Le)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   577
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   578
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   579
lemma prefix_imp_pfixLe:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   580
"<xs,ys>:prefix(nat)==> xs pfixLe ys"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   581
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   582
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   583
apply (rule gen_prefix_mono [THEN subsetD], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   584
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   585
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   586
lemma refl_Ge: "refl(nat, Ge)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   587
by (unfold refl_def Ge_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   588
declare refl_Ge [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   589
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   590
lemma antisym_Ge: "antisym(Ge)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   591
apply (unfold antisym_def Ge_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   592
apply (auto intro: le_anti_sym)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   593
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   594
declare antisym_Ge [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   595
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   596
lemma trans_Ge: "trans(Ge)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   597
apply (unfold trans_def Ge_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   598
apply (auto intro: le_trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   599
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   600
declare trans_Ge [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   601
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   602
lemma pfixGe_refl: "x \<in> list(nat) ==> x pfixGe x"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   603
by (blast intro: refl_gen_prefix [THEN reflD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   604
declare pfixGe_refl [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   605
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   606
lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   607
by (blast intro: trans_gen_prefix [THEN transD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   608
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   609
lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   610
by (blast intro: antisym_gen_prefix [THEN antisymE])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   611
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   612
lemma prefix_imp_pfixGe:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   613
  "<xs,ys>:prefix(nat) ==> xs pfixGe ys"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   614
apply (unfold prefix_def Ge_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   615
apply (rule gen_prefix_mono [THEN subsetD], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   616
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   617
(* Added by Sidi \<in> prefix and take *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   618
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   619
lemma prefix_imp_take:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   620
"<xs, ys> \<in> prefix(A) ==> xs = take(length(xs), ys)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   621
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   622
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   623
apply (erule gen_prefix.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   624
apply (subgoal_tac [3] "length (xs) :nat")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   625
apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: length_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   626
apply (frule gen_prefix.dom_subset [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   627
apply (frule gen_prefix_length_le)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   628
apply (auto simp add: take_append)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   629
apply (subgoal_tac "length (xs) #- length (ys) =0")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   630
apply (simp_all (no_asm_simp) add: diff_is_0_iff)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   631
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   632
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   633
lemma prefix_length_equal: "[|<xs,ys> \<in> prefix(A); length(xs)=length(ys)|] ==> xs = ys"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   634
apply (cut_tac A = A in prefix_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   635
apply (drule subsetD, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   636
apply (drule prefix_imp_take)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   637
apply (erule trans, simp)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   638
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   639
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   640
lemma prefix_length_le_equal: "[|<xs,ys> \<in> prefix(A); length(ys) \<le> length(xs)|] ==> xs = ys"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   641
by (blast intro: prefix_length_equal le_anti_sym prefix_length_le)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   642
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   643
lemma take_prefix [rule_format]: "xs \<in> list(A) ==> \<forall>n \<in> nat. <take(n, xs), xs> \<in> prefix(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   644
apply (unfold prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   645
apply (erule list.induct, simp, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   646
apply (erule natE, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   647
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   648
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   649
lemma prefix_take_iff: "<xs,ys> \<in> prefix(A) \<longleftrightarrow> (xs=take(length(xs), ys) & xs \<in> list(A) & ys \<in> list(A))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   650
apply (rule iffI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   651
apply (frule prefix_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   652
apply (blast intro: prefix_imp_take, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   653
apply (erule ssubst)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   654
apply (blast intro: take_prefix length_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   655
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   656
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   657
lemma prefix_imp_nth: "[| <xs,ys> \<in> prefix(A); i < length(xs)|] ==> nth(i,xs) = nth(i,ys)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   658
by (auto dest!: gen_prefix_imp_nth simp add: prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   659
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   660
lemma nth_imp_prefix:
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   661
     "[|xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys);
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   662
        !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   663
      ==> <xs,ys> \<in> prefix(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   664
apply (auto simp add: prefix_def nth_imp_gen_prefix)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   665
apply (auto intro!: nth_imp_gen_prefix simp add: prefix_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   666
apply (blast intro: nth_type lt_trans2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   667
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   668
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   669
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 15634
diff changeset
   670
lemma length_le_prefix_imp_prefix: "[|length(xs) \<le> length(ys);
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   671
        <xs,zs> \<in> prefix(A); <ys,zs> \<in> prefix(A)|] ==> <xs,ys> \<in> prefix(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   672
apply (cut_tac A = A in prefix_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   673
apply (rule nth_imp_prefix, blast, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   674
 apply assumption
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   675
apply (rule_tac b = "nth (i,zs)" in trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   676
 apply (blast intro: prefix_imp_nth)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   677
apply (blast intro: sym prefix_imp_nth prefix_length_le lt_trans2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   678
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14055
diff changeset
   679
12197
d9320fb0a570 New files
ehmety
parents:
diff changeset
   680
end