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
```