Add forgotten ArityEtaExpand
authorJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 12:02:46 +0000 (12:02 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 12:02:46 +0000 (12:02 +0000)
Launchbury/ArityEtaExpand.thy [new file with mode: 0644]
Launchbury/CallArityEnd2End.thy
Launchbury/CallFutureCardinality.thy
Launchbury/CoCallImplFTree.thy
Launchbury/CoCallImplFTreeCorrect.thy
Launchbury/Env-Set-Cpo.thy [new file with mode: 0644]
Launchbury/Env.thy
Launchbury/FTreeImplCardinality.thy
Launchbury/FTreeImplCardinalityCorrect.thy

diff --git a/Launchbury/ArityEtaExpand.thy b/Launchbury/ArityEtaExpand.thy
new file mode 100644 (file)
index 0000000..1464b91
--- /dev/null
@@ -0,0 +1,21 @@
+theory ArityEtaExpand
+imports ArityAnalysisSig AbstractTransform  ArityEtaExpansionSestoft
+begin
+
+context ArityAnalysisHeapEqvt
+begin
+  sublocale AbstractTransformBound
+    "\<lambda> a . inc\<cdot>a"
+    "\<lambda> a . pred\<cdot>a"
+    "\<lambda> \<Delta> e a . (a, Aheap \<Delta> e\<cdot>a)"
+    "fst"
+    "snd"
+    "Aeta_expand"
+    "snd"
+  apply default
+  apply (((rule eq_reflection)?, perm_simp, rule)+)[7]
+  done
+end
+
+
+end
index 5762092..a994a5e 100644 (file)
@@ -1,5 +1,5 @@
 theory CallArityEnd2End
-imports ArityEtaExpand CoCallAnalysisImpl  CoCallImplFTree FTreeImplCardinality 
+imports ArityEtaExpand CoCallAnalysisImpl
 begin
 
 locale CallArityEnd2End
index 31b07b6..30f5130 100644 (file)
@@ -1,5 +1,5 @@
 theory CallFutureCardinality
-imports Vars "Nominal-HOLCF" Env "Cardinality-Domain" "Set-Cpo"
+imports Vars "Nominal-HOLCF" Env "Cardinality-Domain" "Set-Cpo" "Env-Set-Cpo"
 begin
 
 fun no_call_in_path where
@@ -112,14 +112,5 @@ lemma edom_pathsCard[simp]: "edom (pathsCard ps) = \<Union>(set ` ps)"
 lemma env_restr_pathsCard[simp]: "pathsCard ps f|` S = pathsCard (filter (\<lambda> x. x \<in> S) ` ps)"
   by (auto simp add: pathsCard_def lookup_env_restr_eq)
 
-text {* This is here because it requires @{theory "Set-Cpo"} *}
-
-lemma cont_edom[THEN cont_compose, simp, cont2cont]:
-  "cont (\<lambda> f. edom f)"
-  apply (rule set_contI)
-  apply (auto simp add: edom_def)
-  apply (metis ch2ch_fun lub_eq_bottom_iff lub_fun)
-  apply (metis ch2ch_fun lub_eq_bottom_iff lub_fun)
-  done
 
 end
index b4e5d61..33fe600 100644 (file)
@@ -1,5 +1,5 @@
 theory CoCallImplFTree
-imports FTreeAnalysisSpec CoCallAritySig "CoCallGraph-FTree"
+imports FTreeAnalysisSig "Env-Set-Cpo" CoCallAritySig "CoCallGraph-FTree"
 begin
 
 context CoCallArity
@@ -8,7 +8,8 @@ begin
     where "Fexp e = (\<Lambda> a. ccFTree (edom (Aexp e \<cdot>a)) (ccExp e\<cdot>a))"
   
   lemma Fexp_simp: "Fexp e\<cdot>a = ccFTree (edom (Aexp e \<cdot>a)) (ccExp e\<cdot>a)"
-    unfolding Fexp_def by simp
+    unfolding Fexp_def
+    by simp
 
   sublocale FTreeAnalysis Fexp.
 end
index 79132d0..f76973c 100644 (file)
@@ -1,5 +1,5 @@
 theory CoCallImplFTreeCorrect
-imports CoCallImplFTree CoCallAnalysisSpec
+imports CoCallImplFTree CoCallAnalysisSpec FTreeAnalysisSpec CallFutureCardinality
 begin
 
 hide_const Multiset.single
@@ -523,30 +523,5 @@ proof(rule ftree_belowI)
   qed
 qed
 
-(* TODO: Unused. Remove? *)
-lemma multi_calls_ccFTree:
-  assumes "xs \<in> paths (ccFTree S G)"
-  assumes "\<not> one_call_in_path x xs"
-  shows "x \<in> S" and "x \<in> ccManyCalls G"
-proof-
-  from assms(1) have "xs \<in> valid_lists S G" by simp 
-
-  have "x \<in> set xs" by (metis assms(2) filter_True one_call_in_path_filter)
-  with `xs \<in> valid_lists S G`
-  show "x \<in> S" by (metis  subsetCE valid_lists_subset)
-
-  show "x \<in> ccManyCalls G"
-  proof(rule ccontr)
-    assume "x \<notin> ccManyCalls G"
-    with `xs \<in> valid_lists S G` 
-    have "one_call_in_path x xs"
-    by (induction rule: valid_lists.induct) (auto simp add: no_call_in_path_set_conv)
-    with assms(2)
-    show False..
-  qed
-qed
-
-
-
 end
 
diff --git a/Launchbury/Env-Set-Cpo.thy b/Launchbury/Env-Set-Cpo.thy
new file mode 100644 (file)
index 0000000..669f576
--- /dev/null
@@ -0,0 +1,13 @@
+theory "Env-Set-Cpo"
+imports Env "Set-Cpo"
+begin
+
+lemma cont_edom[THEN cont_compose, simp, cont2cont]:
+  "cont (\<lambda> f. edom f)"
+  apply (rule set_contI)
+  apply (auto simp add: edom_def)
+  apply (metis ch2ch_fun lub_eq_bottom_iff lub_fun)
+  apply (metis ch2ch_fun lub_eq_bottom_iff lub_fun)
+  done
+
+end
index 305af4d..234950e 100644 (file)
@@ -1,5 +1,5 @@
 theory Env
-  imports Main HOLCF  "HOLCF-Join-Classes"
+  imports Main HOLCF "HOLCF-Join-Classes"
 begin
 
 default_sort type
index 03b4234..8e6cca3 100644 (file)
@@ -1,5 +1,5 @@
 theory FTreeImplCardinality
-imports FTreeAnalysisSpec CardinalityAnalysisSpec CallFutureCardinality
+imports FTreeAnalysisSig CardinalityAnalysisSig CallFutureCardinality
 begin
 
 hide_const Multiset.single
index 4ba18a3..2444a0b 100644 (file)
@@ -2,6 +2,8 @@ theory FTreeImplCardinalityCorrect
 imports FTreeImplCardinality FTreeAnalysisSpec CardinalityAnalysisSpec CallFutureCardinality
 begin
 
+hide_const Multiset.single
+
 lemma pathsCard_paths_nxt:  "pathsCard (paths (nxt f x)) \<sqsubseteq> record_call x\<cdot>(pathsCard (paths f))"
   apply transfer
   apply (rule pathsCard_below)