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.
QuotMain.thy
changeset 525 3f657c4fbefa
parent 523 1a4eb39ba834
child 526 7ba2fc25c6a3 
--- a/QuotMain.thy	Fri Dec 04 12:21:15 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 14:11:03 2009 +0100
@@ -956,73 +956,7 @@
 fun unlam t =
   case t of
     (Abs a) => snd (Term.dest_abs a)
-  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))  *}
-
-
-ML {*
-fun inj_repabs_tac ctxt rel_refl trans2 =
-  (FIRST' [
-    (* "cong" rule of the of the relation / transitivity*)
-    (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-    NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [
-      quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
-
-    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
-    NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam),
-
-    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "3" (rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}),
-
-    (* R2 is always equality *)
-    (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
-    NDT ctxt "4" (ball_rsp_tac THEN' quot_true_tac ctxt unlam),
-
-    (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "5" (rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}),
-
-    (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
-    NDT ctxt "6" (bex_rsp_tac THEN' dtac @{thm QT_ext}),
-
-    (* respectfulness of constants *)
-    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
-
-    (* reflexivity of operators arising from Cong_tac *)
-    NDT ctxt "8" (rtac @{thm refl}),
-
-    (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
-    (* observe ---> *) 
-    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
-                  THEN' (RANGE [SOLVES' (quotient_tac ctxt)]))),
-
-    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
-    NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
-                (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
-                        quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
-
-    (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
-    (* merge with previous tactic *)
-    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
-                (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
-
-    (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
-    
-    (* reflexivity of the basic relations *)
-    (* R \<dots> \<dots> *)
-    NDT ctxt "D" (resolve_tac rel_refl),
-
-    (* resolving with R x y assumptions *)
-    NDT ctxt "E" (atac)
-
-    (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
-    (* global simplification *)
-    (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*)
-    ])
-*}
-
-ML {*
-fun all_inj_repabs_tac ctxt rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
+  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
 *}
 
 ML {*
@@ -1050,58 +984,71 @@
   | _ => no_tac)
 *}
 
-(* A faster version *)
-
 ML {*
-fun inj_repabs_tac_fast ctxt trans2 = SUBGOAL (fn (goal, i) =>
+fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
+    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
   ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))
       => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 | (Const (@{const_name "op ="},_) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+    (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+    (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 | Const (@{const_name "op ="},_) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+    (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
 | Const (@{const_name "op ="},_) $ _ $ _ => 
+    (* reflexivity of operators arising from Cong_tac *)
     rtac @{thm refl} ORELSE'
     (resolve_tac trans2 THEN' RANGE [
       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
 | _ $ _ $ _ =>
+    (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
+    (* observe ---> *)
     rep_abs_rsp_tac ctxt
 | _ => error "inj_repabs_tac not a relation"
 ) i)
 *}
 
 ML {*
-fun inj_repabs_tac' ctxt rel_refl trans2 =
+fun inj_repabs_tac ctxt rel_refl trans2 =
   (FIRST' [
-    inj_repabs_tac_fast ctxt trans2,
+    inj_repabs_tac_match ctxt trans2,
+    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
     NDT ctxt "A" (APPLY_RSP1_TAC' ctxt THEN'
                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
+    (* merge with previous tactic *)
     NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
     NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    (* resolving with R x y assumptions *)
     NDT ctxt "E" (atac),
+    (* reflexivity of the basic relations *)
+    (* R \<dots> \<dots> *)
     NDT ctxt "D" (resolve_tac rel_refl),
+    (* respectfulness of constants *)
     NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt))
-(*    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*)
     ])
 *}
 
 ML {*
-fun all_inj_repabs_tac' ctxt rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac' ctxt rel_refl trans2)
+fun all_inj_repabs_tac ctxt rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 *}
 
 
@@ -1360,7 +1307,7 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               rtac thm THEN' all_inj_repabs_tac' lthy rel_refl trans2,
+               rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2,
                clean_tac lthy]]
     end) lthy
 *}
nominal2