Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FSet.thy
changeset 482 767baada01dc
parent 481 7f97c52021c9
child 483 74348dc2f8bb 
--- a/FSet.thy	Wed Dec 02 12:07:54 2009 +0100
+++ b/FSet.thy	Wed Dec 02 14:11:46 2009 +0100
@@ -333,6 +333,8 @@
 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
+
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done
@@ -343,7 +345,6 @@
 
 lemma cheat: "P" sorry
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
@@ -396,6 +397,28 @@
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 done
 
+lemma list_induct_part:
+  assumes a: "P (x :: 'a list) ([] :: 'c list)"
+  assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
+  shows "P x l"
+  apply (rule_tac P="P x" in list.induct)
+  apply (rule a)
+  apply (rule b)
+  apply (assumption)
+  done
+
+lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
+apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+done
+
+lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
+apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+done
+
+lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l"
+apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+done
+
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
@@ -431,115 +454,6 @@
 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
 done
 
-lemma list_induct_part:
-  assumes a: "P (x :: 'a list) ([] :: 'c list)"
-  assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
-  shows "P x l"
-  apply (rule_tac P="P x" in list.induct)
-  apply (rule a)
-  apply (rule b)
-  apply (assumption)
-  done
-
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
+thm all_prs
 
-(* Construction site starts here *)
-lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
-apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-prefer 2
-apply (tactic {* clean_tac @{context} [quot] defs 1 *})
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply assumption
-apply (rule refl)
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply assumption
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply assumption
-apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
-prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-done
-
-ML {* #quot_thm (hd (quotdata_dest @{theory})) *}
-print_quotients
-thm QUOTIENT_fset
 end
nominal2