Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Reordering the code, part 3
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 15 Oct 2009 11:42:14 +0200
changeset 101 4f93c5a026d2
parent 100 09f4d69f7b66
child 102 9d41f680d755
child 103 4aef3882b436
Reordering the code, part 3
QuotMain.thy file | annotate | diff | comparison | revisions
Unused.thy file | annotate | diff | comparison | revisions 
--- a/QuotMain.thy	Thu Oct 15 11:29:38 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 11:42:14 2009 +0200
@@ -774,98 +774,10 @@
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
 
-ML {*
-  fun dest_cbinop t =
-    let
-      val (t2, rhs) = Thm.dest_comb t;
-      val (bop, lhs) = Thm.dest_comb t2;
-    in
-      (bop, (lhs, rhs))
-    end
-*}
-
-ML {*
-  fun dest_ceq t =
-    let
-      val (bop, pair) = dest_cbinop t;
-      val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
-    in
-      if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
-    end
-*}
-
-ML Thm.instantiate
-ML {*@{thm arg_cong2}*}
-ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
-ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
-ML {*
-  Toplevel.program (fn () =>
-    Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2}
-  )
-*}
-
-ML {*
-  fun split_binop_conv t =
-    let
-      val (lhs, rhs) = dest_ceq t;
-      val (bop, _) = dest_cbinop lhs;
-      val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
-      val [cmT, crT] = Thm.dest_ctyp cr2;
-    in
-      Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
-    end
-*}
-
+(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
 ML {*
-  fun split_arg_conv t =
-    let
-      val (lhs, rhs) = dest_ceq t;
-      val (lop, larg) = Thm.dest_comb lhs;
-      val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
-    in
-      Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
-    end
-*}
-
-ML {*
-  fun split_binop_tac n thm =
-    let
-      val concl = Thm.cprem_of thm n;
-      val (_, cconcl) = Thm.dest_comb concl;
-      val rewr = split_binop_conv cconcl;
-    in
-      rtac rewr n thm
-    end
-      handle CTERM _ => Seq.empty
-*}
-
-ML {*
-  fun split_arg_tac n thm =
-    let
-      val concl = Thm.cprem_of thm n;
-      val (_, cconcl) = Thm.dest_comb concl;
-      val rewr = split_arg_conv cconcl;
-    in
-      rtac rewr n thm
-    end
-      handle CTERM _ => Seq.empty
-*}
-
-(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
-
-lemma trueprop_cong:
-  shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
-  by auto
-
-ML {*
-  Cong_Tac.cong_tac
-*}
-
-thm QUOT_TYPE_I_fset.R_trans2
-ML {*
-  fun foo_tac' ctxt =
+  fun transconv_fset_tac' ctxt =
     REPEAT_ALL_NEW (FIRST' [
-(*      rtac @{thm trueprop_cong},*)
       rtac @{thm list_eq_refl},
       rtac @{thm cons_preserves},
       rtac @{thm mem_respects},
@@ -874,8 +786,6 @@
       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
       Cong_Tac.cong_tac @{thm cong},
       rtac @{thm ext}
-(*      rtac @{thm eq_reflection},*)
-(*      CHANGED o (ObjectLogic.full_atomize_tac)*)
     ])
 *}
 
@@ -912,7 +822,7 @@
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (atomize(full))
-  apply (tactic {* foo_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} 1 *})
   done
 
 thm length_append (* Not true but worth checking that the goal is correct *)
@@ -925,7 +835,7 @@
 prove {* Thm.term_of cgoal2 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (atomize(full))
-  apply (tactic {* foo_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} 1 *})
   sorry
 
 thm m2
@@ -938,7 +848,7 @@
 prove {* Thm.term_of cgoal2 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (atomize(full))
-  apply (tactic {* foo_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} 1 *})
   done
 
 thm list_eq.intros(4)
@@ -954,7 +864,7 @@
 prove zzz : {* Thm.term_of cgoal3 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (atomize(full))
-  apply (tactic {* foo_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} 1 *})
   done
 
 lemma zzz' :
@@ -982,7 +892,7 @@
 prove {* Thm.term_of cgoal2 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (atomize(full))
-  apply (tactic {* foo_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} 1 *})
   done
 
 section {* handling quantifiers - regularize *}
@@ -1215,7 +1125,7 @@
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (atomize(full))
-  apply (tactic {* foo_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} 1 *})
   sorry
 
 ML {*
@@ -1225,7 +1135,7 @@
       val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs;
       val cgoal = cterm_of @{theory} goal;
       val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
-      val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (foo_tac' @{context}) 1;
+      val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (transconv_fset_tac' @{context}) 1;
       val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
       val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
       val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
@@ -1380,7 +1290,7 @@
 (*prove aaa: {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (atomize(full))
-  apply (tactic {* foo_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} 1 *})
   done*)
 
 (*
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Unused.thy	Thu Oct 15 11:42:14 2009 +0200
@@ -0,0 +1,74 @@
+
+ML {*
+  fun dest_cbinop t =
+    let
+      val (t2, rhs) = Thm.dest_comb t;
+      val (bop, lhs) = Thm.dest_comb t2;
+    in
+      (bop, (lhs, rhs))
+    end
+*}
+
+ML {*
+  fun dest_ceq t =
+    let
+      val (bop, pair) = dest_cbinop t;
+      val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
+    in
+      if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
+    end
+*}
+
+ML {*
+  fun split_binop_conv t =
+    let
+      val (lhs, rhs) = dest_ceq t;
+      val (bop, _) = dest_cbinop lhs;
+      val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+      val [cmT, crT] = Thm.dest_ctyp cr2;
+    in
+      Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
+    end
+*}
+
+
+ML {*
+  fun split_arg_conv t =
+    let
+      val (lhs, rhs) = dest_ceq t;
+      val (lop, larg) = Thm.dest_comb lhs;
+      val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+    in
+      Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
+    end
+*}
+
+ML {*
+  fun split_binop_tac n thm =
+    let
+      val concl = Thm.cprem_of thm n;
+      val (_, cconcl) = Thm.dest_comb concl;
+      val rewr = split_binop_conv cconcl;
+    in
+      rtac rewr n thm
+    end
+      handle CTERM _ => Seq.empty
+*}
+
+
+ML {*
+  fun split_arg_tac n thm =
+    let
+      val concl = Thm.cprem_of thm n;
+      val (_, cconcl) = Thm.dest_comb concl;
+      val rewr = split_arg_conv cconcl;
+    in
+      rtac rewr n thm
+    end
+      handle CTERM _ => Seq.empty
+*}
+
+
+lemma trueprop_cong:
+  shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)"
+  by auto
nominal2