src/HOL/Proofs/Lambda/InductTermi.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 39157 b98909faaea8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 36862
diff changeset
     1
(*  Title:      HOL/Proofs/Lambda/InductTermi.thy
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     2
    Author:     Tobias Nipkow
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     3
    Copyright   1998 TU Muenchen
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     4
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
     5
Inductive characterization of terminating lambda terms.  Goes back to
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
     6
Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.  Also
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
     7
rediscovered by Matthes and Joachimski.
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     8
*)
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     9
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    10
header {* Inductive characterization of terminating lambda terms *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    11
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12011
diff changeset
    12
theory InductTermi imports ListBeta begin
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
    13
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    14
subsection {* Terminating lambda terms *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    15
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    16
inductive IT :: "dB => bool"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18513
diff changeset
    17
  where
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18513
diff changeset
    18
    Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18513
diff changeset
    19
  | Lambda [intro]: "IT r ==> IT (Abs r)"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18513
diff changeset
    20
  | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    21
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    22
25972
94b15338da8d tuned document;
wenzelm
parents: 23750
diff changeset
    23
subsection {* Every term in @{text "IT"} terminates *}
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    24
9941
fe05af7ec816 renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents: 9906
diff changeset
    25
lemma double_induction_lemma [rule_format]:
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    26
  "termip beta s ==> \<forall>t. termip beta t -->
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    27
    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termip beta (Abs r \<degree> s \<degree>\<degree> ss))"
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    28
  apply (erule accp_induct)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    29
  apply (rule allI)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    30
  apply (rule impI)
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18241
diff changeset
    31
  apply (erule thin_rl)
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    32
  apply (erule accp_induct)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    33
  apply clarify
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    34
  apply (rule accp.accI)
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9762
diff changeset
    35
  apply (safe elim!: apps_betasE)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    36
    apply (blast intro: subst_preserves_beta apps_preserves_beta)
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    37
   apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    38
     dest: accp_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    39
  apply (blast dest: apps_preserves_betas)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    40
  done
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    41
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    42
lemma IT_implies_termi: "IT t ==> termip beta t"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    43
  apply (induct set: IT)
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    44
    apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]])
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 25972
diff changeset
    45
    apply (fast intro!: predicate1I)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    46
    apply (drule lists_accD)
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    47
    apply (erule accp_induct)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    48
    apply (rule accp.accI)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    49
    apply (blast dest: head_Var_reduction)
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    50
   apply (erule accp_induct)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    51
   apply (rule accp.accI)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    52
   apply blast
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    53
  apply (blast intro: double_induction_lemma)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    54
  done
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    55
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    56
25972
94b15338da8d tuned document;
wenzelm
parents: 23750
diff changeset
    57
subsection {* Every terminating term is in @{text "IT"} *}
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    58
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    59
declare Var_apps_neq_Abs_apps [symmetric, simp]
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    60
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11946
diff changeset
    61
lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    62
  by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    63
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    64
lemma [simp]:
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11946
diff changeset
    65
  "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    66
  by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    67
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    68
inductive_cases [elim!]:
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18513
diff changeset
    69
  "IT (Var n \<degree>\<degree> ss)"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18513
diff changeset
    70
  "IT (Abs t)"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18513
diff changeset
    71
  "IT (Abs r \<degree> s \<degree>\<degree> ts)"
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    72
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    73
theorem termi_implies_IT: "termip beta r ==> IT r"
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    74
  apply (erule accp_induct)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    75
  apply (rename_tac r)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    76
  apply (erule thin_rl)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    77
  apply (erule rev_mp)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    78
  apply simp
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    79
  apply (rule_tac t = r in Apps_dB_induct)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    80
   apply clarify
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    81
   apply (rule IT.intros)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    82
   apply clarify
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    83
   apply (drule bspec, assumption)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    84
   apply (erule mp)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    85
   apply clarify
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18513
diff changeset
    86
   apply (drule_tac r=beta in conversepI)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18513
diff changeset
    87
   apply (drule_tac r="beta^--1" in ex_step1I, assumption)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    88
   apply clarify
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    89
   apply (rename_tac us)
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11946
diff changeset
    90
   apply (erule_tac x = "Var n \<degree>\<degree> us" in allE)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    91
   apply force
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    92
   apply (rename_tac u ts)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    93
   apply (case_tac ts)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    94
    apply simp
11946
wenzelm
parents: 11639
diff changeset
    95
    apply blast
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    96
   apply (rename_tac s ss)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    97
   apply simp
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    98
   apply clarify
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
    99
   apply (rule IT.intros)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
   100
    apply (blast intro: apps_preserves_beta)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
   101
   apply (erule mp)
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
   102
   apply clarify
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
   103
   apply (rename_tac t)
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11946
diff changeset
   104
   apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE)
9716
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
   105
   apply force
9be481b4bc85 Lambda/InductTermi made new-style theory;
wenzelm
parents: 9102
diff changeset
   106
   done
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
   107
11639
wenzelm
parents: 9941
diff changeset
   108
end