src/HOL/SizeChange/Size_Change_Termination.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 25314 5eaf3e8b50a4
child 30967 b5d67f83576e
permissions -rw-r--r--
simplified method setup;
krauss@25314
     1
(*  Title:      HOL/Library/Size_Change_Termination.thy
krauss@25314
     2
    ID:         $Id$
krauss@25314
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@25314
     4
*)
krauss@25314
     5
krauss@25314
     6
header "Size-Change Termination"
krauss@25314
     7
krauss@25314
     8
theory Size_Change_Termination
krauss@25314
     9
imports Correctness Interpretation Implementation 
krauss@25314
    10
uses "sct.ML"
krauss@25314
    11
begin
krauss@25314
    12
krauss@25314
    13
subsection {* Simplifier setup *}
krauss@25314
    14
krauss@25314
    15
text {* This is needed to run the SCT algorithm in the simplifier: *}
krauss@25314
    16
krauss@25314
    17
lemma setbcomp_simps:
krauss@25314
    18
  "{x\<in>{}. P x} = {}"
krauss@25314
    19
  "{x\<in>insert y ys. P x} = (if P y then insert y {x\<in>ys. P x} else {x\<in>ys. P x})"
krauss@25314
    20
  by auto
krauss@25314
    21
krauss@25314
    22
lemma setbcomp_cong:
krauss@25314
    23
  "A = B \<Longrightarrow> (\<And>x. P x = Q x) \<Longrightarrow> {x\<in>A. P x} = {x\<in>B. Q x}"
krauss@25314
    24
  by auto
krauss@25314
    25
krauss@25314
    26
lemma cartprod_simps:
krauss@25314
    27
  "{} \<times> A = {}"
krauss@25314
    28
  "insert a A \<times> B = Pair a ` B \<union> (A \<times> B)"
krauss@25314
    29
  by (auto simp:image_def)
krauss@25314
    30
krauss@25314
    31
lemma image_simps:
krauss@25314
    32
  "fu ` {} = {}"
krauss@25314
    33
  "fu ` insert a A = insert (fu a) (fu ` A)"
krauss@25314
    34
  by (auto simp:image_def)
krauss@25314
    35
krauss@25314
    36
lemmas union_simps = 
krauss@25314
    37
  Un_empty_left Un_empty_right Un_insert_left
krauss@25314
    38
  
krauss@25314
    39
lemma subset_simps:
krauss@25314
    40
  "{} \<subseteq> B"
krauss@25314
    41
  "insert a A \<subseteq> B \<equiv> a \<in> B \<and> A \<subseteq> B"
krauss@25314
    42
  by auto 
krauss@25314
    43
krauss@25314
    44
lemma element_simps:
krauss@25314
    45
  "x \<in> {} \<equiv> False"
krauss@25314
    46
  "x \<in> insert a A \<equiv> x = a \<or> x \<in> A"
krauss@25314
    47
  by auto
krauss@25314
    48
krauss@25314
    49
lemma set_eq_simp:
krauss@25314
    50
  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" by auto
krauss@25314
    51
krauss@25314
    52
lemma ball_simps:
krauss@25314
    53
  "\<forall>x\<in>{}. P x \<equiv> True"
krauss@25314
    54
  "(\<forall>x\<in>insert a A. P x) \<equiv> P a \<and> (\<forall>x\<in>A. P x)"
krauss@25314
    55
by auto
krauss@25314
    56
krauss@25314
    57
lemma bex_simps:
krauss@25314
    58
  "\<exists>x\<in>{}. P x \<equiv> False"
krauss@25314
    59
  "(\<exists>x\<in>insert a A. P x) \<equiv> P a \<or> (\<exists>x\<in>A. P x)"
krauss@25314
    60
by auto
krauss@25314
    61
krauss@25314
    62
lemmas set_simps =
krauss@25314
    63
  setbcomp_simps
krauss@25314
    64
  cartprod_simps image_simps union_simps subset_simps
krauss@25314
    65
  element_simps set_eq_simp
krauss@25314
    66
  ball_simps bex_simps
krauss@25314
    67
krauss@25314
    68
lemma sedge_simps:
krauss@25314
    69
  "\<down> * x = \<down>"
krauss@25314
    70
  "\<Down> * x = x"
krauss@25314
    71
  by (auto simp:mult_sedge_def)
krauss@25314
    72
krauss@25314
    73
lemmas sctTest_simps =
krauss@25314
    74
  simp_thms
krauss@25314
    75
  if_True
krauss@25314
    76
  if_False
krauss@25314
    77
  nat.inject
krauss@25314
    78
  nat.distinct
krauss@25314
    79
  Pair_eq 
krauss@25314
    80
krauss@25314
    81
  grcomp_code 
krauss@25314
    82
  edges_match.simps 
krauss@25314
    83
  connect_edges.simps 
krauss@25314
    84
krauss@25314
    85
  sedge_simps
krauss@25314
    86
  sedge.distinct
krauss@25314
    87
  set_simps
krauss@25314
    88
krauss@25314
    89
  graph_mult_def 
krauss@25314
    90
  graph_leq_def
krauss@25314
    91
  dest_graph.simps
krauss@25314
    92
  graph_plus_def
krauss@25314
    93
  graph.inject
krauss@25314
    94
  graph_zero_def
krauss@25314
    95
krauss@25314
    96
  test_SCT_def
krauss@25314
    97
  mk_tcl_code
krauss@25314
    98
krauss@25314
    99
  Let_def
krauss@25314
   100
  split_conv
krauss@25314
   101
krauss@25314
   102
lemmas sctTest_congs = 
krauss@25314
   103
  if_weak_cong let_weak_cong setbcomp_cong
krauss@25314
   104
krauss@25314
   105
krauss@25314
   106
lemma SCT_Main:
krauss@25314
   107
  "finite_acg A \<Longrightarrow> test_SCT A \<Longrightarrow> SCT A"
krauss@25314
   108
  using LJA_Theorem4 SCT'_exec
krauss@25314
   109
  by auto
krauss@25314
   110
krauss@25314
   111
end