Mercurial Mercurial > hg > nominal2 / comparison
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 473 4ce64524ce13
parent 472 cb03d4b3f059
child 474 5e1f4c8ab3de
equal deleted inserted replaced
472:cb03d4b3f059 473:4ce64524ce13 
     2 imports QuotScript QuotList Prove
 
     2 imports QuotScript QuotList Prove
 
     3 uses ("quotient_info.ML") 
     3 uses ("quotient_info.ML") 
     4      ("quotient.ML")
 
     4      ("quotient.ML")
 
     5      ("quotient_def.ML")
 
     5      ("quotient_def.ML")
 
     6 begin
 
     6 begin
 
     7 
       
     8 thm LAMBDA_PRS
 
       
     9 
     7 
    10 ML {*
 
     8 ML {*
 
    11 let
 
     9 let
 
    12    val parser = Args.context -- Scan.lift Args.name_source
 
    10    val parser = Args.context -- Scan.lift Args.name_source
 
    13    fun term_pat (ctxt, str) =
 
    11    fun term_pat (ctxt, str) =
 
   809 
   807 
   810 ML {*
 
   808 ML {*
 
   811 val weak_lambda_res_tac =
 
   809 val weak_lambda_res_tac =
 
   812   SUBGOAL (fn (goal, i) =>
 
   810   SUBGOAL (fn (goal, i) =>
 
   813     case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
 
   811     case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
 
   814        (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1
 
   812        (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i
 
   815      | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1
 
   813      | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i
 
   816      | _ => no_tac)
 
   814      | _ => no_tac)
 
   817 *}
 
   815 *}
 
   818 
   816 
   819 ML {*
 
   817 ML {*
 
   820 val ball_rsp_tac = 
   818 val ball_rsp_tac = 
   821   SUBGOAL (fn (goal, i) =>
 
   819   SUBGOAL (fn (goal, i) =>
 
   822     case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
 
   820     case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
 
   823         (_ $ (Const (@{const_name Ball}, _) $ _) 
   821         (_ $ (Const (@{const_name Ball}, _) $ _) 
   824            $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1
 
   822            $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i
 
   825       |_ => no_tac)
 
   823       |_ => no_tac)
 
   826 *}
 
   824 *}
 
   827 
   825 
   828 ML {*
 
   826 ML {*
 
   829 val bex_rsp_tac = 
   827 val bex_rsp_tac = 
   830   SUBGOAL (fn (goal, i) =>
 
   828   SUBGOAL (fn (goal, i) =>
 
   831     case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
 
   829     case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
 
   832         (_ $ (Const (@{const_name Bex}, _) $ _) 
   830         (_ $ (Const (@{const_name Bex}, _) $ _) 
   833            $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1
 
   831            $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i
 
   834       | _ => no_tac)
 
   832       | _ => no_tac)
 
   835 *}
 
   833 *}
 
   836 
   834 
   837 ML {* (* Legacy *)
 
   835 ML {* (* Legacy *)
 
   838 fun needs_lift (rty as Type (rty_s, _)) ty =
 
   836 fun needs_lift (rty as Type (rty_s, _)) ty =
 
   938     (* "cong" rule of the of the relation / transitivity*)
 
   936     (* "cong" rule of the of the relation / transitivity*)
 
   939     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
 
   937     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
 
   940     DT ctxt "1" (resolve_tac trans2),
 
   938     DT ctxt "1" (resolve_tac trans2),
 
   941 
   939 
   942     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
   940     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
   943     NDT ctxt "2" (lambda_res_tac ctxt),
 
   941     NDT ctxt "2" (lambda_res_tac),
 
   944 
   942 
   945     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   943     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   946     NDT ctxt "3" (rtac @{thm ball_rsp}),
 
   944     NDT ctxt "3" (rtac @{thm ball_rsp}),
 
   947 
   945 
   948     (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
 
   946     (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
 
   949     NDT ctxt "4" (ball_rsp_tac ctxt),
 
   947     NDT ctxt "4" (ball_rsp_tac),
 
   950 
   948 
   951     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   949     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   952     NDT ctxt "5" (rtac @{thm bex_rsp}),
 
   950     NDT ctxt "5" (rtac @{thm bex_rsp}),
 
   953 
   951 
   954     (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
 
   952     (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
 
   955     NDT ctxt "6" (bex_rsp_tac ctxt),
 
   953     NDT ctxt "6" (bex_rsp_tac),
 
   956 
   954 
   957     (* respectfulness of constants *)
 
   955     (* respectfulness of constants *)
 
   958     NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
 
   956     NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
 
   959 
   957 
   960     (* reflexivity of operators arising from Cong_tac *)
 
   958     (* reflexivity of operators arising from Cong_tac *)
nominal2