src/HOL/Library/Size_Change_Termination.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 22665 cf152ff55d16
child 23374 a2f492c599e0
permissions -rw-r--r--
tuned Proof
     1 (*  Title:      HOL/Library/Size_Change_Termination.thy
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 *)
     5 
     6 header ""
     7 
     8 theory Size_Change_Termination
     9 imports SCT_Theorem SCT_Interpretation SCT_Implementation 
    10 uses "sct.ML"
    11 begin
    12 
    13 subsection {* Simplifier setup *}
    14 
    15 text {* This is needed to run the SCT algorithm in the simplifier: *}
    16 
    17 lemma setbcomp_simps:
    18   "{x\<in>{}. P x} = {}"
    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})"
    20   by auto
    21 
    22 lemma setbcomp_cong:
    23   "A = B \<Longrightarrow> (\<And>x. P x = Q x) \<Longrightarrow> {x\<in>A. P x} = {x\<in>B. Q x}"
    24   by auto
    25 
    26 lemma cartprod_simps:
    27   "{} \<times> A = {}"
    28   "insert a A \<times> B = Pair a ` B \<union> (A \<times> B)"
    29   by (auto simp:image_def)
    30 
    31 lemma image_simps:
    32   "fu ` {} = {}"
    33   "fu ` insert a A = insert (fu a) (fu ` A)"
    34   by (auto simp:image_def)
    35 
    36 lemmas union_simps = 
    37   Un_empty_left Un_empty_right Un_insert_left
    38   
    39 lemma subset_simps:
    40   "{} \<subseteq> B"
    41   "insert a A \<subseteq> B \<equiv> a \<in> B \<and> A \<subseteq> B"
    42   by auto 
    43 
    44 lemma element_simps:
    45   "x \<in> {} \<equiv> False"
    46   "x \<in> insert a A \<equiv> x = a \<or> x \<in> A"
    47   by auto
    48 
    49 lemma set_eq_simp:
    50   "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" by auto
    51 
    52 lemma ball_simps:
    53   "\<forall>x\<in>{}. P x \<equiv> True"
    54   "(\<forall>x\<in>insert a A. P x) \<equiv> P a \<and> (\<forall>x\<in>A. P x)"
    55 by auto
    56 
    57 lemma bex_simps:
    58   "\<exists>x\<in>{}. P x \<equiv> False"
    59   "(\<exists>x\<in>insert a A. P x) \<equiv> P a \<or> (\<exists>x\<in>A. P x)"
    60 by auto
    61 
    62 lemmas set_simps =
    63   setbcomp_simps
    64   cartprod_simps image_simps union_simps subset_simps
    65   element_simps set_eq_simp
    66   ball_simps bex_simps
    67 
    68 lemma sedge_simps:
    69   "\<down> * x = \<down>"
    70   "\<Down> * x = x"
    71   by (auto simp:mult_sedge_def)
    72 
    73 lemmas sctTest_simps =
    74   simp_thms
    75   if_True
    76   if_False
    77   nat.inject
    78   nat.distinct
    79   Pair_eq 
    80 
    81   grcomp_code 
    82   edges_match.simps 
    83   connect_edges.simps 
    84 
    85   sedge_simps
    86   sedge.distinct
    87   set_simps
    88 
    89   graph_mult_def 
    90   graph_leq_def
    91   dest_graph.simps
    92   graph_plus_def
    93   graph.inject
    94   graph_zero_def
    95 
    96   test_SCT_def
    97   mk_tcl_code
    98 
    99   Let_def
   100   split_conv
   101 
   102 lemmas sctTest_congs = 
   103   if_weak_cong let_weak_cong setbcomp_cong
   104 
   105 end